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 𝐼 ) ) → ( 𝐼 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) )