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 ‘ 𝐾 )
djaj.h 𝐻 = ( LHyp ‘ 𝐾 )
djaj.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
djaj.j 𝐽 = ( ( vA ‘ 𝐾 ) ‘ 𝑊 )
Assertion djajN ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼 ) ) → ( 𝐼 ‘ ( 𝑋 𝑌 ) ) = ( ( 𝐼𝑋 ) 𝐽 ( 𝐼𝑌 ) ) )

Proof

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