Step | Hyp | Ref
| Expression |
1 | | eldiophb 41480 |
. . 3
β’ (π΄ β (Diophβπ) β (π β β0 β§
βπ β
(β€β₯βπ)βπ β (mzPolyβ(1...π))π΄ = {π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ (πβπ) = 0)})) |
2 | | simp-5r 784 |
. . . . . . . . 9
β’
((((((π β
β0 β§ π
β V) β§ (Β¬ π
β Fin β§ (1...π)
β π)) β§ (π β
(β€β₯βπ) β§ π β (mzPolyβ(1...π)))) β§ π β V) β§ (π:(1...π)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β π β V) |
3 | | simprr 771 |
. . . . . . . . . 10
β’ ((((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β§ (π β (β€β₯βπ) β§ π β (mzPolyβ(1...π)))) β π β (mzPolyβ(1...π))) |
4 | 3 | ad2antrr 724 |
. . . . . . . . 9
β’
((((((π β
β0 β§ π
β V) β§ (Β¬ π
β Fin β§ (1...π)
β π)) β§ (π β
(β€β₯βπ) β§ π β (mzPolyβ(1...π)))) β§ π β V) β§ (π:(1...π)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β π β (mzPolyβ(1...π))) |
5 | | simprl 769 |
. . . . . . . . . 10
β’
((((((π β
β0 β§ π
β V) β§ (Β¬ π
β Fin β§ (1...π)
β π)) β§ (π β
(β€β₯βπ) β§ π β (mzPolyβ(1...π)))) β§ π β V) β§ (π:(1...π)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β π:(1...π)β1-1βπ) |
6 | | f1f 6784 |
. . . . . . . . . 10
β’ (π:(1...π)β1-1βπ β π:(1...π)βΆπ) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
β’
((((((π β
β0 β§ π
β V) β§ (Β¬ π
β Fin β§ (1...π)
β π)) β§ (π β
(β€β₯βπ) β§ π β (mzPolyβ(1...π)))) β§ π β V) β§ (π:(1...π)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β π:(1...π)βΆπ) |
8 | | mzprename 41472 |
. . . . . . . . 9
β’ ((π β V β§ π β (mzPolyβ(1...π)) β§ π:(1...π)βΆπ) β (π β (β€ βm π) β¦ (πβ(π β π))) β (mzPolyβπ)) |
9 | 2, 4, 7, 8 | syl3anc 1371 |
. . . . . . . 8
β’
((((((π β
β0 β§ π
β V) β§ (Β¬ π
β Fin β§ (1...π)
β π)) β§ (π β
(β€β₯βπ) β§ π β (mzPolyβ(1...π)))) β§ π β V) β§ (π:(1...π)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β (π β (β€ βm π) β¦ (πβ(π β π))) β (mzPolyβπ)) |
10 | | simprr 771 |
. . . . . . . . 9
β’
((((((π β
β0 β§ π
β V) β§ (Β¬ π
β Fin β§ (1...π)
β π)) β§ (π β
(β€β₯βπ) β§ π β (mzPolyβ(1...π)))) β§ π β V) β§ (π:(1...π)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β (π βΎ (1...π)) = ( I βΎ (1...π))) |
11 | | diophrw 41482 |
. . . . . . . . . 10
β’ ((π β V β§ π:(1...π)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π))) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π β π)))βπ’) = 0)} = {π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ (πβπ) = 0)}) |
12 | 11 | eqcomd 2738 |
. . . . . . . . 9
β’ ((π β V β§ π:(1...π)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π))) β {π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ (πβπ) = 0)} = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π β π)))βπ’) = 0)}) |
13 | 2, 5, 10, 12 | syl3anc 1371 |
. . . . . . . 8
β’
((((((π β
β0 β§ π
β V) β§ (Β¬ π
β Fin β§ (1...π)
β π)) β§ (π β
(β€β₯βπ) β§ π β (mzPolyβ(1...π)))) β§ π β V) β§ (π:(1...π)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β {π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ (πβπ) = 0)} = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π β π)))βπ’) = 0)}) |
14 | | fveq1 6887 |
. . . . . . . . . . . . 13
β’ (π = (π β (β€ βm π) β¦ (πβ(π β π))) β (πβπ’) = ((π β (β€ βm π) β¦ (πβ(π β π)))βπ’)) |
15 | 14 | eqeq1d 2734 |
. . . . . . . . . . . 12
β’ (π = (π β (β€ βm π) β¦ (πβ(π β π))) β ((πβπ’) = 0 β ((π β (β€ βm π) β¦ (πβ(π β π)))βπ’) = 0)) |
16 | 15 | anbi2d 629 |
. . . . . . . . . . 11
β’ (π = (π β (β€ βm π) β¦ (πβ(π β π))) β ((π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0) β (π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π β π)))βπ’) = 0))) |
17 | 16 | rexbidv 3178 |
. . . . . . . . . 10
β’ (π = (π β (β€ βm π) β¦ (πβ(π β π))) β (βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0) β βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π β π)))βπ’) = 0))) |
18 | 17 | abbidv 2801 |
. . . . . . . . 9
β’ (π = (π β (β€ βm π) β¦ (πβ(π β π))) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π β π)))βπ’) = 0)}) |
19 | 18 | rspceeqv 3632 |
. . . . . . . 8
β’ (((π β (β€
βm π)
β¦ (πβ(π β π))) β (mzPolyβπ) β§ {π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ (πβπ) = 0)} = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ ((π β (β€ βm π) β¦ (πβ(π β π)))βπ’) = 0)}) β βπ β (mzPolyβπ){π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ (πβπ) = 0)} = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) |
20 | 9, 13, 19 | syl2anc 584 |
. . . . . . 7
β’
((((((π β
β0 β§ π
β V) β§ (Β¬ π
β Fin β§ (1...π)
β π)) β§ (π β
(β€β₯βπ) β§ π β (mzPolyβ(1...π)))) β§ π β V) β§ (π:(1...π)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) β βπ β (mzPolyβπ){π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ (πβπ) = 0)} = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) |
21 | | simplll 773 |
. . . . . . . . 9
β’ ((((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β§ (π β (β€β₯βπ) β§ π β (mzPolyβ(1...π)))) β π β
β0) |
22 | | simplrl 775 |
. . . . . . . . 9
β’ ((((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β§ (π β (β€β₯βπ) β§ π β (mzPolyβ(1...π)))) β Β¬ π β Fin) |
23 | | simplrr 776 |
. . . . . . . . 9
β’ ((((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β§ (π β (β€β₯βπ) β§ π β (mzPolyβ(1...π)))) β (1...π) β π) |
24 | | simprl 769 |
. . . . . . . . 9
β’ ((((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β§ (π β (β€β₯βπ) β§ π β (mzPolyβ(1...π)))) β π β (β€β₯βπ)) |
25 | | eldioph2lem2 41484 |
. . . . . . . . 9
β’ (((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π β (β€β₯βπ))) β βπ(π:(1...π)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) |
26 | 21, 22, 23, 24, 25 | syl22anc 837 |
. . . . . . . 8
β’ ((((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β§ (π β (β€β₯βπ) β§ π β (mzPolyβ(1...π)))) β βπ(π:(1...π)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) |
27 | | rexv 3499 |
. . . . . . . 8
β’
(βπ β V
(π:(1...π)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π))) β βπ(π:(1...π)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) |
28 | 26, 27 | sylibr 233 |
. . . . . . 7
β’ ((((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β§ (π β (β€β₯βπ) β§ π β (mzPolyβ(1...π)))) β βπ β V (π:(1...π)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) |
29 | 20, 28 | r19.29a 3162 |
. . . . . 6
β’ ((((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β§ (π β (β€β₯βπ) β§ π β (mzPolyβ(1...π)))) β βπ β (mzPolyβπ){π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ (πβπ) = 0)} = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) |
30 | | eqeq1 2736 |
. . . . . . 7
β’ (π΄ = {π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ (πβπ) = 0)} β (π΄ = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β {π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ (πβπ) = 0)} = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)})) |
31 | 30 | rexbidv 3178 |
. . . . . 6
β’ (π΄ = {π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ (πβπ) = 0)} β (βπ β (mzPolyβπ)π΄ = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β βπ β (mzPolyβπ){π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ (πβπ) = 0)} = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)})) |
32 | 29, 31 | syl5ibrcom 246 |
. . . . 5
β’ ((((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β§ (π β (β€β₯βπ) β§ π β (mzPolyβ(1...π)))) β (π΄ = {π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ (πβπ) = 0)} β βπ β (mzPolyβπ)π΄ = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)})) |
33 | 32 | rexlimdvva 3211 |
. . . 4
β’ (((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β (βπ β
(β€β₯βπ)βπ β (mzPolyβ(1...π))π΄ = {π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ (πβπ) = 0)} β βπ β (mzPolyβπ)π΄ = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)})) |
34 | 33 | adantld 491 |
. . 3
β’ (((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β ((π β β0 β§
βπ β
(β€β₯βπ)βπ β (mzPolyβ(1...π))π΄ = {π‘ β£ βπ β (β0
βm (1...π))(π‘ = (π βΎ (1...π)) β§ (πβπ) = 0)}) β βπ β (mzPolyβπ)π΄ = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)})) |
35 | 1, 34 | biimtrid 241 |
. 2
β’ (((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β (π΄ β (Diophβπ) β βπ β (mzPolyβπ)π΄ = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)})) |
36 | | simpr 485 |
. . . 4
β’
(((((π β
β0 β§ π
β V) β§ (Β¬ π
β Fin β§ (1...π)
β π)) β§ π β (mzPolyβπ)) β§ π΄ = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) β π΄ = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) |
37 | | simplll 773 |
. . . . . 6
β’ ((((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β§ π β (mzPolyβπ)) β π β
β0) |
38 | | simpllr 774 |
. . . . . 6
β’ ((((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β§ π β (mzPolyβπ)) β π β V) |
39 | | simplrr 776 |
. . . . . 6
β’ ((((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β§ π β (mzPolyβπ)) β (1...π) β π) |
40 | | simpr 485 |
. . . . . 6
β’ ((((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β§ π β (mzPolyβπ)) β π β (mzPolyβπ)) |
41 | | eldioph2 41485 |
. . . . . 6
β’ ((π β β0
β§ (π β V β§
(1...π) β π) β§ π β (mzPolyβπ)) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β (Diophβπ)) |
42 | 37, 38, 39, 40, 41 | syl121anc 1375 |
. . . . 5
β’ ((((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β§ π β (mzPolyβπ)) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β (Diophβπ)) |
43 | 42 | adantr 481 |
. . . 4
β’
(((((π β
β0 β§ π
β V) β§ (Β¬ π
β Fin β§ (1...π)
β π)) β§ π β (mzPolyβπ)) β§ π΄ = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) β {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β (Diophβπ)) |
44 | 36, 43 | eqeltrd 2833 |
. . 3
β’
(((((π β
β0 β§ π
β V) β§ (Β¬ π
β Fin β§ (1...π)
β π)) β§ π β (mzPolyβπ)) β§ π΄ = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) β π΄ β (Diophβπ)) |
45 | 44 | rexlimdva2 3157 |
. 2
β’ (((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β (βπ β (mzPolyβπ)π΄ = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β π΄ β (Diophβπ))) |
46 | 35, 45 | impbid 211 |
1
β’ (((π β β0
β§ π β V) β§
(Β¬ π β Fin β§
(1...π) β π)) β (π΄ β (Diophβπ) β βπ β (mzPolyβπ)π΄ = {π‘ β£ βπ’ β (β0
βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)})) |