Step | Hyp | Ref
| Expression |
1 | | simpl1 1191 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β HL) |
2 | | simpl2 1192 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
3 | | pl42lem.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
4 | | eqid 2736 |
. . . . . 6
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
5 | | pl42lem.f |
. . . . . 6
β’ πΉ = (pmapβπΎ) |
6 | 3, 4, 5 | pmapssat 37812 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅) β (πΉβπ) β (AtomsβπΎ)) |
7 | 1, 2, 6 | syl2anc 585 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (πΉβπ) β (AtomsβπΎ)) |
8 | | simpl3 1193 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
9 | 3, 4, 5 | pmapssat 37812 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅) β (πΉβπ) β (AtomsβπΎ)) |
10 | 1, 8, 9 | syl2anc 585 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (πΉβπ) β (AtomsβπΎ)) |
11 | | pl42lem.p |
. . . . 5
β’ + =
(+πβπΎ) |
12 | 4, 11 | paddssat 37867 |
. . . 4
β’ ((πΎ β HL β§ (πΉβπ) β (AtomsβπΎ) β§ (πΉβπ) β (AtomsβπΎ)) β ((πΉβπ) + (πΉβπ)) β (AtomsβπΎ)) |
13 | 1, 7, 10, 12 | syl3anc 1371 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((πΉβπ) + (πΉβπ)) β (AtomsβπΎ)) |
14 | | simpr2 1195 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
15 | 3, 4, 5 | pmapssat 37812 |
. . . 4
β’ ((πΎ β HL β§ π β π΅) β (πΉβπ) β (AtomsβπΎ)) |
16 | 1, 14, 15 | syl2anc 585 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (πΉβπ) β (AtomsβπΎ)) |
17 | | inss1 4168 |
. . . 4
β’ (((πΉβπ) + (πΉβπ)) β© (πΉβπ)) β ((πΉβπ) + (πΉβπ)) |
18 | 4, 11 | paddss1 37870 |
. . . 4
β’ ((πΎ β HL β§ ((πΉβπ) + (πΉβπ)) β (AtomsβπΎ) β§ (πΉβπ) β (AtomsβπΎ)) β ((((πΉβπ) + (πΉβπ)) β© (πΉβπ)) β ((πΉβπ) + (πΉβπ)) β ((((πΉβπ) + (πΉβπ)) β© (πΉβπ)) + (πΉβπ)) β (((πΉβπ) + (πΉβπ)) + (πΉβπ)))) |
19 | 17, 18 | mpi 20 |
. . 3
β’ ((πΎ β HL β§ ((πΉβπ) + (πΉβπ)) β (AtomsβπΎ) β§ (πΉβπ) β (AtomsβπΎ)) β ((((πΉβπ) + (πΉβπ)) β© (πΉβπ)) + (πΉβπ)) β (((πΉβπ) + (πΉβπ)) + (πΉβπ))) |
20 | 1, 13, 16, 19 | syl3anc 1371 |
. 2
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((((πΉβπ) + (πΉβπ)) β© (πΉβπ)) + (πΉβπ)) β (((πΉβπ) + (πΉβπ)) + (πΉβπ))) |
21 | | simpr3 1196 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
22 | 3, 4, 5 | pmapssat 37812 |
. . . 4
β’ ((πΎ β HL β§ π β π΅) β (πΉβπ) β (AtomsβπΎ)) |
23 | 1, 21, 22 | syl2anc 585 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (πΉβπ) β (AtomsβπΎ)) |
24 | 4, 11 | sspadd2 37869 |
. . 3
β’ ((πΎ β HL β§ (πΉβπ) β (AtomsβπΎ) β§ ((πΉβπ) + (πΉβπ)) β (AtomsβπΎ)) β (πΉβπ) β (((πΉβπ) + (πΉβπ)) + (πΉβπ))) |
25 | 1, 23, 13, 24 | syl3anc 1371 |
. 2
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (πΉβπ) β (((πΉβπ) + (πΉβπ)) + (πΉβπ))) |
26 | | ss2in 4176 |
. 2
β’
((((((πΉβπ) + (πΉβπ)) β© (πΉβπ)) + (πΉβπ)) β (((πΉβπ) + (πΉβπ)) + (πΉβπ)) β§ (πΉβπ) β (((πΉβπ) + (πΉβπ)) + (πΉβπ))) β (((((πΉβπ) + (πΉβπ)) β© (πΉβπ)) + (πΉβπ)) β© (πΉβπ)) β ((((πΉβπ) + (πΉβπ)) + (πΉβπ)) β© (((πΉβπ) + (πΉβπ)) + (πΉβπ)))) |
27 | 20, 25, 26 | syl2anc 585 |
1
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((((πΉβπ) + (πΉβπ)) β© (πΉβπ)) + (πΉβπ)) β© (πΉβπ)) β ((((πΉβπ) + (πΉβπ)) + (πΉβπ)) β© (((πΉβπ) + (πΉβπ)) + (πΉβπ)))) |