Proof of Theorem 2atm2atN
Step | Hyp | Ref
| Expression |
1 | | hlop 36999 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
2 | 1 | adantr 484 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝐾 ∈ OP) |
3 | | simpr3 1197 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑅 ∈ 𝐴) |
4 | | 2atm2at.z |
. . . . 5
⊢ 0 =
(0.‘𝐾) |
5 | | eqid 2738 |
. . . . 5
⊢
(lt‘𝐾) =
(lt‘𝐾) |
6 | | 2atm2at.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
7 | 4, 5, 6 | 0ltat 36928 |
. . . 4
⊢ ((𝐾 ∈ OP ∧ 𝑅 ∈ 𝐴) → 0 (lt‘𝐾)𝑅) |
8 | 2, 3, 7 | syl2anc 587 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 0 (lt‘𝐾)𝑅) |
9 | | simpl 486 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝐾 ∈ HL) |
10 | | simpr1 1195 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑃 ∈ 𝐴) |
11 | | eqid 2738 |
. . . . . 6
⊢
(le‘𝐾) =
(le‘𝐾) |
12 | | 2atm2at.j |
. . . . . 6
⊢ ∨ =
(join‘𝐾) |
13 | 11, 12, 6 | hlatlej1 37012 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → 𝑅(le‘𝐾)(𝑅 ∨ 𝑃)) |
14 | 9, 3, 10, 13 | syl3anc 1372 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑅(le‘𝐾)(𝑅 ∨ 𝑃)) |
15 | | simpr2 1196 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑄 ∈ 𝐴) |
16 | 11, 12, 6 | hlatlej1 37012 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑅(le‘𝐾)(𝑅 ∨ 𝑄)) |
17 | 9, 3, 15, 16 | syl3anc 1372 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑅(le‘𝐾)(𝑅 ∨ 𝑄)) |
18 | | hllat 37000 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
19 | 18 | adantr 484 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝐾 ∈ Lat) |
20 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝐾) =
(Base‘𝐾) |
21 | 20, 6 | atbase 36926 |
. . . . . 6
⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾)) |
22 | 3, 21 | syl 17 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑅 ∈ (Base‘𝐾)) |
23 | 20, 12, 6 | hlatjcl 37004 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → (𝑅 ∨ 𝑃) ∈ (Base‘𝐾)) |
24 | 9, 3, 10, 23 | syl3anc 1372 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑅 ∨ 𝑃) ∈ (Base‘𝐾)) |
25 | 20, 12, 6 | hlatjcl 37004 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑅 ∨ 𝑄) ∈ (Base‘𝐾)) |
26 | 9, 3, 15, 25 | syl3anc 1372 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑅 ∨ 𝑄) ∈ (Base‘𝐾)) |
27 | | 2atm2at.m |
. . . . . 6
⊢ ∧ =
(meet‘𝐾) |
28 | 20, 11, 27 | latlem12 17804 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑅 ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑃) ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑄) ∈ (Base‘𝐾))) → ((𝑅(le‘𝐾)(𝑅 ∨ 𝑃) ∧ 𝑅(le‘𝐾)(𝑅 ∨ 𝑄)) ↔ 𝑅(le‘𝐾)((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄)))) |
29 | 19, 22, 24, 26, 28 | syl13anc 1373 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑅(le‘𝐾)(𝑅 ∨ 𝑃) ∧ 𝑅(le‘𝐾)(𝑅 ∨ 𝑄)) ↔ 𝑅(le‘𝐾)((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄)))) |
30 | 14, 17, 29 | mpbi2and 712 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑅(le‘𝐾)((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄))) |
31 | | hlpos 37003 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset) |
32 | 31 | adantr 484 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝐾 ∈ Poset) |
33 | 20, 4 | op0cl 36821 |
. . . . 5
⊢ (𝐾 ∈ OP → 0 ∈
(Base‘𝐾)) |
34 | 2, 33 | syl 17 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 0 ∈ (Base‘𝐾)) |
35 | 20, 27 | latmcl 17778 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑅 ∨ 𝑃) ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑄) ∈ (Base‘𝐾)) → ((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄)) ∈ (Base‘𝐾)) |
36 | 19, 24, 26, 35 | syl3anc 1372 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄)) ∈ (Base‘𝐾)) |
37 | 20, 11, 5 | pltletr 17697 |
. . . 4
⊢ ((𝐾 ∈ Poset ∧ ( 0 ∈
(Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾) ∧ ((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄)) ∈ (Base‘𝐾))) → (( 0 (lt‘𝐾)𝑅 ∧ 𝑅(le‘𝐾)((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄))) → 0 (lt‘𝐾)((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄)))) |
38 | 32, 34, 22, 36, 37 | syl13anc 1373 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (( 0 (lt‘𝐾)𝑅 ∧ 𝑅(le‘𝐾)((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄))) → 0 (lt‘𝐾)((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄)))) |
39 | 8, 30, 38 | mp2and 699 |
. 2
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 0 (lt‘𝐾)((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄))) |
40 | 20, 5, 4 | opltn0 36827 |
. . 3
⊢ ((𝐾 ∈ OP ∧ ((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄)) ∈ (Base‘𝐾)) → ( 0 (lt‘𝐾)((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄)) ↔ ((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄)) ≠ 0 )) |
41 | 2, 36, 40 | syl2anc 587 |
. 2
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ( 0 (lt‘𝐾)((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄)) ↔ ((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄)) ≠ 0 )) |
42 | 39, 41 | mpbid 235 |
1
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄)) ≠ 0 ) |