This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )