This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem doca2N

Description: Double orthocomplement of partial isomorphism A. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses doca2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
doca2.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
doca2.n ⊢ ⊥ = ( ( ocA ‘ 𝐾 ) ‘ 𝑊 )
Assertion doca2N ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐼 ‘ 𝑋 ) ) ) = ( 𝐼 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 doca2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 doca2.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
3 doca2.n ⊢ ⊥ = ( ( ocA ‘ 𝐾 ) ‘ 𝑊 )
4 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
5 4 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → 𝐾 ∈ OL )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 6 1 2 diadmclN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
8 6 1 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
9 8 ad2antlr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
10 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
11 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
12 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
13 6 10 11 12 oldmm1 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) )
14 5 7 9 13 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) )
15 14 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) )
16 15 eqcomd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) = ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) )
17 16 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) )
18 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
19 18 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → 𝐾 ∈ Lat )
20 6 11 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
21 19 7 9 20 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
22 6 10 11 12 oldmm2 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) )
23 5 21 9 22 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) )
24 17 23 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) )
25 24 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) )
26 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
27 26 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → 𝐾 ∈ OP )
28 6 12 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
29 27 9 28 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
30 6 10 latjass ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( join ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
31 19 21 29 29 30 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( join ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
32 6 10 latjidm ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) )
33 19 29 32 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) )
34 33 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( join ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) )
35 31 34 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) )
36 25 35 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) )
37 36 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) = ( ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) )
38 hloml ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OML )
39 38 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → 𝐾 ∈ OML )
40 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
41 6 40 11 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( le ‘ 𝐾 ) 𝑊 )
42 19 7 9 41 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( le ‘ 𝐾 ) 𝑊 )
43 6 40 10 11 12 omlspjN ⊢ ( ( 𝐾 ∈ OML ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( le ‘ 𝐾 ) 𝑊 ) → ( ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) = ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) )
44 39 21 9 42 43 syl121anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) = ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) )
45 40 1 2 diadmleN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → 𝑋 ( le ‘ 𝐾 ) 𝑊 )
46 6 40 11 latleeqm1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑊 ↔ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) = 𝑋 ) )
47 19 7 9 46 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑊 ↔ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) = 𝑋 ) )
48 45 47 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) = 𝑋 )
49 37 44 48 3eqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → 𝑋 = ( ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) )
50 49 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑋 ) = ( 𝐼 ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) )
51 6 12 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
52 27 7 51 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
53 6 10 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
54 19 52 29 53 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
55 6 11 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
56 19 54 9 55 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
57 6 40 11 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ( le ‘ 𝐾 ) 𝑊 )
58 19 54 9 57 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ( le ‘ 𝐾 ) 𝑊 )
59 6 40 1 2 diaeldm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ dom 𝐼 ↔ ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ( le ‘ 𝐾 ) 𝑊 ) ) )
60 59 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ dom 𝐼 ↔ ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ( le ‘ 𝐾 ) 𝑊 ) ) )
61 56 58 60 mpbir2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ dom 𝐼 )
62 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
63 10 11 12 1 62 2 3 diaocN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ dom 𝐼 ) → ( 𝐼 ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ⊥ ‘ ( 𝐼 ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
64 61 63 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝐼 ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ⊥ ‘ ( 𝐼 ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
65 10 11 12 1 62 2 3 diaocN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝐼 ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ⊥ ‘ ( 𝐼 ‘ 𝑋 ) ) )
66 65 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ⊥ ‘ ( 𝐼 ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐼 ‘ 𝑋 ) ) ) )
67 50 64 66 3eqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐼 ‘ 𝑋 ) ) ) = ( 𝐼 ‘ 𝑋 ) )