Definition of uniform subspace I would like some help with the definition of a uniform subspace. 
The textbook I refer to is Topological and Uniform Spaces by IM James, and he defines the uniform subspace on page 97. Here is his definition:

Suppose now that we have a uniform space $X$ and a subset $A$ of $X$. For each subset $D$ of $X \times X$ the trace $(A \times A) \cap D$ on $A \times A$ is just the inverse image of $D$ under the injection $A \times A \to X \times X$. [...] We take the entourages of $A$ to be the traces on $A \times A$ of the entourages of $X$. 

Let the uniformity on $X$ be denoted by $\Phi$. Am I right to understand this as saying that 
$$ \Phi_A := \{\, U \subseteq A \times A \mid \exists V \in \Phi \text{ such that } U = V \cap (A \times A) \,\} $$
forms a uniformity on $A$?

Let me assume that the above was correct. I follow the definition of a uniformity on Wikipedia. I'm very uncertain of my proofs, especially (2) and (4). Here it is:
Observe that $A \times A = (X \times X) \cap (A \times A)$, so $A \times A$ belongs to $\Phi_A$ and $\Phi_A$ is non-empty. 

  
*
  
*If $U \in \Phi_A$, then $\Delta A \subseteq U$.
  

Let $\Delta A = \Delta X \cap (A \times A)$ be the diagonal of $A \times A$. Since $\Delta X \subseteq V$ for all $V \in \Phi$, it follows that $\Delta A \subseteq U$. 


  
*If $U \in \Phi_A$ and $U \subseteq U' \subseteq A \times A$, then $U' \in \Phi_A$.
  

Suppose $U = V \cap (A \times A)$ for some $V \in \Phi$, and $U' = V' \cap (A \times A)$ for some $V' \subseteq X \times X$. Define $W = V \cup V' \subseteq X \times X$. Then $W$ is in $\Phi$ because uniformities are upward-closed, and
\begin{align*} 
W \cap (A \times A) &= (V \cap (A \times A)) \cup (V' \cap (A \times A)) \\
&= U \cup U' \\
&= U'.
\end{align*}
Therefore we have shown that $U'$ is in $\Phi_A$.


  
*If $U_1 \in \Phi_A$ and $U_2 \in \Phi_A$, then $U_1 \cap U_2 \in \Phi_A$.
  

Suppose $U_i = V_i \cap (A \times A)$ for some $V_i \in \Phi$ for $i = 1,2$. Then we have $U_1 \cap U_2 = (V_1 \cap V_2) \cap (A \times A)$. Since $\Phi$ is closed under finite intersection, the set $V_1 \cap V_2$ belongs to $\Phi$. This implies that $U_1 \cap U_2$ is in $\Phi_A$. 


  
*If $U \in \Phi_A$, then there exists $U' \in \Phi_A$ such that $U' \circ U' \subseteq U$.
  

Fix $U \in \Phi_A$ and suppose $U = V \cap (A \times A)$ for some $V \in \Phi$, then there exists $V' \in \Phi$ such that $V' \circ V' \subseteq V$. 
Let $U' = V' \cap (A \times A)$. We have
\begin{align*}
U' \circ U' &= \{\, (x,z) \in A \times A \mid \exists y \in A \text{ such that } (x,y), (y,z) \in U'\, \} \\
&\subseteq \{\, (x,z) \in X \times X \mid \exists y \in X \text{ such that } (x,y),(y,z) \in V'\, \} \cap (A \times A) \\
&= (V' \circ V') \cap (A \times A)\\
&\subseteq V \cap (A \times A) \\
&= U.
\end{align*}


  
*If $U \in \Phi_A$, then $U^{-1} \in \Phi_A$.
  

Suppose $U = V \cap (A \times A)$ for some $V \in \Phi$. Then we have
\begin{align*}
U^{-1} &= \{\, (y,x) \in A \times A \mid (x,y) \in U \, \}\\
&= \{\, (y,x) \in X \times X \mid (x,y) \in V\, \} \cap (A \times A)\\
&= V^{-1} \cap (A \times A).
\end{align*}
So $U^{-1}$ is in $\Phi_A$ because $V^{-1}$ is in $\Phi$.

Sorry for the long post. I'd really appreciate any comments/hints. Thanks!
 A: In (2) you have to start with $U \in \Phi_A$ so $U = V \cap (A \times A)$ with $V \in \Phi_X$. Then assume $U \subseteq U' \subseteq A \times A$ and note that 
$$(V \cup U') \cap (A \times A) = (V \cap (A \times A)) \cup (U' \cap (A \times A)) = (V \cap (A \times A)) \cup U' = U \cup U'  =U'$$ and $V \cup A' \in \Phi_X$ by upwards closedness. And thus also $U' \in \Phi_A$.
So I did not assume $U'$ was already a subset of $X \times X$ intersected with $A \times A$, but simply showed it to be of this form.
(4) is essentially fine. If $U \in \Phi_A$ is of the form $V \cap (A \times A)$ and we have $V' \in \Phi_X$ with $V' \circ V' \subseteq V$ then indeed $U':= V' \cap (A \times A)\in \Phi_A$ is as required, as $$U' \circ U' = (V' \cap (A \times A)) \circ (V' \cap (A \times A))= (V' \circ V') \cap (A \times A) \subseteq V \cap (A \times A) = U $$
where the first distributivity between $\circ$ and $\cap$ is a general fact of relations and easy to see by definition analysis.
No problems that I could see so far in the rest.
