Step | Hyp | Ref
| Expression |
1 | | simp3 1137 |
. . 3
β’ ((πΎ β HL β§ π β π΄ β§ π β π) β π β π) |
2 | | iinss1 5012 |
. . 3
β’ (π β π β β©
π β π ((pmapβπΎ)β((ocβπΎ)βπ)) β β© π β π ((pmapβπΎ)β((ocβπΎ)βπ))) |
3 | | sslin 4234 |
. . 3
β’ (β© π β π ((pmapβπΎ)β((ocβπΎ)βπ)) β β© π β π ((pmapβπΎ)β((ocβπΎ)βπ)) β (π΄ β© β©
π β π ((pmapβπΎ)β((ocβπΎ)βπ))) β (π΄ β© β©
π β π ((pmapβπΎ)β((ocβπΎ)βπ)))) |
4 | 1, 2, 3 | 3syl 18 |
. 2
β’ ((πΎ β HL β§ π β π΄ β§ π β π) β (π΄ β© β©
π β π ((pmapβπΎ)β((ocβπΎ)βπ))) β (π΄ β© β©
π β π ((pmapβπΎ)β((ocβπΎ)βπ)))) |
5 | | eqid 2731 |
. . . 4
β’
(ocβπΎ) =
(ocβπΎ) |
6 | | 2polss.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
7 | | eqid 2731 |
. . . 4
β’
(pmapβπΎ) =
(pmapβπΎ) |
8 | | 2polss.p |
. . . 4
β’ β₯ =
(β₯πβπΎ) |
9 | 5, 6, 7, 8 | polvalN 39080 |
. . 3
β’ ((πΎ β HL β§ π β π΄) β ( β₯ βπ) = (π΄ β© β©
π β π ((pmapβπΎ)β((ocβπΎ)βπ)))) |
10 | 9 | 3adant3 1131 |
. 2
β’ ((πΎ β HL β§ π β π΄ β§ π β π) β ( β₯ βπ) = (π΄ β© β©
π β π ((pmapβπΎ)β((ocβπΎ)βπ)))) |
11 | | simp1 1135 |
. . 3
β’ ((πΎ β HL β§ π β π΄ β§ π β π) β πΎ β HL) |
12 | | simp2 1136 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ π β π) β π β π΄) |
13 | 1, 12 | sstrd 3992 |
. . 3
β’ ((πΎ β HL β§ π β π΄ β§ π β π) β π β π΄) |
14 | 5, 6, 7, 8 | polvalN 39080 |
. . 3
β’ ((πΎ β HL β§ π β π΄) β ( β₯ βπ) = (π΄ β© β©
π β π ((pmapβπΎ)β((ocβπΎ)βπ)))) |
15 | 11, 13, 14 | syl2anc 583 |
. 2
β’ ((πΎ β HL β§ π β π΄ β§ π β π) β ( β₯ βπ) = (π΄ β© β©
π β π ((pmapβπΎ)β((ocβπΎ)βπ)))) |
16 | 4, 10, 15 | 3sstr4d 4029 |
1
β’ ((πΎ β HL β§ π β π΄ β§ π β π) β ( β₯ βπ) β ( β₯ βπ)) |