Metamath Proof Explorer

Theorem djajN

Description: Transfer lattice join to DVecA partial vector space closed subspace join. Part of Lemma M of Crawley p. 120 line 29, with closed subspace join rather than subspace sum. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses djaj.k 
|- .\/ = ( join ` K )
djaj.h 
|- H = ( LHyp ` K )
djaj.i 
|- I = ( ( DIsoA ` K ) ` W )
djaj.j 
|- J = ( ( vA ` K ) ` W )
Assertion djajN 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( I ` ( X .\/ Y ) ) = ( ( I ` X ) J ( I ` Y ) ) )

Proof

Step Hyp Ref Expression
1 djaj.k 
 |-  .\/ = ( join ` K )
2 djaj.h 
 |-  H = ( LHyp ` K )
3 djaj.i 
 |-  I = ( ( DIsoA ` K ) ` W )
4 djaj.j 
 |-  J = ( ( vA ` K ) ` W )
5 hllat 
 |-  ( K e. HL -> K e. Lat )
6 5 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> K e. Lat )
7 hlop 
 |-  ( K e. HL -> K e. OP )
8 7 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> K e. OP )
9 eqid 
 |-  ( Base ` K ) = ( Base ` K )
10 9 2 3 diadmclN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> X e. ( Base ` K ) )
11 10 adantrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> X e. ( Base ` K ) )
12 eqid 
 |-  ( oc ` K ) = ( oc ` K )
13 9 12 opoccl 
 |-  ( ( K e. OP /\ X e. ( Base ` K ) ) -> ( ( oc ` K ) ` X ) e. ( Base ` K ) )
14 8 11 13 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( oc ` K ) ` X ) e. ( Base ` K ) )
15 9 2 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
16 15 ad2antlr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> W e. ( Base ` K ) )
17 9 12 opoccl 
 |-  ( ( K e. OP /\ W e. ( Base ` K ) ) -> ( ( oc ` K ) ` W ) e. ( Base ` K ) )
18 8 16 17 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( oc ` K ) ` W ) e. ( Base ` K ) )
19 9 1 latjcl 
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` X ) e. ( Base ` K ) /\ ( ( oc ` K ) ` W ) e. ( Base ` K ) ) -> ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) e. ( Base ` K ) )
20 6 14 18 19 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) e. ( Base ` K ) )
21 eqid 
 |-  ( meet ` K ) = ( meet ` K )
22 9 21 latmcl 
 |-  ( ( K e. Lat /\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) )
23 6 20 16 22 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) )
24 9 2 3 diadmclN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. dom I ) -> Y e. ( Base ` K ) )
25 24 adantrl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> Y e. ( Base ` K ) )
26 9 12 opoccl 
 |-  ( ( K e. OP /\ Y e. ( Base ` K ) ) -> ( ( oc ` K ) ` Y ) e. ( Base ` K ) )
27 8 25 26 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( oc ` K ) ` Y ) e. ( Base ` K ) )
28 9 1 latjcl 
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` Y ) e. ( Base ` K ) /\ ( ( oc ` K ) ` W ) e. ( Base ` K ) ) -> ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) e. ( Base ` K ) )
29 6 27 18 28 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) e. ( Base ` K ) )
30 9 21 latmcl 
 |-  ( ( K e. Lat /\ ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) )
31 6 29 16 30 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) )
32 9 21 latmcl 
 |-  ( ( K e. Lat /\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) /\ ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) ) -> ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) e. ( Base ` K ) )
33 6 23 31 32 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) e. ( Base ` K ) )
34 eqid 
 |-  ( le ` K ) = ( le ` K )
35 9 34 21 latmle2 
 |-  ( ( K e. Lat /\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) /\ ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) ) -> ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ( le ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) )
36 6 23 31 35 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ( le ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) )
37 9 34 21 latmle2 
 |-  ( ( K e. Lat /\ ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( le ` K ) W )
