Step | Hyp | Ref
| Expression |
1 | | simpl 482 |
. . . . 5
β’ ((πΎ β π΅ β§ π β π) β πΎ β π΅) |
2 | | eqid 2731 |
. . . . . 6
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
3 | | paddidm.s |
. . . . . 6
β’ π = (PSubSpβπΎ) |
4 | 2, 3 | psubssat 38929 |
. . . . 5
β’ ((πΎ β π΅ β§ π β π) β π β (AtomsβπΎ)) |
5 | | eqid 2731 |
. . . . . 6
β’
(leβπΎ) =
(leβπΎ) |
6 | | eqid 2731 |
. . . . . 6
β’
(joinβπΎ) =
(joinβπΎ) |
7 | | paddidm.p |
. . . . . 6
β’ + =
(+πβπΎ) |
8 | 5, 6, 2, 7 | elpadd 38974 |
. . . . 5
β’ ((πΎ β π΅ β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β (π β (π + π) β ((π β π β¨ π β π) β¨ (π β (AtomsβπΎ) β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π))))) |
9 | 1, 4, 4, 8 | syl3anc 1370 |
. . . 4
β’ ((πΎ β π΅ β§ π β π) β (π β (π + π) β ((π β π β¨ π β π) β¨ (π β (AtomsβπΎ) β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π))))) |
10 | | pm1.2 901 |
. . . . . 6
β’ ((π β π β¨ π β π) β π β π) |
11 | 10 | a1i 11 |
. . . . 5
β’ ((πΎ β π΅ β§ π β π) β ((π β π β¨ π β π) β π β π)) |
12 | 5, 6, 2, 3 | psubspi 38922 |
. . . . . . 7
β’ (((πΎ β π΅ β§ π β π β§ π β (AtomsβπΎ)) β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)) β π β π) |
13 | 12 | 3exp1 1351 |
. . . . . 6
β’ (πΎ β π΅ β (π β π β (π β (AtomsβπΎ) β (βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π) β π β π)))) |
14 | 13 | imp4b 421 |
. . . . 5
β’ ((πΎ β π΅ β§ π β π) β ((π β (AtomsβπΎ) β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)) β π β π)) |
15 | 11, 14 | jaod 856 |
. . . 4
β’ ((πΎ β π΅ β§ π β π) β (((π β π β¨ π β π) β¨ (π β (AtomsβπΎ) β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π))) β π β π)) |
16 | 9, 15 | sylbid 239 |
. . 3
β’ ((πΎ β π΅ β§ π β π) β (π β (π + π) β π β π)) |
17 | 16 | ssrdv 3988 |
. 2
β’ ((πΎ β π΅ β§ π β π) β (π + π) β π) |
18 | 2, 7 | sspadd1 38990 |
. . 3
β’ ((πΎ β π΅ β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β π β (π + π)) |
19 | 1, 4, 4, 18 | syl3anc 1370 |
. 2
β’ ((πΎ β π΅ β§ π β π) β π β (π + π)) |
20 | 17, 19 | eqssd 3999 |
1
β’ ((πΎ β π΅ β§ π β π) β (π + π) = π) |