Proof of Theorem pmodN
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | incom 4209 | . 2
⊢ (𝑋 ∩ ((𝑋 ∩ 𝑍) + 𝑌)) = (((𝑋 ∩ 𝑍) + 𝑌) ∩ 𝑋) | 
| 2 |  | hllat 39364 | . . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) | 
| 3 | 2 | adantr 480 | . . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝐾 ∈ Lat) | 
| 4 |  | simpr2 1196 | . . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝑌 ⊆ 𝐴) | 
| 5 |  | inss2 4238 | . . . . 5
⊢ (𝑋 ∩ 𝑍) ⊆ 𝑍 | 
| 6 |  | simpr3 1197 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝑍 ⊆ 𝐴) | 
| 7 | 5, 6 | sstrid 3995 | . . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 ∩ 𝑍) ⊆ 𝐴) | 
| 8 |  | pmod.a | . . . . 5
⊢ 𝐴 = (Atoms‘𝐾) | 
| 9 |  | pmod.p | . . . . 5
⊢  + =
(+𝑃‘𝐾) | 
| 10 | 8, 9 | paddcom 39815 | . . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ⊆ 𝐴 ∧ (𝑋 ∩ 𝑍) ⊆ 𝐴) → (𝑌 + (𝑋 ∩ 𝑍)) = ((𝑋 ∩ 𝑍) + 𝑌)) | 
| 11 | 3, 4, 7, 10 | syl3anc 1373 | . . 3
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑌 + (𝑋 ∩ 𝑍)) = ((𝑋 ∩ 𝑍) + 𝑌)) | 
| 12 | 11 | ineq2d 4220 | . 2
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 ∩ (𝑌 + (𝑋 ∩ 𝑍))) = (𝑋 ∩ ((𝑋 ∩ 𝑍) + 𝑌))) | 
| 13 |  | incom 4209 | . . . 4
⊢ (𝑋 ∩ 𝑌) = (𝑌 ∩ 𝑋) | 
| 14 | 13 | oveq2i 7442 | . . 3
⊢ ((𝑋 ∩ 𝑍) + (𝑋 ∩ 𝑌)) = ((𝑋 ∩ 𝑍) + (𝑌 ∩ 𝑋)) | 
| 15 |  | inss2 4238 | . . . . 5
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑌 | 
| 16 | 15, 4 | sstrid 3995 | . . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 ∩ 𝑌) ⊆ 𝐴) | 
| 17 | 8, 9 | paddcom 39815 | . . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∩ 𝑌) ⊆ 𝐴 ∧ (𝑋 ∩ 𝑍) ⊆ 𝐴) → ((𝑋 ∩ 𝑌) + (𝑋 ∩ 𝑍)) = ((𝑋 ∩ 𝑍) + (𝑋 ∩ 𝑌))) | 
| 18 | 3, 16, 7, 17 | syl3anc 1373 | . . 3
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 ∩ 𝑌) + (𝑋 ∩ 𝑍)) = ((𝑋 ∩ 𝑍) + (𝑋 ∩ 𝑌))) | 
| 19 |  | simpr1 1195 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝑋 ∈ 𝑆) | 
| 20 | 7, 4, 19 | 3jca 1129 | . . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 ∩ 𝑍) ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆)) | 
| 21 |  | inss1 4237 | . . . . 5
⊢ (𝑋 ∩ 𝑍) ⊆ 𝑋 | 
| 22 |  | pmod.s | . . . . . 6
⊢ 𝑆 = (PSubSp‘𝐾) | 
| 23 | 8, 22, 9 | pmod1i 39850 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ ((𝑋 ∩ 𝑍) ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆)) → ((𝑋 ∩ 𝑍) ⊆ 𝑋 → (((𝑋 ∩ 𝑍) + 𝑌) ∩ 𝑋) = ((𝑋 ∩ 𝑍) + (𝑌 ∩ 𝑋)))) | 
| 24 | 21, 23 | mpi 20 | . . . 4
⊢ ((𝐾 ∈ HL ∧ ((𝑋 ∩ 𝑍) ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆)) → (((𝑋 ∩ 𝑍) + 𝑌) ∩ 𝑋) = ((𝑋 ∩ 𝑍) + (𝑌 ∩ 𝑋))) | 
| 25 | 20, 24 | syldan 591 | . . 3
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (((𝑋 ∩ 𝑍) + 𝑌) ∩ 𝑋) = ((𝑋 ∩ 𝑍) + (𝑌 ∩ 𝑋))) | 
| 26 | 14, 18, 25 | 3eqtr4a 2803 | . 2
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 ∩ 𝑌) + (𝑋 ∩ 𝑍)) = (((𝑋 ∩ 𝑍) + 𝑌) ∩ 𝑋)) | 
| 27 | 1, 12, 26 | 3eqtr4a 2803 | 1
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 ∩ (𝑌 + (𝑋 ∩ 𝑍))) = ((𝑋 ∩ 𝑌) + (𝑋 ∩ 𝑍))) |