38 6 29 16 37 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( le ` K ) W )
39 9 34 6 33 31 16 36 38 lattrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ( le ` K ) W )
40 9 34 2 3 diaeldm 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) e. dom I <-> ( ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) e. ( Base ` K ) /\ ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ( le ` K ) W ) ) )
41 40 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) e. dom I <-> ( ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) e. ( Base ` K ) /\ ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ( le ` K ) W ) ) )
42 33 39 41 mpbir2and 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) e. dom I )
43 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
44 eqid 
 |-  ( ( ocA ` K ) ` W ) = ( ( ocA ` K ) ` W )
45 1 21 12 2 43 3 44 diaocN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) e. dom I ) -> ( I ` ( ( ( ( oc ` K ) ` ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) = ( ( ( ocA ` K ) ` W ) ` ( I ` ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) ) )
46 42 45 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( I ` ( ( ( ( oc ` K ) ` ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) = ( ( ( ocA ` K ) ` W ) ` ( I ` ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) ) )
47 hloml 
 |-  ( K e. HL -> K e. OML )
48 47 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> K e. OML )
49 9 1 latjcl 
 |-  ( ( K e. Lat /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( X .\/ Y ) e. ( Base ` K ) )
50 6 11 25 49 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( X .\/ Y ) e. ( Base ` K ) )
51 34 2 3 diadmleN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> X ( le ` K ) W )
52 51 adantrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> X ( le ` K ) W )
53 34 2 3 diadmleN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. dom I ) -> Y ( le ` K ) W )
54 53 adantrl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> Y ( le ` K ) W )
55 9 34 1 latjle12 
 |-  ( ( K e. Lat /\ ( X e. ( Base ` K ) /\ Y e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( X ( le ` K ) W /\ Y ( le ` K ) W ) <-> ( X .\/ Y ) ( le ` K ) W ) )
56 6 11 25 16 55 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( X ( le ` K ) W /\ Y ( le ` K ) W ) <-> ( X .\/ Y ) ( le ` K ) W ) )
57 52 54 56 mpbi2and 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( X .\/ Y ) ( le ` K ) W )
58 9 34 1 21 12 omlspjN 
 |-  ( ( K e. OML /\ ( ( X .\/ Y ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) /\ ( X .\/ Y ) ( le ` K ) W ) -> ( ( ( X .\/ Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) = ( X .\/ Y ) )
59 48 50 16 57 58 syl121anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( X .\/ Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) = ( X .\/ Y ) )
60 9 1 latjidm 
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` W ) e. ( Base ` K ) ) -> ( ( ( oc ` K ) ` W ) .\/ ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) )
61 6 18 60 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( oc ` K ) ` W ) .\/ ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) )
62 61 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( X .\/ Y ) .\/ ( ( ( oc ` K ) ` W ) .\/ ( ( oc ` K ) ` W ) ) ) = ( ( X .\/ Y ) .\/ ( ( oc ` K ) ` W ) ) )
63 9 1 latjass 
 |-  ( ( K e. Lat /\ ( ( X .\/ Y ) e. ( Base ` K ) /\ ( ( oc ` K ) ` W ) e. ( Base ` K ) /\ ( ( oc ` K ) ` W ) e. ( Base ` K ) ) ) -> ( ( ( X .\/ Y ) .\/ ( ( oc ` K ) ` W ) ) .\/ ( ( oc ` K ) ` W ) ) = ( ( X .\/ Y ) .\/ ( ( ( oc ` K ) ` W ) .\/ ( ( oc ` K ) ` W ) ) ) )
64 6 50 18 18 63 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( X .\/ Y ) .\/ ( ( oc ` K ) ` W ) ) .\/ ( ( oc ` K ) ` W ) ) = ( ( X .\/ Y ) .\/ ( ( ( oc ` K ) ` W ) .\/ ( ( oc ` K ) ` W ) ) ) )
65 hlol 
 |-  ( K e. HL -> K e. OL )
66 65 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> K e. OL )
67 9 1 21 12 oldmm2 
 |-  ( ( K e. OL /\ ( X .\/ Y ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( X .\/ Y ) ) ( meet ` K ) W ) ) = ( ( X .\/ Y ) .\/ ( ( oc ` K ) ` W ) ) )
68 66 50 16 67 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( X .\/ Y ) ) ( meet ` K ) W ) ) = ( ( X .\/ Y ) .\/ ( ( oc ` K ) ` W ) ) )
69 9 1 21 12 oldmj1 
 |-  ( ( K e. OL /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( X .\/ Y ) ) = ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) )
70 66 11 25 69 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( oc ` K ) ` ( X .\/ Y ) ) = ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) )
71 9 34 21 latleeqm1 
 |-  ( ( K e. Lat /\ X e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( X ( le ` K ) W <-> ( X ( meet ` K ) W ) = X ) )
