Step | Hyp | Ref
| Expression |
1 | | simp1 1134 |
. . 3
β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β πΎ β π) |
2 | | pclun.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
3 | | pclun.p |
. . . 4
β’ + =
(+πβπΎ) |
4 | 2, 3 | paddunssN 38982 |
. . 3
β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β (π βͺ π) β (π + π)) |
5 | 2, 3 | paddssat 38988 |
. . 3
β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β (π + π) β π΄) |
6 | | pclun.c |
. . . 4
β’ π = (PClβπΎ) |
7 | 2, 6 | pclssN 39068 |
. . 3
β’ ((πΎ β π β§ (π βͺ π) β (π + π) β§ (π + π) β π΄) β (πβ(π βͺ π)) β (πβ(π + π))) |
8 | 1, 4, 5, 7 | syl3anc 1369 |
. 2
β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β (πβ(π βͺ π)) β (πβ(π + π))) |
9 | | unss 4183 |
. . . . . . . . 9
β’ ((π β π΄ β§ π β π΄) β (π βͺ π) β π΄) |
10 | 9 | biimpi 215 |
. . . . . . . 8
β’ ((π β π΄ β§ π β π΄) β (π βͺ π) β π΄) |
11 | 10 | 3adant1 1128 |
. . . . . . 7
β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β (π βͺ π) β π΄) |
12 | 2, 6 | pclssidN 39069 |
. . . . . . 7
β’ ((πΎ β π β§ (π βͺ π) β π΄) β (π βͺ π) β (πβ(π βͺ π))) |
13 | 1, 11, 12 | syl2anc 582 |
. . . . . 6
β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β (π βͺ π) β (πβ(π βͺ π))) |
14 | | unss 4183 |
. . . . . 6
β’ ((π β (πβ(π βͺ π)) β§ π β (πβ(π βͺ π))) β (π βͺ π) β (πβ(π βͺ π))) |
15 | 13, 14 | sylibr 233 |
. . . . 5
β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β (π β (πβ(π βͺ π)) β§ π β (πβ(π βͺ π)))) |
16 | | simp2 1135 |
. . . . . 6
β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β π β π΄) |
17 | | simp3 1136 |
. . . . . 6
β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β π β π΄) |
18 | | eqid 2730 |
. . . . . . . 8
β’
(PSubSpβπΎ) =
(PSubSpβπΎ) |
19 | 2, 18, 6 | pclclN 39065 |
. . . . . . 7
β’ ((πΎ β π β§ (π βͺ π) β π΄) β (πβ(π βͺ π)) β (PSubSpβπΎ)) |
20 | 1, 11, 19 | syl2anc 582 |
. . . . . 6
β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β (πβ(π βͺ π)) β (PSubSpβπΎ)) |
21 | 2, 18, 3 | paddss 39019 |
. . . . . 6
β’ ((πΎ β π β§ (π β π΄ β§ π β π΄ β§ (πβ(π βͺ π)) β (PSubSpβπΎ))) β ((π β (πβ(π βͺ π)) β§ π β (πβ(π βͺ π))) β (π + π) β (πβ(π βͺ π)))) |
22 | 1, 16, 17, 20, 21 | syl13anc 1370 |
. . . . 5
β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β ((π β (πβ(π βͺ π)) β§ π β (πβ(π βͺ π))) β (π + π) β (πβ(π βͺ π)))) |
23 | 15, 22 | mpbid 231 |
. . . 4
β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β (π + π) β (πβ(π βͺ π))) |
24 | 2, 18 | psubssat 38928 |
. . . . 5
β’ ((πΎ β π β§ (πβ(π βͺ π)) β (PSubSpβπΎ)) β (πβ(π βͺ π)) β π΄) |
25 | 1, 20, 24 | syl2anc 582 |
. . . 4
β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β (πβ(π βͺ π)) β π΄) |
26 | 2, 6 | pclssN 39068 |
. . . 4
β’ ((πΎ β π β§ (π + π) β (πβ(π βͺ π)) β§ (πβ(π βͺ π)) β π΄) β (πβ(π + π)) β (πβ(πβ(π βͺ π)))) |
27 | 1, 23, 25, 26 | syl3anc 1369 |
. . 3
β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β (πβ(π + π)) β (πβ(πβ(π βͺ π)))) |
28 | 18, 6 | pclidN 39070 |
. . . 4
β’ ((πΎ β π β§ (πβ(π βͺ π)) β (PSubSpβπΎ)) β (πβ(πβ(π βͺ π))) = (πβ(π βͺ π))) |
29 | 1, 20, 28 | syl2anc 582 |
. . 3
β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β (πβ(πβ(π βͺ π))) = (πβ(π βͺ π))) |
30 | 27, 29 | sseqtrd 4021 |
. 2
β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β (πβ(π + π)) β (πβ(π βͺ π))) |
31 | 8, 30 | eqssd 3998 |
1
β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β (πβ(π βͺ π)) = (πβ(π + π))) |