Proof of Theorem islvol2aN
Step | Hyp | Ref
| Expression |
1 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑃 = 𝑄 → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑄)) |
2 | | simpl1 1057 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝐾 ∈ HL) |
3 | | simpl3 1059 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝑄 ∈ 𝐴) |
4 | | islvol2a.j |
. . . . . . . . . . 11
⊢ ∨ =
(join‘𝐾) |
5 | | islvol2a.a |
. . . . . . . . . . 11
⊢ 𝐴 = (Atoms‘𝐾) |
6 | 4, 5 | hlatjidm 33673 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴) → (𝑄 ∨ 𝑄) = 𝑄) |
7 | 2, 3, 6 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (𝑄 ∨ 𝑄) = 𝑄) |
8 | 1, 7 | sylan9eqr 2666 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 = 𝑄) → (𝑃 ∨ 𝑄) = 𝑄) |
9 | 8 | oveq1d 6564 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 = 𝑄) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑄 ∨ 𝑅)) |
10 | 9 | oveq1d 6564 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 = 𝑄) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = ((𝑄 ∨ 𝑅) ∨ 𝑆)) |
11 | | simprl 790 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝑅 ∈ 𝐴) |
12 | | simprr 792 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝑆 ∈ 𝐴) |
13 | | islvol2a.v |
. . . . . . . . 9
⊢ 𝑉 = (LVols‘𝐾) |
14 | 4, 5, 13 | 3atnelvolN 33890 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ¬ ((𝑄 ∨ 𝑅) ∨ 𝑆) ∈ 𝑉) |
15 | 2, 3, 11, 12, 14 | syl13anc 1320 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ¬ ((𝑄 ∨ 𝑅) ∨ 𝑆) ∈ 𝑉) |
16 | 15 | adantr 480 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 = 𝑄) → ¬ ((𝑄 ∨ 𝑅) ∨ 𝑆) ∈ 𝑉) |
17 | 10, 16 | eqneltrd 2707 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 = 𝑄) → ¬ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉) |
18 | 17 | ex 449 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (𝑃 = 𝑄 → ¬ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉)) |
19 | 18 | necon2ad 2797 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉 → 𝑃 ≠ 𝑄)) |
20 | | hllat 33668 |
. . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
21 | 2, 20 | syl 17 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝐾 ∈ Lat) |
22 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝐾) =
(Base‘𝐾) |
23 | 22, 5 | atbase 33594 |
. . . . . . 7
⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾)) |
24 | 23 | ad2antrl 760 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝑅 ∈ (Base‘𝐾)) |
25 | 22, 4, 5 | hlatjcl 33671 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
26 | 25 | adantr 480 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
27 | | islvol2a.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
28 | 22, 27, 4 | latleeqj2 16887 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) → (𝑅 ≤ (𝑃 ∨ 𝑄) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄))) |
29 | 21, 24, 26, 28 | syl3anc 1318 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (𝑅 ≤ (𝑃 ∨ 𝑄) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄))) |
30 | | simpl2 1058 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝑃 ∈ 𝐴) |
31 | 4, 5, 13 | 3atnelvolN 33890 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ¬ ((𝑃 ∨ 𝑄) ∨ 𝑆) ∈ 𝑉) |
32 | 2, 30, 3, 12, 31 | syl13anc 1320 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ¬ ((𝑃 ∨ 𝑄) ∨ 𝑆) ∈ 𝑉) |
33 | | oveq1 6556 |
. . . . . . . 8
⊢ (((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = ((𝑃 ∨ 𝑄) ∨ 𝑆)) |
34 | 33 | eleq1d 2672 |
. . . . . . 7
⊢ (((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉 ↔ ((𝑃 ∨ 𝑄) ∨ 𝑆) ∈ 𝑉)) |
35 | 34 | notbid 307 |
. . . . . 6
⊢ (((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄) → (¬ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉 ↔ ¬ ((𝑃 ∨ 𝑄) ∨ 𝑆) ∈ 𝑉)) |
36 | 32, 35 | syl5ibrcom 236 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄) → ¬ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉)) |
37 | 29, 36 | sylbid 229 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (𝑅 ≤ (𝑃 ∨ 𝑄) → ¬ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉)) |
38 | 37 | con2d 128 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉 → ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) |
39 | 22, 5 | atbase 33594 |
. . . . . . 7
⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ (Base‘𝐾)) |
40 | 39 | ad2antll 761 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝑆 ∈ (Base‘𝐾)) |
41 | 22, 4 | latjcl 16874 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾)) |
42 | 21, 26, 24, 41 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾)) |
43 | 22, 27, 4 | latleeqj2 16887 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾)) → (𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = ((𝑃 ∨ 𝑄) ∨ 𝑅))) |
44 | 21, 40, 42, 43 | syl3anc 1318 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = ((𝑃 ∨ 𝑄) ∨ 𝑅))) |
45 | 4, 5, 13 | 3atnelvolN 33890 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ¬ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑉) |
46 | 2, 30, 3, 11, 45 | syl13anc 1320 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ¬ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑉) |
47 | | eleq1 2676 |
. . . . . . 7
⊢ ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = ((𝑃 ∨ 𝑄) ∨ 𝑅) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉 ↔ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑉)) |
48 | 47 | notbid 307 |
. . . . . 6
⊢ ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = ((𝑃 ∨ 𝑄) ∨ 𝑅) → (¬ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉 ↔ ¬ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑉)) |
49 | 46, 48 | syl5ibrcom 236 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = ((𝑃 ∨ 𝑄) ∨ 𝑅) → ¬ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉)) |
50 | 44, 49 | sylbid 229 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) → ¬ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉)) |
51 | 50 | con2d 128 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉 → ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) |
52 | 19, 38, 51 | 3jcad 1236 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉 → (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))) |
53 | 27, 4, 5, 13 | lvoli2 33885 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉) |
54 | 53 | 3expia 1259 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉)) |
55 | 52, 54 | impbid 201 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉 ↔ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))) |