Step | Hyp | Ref
| Expression |
1 | | eldioph3b 42081 |
. 2
β’ (π΄ β (Diophβπ΅) β (π΅ β β0 β§
βπ β
(mzPolyββ)π΄ =
{π β£ βπ β (β0
βm β)(π = (π βΎ (1...π΅)) β§ (πβπ) = 0)})) |
2 | | simpr 484 |
. . . 4
β’ (((π΅ β β0
β§ π β
(mzPolyββ)) β§ π΄ = {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π΅)) β§ (πβπ) = 0)}) β π΄ = {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π΅)) β§ (πβπ) = 0)}) |
3 | | vex 3472 |
. . . . . . . 8
β’ π β V |
4 | | eqeq1 2730 |
. . . . . . . . . 10
β’ (π = π β (π = (π βΎ (1...π΅)) β π = (π βΎ (1...π΅)))) |
5 | 4 | anbi1d 629 |
. . . . . . . . 9
β’ (π = π β ((π = (π βΎ (1...π΅)) β§ (πβπ) = 0) β (π = (π βΎ (1...π΅)) β§ (πβπ) = 0))) |
6 | 5 | rexbidv 3172 |
. . . . . . . 8
β’ (π = π β (βπ β (β0
βm β)(π = (π βΎ (1...π΅)) β§ (πβπ) = 0) β βπ β (β0
βm β)(π = (π βΎ (1...π΅)) β§ (πβπ) = 0))) |
7 | 3, 6 | elab 3663 |
. . . . . . 7
β’ (π β {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π΅)) β§ (πβπ) = 0)} β βπ β (β0
βm β)(π = (π βΎ (1...π΅)) β§ (πβπ) = 0)) |
8 | | simpr 484 |
. . . . . . . . . . 11
β’ ((((π΅ β β0
β§ π β
(mzPolyββ)) β§ π β (β0
βm β)) β§ π = (π βΎ (1...π΅))) β π = (π βΎ (1...π΅))) |
9 | | elfznn 13536 |
. . . . . . . . . . . . . 14
β’ (π β (1...π΅) β π β β) |
10 | 9 | ssriv 3981 |
. . . . . . . . . . . . 13
β’
(1...π΅) β
β |
11 | | elmapssres 8863 |
. . . . . . . . . . . . 13
β’ ((π β (β0
βm β) β§ (1...π΅) β β) β (π βΎ (1...π΅)) β (β0
βm (1...π΅))) |
12 | 10, 11 | mpan2 688 |
. . . . . . . . . . . 12
β’ (π β (β0
βm β) β (π βΎ (1...π΅)) β (β0
βm (1...π΅))) |
13 | 12 | ad2antlr 724 |
. . . . . . . . . . 11
β’ ((((π΅ β β0
β§ π β
(mzPolyββ)) β§ π β (β0
βm β)) β§ π = (π βΎ (1...π΅))) β (π βΎ (1...π΅)) β (β0
βm (1...π΅))) |
14 | 8, 13 | eqeltrd 2827 |
. . . . . . . . . 10
β’ ((((π΅ β β0
β§ π β
(mzPolyββ)) β§ π β (β0
βm β)) β§ π = (π βΎ (1...π΅))) β π β (β0
βm (1...π΅))) |
15 | 14 | ex 412 |
. . . . . . . . 9
β’ (((π΅ β β0
β§ π β
(mzPolyββ)) β§ π β (β0
βm β)) β (π = (π βΎ (1...π΅)) β π β (β0
βm (1...π΅)))) |
16 | 15 | adantrd 491 |
. . . . . . . 8
β’ (((π΅ β β0
β§ π β
(mzPolyββ)) β§ π β (β0
βm β)) β ((π = (π βΎ (1...π΅)) β§ (πβπ) = 0) β π β (β0
βm (1...π΅)))) |
17 | 16 | rexlimdva 3149 |
. . . . . . 7
β’ ((π΅ β β0
β§ π β
(mzPolyββ)) β (βπ β (β0
βm β)(π = (π βΎ (1...π΅)) β§ (πβπ) = 0) β π β (β0
βm (1...π΅)))) |
18 | 7, 17 | biimtrid 241 |
. . . . . 6
β’ ((π΅ β β0
β§ π β
(mzPolyββ)) β (π β {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π΅)) β§ (πβπ) = 0)} β π β (β0
βm (1...π΅)))) |
19 | 18 | ssrdv 3983 |
. . . . 5
β’ ((π΅ β β0
β§ π β
(mzPolyββ)) β {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π΅)) β§ (πβπ) = 0)} β (β0
βm (1...π΅))) |
20 | 19 | adantr 480 |
. . . 4
β’ (((π΅ β β0
β§ π β
(mzPolyββ)) β§ π΄ = {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π΅)) β§ (πβπ) = 0)}) β {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π΅)) β§ (πβπ) = 0)} β (β0
βm (1...π΅))) |
21 | 2, 20 | eqsstrd 4015 |
. . 3
β’ (((π΅ β β0
β§ π β
(mzPolyββ)) β§ π΄ = {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π΅)) β§ (πβπ) = 0)}) β π΄ β (β0
βm (1...π΅))) |
22 | 21 | r19.29an 3152 |
. 2
β’ ((π΅ β β0
β§ βπ β
(mzPolyββ)π΄ =
{π β£ βπ β (β0
βm β)(π = (π βΎ (1...π΅)) β§ (πβπ) = 0)}) β π΄ β (β0
βm (1...π΅))) |
23 | 1, 22 | sylbi 216 |
1
β’ (π΄ β (Diophβπ΅) β π΄ β (β0
βm (1...π΅))) |