Theorem dvhopclN

Description: Closure of a DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	dvhopclN	$$⊢\left(F\in T\wedge U\in E\right)\to ⟨F,U⟩\in \left(T\times E\right)$$

Proof

Step	Hyp	Ref	Expression
1		opelxpi	$$⊢\left(F\in T\wedge U\in E\right)\to ⟨F,U⟩\in \left(T\times E\right)$$