Metamath Proof Explorer

Theorem djhlj

Description: Transfer lattice join to DVecH vector space closed subspace join. (Contributed by NM, 19-Jul-2014)

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 )
Assertion djhlj 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( I ` ( X .\/ Y ) ) = ( ( 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 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( K e. HL /\ W e. H ) )
7 simprl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> X e. B )
8 eqid 
 |-  ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
9 eqid 
 |-  ( Base ` ( ( DVecH ` K ) ` W ) ) = ( Base ` ( ( DVecH ` K ) ` W ) )
10 1 3 4 8 9 dihss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( I ` X ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
11 7 10 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( I ` X ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
12 simprr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> Y e. B )
13 1 3 4 8 9 dihss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. B ) -> ( I ` Y ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
14 12 13 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( I ` Y ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
15 eqid 
 |-  ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
16 3 8 9 15 5 djhval 
 |-  ( ( ( 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 ) ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ( ocH ` K ) ` W ) ` ( I ` X ) ) i^i ( ( ( ocH ` K ) ` W ) ` ( I ` Y ) ) ) ) )
17 6 11 14 16 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( ( I ` X ) J ( I ` Y ) ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ( ocH ` K ) ` W ) ` ( I ` X ) ) i^i ( ( ( ocH ` K ) ` W ) ` ( I ` Y ) ) ) ) )
18 hlop 
 |-  ( K e. HL -> K e. OP )
19 18 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> K e. OP )
20 eqid 
 |-  ( oc ` K ) = ( oc ` K )
21 1 20 opoccl 
 |-  ( ( K e. OP /\ X e. B ) -> ( ( oc ` K ) ` X ) e. B )
22 19 7 21 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( ( oc ` K ) ` X ) e. B )
23 1 20 opoccl 
 |-  ( ( K e. OP /\ Y e. B ) -> ( ( oc ` K ) ` Y ) e. B )
24 19 12 23 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( ( oc ` K ) ` Y ) e. B )
25 eqid 
 |-  ( meet ` K ) = ( meet ` K )
26 1 25 3 4 dihmeet 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( oc ` K ) ` X ) e. B /\ ( ( oc ` K ) ` Y ) e. B ) -> ( I ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) = ( ( I ` ( ( oc ` K ) ` X ) ) i^i ( I ` ( ( oc ` K ) ` Y ) ) ) )
27 6 22 24 26 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( I ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) = ( ( I ` ( ( oc ` K ) ` X ) ) i^i ( I ` ( ( oc ` K ) ` Y ) ) ) )
28 1 20 3 4 15 dochvalr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( ( ( ocH ` K ) ` W ) ` ( I ` X ) ) = ( I ` ( ( oc ` K ) ` X ) ) )
29 7 28 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( ( ( ocH ` K ) ` W ) ` ( I ` X ) ) = ( I ` ( ( oc ` K ) ` X ) ) )
30 1 20 3 4 15 dochvalr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. B ) -> ( ( ( ocH ` K ) ` W ) ` ( I ` Y ) ) = ( I ` ( ( oc ` K ) ` Y ) ) )
31 12 30 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( ( ( ocH ` K ) ` W ) ` ( I ` Y ) ) = ( I ` ( ( oc ` K ) ` Y ) ) )
32 29 31 ineq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( ( ( ( ocH ` K ) ` W ) ` ( I ` X ) ) i^i ( ( ( ocH ` K ) ` W ) ` ( I ` Y ) ) ) = ( ( I ` ( ( oc ` K ) ` X ) ) i^i ( I ` ( ( oc ` K ) ` Y ) ) ) )
33 27 32 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( I ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) = ( ( ( ( ocH ` K ) ` W ) ` ( I ` X ) ) i^i ( ( ( ocH ` K ) ` W ) ` ( I ` Y ) ) ) )
34 33 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( ( ( ocH ` K ) ` W ) ` ( I ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ( ocH ` K ) ` W ) ` ( I ` X ) ) i^i ( ( ( ocH ` K ) ` W ) ` ( I ` Y ) ) ) ) )
35 hllat 
 |-  ( K e. HL -> K e. Lat )
36 35 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> K e. Lat )
37 1 25 latmcl 
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` X ) e. B /\ ( ( oc ` K ) ` Y ) e. B ) -> ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) e. B )
38 36 22 24 37 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) e. B )
39 1 20 3 4 15 dochvalr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) e. B ) -> ( ( ( ocH ` K ) ` W ) ` ( I ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) ) = ( I ` ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) ) )
40 38 39 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( ( ( ocH ` K ) ` W ) ` ( I ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) ) = ( I ` ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) ) )
41 34 40 eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( ( ( ocH ` K ) ` W ) ` ( ( ( ( ocH ` K ) ` W ) ` ( I ` X ) ) i^i ( ( ( ocH ` K ) ` W ) ` ( I ` Y ) ) ) ) = ( I ` ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) ) )
42 hlol 
 |-  ( K e. HL -> K e. OL )
43 42 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> K e. OL )
44 1 2 25 20 oldmm4 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) = ( X .\/ Y ) )
45 43 7 12 44 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) = ( X .\/ Y ) )
46 45 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( I ` ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) ) ) = ( I ` ( X .\/ Y ) ) )
47 17 41 46 3eqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( I ` ( X .\/ Y ) ) = ( ( I ` X ) J ( I ` Y ) ) )