Theorem djhcom

Description: Subspace join commutes. (Contributed by NM, 8-Aug-2014)

	Ref	Expression
Hypotheses	djhcom.h	|- H = ( LHyp ` K )
	djhcom.u	|- U = ( ( DVecH ` K ) ` W )
	djhcom.v	|- V = ( Base ` U )
	djhcom.j	|- .\/ = ( ( joinH ` K ) ` W )
	djhcom.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	djhcom.x	|- ( ph -> X C_ V )
	djhcom.y	|- ( ph -> Y C_ V )
Assertion	djhcom	|- ( ph -> ( X .\/ Y ) = ( Y .\/ X ) )

Proof

Step	Hyp	Ref	Expression
1		djhcom.h	|- H = ( LHyp ` K )
2		djhcom.u	|- U = ( ( DVecH ` K ) ` W )
3		djhcom.v	|- V = ( Base ` U )
4		djhcom.j	|- .\/ = ( ( joinH ` K ) ` W )
5		djhcom.k	|- ( ph -> ( K e. HL /\ W e. H ) )
6		djhcom.x	|- ( ph -> X C_ V )
7		djhcom.y	|- ( ph -> Y C_ V )
8		uncom	|- ( X u. Y ) = ( Y u. X )
9	8	fveq2i	|- ( ( ( ocH ` K ) ` W ) ` ( X u. Y ) ) = ( ( ( ocH ` K ) ` W ) ` ( Y u. X ) )
10	9	fveq2i	|- ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( X u. Y ) ) ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( Y u. X ) ) )
11		eqid	|- ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
12	1 2 3 11 4	djhval2	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( X .\/ Y ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( X u. Y ) ) ) )
13	5 6 7 12	syl3anc	|- ( ph -> ( X .\/ Y ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( X u. Y ) ) ) )
14	1 2 3 11 4	djhval2	|- ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ V ) -> ( Y .\/ X ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( Y u. X ) ) ) )
15	5 7 6 14	syl3anc	|- ( ph -> ( Y .\/ X ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( Y u. X ) ) ) )
16	10 13 15	3eqtr4a	|- ( ph -> ( X .\/ Y ) = ( Y .\/ X ) )