Theorem dihopcl

Description: Closure of an ordered pair (vector) member of a value of isomorphism H. (Contributed by NM, 26-Sep-2014)

	Ref	Expression
Hypotheses	dihopcl.b	$$⊢B={\mathrm{Base}}_K$$
	dihopcl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihopcl.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dihopcl.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	dihopcl.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dihopcl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dihopcl.x	$$⊢\phi \to X\in B$$
	dihopcl.y	$$⊢\phi \to ⟨F,S⟩\in I\left(X\right)$$
Assertion	dihopcl	$$⊢\phi \to \left(F\in T\wedge S\in E\right)$$

Proof

Step	Hyp	Ref	Expression
1		dihopcl.b	$$⊢B={\mathrm{Base}}_K$$
2		dihopcl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
3		dihopcl.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
4		dihopcl.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
5		dihopcl.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
6		dihopcl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
7		dihopcl.x	$$⊢\phi \to X\in B$$
8		dihopcl.y	$$⊢\phi \to ⟨F,S⟩\in I\left(X\right)$$
9	1 2 3 4 5 6 7	dihssxp	$$⊢\phi \to I\left(X\right)\subseteq T\times E$$
10	9 8	sseldd	$$⊢\phi \to ⟨F,S⟩\in \left(T\times E\right)$$
11		opelxp	$$⊢⟨F,S⟩\in \left(T\times E\right)\leftrightarrow \left(F\in T\wedge S\in E\right)$$
12	10 11	sylib	$$⊢\phi \to \left(F\in T\wedge S\in E\right)$$