Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. 2
β’ ((π β β0
β§ π β
(mzPolyββ)) β π β
β0) |
2 | | simpr 486 |
. . 3
β’ ((π β β0
β§ π β
(mzPolyββ)) β π β
(mzPolyββ)) |
3 | | eqidd 2734 |
. . 3
β’ ((π β β0
β§ π β
(mzPolyββ)) β {π‘ β£ βπ’ β (β0
βm β)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm β)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) |
4 | | fveq1 6891 |
. . . . . . . . 9
β’ (π = π β (πβπ) = (πβπ)) |
5 | 4 | eqeq1d 2735 |
. . . . . . . 8
β’ (π = π β ((πβπ) = 0 β (πβπ) = 0)) |
6 | 5 | anbi2d 630 |
. . . . . . 7
β’ (π = π β ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β (π = (π βΎ (1...π)) β§ (πβπ) = 0))) |
7 | 6 | rexbidv 3179 |
. . . . . 6
β’ (π = π β (βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0) β βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0))) |
8 | 7 | abbidv 2802 |
. . . . 5
β’ (π = π β {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)} = {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)}) |
9 | | eqeq1 2737 |
. . . . . . . . 9
β’ (π = π‘ β (π = (π βΎ (1...π)) β π‘ = (π βΎ (1...π)))) |
10 | 9 | anbi1d 631 |
. . . . . . . 8
β’ (π = π‘ β ((π = (π βΎ (1...π)) β§ (πβπ) = 0) β (π‘ = (π βΎ (1...π)) β§ (πβπ) = 0))) |
11 | 10 | rexbidv 3179 |
. . . . . . 7
β’ (π = π‘ β (βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0) β βπ β (β0
βm β)(π‘ = (π βΎ (1...π)) β§ (πβπ) = 0))) |
12 | | reseq1 5976 |
. . . . . . . . . 10
β’ (π = π’ β (π βΎ (1...π)) = (π’ βΎ (1...π))) |
13 | 12 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π = π’ β (π‘ = (π βΎ (1...π)) β π‘ = (π’ βΎ (1...π)))) |
14 | | fveqeq2 6901 |
. . . . . . . . 9
β’ (π = π’ β ((πβπ) = 0 β (πβπ’) = 0)) |
15 | 13, 14 | anbi12d 632 |
. . . . . . . 8
β’ (π = π’ β ((π‘ = (π βΎ (1...π)) β§ (πβπ) = 0) β (π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0))) |
16 | 15 | cbvrexvw 3236 |
. . . . . . 7
β’
(βπ β
(β0 βm β)(π‘ = (π βΎ (1...π)) β§ (πβπ) = 0) β βπ’ β (β0
βm β)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)) |
17 | 11, 16 | bitrdi 287 |
. . . . . 6
β’ (π = π‘ β (βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0) β βπ’ β (β0
βm β)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0))) |
18 | 17 | cbvabv 2806 |
. . . . 5
β’ {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)} = {π‘ β£ βπ’ β (β0
βm β)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} |
19 | 8, 18 | eqtrdi 2789 |
. . . 4
β’ (π = π β {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)} = {π‘ β£ βπ’ β (β0
βm β)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) |
20 | 19 | rspceeqv 3634 |
. . 3
β’ ((π β (mzPolyββ)
β§ {π‘ β£
βπ’ β
(β0 βm β)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm β)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) β βπ β (mzPolyββ){π‘ β£ βπ’ β (β0
βm β)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)}) |
21 | 2, 3, 20 | syl2anc 585 |
. 2
β’ ((π β β0
β§ π β
(mzPolyββ)) β βπ β (mzPolyββ){π‘ β£ βπ’ β (β0
βm β)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)}) |
22 | | eldioph3b 41503 |
. 2
β’ ({π‘ β£ βπ’ β (β0
βm β)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β (Diophβπ) β (π β β0 β§
βπ β
(mzPolyββ){π‘
β£ βπ’ β
(β0 βm β)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π β£ βπ β (β0
βm β)(π = (π βΎ (1...π)) β§ (πβπ) = 0)})) |
23 | 1, 21, 22 | sylanbrc 584 |
1
β’ ((π β β0
β§ π β
(mzPolyββ)) β {π‘ β£ βπ’ β (β0
βm β)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β (Diophβπ)) |