Proof of Theorem omlspjN
Step | Hyp | Ref
| Expression |
1 | | omllat 37256 |
. . . . . 6
⊢ (𝐾 ∈ OML → 𝐾 ∈ Lat) |
2 | 1 | 3ad2ant1 1132 |
. . . . 5
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → 𝐾 ∈ Lat) |
3 | | omlop 37255 |
. . . . . . 7
⊢ (𝐾 ∈ OML → 𝐾 ∈ OP) |
4 | 3 | 3ad2ant1 1132 |
. . . . . 6
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → 𝐾 ∈ OP) |
5 | | simp2r 1199 |
. . . . . 6
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → 𝑌 ∈ 𝐵) |
6 | | omlspj.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
7 | | omlspj.o |
. . . . . . 7
⊢ ⊥ =
(oc‘𝐾) |
8 | 6, 7 | opoccl 37208 |
. . . . . 6
⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑌) ∈ 𝐵) |
9 | 4, 5, 8 | syl2anc 584 |
. . . . 5
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → ( ⊥ ‘𝑌) ∈ 𝐵) |
10 | | omlspj.m |
. . . . . 6
⊢ ∧ =
(meet‘𝐾) |
11 | 6, 10 | latmcom 18181 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ ( ⊥
‘𝑌) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑌) ∧ 𝑌) = (𝑌 ∧ ( ⊥ ‘𝑌))) |
12 | 2, 9, 5, 11 | syl3anc 1370 |
. . . 4
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (( ⊥ ‘𝑌) ∧ 𝑌) = (𝑌 ∧ ( ⊥ ‘𝑌))) |
13 | | eqid 2738 |
. . . . . 6
⊢
(0.‘𝐾) =
(0.‘𝐾) |
14 | 6, 7, 10, 13 | opnoncon 37222 |
. . . . 5
⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵) → (𝑌 ∧ ( ⊥ ‘𝑌)) = (0.‘𝐾)) |
15 | 4, 5, 14 | syl2anc 584 |
. . . 4
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑌 ∧ ( ⊥ ‘𝑌)) = (0.‘𝐾)) |
16 | 12, 15 | eqtrd 2778 |
. . 3
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (( ⊥ ‘𝑌) ∧ 𝑌) = (0.‘𝐾)) |
17 | 16 | oveq2d 7291 |
. 2
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 ∨ (( ⊥ ‘𝑌) ∧ 𝑌)) = (𝑋 ∨ (0.‘𝐾))) |
18 | | simp1 1135 |
. . 3
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → 𝐾 ∈ OML) |
19 | | simp2l 1198 |
. . 3
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → 𝑋 ∈ 𝐵) |
20 | | simp3 1137 |
. . 3
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → 𝑋 ≤ 𝑌) |
21 | | eqid 2738 |
. . . . . 6
⊢
(cm‘𝐾) =
(cm‘𝐾) |
22 | 6, 21 | cmtidN 37271 |
. . . . 5
⊢ ((𝐾 ∈ OML ∧ 𝑌 ∈ 𝐵) → 𝑌(cm‘𝐾)𝑌) |
23 | 18, 5, 22 | syl2anc 584 |
. . . 4
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → 𝑌(cm‘𝐾)𝑌) |
24 | 6, 7, 21 | cmt3N 37265 |
. . . . 5
⊢ ((𝐾 ∈ OML ∧ 𝑌 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑌(cm‘𝐾)𝑌 ↔ ( ⊥ ‘𝑌)(cm‘𝐾)𝑌)) |
25 | 18, 5, 5, 24 | syl3anc 1370 |
. . . 4
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑌(cm‘𝐾)𝑌 ↔ ( ⊥ ‘𝑌)(cm‘𝐾)𝑌)) |
26 | 23, 25 | mpbid 231 |
. . 3
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → ( ⊥ ‘𝑌)(cm‘𝐾)𝑌) |
27 | | omlspj.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
28 | | omlspj.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
29 | 6, 27, 28, 10, 21 | omlmod1i2N 37274 |
. . 3
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ ( ⊥ ‘𝑌) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ≤ 𝑌 ∧ ( ⊥ ‘𝑌)(cm‘𝐾)𝑌)) → (𝑋 ∨ (( ⊥ ‘𝑌) ∧ 𝑌)) = ((𝑋 ∨ ( ⊥ ‘𝑌)) ∧ 𝑌)) |
30 | 18, 19, 9, 5, 20, 26, 29 | syl132anc 1387 |
. 2
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 ∨ (( ⊥ ‘𝑌) ∧ 𝑌)) = ((𝑋 ∨ ( ⊥ ‘𝑌)) ∧ 𝑌)) |
31 | | omlol 37254 |
. . . 4
⊢ (𝐾 ∈ OML → 𝐾 ∈ OL) |
32 | 31 | 3ad2ant1 1132 |
. . 3
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → 𝐾 ∈ OL) |
33 | 6, 28, 13 | olj01 37239 |
. . 3
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ (0.‘𝐾)) = 𝑋) |
34 | 32, 19, 33 | syl2anc 584 |
. 2
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 ∨ (0.‘𝐾)) = 𝑋) |
35 | 17, 30, 34 | 3eqtr3d 2786 |
1
⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → ((𝑋 ∨ ( ⊥ ‘𝑌)) ∧ 𝑌) = 𝑋) |