Proof of Theorem paddass
| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝐾 ∈ HL) |
| 2 | | simpr3 1197 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝑍 ⊆ 𝐴) |
| 3 | | simpr2 1196 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝑌 ⊆ 𝐴) |
| 4 | | simpr1 1195 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝑋 ⊆ 𝐴) |
| 5 | | paddass.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
| 6 | | paddass.p |
. . . . 5
⊢ + =
(+𝑃‘𝐾) |
| 7 | 5, 6 | paddasslem18 39839 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑍 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝐴)) → (𝑍 + (𝑌 + 𝑋)) ⊆ ((𝑍 + 𝑌) + 𝑋)) |
| 8 | 1, 2, 3, 4, 7 | syl13anc 1374 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑍 + (𝑌 + 𝑋)) ⊆ ((𝑍 + 𝑌) + 𝑋)) |
| 9 | | hllat 39364 |
. . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
| 10 | 5, 6 | paddcom 39815 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) |
| 11 | 9, 10 | syl3an1 1164 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) |
| 12 | 11 | 3adant3r3 1185 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) |
| 13 | 12 | oveq1d 7446 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 + 𝑌) + 𝑍) = ((𝑌 + 𝑋) + 𝑍)) |
| 14 | 5, 6 | paddssat 39816 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝐴) → (𝑌 + 𝑋) ⊆ 𝐴) |
| 15 | 1, 3, 4, 14 | syl3anc 1373 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑌 + 𝑋) ⊆ 𝐴) |
| 16 | 5, 6 | paddcom 39815 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ (𝑌 + 𝑋) ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → ((𝑌 + 𝑋) + 𝑍) = (𝑍 + (𝑌 + 𝑋))) |
| 17 | 9, 16 | syl3an1 1164 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑌 + 𝑋) ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → ((𝑌 + 𝑋) + 𝑍) = (𝑍 + (𝑌 + 𝑋))) |
| 18 | 1, 15, 2, 17 | syl3anc 1373 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑌 + 𝑋) + 𝑍) = (𝑍 + (𝑌 + 𝑋))) |
| 19 | 13, 18 | eqtrd 2777 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 + 𝑌) + 𝑍) = (𝑍 + (𝑌 + 𝑋))) |
| 20 | 5, 6 | paddcom 39815 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑌 + 𝑍) = (𝑍 + 𝑌)) |
| 21 | 9, 20 | syl3an1 1164 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑌 + 𝑍) = (𝑍 + 𝑌)) |
| 22 | 21 | 3adant3r1 1183 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑌 + 𝑍) = (𝑍 + 𝑌)) |
| 23 | 22 | oveq2d 7447 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 + (𝑍 + 𝑌))) |
| 24 | 5, 6 | paddssat 39816 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑍 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑍 + 𝑌) ⊆ 𝐴) |
| 25 | 1, 2, 3, 24 | syl3anc 1373 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑍 + 𝑌) ⊆ 𝐴) |
| 26 | 5, 6 | paddcom 39815 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ (𝑍 + 𝑌) ⊆ 𝐴) → (𝑋 + (𝑍 + 𝑌)) = ((𝑍 + 𝑌) + 𝑋)) |
| 27 | 9, 26 | syl3an1 1164 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ (𝑍 + 𝑌) ⊆ 𝐴) → (𝑋 + (𝑍 + 𝑌)) = ((𝑍 + 𝑌) + 𝑋)) |
| 28 | 1, 4, 25, 27 | syl3anc 1373 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (𝑍 + 𝑌)) = ((𝑍 + 𝑌) + 𝑋)) |
| 29 | 23, 28 | eqtrd 2777 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (𝑌 + 𝑍)) = ((𝑍 + 𝑌) + 𝑋)) |
| 30 | 8, 19, 29 | 3sstr4d 4039 |
. 2
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 + 𝑌) + 𝑍) ⊆ (𝑋 + (𝑌 + 𝑍))) |
| 31 | 5, 6 | paddasslem18 39839 |
. 2
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍)) |
| 32 | 30, 31 | eqssd 4001 |
1
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |