Proof of Theorem pclunN
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp1 1137 | . . 3
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → 𝐾 ∈ 𝑉) | 
| 2 |  | pclun.a | . . . 4
⊢ 𝐴 = (Atoms‘𝐾) | 
| 3 |  | pclun.p | . . . 4
⊢  + =
(+𝑃‘𝐾) | 
| 4 | 2, 3 | paddunssN 39810 | . . 3
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ∪ 𝑌) ⊆ (𝑋 + 𝑌)) | 
| 5 | 2, 3 | paddssat 39816 | . . 3
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) ⊆ 𝐴) | 
| 6 |  | pclun.c | . . . 4
⊢ 𝑈 = (PCl‘𝐾) | 
| 7 | 2, 6 | pclssN 39896 | . . 3
⊢ ((𝐾 ∈ 𝑉 ∧ (𝑋 ∪ 𝑌) ⊆ (𝑋 + 𝑌) ∧ (𝑋 + 𝑌) ⊆ 𝐴) → (𝑈‘(𝑋 ∪ 𝑌)) ⊆ (𝑈‘(𝑋 + 𝑌))) | 
| 8 | 1, 4, 5, 7 | syl3anc 1373 | . 2
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘(𝑋 ∪ 𝑌)) ⊆ (𝑈‘(𝑋 + 𝑌))) | 
| 9 |  | unss 4190 | . . . . . . . . 9
⊢ ((𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ↔ (𝑋 ∪ 𝑌) ⊆ 𝐴) | 
| 10 | 9 | biimpi 216 | . . . . . . . 8
⊢ ((𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ∪ 𝑌) ⊆ 𝐴) | 
| 11 | 10 | 3adant1 1131 | . . . . . . 7
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ∪ 𝑌) ⊆ 𝐴) | 
| 12 | 2, 6 | pclssidN 39897 | . . . . . . 7
⊢ ((𝐾 ∈ 𝑉 ∧ (𝑋 ∪ 𝑌) ⊆ 𝐴) → (𝑋 ∪ 𝑌) ⊆ (𝑈‘(𝑋 ∪ 𝑌))) | 
| 13 | 1, 11, 12 | syl2anc 584 | . . . . . 6
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ∪ 𝑌) ⊆ (𝑈‘(𝑋 ∪ 𝑌))) | 
| 14 |  | unss 4190 | . . . . . 6
⊢ ((𝑋 ⊆ (𝑈‘(𝑋 ∪ 𝑌)) ∧ 𝑌 ⊆ (𝑈‘(𝑋 ∪ 𝑌))) ↔ (𝑋 ∪ 𝑌) ⊆ (𝑈‘(𝑋 ∪ 𝑌))) | 
| 15 | 13, 14 | sylibr 234 | . . . . 5
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ⊆ (𝑈‘(𝑋 ∪ 𝑌)) ∧ 𝑌 ⊆ (𝑈‘(𝑋 ∪ 𝑌)))) | 
| 16 |  | simp2 1138 | . . . . . 6
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → 𝑋 ⊆ 𝐴) | 
| 17 |  | simp3 1139 | . . . . . 6
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → 𝑌 ⊆ 𝐴) | 
| 18 |  | eqid 2737 | . . . . . . . 8
⊢
(PSubSp‘𝐾) =
(PSubSp‘𝐾) | 
| 19 | 2, 18, 6 | pclclN 39893 | . . . . . . 7
⊢ ((𝐾 ∈ 𝑉 ∧ (𝑋 ∪ 𝑌) ⊆ 𝐴) → (𝑈‘(𝑋 ∪ 𝑌)) ∈ (PSubSp‘𝐾)) | 
| 20 | 1, 11, 19 | syl2anc 584 | . . . . . 6
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘(𝑋 ∪ 𝑌)) ∈ (PSubSp‘𝐾)) | 
| 21 | 2, 18, 3 | paddss 39847 | . . . . . 6
⊢ ((𝐾 ∈ 𝑉 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ (𝑈‘(𝑋 ∪ 𝑌)) ∈ (PSubSp‘𝐾))) → ((𝑋 ⊆ (𝑈‘(𝑋 ∪ 𝑌)) ∧ 𝑌 ⊆ (𝑈‘(𝑋 ∪ 𝑌))) ↔ (𝑋 + 𝑌) ⊆ (𝑈‘(𝑋 ∪ 𝑌)))) | 
| 22 | 1, 16, 17, 20, 21 | syl13anc 1374 | . . . . 5
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝑋 ⊆ (𝑈‘(𝑋 ∪ 𝑌)) ∧ 𝑌 ⊆ (𝑈‘(𝑋 ∪ 𝑌))) ↔ (𝑋 + 𝑌) ⊆ (𝑈‘(𝑋 ∪ 𝑌)))) | 
| 23 | 15, 22 | mpbid 232 | . . . 4
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) ⊆ (𝑈‘(𝑋 ∪ 𝑌))) | 
| 24 | 2, 18 | psubssat 39756 | . . . . 5
⊢ ((𝐾 ∈ 𝑉 ∧ (𝑈‘(𝑋 ∪ 𝑌)) ∈ (PSubSp‘𝐾)) → (𝑈‘(𝑋 ∪ 𝑌)) ⊆ 𝐴) | 
| 25 | 1, 20, 24 | syl2anc 584 | . . . 4
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘(𝑋 ∪ 𝑌)) ⊆ 𝐴) | 
| 26 | 2, 6 | pclssN 39896 | . . . 4
⊢ ((𝐾 ∈ 𝑉 ∧ (𝑋 + 𝑌) ⊆ (𝑈‘(𝑋 ∪ 𝑌)) ∧ (𝑈‘(𝑋 ∪ 𝑌)) ⊆ 𝐴) → (𝑈‘(𝑋 + 𝑌)) ⊆ (𝑈‘(𝑈‘(𝑋 ∪ 𝑌)))) | 
| 27 | 1, 23, 25, 26 | syl3anc 1373 | . . 3
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘(𝑋 + 𝑌)) ⊆ (𝑈‘(𝑈‘(𝑋 ∪ 𝑌)))) | 
| 28 | 18, 6 | pclidN 39898 | . . . 4
⊢ ((𝐾 ∈ 𝑉 ∧ (𝑈‘(𝑋 ∪ 𝑌)) ∈ (PSubSp‘𝐾)) → (𝑈‘(𝑈‘(𝑋 ∪ 𝑌))) = (𝑈‘(𝑋 ∪ 𝑌))) | 
| 29 | 1, 20, 28 | syl2anc 584 | . . 3
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘(𝑈‘(𝑋 ∪ 𝑌))) = (𝑈‘(𝑋 ∪ 𝑌))) | 
| 30 | 27, 29 | sseqtrd 4020 | . 2
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘(𝑋 + 𝑌)) ⊆ (𝑈‘(𝑋 ∪ 𝑌))) | 
| 31 | 8, 30 | eqssd 4001 | 1
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘(𝑋 ∪ 𝑌)) = (𝑈‘(𝑋 + 𝑌))) |