Theorem djhj

Description: DVecH vector space closed subspace join in terms of lattice join. (Contributed by NM, 17-Aug-2014)

	Ref	Expression
Hypotheses	djhj.k	|- .\/ = ( join ` K )
	djhj.h	|- H = ( LHyp ` K )
	djhj.i	|- I = ( ( DIsoH ` K ) ` W )
	djhj.j	|- J = ( ( joinH ` K ) ` W )
	djhj.w	|- ( ph -> ( K e. HL /\ W e. H ) )
	djhj.x	|- ( ph -> X e. ran I )
	djhj.y	|- ( ph -> Y e. ran I )
Assertion	djhj	|- ( ph -> ( `' I ` ( X J Y ) ) = ( ( `' I ` X ) .\/ ( `' I ` Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		djhj.k	|- .\/ = ( join ` K )
2		djhj.h	|- H = ( LHyp ` K )
3		djhj.i	|- I = ( ( DIsoH ` K ) ` W )
4		djhj.j	|- J = ( ( joinH ` K ) ` W )
5		djhj.w	|- ( ph -> ( K e. HL /\ W e. H ) )
6		djhj.x	|- ( ph -> X e. ran I )
7		djhj.y	|- ( ph -> Y e. ran I )
8	1 2 3 4 5 6 7	djhjlj	|- ( ph -> ( X J Y ) = ( I ` ( ( `' I ` X ) .\/ ( `' I ` Y ) ) ) )
9	8	fveq2d	|- ( ph -> ( `' I ` ( X J Y ) ) = ( `' I ` ( I ` ( ( `' I ` X ) .\/ ( `' I ` Y ) ) ) ) )
10	5	simpld	|- ( ph -> K e. HL )
11	10	hllatd	|- ( ph -> K e. Lat )
12		eqid	|- ( Base ` K ) = ( Base ` K )
13	12 2 3	dihcnvcl	|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` X ) e. ( Base ` K ) )
14	5 6 13	syl2anc	|- ( ph -> ( `' I ` X ) e. ( Base ` K ) )
15	12 2 3	dihcnvcl	|- ( ( ( K e. HL /\ W e. H ) /\ Y e. ran I ) -> ( `' I ` Y ) e. ( Base ` K ) )
16	5 7 15	syl2anc	|- ( ph -> ( `' I ` Y ) e. ( Base ` K ) )
17	12 1	latjcl	|- ( ( K e. Lat /\ ( `' I ` X ) e. ( Base ` K ) /\ ( `' I ` Y ) e. ( Base ` K ) ) -> ( ( `' I ` X ) .\/ ( `' I ` Y ) ) e. ( Base ` K ) )
18	11 14 16 17	syl3anc	|- ( ph -> ( ( `' I ` X ) .\/ ( `' I ` Y ) ) e. ( Base ` K ) )
19	12 2 3	dihcnvid1	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( `' I ` X ) .\/ ( `' I ` Y ) ) e. ( Base ` K ) ) -> ( `' I ` ( I ` ( ( `' I ` X ) .\/ ( `' I ` Y ) ) ) ) = ( ( `' I ` X ) .\/ ( `' I ` Y ) ) )
20	5 18 19	syl2anc	|- ( ph -> ( `' I ` ( I ` ( ( `' I ` X ) .\/ ( `' I ` Y ) ) ) ) = ( ( `' I ` X ) .\/ ( `' I ` Y ) ) )
21	9 20	eqtrd	|- ( ph -> ( `' I ` ( X J Y ) ) = ( ( `' I ` X ) .\/ ( `' I ` Y ) ) )