Proof of Theorem oldmm1
Step | Hyp | Ref
| Expression |
1 | | oldmm1.b |
. 2
⊢ 𝐵 = (Base‘𝐾) |
2 | | eqid 2738 |
. 2
⊢
(le‘𝐾) =
(le‘𝐾) |
3 | | ollat 36850 |
. . 3
⊢ (𝐾 ∈ OL → 𝐾 ∈ Lat) |
4 | 3 | 3ad2ant1 1134 |
. 2
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat) |
5 | | olop 36851 |
. . . 4
⊢ (𝐾 ∈ OL → 𝐾 ∈ OP) |
6 | 5 | 3ad2ant1 1134 |
. . 3
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ OP) |
7 | | oldmm1.m |
. . . . 5
⊢ ∧ =
(meet‘𝐾) |
8 | 1, 7 | latmcl 17778 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵) |
9 | 3, 8 | syl3an1 1164 |
. . 3
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵) |
10 | | oldmm1.o |
. . . 4
⊢ ⊥ =
(oc‘𝐾) |
11 | 1, 10 | opoccl 36831 |
. . 3
⊢ ((𝐾 ∈ OP ∧ (𝑋 ∧ 𝑌) ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ 𝑌)) ∈ 𝐵) |
12 | 6, 9, 11 | syl2anc 587 |
. 2
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ 𝑌)) ∈ 𝐵) |
13 | 1, 10 | opoccl 36831 |
. . . . 5
⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵) |
14 | 5, 13 | sylan 583 |
. . . 4
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵) |
15 | 14 | 3adant3 1133 |
. . 3
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵) |
16 | 1, 10 | opoccl 36831 |
. . . . 5
⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑌) ∈ 𝐵) |
17 | 5, 16 | sylan 583 |
. . . 4
⊢ ((𝐾 ∈ OL ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑌) ∈ 𝐵) |
18 | 17 | 3adant2 1132 |
. . 3
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑌) ∈ 𝐵) |
19 | | oldmm1.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
20 | 1, 19 | latjcl 17777 |
. . 3
⊢ ((𝐾 ∈ Lat ∧ ( ⊥
‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘𝑌) ∈ 𝐵) → (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌)) ∈ 𝐵) |
21 | 4, 15, 18, 20 | syl3anc 1372 |
. 2
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌)) ∈ 𝐵) |
22 | 1, 2, 19 | latlej1 17786 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ ( ⊥
‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘𝑌) ∈ 𝐵) → ( ⊥ ‘𝑋)(le‘𝐾)(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) |
23 | 4, 15, 18, 22 | syl3anc 1372 |
. . . . 5
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑋)(le‘𝐾)(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) |
24 | | simp2 1138 |
. . . . . 6
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
25 | 1, 2, 10 | oplecon1b 36838 |
. . . . . 6
⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌)) ∈ 𝐵) → (( ⊥ ‘𝑋)(le‘𝐾)(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌)) ↔ ( ⊥ ‘(( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌)))(le‘𝐾)𝑋)) |
26 | 6, 24, 21, 25 | syl3anc 1372 |
. . . . 5
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋)(le‘𝐾)(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌)) ↔ ( ⊥ ‘(( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌)))(le‘𝐾)𝑋)) |
27 | 23, 26 | mpbid 235 |
. . . 4
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌)))(le‘𝐾)𝑋) |
28 | 1, 2, 19 | latlej2 17787 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ ( ⊥
‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘𝑌) ∈ 𝐵) → ( ⊥ ‘𝑌)(le‘𝐾)(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) |
29 | 4, 15, 18, 28 | syl3anc 1372 |
. . . . 5
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑌)(le‘𝐾)(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) |
30 | | simp3 1139 |
. . . . . 6
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) |
31 | 1, 2, 10 | oplecon1b 36838 |
. . . . . 6
⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ∧ (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌)) ∈ 𝐵) → (( ⊥ ‘𝑌)(le‘𝐾)(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌)) ↔ ( ⊥ ‘(( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌)))(le‘𝐾)𝑌)) |
32 | 6, 30, 21, 31 | syl3anc 1372 |
. . . . 5
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑌)(le‘𝐾)(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌)) ↔ ( ⊥ ‘(( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌)))(le‘𝐾)𝑌)) |
33 | 29, 32 | mpbid 235 |
. . . 4
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌)))(le‘𝐾)𝑌) |
34 | 1, 10 | opoccl 36831 |
. . . . . 6
⊢ ((𝐾 ∈ OP ∧ (( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌)) ∈ 𝐵) → ( ⊥ ‘(( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌))) ∈ 𝐵) |
35 | 6, 21, 34 | syl2anc 587 |
. . . . 5
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌))) ∈ 𝐵) |
36 | 1, 2, 7 | latlem12 17804 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (( ⊥
‘(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((( ⊥ ‘(( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌)))(le‘𝐾)𝑋 ∧ ( ⊥ ‘(( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌)))(le‘𝐾)𝑌) ↔ ( ⊥ ‘(( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌)))(le‘𝐾)(𝑋 ∧ 𝑌))) |
37 | 4, 35, 24, 30, 36 | syl13anc 1373 |
. . . 4
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((( ⊥ ‘(( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌)))(le‘𝐾)𝑋 ∧ ( ⊥ ‘(( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌)))(le‘𝐾)𝑌) ↔ ( ⊥ ‘(( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌)))(le‘𝐾)(𝑋 ∧ 𝑌))) |
38 | 27, 33, 37 | mpbi2and 712 |
. . 3
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌)))(le‘𝐾)(𝑋 ∧ 𝑌)) |
39 | 1, 2, 10 | oplecon1b 36838 |
. . . 4
⊢ ((𝐾 ∈ OP ∧ (( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌)) ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ∈ 𝐵) → (( ⊥ ‘(( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌)))(le‘𝐾)(𝑋 ∧ 𝑌) ↔ ( ⊥ ‘(𝑋 ∧ 𝑌))(le‘𝐾)(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌)))) |
40 | 6, 21, 9, 39 | syl3anc 1372 |
. . 3
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘(( ⊥
‘𝑋) ∨ ( ⊥
‘𝑌)))(le‘𝐾)(𝑋 ∧ 𝑌) ↔ ( ⊥ ‘(𝑋 ∧ 𝑌))(le‘𝐾)(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌)))) |
41 | 38, 40 | mpbid 235 |
. 2
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ 𝑌))(le‘𝐾)(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) |
42 | 1, 2, 7 | latmle1 17802 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌)(le‘𝐾)𝑋) |
43 | 3, 42 | syl3an1 1164 |
. . . 4
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌)(le‘𝐾)𝑋) |
44 | 1, 2, 10 | oplecon3b 36837 |
. . . . 5
⊢ ((𝐾 ∈ OP ∧ (𝑋 ∧ 𝑌) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((𝑋 ∧ 𝑌)(le‘𝐾)𝑋 ↔ ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘(𝑋 ∧ 𝑌)))) |
45 | 6, 9, 24, 44 | syl3anc 1372 |
. . . 4
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)(le‘𝐾)𝑋 ↔ ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘(𝑋 ∧ 𝑌)))) |
46 | 43, 45 | mpbid 235 |
. . 3
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘(𝑋 ∧ 𝑌))) |
47 | 1, 2, 7 | latmle2 17803 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌)(le‘𝐾)𝑌) |
48 | 3, 47 | syl3an1 1164 |
. . . 4
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌)(le‘𝐾)𝑌) |
49 | 1, 2, 10 | oplecon3b 36837 |
. . . . 5
⊢ ((𝐾 ∈ OP ∧ (𝑋 ∧ 𝑌) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)(le‘𝐾)𝑌 ↔ ( ⊥ ‘𝑌)(le‘𝐾)( ⊥ ‘(𝑋 ∧ 𝑌)))) |
50 | 6, 9, 30, 49 | syl3anc 1372 |
. . . 4
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)(le‘𝐾)𝑌 ↔ ( ⊥ ‘𝑌)(le‘𝐾)( ⊥ ‘(𝑋 ∧ 𝑌)))) |
51 | 48, 50 | mpbid 235 |
. . 3
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑌)(le‘𝐾)( ⊥ ‘(𝑋 ∧ 𝑌))) |
52 | 1, 2, 19 | latjle12 17788 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ (( ⊥
‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘𝑌) ∈ 𝐵 ∧ ( ⊥ ‘(𝑋 ∧ 𝑌)) ∈ 𝐵)) → ((( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘(𝑋 ∧ 𝑌)) ∧ ( ⊥ ‘𝑌)(le‘𝐾)( ⊥ ‘(𝑋 ∧ 𝑌))) ↔ (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))(le‘𝐾)( ⊥ ‘(𝑋 ∧ 𝑌)))) |
53 | 4, 15, 18, 12, 52 | syl13anc 1373 |
. . 3
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘(𝑋 ∧ 𝑌)) ∧ ( ⊥ ‘𝑌)(le‘𝐾)( ⊥ ‘(𝑋 ∧ 𝑌))) ↔ (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))(le‘𝐾)( ⊥ ‘(𝑋 ∧ 𝑌)))) |
54 | 46, 51, 53 | mpbi2and 712 |
. 2
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))(le‘𝐾)( ⊥ ‘(𝑋 ∧ 𝑌))) |
55 | 1, 2, 4, 12, 21, 41, 54 | latasymd 17783 |
1
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ 𝑌)) = (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) |