Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . 3
β’ ((πΎ β HL β§ π β π β§ π β π) β πΎ β HL) |
2 | | eqid 2731 |
. . . . 5
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
3 | | paddidm.s |
. . . . 5
β’ π = (PSubSpβπΎ) |
4 | 2, 3 | psubssat 38323 |
. . . 4
β’ ((πΎ β HL β§ π β π) β π β (AtomsβπΎ)) |
5 | 4 | 3adant3 1132 |
. . 3
β’ ((πΎ β HL β§ π β π β§ π β π) β π β (AtomsβπΎ)) |
6 | 2, 3 | psubssat 38323 |
. . . 4
β’ ((πΎ β HL β§ π β π) β π β (AtomsβπΎ)) |
7 | 6 | 3adant2 1131 |
. . 3
β’ ((πΎ β HL β§ π β π β§ π β π) β π β (AtomsβπΎ)) |
8 | | paddidm.p |
. . . 4
β’ + =
(+πβπΎ) |
9 | 2, 8 | paddssat 38383 |
. . 3
β’ ((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β (π + π) β (AtomsβπΎ)) |
10 | 1, 5, 7, 9 | syl3anc 1371 |
. 2
β’ ((πΎ β HL β§ π β π β§ π β π) β (π + π) β (AtomsβπΎ)) |
11 | | olc 866 |
. . . . 5
β’ ((π β (AtomsβπΎ) β§ βπ β (π + π)βπ β (π + π)π(leβπΎ)(π(joinβπΎ)π)) β ((π β (π + π) β¨ π β (π + π)) β¨ (π β (AtomsβπΎ) β§ βπ β (π + π)βπ β (π + π)π(leβπΎ)(π(joinβπΎ)π)))) |
12 | | eqid 2731 |
. . . . . . . 8
β’
(leβπΎ) =
(leβπΎ) |
13 | | eqid 2731 |
. . . . . . . 8
β’
(joinβπΎ) =
(joinβπΎ) |
14 | 12, 13, 2, 8 | elpadd 38368 |
. . . . . . 7
β’ ((πΎ β HL β§ (π + π) β (AtomsβπΎ) β§ (π + π) β (AtomsβπΎ)) β (π β ((π + π) + (π + π)) β ((π β (π + π) β¨ π β (π + π)) β¨ (π β (AtomsβπΎ) β§ βπ β (π + π)βπ β (π + π)π(leβπΎ)(π(joinβπΎ)π))))) |
15 | 1, 10, 10, 14 | syl3anc 1371 |
. . . . . 6
β’ ((πΎ β HL β§ π β π β§ π β π) β (π β ((π + π) + (π + π)) β ((π β (π + π) β¨ π β (π + π)) β¨ (π β (AtomsβπΎ) β§ βπ β (π + π)βπ β (π + π)π(leβπΎ)(π(joinβπΎ)π))))) |
16 | 2, 8 | padd4N 38409 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β ((π + π) + (π + π)) = ((π + π) + (π + π))) |
17 | 1, 5, 7, 5, 7, 16 | syl122anc 1379 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π β§ π β π) β ((π + π) + (π + π)) = ((π + π) + (π + π))) |
18 | 3, 8 | paddidm 38410 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π) β (π + π) = π) |
19 | 18 | 3adant3 1132 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π β§ π β π) β (π + π) = π) |
20 | 3, 8 | paddidm 38410 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π) β (π + π) = π) |
21 | 20 | 3adant2 1131 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π β§ π β π) β (π + π) = π) |
22 | 19, 21 | oveq12d 7395 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π β§ π β π) β ((π + π) + (π + π)) = (π + π)) |
23 | 17, 22 | eqtrd 2771 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π β§ π β π) β ((π + π) + (π + π)) = (π + π)) |
24 | 23 | eleq2d 2818 |
. . . . . 6
β’ ((πΎ β HL β§ π β π β§ π β π) β (π β ((π + π) + (π + π)) β π β (π + π))) |
25 | 15, 24 | bitr3d 280 |
. . . . 5
β’ ((πΎ β HL β§ π β π β§ π β π) β (((π β (π + π) β¨ π β (π + π)) β¨ (π β (AtomsβπΎ) β§ βπ β (π + π)βπ β (π + π)π(leβπΎ)(π(joinβπΎ)π))) β π β (π + π))) |
26 | 11, 25 | imbitrid 243 |
. . . 4
β’ ((πΎ β HL β§ π β π β§ π β π) β ((π β (AtomsβπΎ) β§ βπ β (π + π)βπ β (π + π)π(leβπΎ)(π(joinβπΎ)π)) β π β (π + π))) |
27 | 26 | expd 416 |
. . 3
β’ ((πΎ β HL β§ π β π β§ π β π) β (π β (AtomsβπΎ) β (βπ β (π + π)βπ β (π + π)π(leβπΎ)(π(joinβπΎ)π) β π β (π + π)))) |
28 | 27 | ralrimiv 3144 |
. 2
β’ ((πΎ β HL β§ π β π β§ π β π) β βπ β (AtomsβπΎ)(βπ β (π + π)βπ β (π + π)π(leβπΎ)(π(joinβπΎ)π) β π β (π + π))) |
29 | 12, 13, 2, 3 | ispsubsp2 38315 |
. . 3
β’ (πΎ β HL β ((π + π) β π β ((π + π) β (AtomsβπΎ) β§ βπ β (AtomsβπΎ)(βπ β (π + π)βπ β (π + π)π(leβπΎ)(π(joinβπΎ)π) β π β (π + π))))) |
30 | 29 | 3ad2ant1 1133 |
. 2
β’ ((πΎ β HL β§ π β π β§ π β π) β ((π + π) β π β ((π + π) β (AtomsβπΎ) β§ βπ β (AtomsβπΎ)(βπ β (π + π)βπ β (π + π)π(leβπΎ)(π(joinβπΎ)π) β π β (π + π))))) |
31 | 10, 28, 30 | mpbir2and 711 |
1
β’ ((πΎ β HL β§ π β π β§ π β π) β (π + π) β π) |