Metamath Proof Explorer

Theorem djhljjN

Description: Lattice join in terms of DVecH vector space closed subspace join. (Contributed by NM, 17-Aug-2014) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 djhlj.b 
 |-  B = ( Base ` K )
2 djhlj.k 
 |-  .\/ = ( join ` K )
3 djhlj.h 
 |-  H = ( LHyp ` K )
4 djhlj.i 
 |-  I = ( ( DIsoH ` K ) ` W )
5 djhlj.j 
 |-  J = ( ( joinH ` K ) ` W )
6 djhljj.w 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
7 djhljj.x 
 |-  ( ph -> X e. B )
8 djhljj.y 
 |-  ( ph -> Y e. B )
9 1 2 3 4 5 djhlj 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( I ` ( X .\/ Y ) ) = ( ( I ` X ) J ( I ` Y ) ) )
10 6 7 8 9 syl12anc 
 |-  ( ph -> ( I ` ( X .\/ Y ) ) = ( ( I ` X ) J ( I ` Y ) ) )
11 1 3 4 dihcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( I ` X ) e. ran I )
12 6 7 11 syl2anc 
 |-  ( ph -> ( I ` X ) e. ran I )
13 eqid 
 |-  ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
14 eqid 
 |-  ( Base ` ( ( DVecH ` K ) ` W ) ) = ( Base ` ( ( DVecH ` K ) ` W ) )
15 3 13 4 14 dihrnss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( I ` X ) e. ran I ) -> ( I ` X ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
16 6 12 15 syl2anc 
 |-  ( ph -> ( I ` X ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
17 1 3 4 dihcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. B ) -> ( I ` Y ) e. ran I )
18 6 8 17 syl2anc 
 |-  ( ph -> ( I ` Y ) e. ran I )
19 3 13 4 14 dihrnss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( I ` Y ) e. ran I ) -> ( I ` Y ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
20 6 18 19 syl2anc 
 |-  ( ph -> ( I ` Y ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
21 3 4 13 14 5 djhcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( I ` X ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) /\ ( I ` Y ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) ) ) -> ( ( I ` X ) J ( I ` Y ) ) e. ran I )
22 6 16 20 21 syl12anc 
 |-  ( ph -> ( ( I ` X ) J ( I ` Y ) ) e. ran I )
23 3 4 dihcnvid2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( I ` X ) J ( I ` Y ) ) e. ran I ) -> ( I ` ( `' I ` ( ( I ` X ) J ( I ` Y ) ) ) ) = ( ( I ` X ) J ( I ` Y ) ) )
24 6 22 23 syl2anc 
 |-  ( ph -> ( I ` ( `' I ` ( ( I ` X ) J ( I ` Y ) ) ) ) = ( ( I ` X ) J ( I ` Y ) ) )
25 10 24 eqtr4d 
 |-  ( ph -> ( I ` ( X .\/ Y ) ) = ( I ` ( `' I ` ( ( I ` X ) J ( I ` Y ) ) ) ) )
26 6 simpld 
 |-  ( ph -> K e. HL )
27 26 hllatd 
 |-  ( ph -> K e. Lat )
28 1 2 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
29 27 7 8 28 syl3anc 
 |-  ( ph -> ( X .\/ Y ) e. B )
30 1 3 4 dihcnvcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( I ` X ) J ( I ` Y ) ) e. ran I ) -> ( `' I ` ( ( I ` X ) J ( I ` Y ) ) ) e. B )
31 6 22 30 syl2anc 
 |-  ( ph -> ( `' I ` ( ( I ` X ) J ( I ` Y ) ) ) e. B )
32 1 3 4 dih11 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X .\/ Y ) e. B /\ ( `' I ` ( ( I ` X ) J ( I ` Y ) ) ) e. B ) -> ( ( I ` ( X .\/ Y ) ) = ( I ` ( `' I ` ( ( I ` X ) J ( I ` Y ) ) ) ) <-> ( X .\/ Y ) = ( `' I ` ( ( I ` X ) J ( I ` Y ) ) ) ) )
33 6 29 31 32 syl3anc 
 |-  ( ph -> ( ( I ` ( X .\/ Y ) ) = ( I ` ( `' I ` ( ( I ` X ) J ( I ` Y ) ) ) ) <-> ( X .\/ Y ) = ( `' I ` ( ( I ` X ) J ( I ` Y ) ) ) ) )
34 25 33 mpbid 
 |-  ( ph -> ( X .\/ Y ) = ( `' I ` ( ( I ` X ) J ( I ` Y ) ) ) )