Proof of Theorem pmodN
Step | Hyp | Ref
| Expression |
1 | | incom 4091 |
. 2
⊢ (𝑋 ∩ ((𝑋 ∩ 𝑍) + 𝑌)) = (((𝑋 ∩ 𝑍) + 𝑌) ∩ 𝑋) |
2 | | hllat 37000 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
3 | 2 | adantr 484 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝐾 ∈ Lat) |
4 | | simpr2 1196 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝑌 ⊆ 𝐴) |
5 | | inss2 4120 |
. . . . 5
⊢ (𝑋 ∩ 𝑍) ⊆ 𝑍 |
6 | | simpr3 1197 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝑍 ⊆ 𝐴) |
7 | 5, 6 | sstrid 3888 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 ∩ 𝑍) ⊆ 𝐴) |
8 | | pmod.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
9 | | pmod.p |
. . . . 5
⊢ + =
(+𝑃‘𝐾) |
10 | 8, 9 | paddcom 37450 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ⊆ 𝐴 ∧ (𝑋 ∩ 𝑍) ⊆ 𝐴) → (𝑌 + (𝑋 ∩ 𝑍)) = ((𝑋 ∩ 𝑍) + 𝑌)) |
11 | 3, 4, 7, 10 | syl3anc 1372 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑌 + (𝑋 ∩ 𝑍)) = ((𝑋 ∩ 𝑍) + 𝑌)) |
12 | 11 | ineq2d 4103 |
. 2
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 ∩ (𝑌 + (𝑋 ∩ 𝑍))) = (𝑋 ∩ ((𝑋 ∩ 𝑍) + 𝑌))) |
13 | | incom 4091 |
. . . 4
⊢ (𝑋 ∩ 𝑌) = (𝑌 ∩ 𝑋) |
14 | 13 | oveq2i 7181 |
. . 3
⊢ ((𝑋 ∩ 𝑍) + (𝑋 ∩ 𝑌)) = ((𝑋 ∩ 𝑍) + (𝑌 ∩ 𝑋)) |
15 | | inss2 4120 |
. . . . 5
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑌 |
16 | 15, 4 | sstrid 3888 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 ∩ 𝑌) ⊆ 𝐴) |
17 | 8, 9 | paddcom 37450 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∩ 𝑌) ⊆ 𝐴 ∧ (𝑋 ∩ 𝑍) ⊆ 𝐴) → ((𝑋 ∩ 𝑌) + (𝑋 ∩ 𝑍)) = ((𝑋 ∩ 𝑍) + (𝑋 ∩ 𝑌))) |
18 | 3, 16, 7, 17 | syl3anc 1372 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 ∩ 𝑌) + (𝑋 ∩ 𝑍)) = ((𝑋 ∩ 𝑍) + (𝑋 ∩ 𝑌))) |
19 | | simpr1 1195 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝑋 ∈ 𝑆) |
20 | 7, 4, 19 | 3jca 1129 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 ∩ 𝑍) ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆)) |
21 | | inss1 4119 |
. . . . 5
⊢ (𝑋 ∩ 𝑍) ⊆ 𝑋 |
22 | | pmod.s |
. . . . . 6
⊢ 𝑆 = (PSubSp‘𝐾) |
23 | 8, 22, 9 | pmod1i 37485 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ ((𝑋 ∩ 𝑍) ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆)) → ((𝑋 ∩ 𝑍) ⊆ 𝑋 → (((𝑋 ∩ 𝑍) + 𝑌) ∩ 𝑋) = ((𝑋 ∩ 𝑍) + (𝑌 ∩ 𝑋)))) |
24 | 21, 23 | mpi 20 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ ((𝑋 ∩ 𝑍) ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆)) → (((𝑋 ∩ 𝑍) + 𝑌) ∩ 𝑋) = ((𝑋 ∩ 𝑍) + (𝑌 ∩ 𝑋))) |
25 | 20, 24 | syldan 594 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (((𝑋 ∩ 𝑍) + 𝑌) ∩ 𝑋) = ((𝑋 ∩ 𝑍) + (𝑌 ∩ 𝑋))) |
26 | 14, 18, 25 | 3eqtr4a 2799 |
. 2
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 ∩ 𝑌) + (𝑋 ∩ 𝑍)) = (((𝑋 ∩ 𝑍) + 𝑌) ∩ 𝑋)) |
27 | 1, 12, 26 | 3eqtr4a 2799 |
1
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 ∩ (𝑌 + (𝑋 ∩ 𝑍))) = ((𝑋 ∩ 𝑌) + (𝑋 ∩ 𝑍))) |