Proof of Theorem 1cvrjat
Step | Hyp | Ref
| Expression |
1 | | simprr 792 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → ¬ 𝑃 ≤ 𝑋) |
2 | | 1cvrjat.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐾) |
3 | | 1cvrjat.l |
. . . . . . . 8
⊢ ≤ =
(le‘𝐾) |
4 | | 1cvrjat.j |
. . . . . . . 8
⊢ ∨ =
(join‘𝐾) |
5 | | 1cvrjat.c |
. . . . . . . 8
⊢ 𝐶 = ( ⋖ ‘𝐾) |
6 | | 1cvrjat.a |
. . . . . . . 8
⊢ 𝐴 = (Atoms‘𝐾) |
7 | 2, 3, 4, 5, 6 | cvr1 33714 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (¬ 𝑃 ≤ 𝑋 ↔ 𝑋𝐶(𝑋 ∨ 𝑃))) |
8 | 7 | adantr 480 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → (¬ 𝑃 ≤ 𝑋 ↔ 𝑋𝐶(𝑋 ∨ 𝑃))) |
9 | 1, 8 | mpbid 221 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → 𝑋𝐶(𝑋 ∨ 𝑃)) |
10 | | simpl1 1057 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → 𝐾 ∈ HL) |
11 | | hlop 33667 |
. . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
12 | 10, 11 | syl 17 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → 𝐾 ∈ OP) |
13 | | simpl2 1058 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → 𝑋 ∈ 𝐵) |
14 | | hllat 33668 |
. . . . . . . 8
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
15 | 10, 14 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → 𝐾 ∈ Lat) |
16 | | simpl3 1059 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → 𝑃 ∈ 𝐴) |
17 | 2, 6 | atbase 33594 |
. . . . . . . 8
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → 𝑃 ∈ 𝐵) |
19 | 2, 4 | latjcl 16874 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵) → (𝑋 ∨ 𝑃) ∈ 𝐵) |
20 | 15, 13, 18, 19 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → (𝑋 ∨ 𝑃) ∈ 𝐵) |
21 | | eqid 2610 |
. . . . . . 7
⊢
(oc‘𝐾) =
(oc‘𝐾) |
22 | 2, 21, 5 | cvrcon3b 33582 |
. . . . . 6
⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ (𝑋 ∨ 𝑃) ∈ 𝐵) → (𝑋𝐶(𝑋 ∨ 𝑃) ↔ ((oc‘𝐾)‘(𝑋 ∨ 𝑃))𝐶((oc‘𝐾)‘𝑋))) |
23 | 12, 13, 20, 22 | syl3anc 1318 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → (𝑋𝐶(𝑋 ∨ 𝑃) ↔ ((oc‘𝐾)‘(𝑋 ∨ 𝑃))𝐶((oc‘𝐾)‘𝑋))) |
24 | 9, 23 | mpbid 221 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → ((oc‘𝐾)‘(𝑋 ∨ 𝑃))𝐶((oc‘𝐾)‘𝑋)) |
25 | | hlatl 33665 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
26 | 10, 25 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → 𝐾 ∈ AtLat) |
27 | 2, 21 | opoccl 33499 |
. . . . . 6
⊢ ((𝐾 ∈ OP ∧ (𝑋 ∨ 𝑃) ∈ 𝐵) → ((oc‘𝐾)‘(𝑋 ∨ 𝑃)) ∈ 𝐵) |
28 | 12, 20, 27 | syl2anc 691 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → ((oc‘𝐾)‘(𝑋 ∨ 𝑃)) ∈ 𝐵) |
29 | 2, 21 | opoccl 33499 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵) |
30 | 12, 13, 29 | syl2anc 691 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → ((oc‘𝐾)‘𝑋) ∈ 𝐵) |
31 | | eqid 2610 |
. . . . . . . . 9
⊢
(0.‘𝐾) =
(0.‘𝐾) |
32 | | 1cvrjat.u |
. . . . . . . . 9
⊢ 1 =
(1.‘𝐾) |
33 | 31, 32, 21 | opoc1 33507 |
. . . . . . . 8
⊢ (𝐾 ∈ OP →
((oc‘𝐾)‘ 1 ) =
(0.‘𝐾)) |
34 | 10, 11, 33 | 3syl 18 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → ((oc‘𝐾)‘ 1 ) = (0.‘𝐾)) |
35 | | simprl 790 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → 𝑋𝐶 1 ) |
36 | 2, 32 | op1cl 33490 |
. . . . . . . . . 10
⊢ (𝐾 ∈ OP → 1 ∈ 𝐵) |
37 | 10, 11, 36 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → 1 ∈ 𝐵) |
38 | 2, 21, 5 | cvrcon3b 33582 |
. . . . . . . . 9
⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 1 ∈ 𝐵) → (𝑋𝐶 1 ↔ ((oc‘𝐾)‘ 1 )𝐶((oc‘𝐾)‘𝑋))) |
39 | 12, 13, 37, 38 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → (𝑋𝐶 1 ↔ ((oc‘𝐾)‘ 1 )𝐶((oc‘𝐾)‘𝑋))) |
40 | 35, 39 | mpbid 221 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → ((oc‘𝐾)‘ 1 )𝐶((oc‘𝐾)‘𝑋)) |
41 | 34, 40 | eqbrtrrd 4607 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → (0.‘𝐾)𝐶((oc‘𝐾)‘𝑋)) |
42 | 2, 31, 5, 6 | isat 33591 |
. . . . . . 7
⊢ (𝐾 ∈ HL →
(((oc‘𝐾)‘𝑋) ∈ 𝐴 ↔ (((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ (0.‘𝐾)𝐶((oc‘𝐾)‘𝑋)))) |
43 | 10, 42 | syl 17 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → (((oc‘𝐾)‘𝑋) ∈ 𝐴 ↔ (((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ (0.‘𝐾)𝐶((oc‘𝐾)‘𝑋)))) |
44 | 30, 41, 43 | mpbir2and 959 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → ((oc‘𝐾)‘𝑋) ∈ 𝐴) |
45 | 2, 3, 31, 5, 6 | atcvreq0 33619 |
. . . . 5
⊢ ((𝐾 ∈ AtLat ∧
((oc‘𝐾)‘(𝑋 ∨ 𝑃)) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐴) → (((oc‘𝐾)‘(𝑋 ∨ 𝑃))𝐶((oc‘𝐾)‘𝑋) ↔ ((oc‘𝐾)‘(𝑋 ∨ 𝑃)) = (0.‘𝐾))) |
46 | 26, 28, 44, 45 | syl3anc 1318 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → (((oc‘𝐾)‘(𝑋 ∨ 𝑃))𝐶((oc‘𝐾)‘𝑋) ↔ ((oc‘𝐾)‘(𝑋 ∨ 𝑃)) = (0.‘𝐾))) |
47 | 24, 46 | mpbid 221 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → ((oc‘𝐾)‘(𝑋 ∨ 𝑃)) = (0.‘𝐾)) |
48 | 47 | fveq2d 6107 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → ((oc‘𝐾)‘((oc‘𝐾)‘(𝑋 ∨ 𝑃))) = ((oc‘𝐾)‘(0.‘𝐾))) |
49 | 2, 21 | opococ 33500 |
. . 3
⊢ ((𝐾 ∈ OP ∧ (𝑋 ∨ 𝑃) ∈ 𝐵) → ((oc‘𝐾)‘((oc‘𝐾)‘(𝑋 ∨ 𝑃))) = (𝑋 ∨ 𝑃)) |
50 | 12, 20, 49 | syl2anc 691 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → ((oc‘𝐾)‘((oc‘𝐾)‘(𝑋 ∨ 𝑃))) = (𝑋 ∨ 𝑃)) |
51 | 31, 32, 21 | opoc0 33508 |
. . 3
⊢ (𝐾 ∈ OP →
((oc‘𝐾)‘(0.‘𝐾)) = 1 ) |
52 | 10, 11, 51 | 3syl 18 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → ((oc‘𝐾)‘(0.‘𝐾)) = 1 ) |
53 | 48, 50, 52 | 3eqtr3d 2652 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → (𝑋 ∨ 𝑃) = 1 ) |