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