Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . 4
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π)) β πΎ β π΅) |
2 | | simpr1 1194 |
. . . 4
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π)) β π β π΄) |
3 | | simpr2 1195 |
. . . 4
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π)) β π β π΄) |
4 | | paddss.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
5 | | paddss.s |
. . . . . 6
β’ π = (PSubSpβπΎ) |
6 | 4, 5 | psubssat 38323 |
. . . . 5
β’ ((πΎ β π΅ β§ π β π) β π β π΄) |
7 | 6 | 3ad2antr3 1190 |
. . . 4
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π)) β π β π΄) |
8 | | paddss.p |
. . . . 5
β’ + =
(+πβπΎ) |
9 | 4, 8 | paddssw1 38412 |
. . . 4
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β π β§ π β π) β (π + π) β (π + π))) |
10 | 1, 2, 3, 7, 9 | syl13anc 1372 |
. . 3
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π)) β ((π β π β§ π β π) β (π + π) β (π + π))) |
11 | 5, 8 | paddidm 38410 |
. . . . 5
β’ ((πΎ β π΅ β§ π β π) β (π + π) = π) |
12 | 11 | 3ad2antr3 1190 |
. . . 4
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π)) β (π + π) = π) |
13 | 12 | sseq2d 3994 |
. . 3
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π)) β ((π + π) β (π + π) β (π + π) β π)) |
14 | 10, 13 | sylibd 238 |
. 2
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π)) β ((π β π β§ π β π) β (π + π) β π)) |
15 | 4, 8 | paddssw2 38413 |
. . 3
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π + π) β π β (π β π β§ π β π))) |
16 | 1, 2, 3, 7, 15 | syl13anc 1372 |
. 2
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π)) β ((π + π) β π β (π β π β§ π β π))) |
17 | 14, 16 | impbid 211 |
1
β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π)) β ((π β π β§ π β π) β (π + π) β π)) |