Proof of Theorem cmt2N
| Step | Hyp | Ref
| Expression |
| 1 | | omllat 39243 |
. . . . . 6
⊢ (𝐾 ∈ OML → 𝐾 ∈ Lat) |
| 2 | 1 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat) |
| 3 | | cmt2.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
| 4 | | eqid 2737 |
. . . . . . 7
⊢
(meet‘𝐾) =
(meet‘𝐾) |
| 5 | 3, 4 | latmcl 18485 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)𝑌) ∈ 𝐵) |
| 6 | 1, 5 | syl3an1 1164 |
. . . . 5
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)𝑌) ∈ 𝐵) |
| 7 | | simp2 1138 |
. . . . . 6
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
| 8 | | omlop 39242 |
. . . . . . . 8
⊢ (𝐾 ∈ OML → 𝐾 ∈ OP) |
| 9 | 8 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ OP) |
| 10 | | simp3 1139 |
. . . . . . 7
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) |
| 11 | | cmt2.o |
. . . . . . . 8
⊢ ⊥ =
(oc‘𝐾) |
| 12 | 3, 11 | opoccl 39195 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑌) ∈ 𝐵) |
| 13 | 9, 10, 12 | syl2anc 584 |
. . . . . 6
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑌) ∈ 𝐵) |
| 14 | 3, 4 | latmcl 18485 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘𝑌) ∈ 𝐵) → (𝑋(meet‘𝐾)( ⊥ ‘𝑌)) ∈ 𝐵) |
| 15 | 2, 7, 13, 14 | syl3anc 1373 |
. . . . 5
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)( ⊥ ‘𝑌)) ∈ 𝐵) |
| 16 | | eqid 2737 |
. . . . . 6
⊢
(join‘𝐾) =
(join‘𝐾) |
| 17 | 3, 16 | latjcom 18492 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑋(meet‘𝐾)𝑌) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑌)) ∈ 𝐵) → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘𝑌))) = ((𝑋(meet‘𝐾)( ⊥ ‘𝑌))(join‘𝐾)(𝑋(meet‘𝐾)𝑌))) |
| 18 | 2, 6, 15, 17 | syl3anc 1373 |
. . . 4
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘𝑌))) = ((𝑋(meet‘𝐾)( ⊥ ‘𝑌))(join‘𝐾)(𝑋(meet‘𝐾)𝑌))) |
| 19 | 3, 11 | opococ 39196 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘( ⊥
‘𝑌)) = 𝑌) |
| 20 | 9, 10, 19 | syl2anc 584 |
. . . . . 6
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘( ⊥
‘𝑌)) = 𝑌) |
| 21 | 20 | oveq2d 7447 |
. . . . 5
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)( ⊥ ‘( ⊥
‘𝑌))) = (𝑋(meet‘𝐾)𝑌)) |
| 22 | 21 | oveq2d 7447 |
. . . 4
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(meet‘𝐾)( ⊥ ‘𝑌))(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘( ⊥
‘𝑌)))) = ((𝑋(meet‘𝐾)( ⊥ ‘𝑌))(join‘𝐾)(𝑋(meet‘𝐾)𝑌))) |
| 23 | 18, 22 | eqtr4d 2780 |
. . 3
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘𝑌))) = ((𝑋(meet‘𝐾)( ⊥ ‘𝑌))(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘( ⊥
‘𝑌))))) |
| 24 | 23 | eqeq2d 2748 |
. 2
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘𝑌))) ↔ 𝑋 = ((𝑋(meet‘𝐾)( ⊥ ‘𝑌))(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘( ⊥
‘𝑌)))))) |
| 25 | | cmt2.c |
. . 3
⊢ 𝐶 = (cm‘𝐾) |
| 26 | 3, 16, 4, 11, 25 | cmtvalN 39212 |
. 2
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘𝑌))))) |
| 27 | 3, 16, 4, 11, 25 | cmtvalN 39212 |
. . 3
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘𝑌) ∈ 𝐵) → (𝑋𝐶( ⊥ ‘𝑌) ↔ 𝑋 = ((𝑋(meet‘𝐾)( ⊥ ‘𝑌))(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘( ⊥
‘𝑌)))))) |
| 28 | 13, 27 | syld3an3 1411 |
. 2
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶( ⊥ ‘𝑌) ↔ 𝑋 = ((𝑋(meet‘𝐾)( ⊥ ‘𝑌))(join‘𝐾)(𝑋(meet‘𝐾)( ⊥ ‘( ⊥
‘𝑌)))))) |
| 29 | 24, 26, 28 | 3bitr4d 311 |
1
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋𝐶( ⊥ ‘𝑌))) |