Proof of Theorem cmt2N
Step | Hyp | Ref
| Expression |
1 | | omllat 37256 |
. . . . . 6
⊢ (𝐾 ∈ OML → 𝐾 ∈ Lat) |
2 | 1 | 3ad2ant1 1132 |
. . . . 5
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat) |
3 | | cmt2.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
4 | | eqid 2738 |
. . . . . . 7
⊢
(meet‘𝐾) =
(meet‘𝐾) |
5 | 3, 4 | latmcl 18158 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)𝑌) ∈ 𝐵) |
6 | 1, 5 | syl3an1 1162 |
. . . . 5
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)𝑌) ∈ 𝐵) |
7 | | simp2 1136 |
. . . . . 6
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
8 | | omlop 37255 |
. . . . . . . 8
⊢ (𝐾 ∈ OML → 𝐾 ∈ OP) |
9 | 8 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ OP) |
10 | | simp3 1137 |
. . . . . . 7
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) |
11 | | cmt2.o |
. . . . . . . 8
⊢ ⊥ =
(oc‘𝐾) |
12 | 3, 11 | opoccl 37208 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑌) ∈ 𝐵) |
13 | 9, 10, 12 | syl2anc 584 |
. . . . . 6
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑌) ∈ 𝐵) |
14 | 3, 4 | latmcl 18158 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘𝑌) ∈ 𝐵) → (𝑋(meet‘𝐾)( ⊥ ‘𝑌)) ∈ 𝐵) |
15 | 2, 7, 13, 14 | syl3anc 1370 |
. . . . 5
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)( ⊥ ‘𝑌)) ∈ 𝐵) |
16 | | eqid 2738 |
. . . . . 6
⊢
(join‘𝐾) =
(join‘𝐾) |
17 | 3, 16 | latjcom 18165 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑋(meet‘𝐾)𝑌) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑌)) ∈ 𝐵) → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘𝑌))) = ((𝑋(meet‘𝐾)( ⊥ ‘𝑌))(join‘𝐾)(𝑋(meet‘𝐾)𝑌))) |
18 | 2, 6, 15, 17 | syl3anc 1370 |
. . . 4
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘𝑌))) = ((𝑋(meet‘𝐾)( ⊥ ‘𝑌))(join‘𝐾)(𝑋(meet‘𝐾)𝑌))) |
19 | 3, 11 | opococ 37209 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘( ⊥
‘𝑌)) = 𝑌) |
20 | 9, 10, 19 | syl2anc 584 |
. . . . . 6
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘( ⊥
‘𝑌)) = 𝑌) |
21 | 20 | oveq2d 7291 |
. . . . 5
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)( ⊥ ‘( ⊥
‘𝑌))) = (𝑋(meet‘𝐾)𝑌)) |
22 | 21 | oveq2d 7291 |
. . . 4
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(meet‘𝐾)( ⊥ ‘𝑌))(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘( ⊥
‘𝑌)))) = ((𝑋(meet‘𝐾)( ⊥ ‘𝑌))(join‘𝐾)(𝑋(meet‘𝐾)𝑌))) |
23 | 18, 22 | eqtr4d 2781 |
. . 3
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘𝑌))) = ((𝑋(meet‘𝐾)( ⊥ ‘𝑌))(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘( ⊥
‘𝑌))))) |
24 | 23 | eqeq2d 2749 |
. 2
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘𝑌))) ↔ 𝑋 = ((𝑋(meet‘𝐾)( ⊥ ‘𝑌))(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘( ⊥
‘𝑌)))))) |
25 | | cmt2.c |
. . 3
⊢ 𝐶 = (cm‘𝐾) |
26 | 3, 16, 4, 11, 25 | cmtvalN 37225 |
. 2
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘𝑌))))) |
27 | 3, 16, 4, 11, 25 | cmtvalN 37225 |
. . 3
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘𝑌) ∈ 𝐵) → (𝑋𝐶( ⊥ ‘𝑌) ↔ 𝑋 = ((𝑋(meet‘𝐾)( ⊥ ‘𝑌))(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘( ⊥
‘𝑌)))))) |
28 | 13, 27 | syld3an3 1408 |
. 2
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶( ⊥ ‘𝑌) ↔ 𝑋 = ((𝑋(meet‘𝐾)( ⊥ ‘𝑌))(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘( ⊥
‘𝑌)))))) |
29 | 24, 26, 28 | 3bitr4d 311 |
1
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋𝐶( ⊥ ‘𝑌))) |