72 6 11 16 71 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( X ( le ` K ) W <-> ( X ( meet ` K ) W ) = X ) )
73 52 72 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( X ( meet ` K ) W ) = X )
74 73 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( oc ` K ) ` ( X ( meet ` K ) W ) ) = ( ( oc ` K ) ` X ) )
75 9 1 21 12 oldmm1 
 |-  ( ( K e. OL /\ X e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( X ( meet ` K ) W ) ) = ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) )
76 66 11 16 75 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( oc ` K ) ` ( X ( meet ` K ) W ) ) = ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) )
77 74 76 eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( oc ` K ) ` X ) = ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) )
78 9 34 21 latleeqm1 
 |-  ( ( K e. Lat /\ Y e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( Y ( le ` K ) W <-> ( Y ( meet ` K ) W ) = Y ) )
79 6 25 16 78 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( Y ( le ` K ) W <-> ( Y ( meet ` K ) W ) = Y ) )
80 54 79 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( Y ( meet ` K ) W ) = Y )
81 80 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( oc ` K ) ` ( Y ( meet ` K ) W ) ) = ( ( oc ` K ) ` Y ) )
82 9 1 21 12 oldmm1 
 |-  ( ( K e. OL /\ Y e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( Y ( meet ` K ) W ) ) = ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) )
83 66 25 16 82 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( oc ` K ) ` ( Y ( meet ` K ) W ) ) = ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) )
84 81 83 eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( oc ` K ) ` Y ) = ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) )
85 77 84 oveq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( oc ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` Y ) ) = ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ) )
86 70 85 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( oc ` K ) ` ( X .\/ Y ) ) = ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ) )
87 86 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( oc ` K ) ` ( X .\/ Y ) ) ( meet ` K ) W ) = ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ) ( meet ` K ) W ) )
88 9 21 latmmdir 
 |-  ( ( K e. OL /\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) e. ( Base ` K ) /\ ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ) ( meet ` K ) W ) = ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) )
89 66 20 29 16 88 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ) ( meet ` K ) W ) = ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) )
90 87 89 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( oc ` K ) ` ( X .\/ Y ) ) ( meet ` K ) W ) = ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) )
91 90 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( X .\/ Y ) ) ( meet ` K ) W ) ) = ( ( oc ` K ) ` ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) )
92 68 91 eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( X .\/ Y ) .\/ ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) )
93 92 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( X .\/ Y ) .\/ ( ( oc ` K ) ` W ) ) .\/ ( ( oc ` K ) ` W ) ) = ( ( ( oc ` K ) ` ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) .\/ ( ( oc ` K ) ` W ) ) )
94 64 93 eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( X .\/ Y ) .\/ ( ( ( oc ` K ) ` W ) .\/ ( ( oc ` K ) ` W ) ) ) = ( ( ( oc ` K ) ` ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) .\/ ( ( oc ` K ) ` W ) ) )
95 62 94 eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( X .\/ Y ) .\/ ( ( oc ` K ) ` W ) ) = ( ( ( oc ` K ) ` ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) .\/ ( ( oc ` K ) ` W ) ) )
96 95 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( X .\/ Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) = ( ( ( ( oc ` K ) ` ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) )
97 59 96 eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( X .\/ Y ) = ( ( ( ( oc ` K ) ` ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) )
98 97 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( I ` ( X .\/ Y ) ) = ( I ` ( ( ( ( oc ` K ) ` ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) )
99 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( K e. HL /\ W e. H ) )
100 2 3 diaclN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` X ) e. ran I )
101 100 adantrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( I ` X ) e. ran I )
102 2 43 3 diaelrnN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( I ` X ) e. ran I ) -> ( I ` X ) C_ ( ( LTrn ` K ) ` W ) )
103 101 102 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( I ` X ) C_ ( ( LTrn ` K ) ` W ) )
104 2 3 diaclN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. dom I ) -> ( I ` Y ) e. ran I )
105 104 adantrl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( I ` Y ) e. ran I )
106 2 43 3 diaelrnN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( I ` Y ) e. ran I ) -> ( I ` Y ) C_ ( ( LTrn ` K ) ` W ) )
107 105 106 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( I ` Y ) C_ ( ( LTrn ` K ) ` W ) )
108 2 43 3 44 4 djavalN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( I ` X ) C_ ( ( LTrn ` K ) ` W ) /\ ( I ` Y ) C_ ( ( LTrn ` K ) ` W ) ) ) -> ( ( I ` X ) J ( I ` Y ) ) = ( ( ( ocA ` K ) ` W ) ` ( ( ( ( ocA ` K ) ` W ) ` ( I ` X ) ) i^i ( ( ( ocA ` K ) ` W ) ` ( I ` Y ) ) ) ) )
109 99 103 107 108 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( I ` X ) J ( I ` Y ) ) = ( ( ( ocA ` K ) ` W ) ` ( ( ( ( ocA ` K ) ` W ) ` ( I ` X ) ) i^i ( ( ( ocA ` K ) ` W ) ` ( I ` Y ) ) ) ) )
110 9 34 21 latmle2 
 |-  ( ( K e. Lat /\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( le ` K ) W )
111 6 20 16 110 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( le ` K ) W )
112 9 34 2 3 diaeldm 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. dom I <-> ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) /\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( le ` K ) W ) ) )
113 112 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. dom I <-> ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) /\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( le ` K ) W ) ) )
114 23 111 113 mpbir2and 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. dom I )
115 9 34 2 3 diaeldm 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. dom I <-> ( ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) /\ ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( le ` K ) W ) ) )
116 115 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. dom I <-> ( ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) /\ ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( le ` K ) W ) ) )
117 31 38 116 mpbir2and 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. dom I )
118 21 2 3 diameetN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. dom I /\ ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. dom I ) ) -> ( I ` ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) = ( ( I ` ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) i^i ( I ` ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) )
119 99 114 117 118 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( I ` ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) = ( ( I ` ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) i^i ( I ` ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) )
120 1 21 12 2 43 3 44 diaocN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) = ( ( ( ocA ` K ) ` W ) ` ( I ` X ) ) )
121 120 adantrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( I ` ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) = ( ( ( ocA ` K ) ` W ) ` ( I ` X ) ) )
122 1 21 12 2 43 3 44 diaocN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. dom I ) -> ( I ` ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) = ( ( ( ocA ` K ) ` W ) ` ( I ` Y ) ) )
123 122 adantrl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( I ` ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) = ( ( ( ocA ` K ) ` W ) ` ( I ` Y ) ) )
124 121 123 ineq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( I ` ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) i^i ( I ` ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) = ( ( ( ( ocA ` K ) ` W ) ` ( I ` X ) ) i^i ( ( ( ocA ` K ) ` W ) ` ( I ` Y ) ) ) )
125 119 124 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( I ` ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) = ( ( ( ( ocA ` K ) ` W ) ` ( I ` X ) ) i^i ( ( ( ocA ` K ) ` W ) ` ( I ` Y ) ) ) )
126 125 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( ( ocA ` K ) ` W ) ` ( I ` ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) ) = ( ( ( ocA ` K ) ` W ) ` ( ( ( ( ocA ` K ) ` W ) ` ( I ` X ) ) i^i ( ( ( ocA ` K ) ` W ) ` ( I ` Y ) ) ) ) )
127 109 126 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( ( I ` X ) J ( I ` Y ) ) = ( ( ( ocA ` K ) ` W ) ` ( I ` ( ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( meet ` K ) ( ( ( ( oc ` K ) ` Y ) .\/ ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) ) )
128 46 98 127 3eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( I ` ( X .\/ Y ) ) = ( ( I ` X ) J ( I ` Y ) ) )