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 = ( Base ` K )
	dihopcl.h	|- H = ( LHyp ` K )
	dihopcl.t	|- T = ( ( LTrn ` K ) ` W )
	dihopcl.e	|- E = ( ( TEndo ` K ) ` W )
	dihopcl.i	|- I = ( ( DIsoH ` K ) ` W )
	dihopcl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dihopcl.x	|- ( ph -> X e. B )
	dihopcl.y	|- ( ph -> <. F , S >. e. ( I ` X ) )
Assertion	dihopcl	|- ( ph -> ( F e. T /\ S e. E ) )

Proof

Step	Hyp	Ref	Expression
1		dihopcl.b	|- B = ( Base ` K )
2		dihopcl.h	|- H = ( LHyp ` K )
3		dihopcl.t	|- T = ( ( LTrn ` K ) ` W )
4		dihopcl.e	|- E = ( ( TEndo ` K ) ` W )
5		dihopcl.i	|- I = ( ( DIsoH ` K ) ` W )
6		dihopcl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		dihopcl.x	|- ( ph -> X e. B )
8		dihopcl.y	|- ( ph -> <. F , S >. e. ( I ` X ) )
9	1 2 3 4 5 6 7	dihssxp	|- ( ph -> ( I ` X ) C_ ( T X. E ) )
10	9 8	sseldd	|- ( ph -> <. F , S >. e. ( T X. E ) )
11		opelxp	|- ( <. F , S >. e. ( T X. E ) <-> ( F e. T /\ S e. E ) )
12	10 11	sylib	|- ( ph -> ( F e. T /\ S e. E ) )