Step | Hyp | Ref
| Expression |
1 | | fveq2 6891 |
. . . . . 6
β’ (π₯ = 0 β ((β
Dπ πΉ)βπ₯) = ((β Dπ πΉ)β0)) |
2 | 1 | eleq1d 2818 |
. . . . 5
β’ (π₯ = 0 β (((β
Dπ πΉ)βπ₯) β (Polyβπ) β ((β Dπ
πΉ)β0) β
(Polyβπ))) |
3 | 2 | imbi2d 340 |
. . . 4
β’ (π₯ = 0 β (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β ((β Dπ
πΉ)βπ₯) β (Polyβπ)) β ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β ((β Dπ
πΉ)β0) β
(Polyβπ)))) |
4 | | fveq2 6891 |
. . . . . 6
β’ (π₯ = π β ((β Dπ πΉ)βπ₯) = ((β Dπ πΉ)βπ)) |
5 | 4 | eleq1d 2818 |
. . . . 5
β’ (π₯ = π β (((β Dπ
πΉ)βπ₯) β (Polyβπ) β ((β Dπ
πΉ)βπ) β (Polyβπ))) |
6 | 5 | imbi2d 340 |
. . . 4
β’ (π₯ = π β (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β ((β Dπ
πΉ)βπ₯) β (Polyβπ)) β ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β ((β Dπ
πΉ)βπ) β (Polyβπ)))) |
7 | | fveq2 6891 |
. . . . . 6
β’ (π₯ = (π + 1) β ((β Dπ
πΉ)βπ₯) = ((β Dπ πΉ)β(π + 1))) |
8 | 7 | eleq1d 2818 |
. . . . 5
β’ (π₯ = (π + 1) β (((β Dπ
πΉ)βπ₯) β (Polyβπ) β ((β Dπ
πΉ)β(π + 1)) β (Polyβπ))) |
9 | 8 | imbi2d 340 |
. . . 4
β’ (π₯ = (π + 1) β (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β ((β Dπ
πΉ)βπ₯) β (Polyβπ)) β ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β ((β Dπ
πΉ)β(π + 1)) β (Polyβπ)))) |
10 | | fveq2 6891 |
. . . . . 6
β’ (π₯ = π β ((β Dπ
πΉ)βπ₯) = ((β Dπ πΉ)βπ)) |
11 | 10 | eleq1d 2818 |
. . . . 5
β’ (π₯ = π β (((β Dπ
πΉ)βπ₯) β (Polyβπ) β ((β Dπ
πΉ)βπ) β (Polyβπ))) |
12 | 11 | imbi2d 340 |
. . . 4
β’ (π₯ = π β (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β ((β Dπ
πΉ)βπ₯) β (Polyβπ)) β ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β ((β Dπ
πΉ)βπ) β (Polyβπ)))) |
13 | | ssid 4004 |
. . . . . 6
β’ β
β β |
14 | | cnex 11193 |
. . . . . . 7
β’ β
β V |
15 | | plyf 25936 |
. . . . . . . 8
β’ (πΉ β (Polyβπ) β πΉ:ββΆβ) |
16 | 15 | adantl 482 |
. . . . . . 7
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β πΉ:ββΆβ) |
17 | | fpmg 8864 |
. . . . . . 7
β’ ((β
β V β§ β β V β§ πΉ:ββΆβ) β πΉ β (β
βpm β)) |
18 | 14, 14, 16, 17 | mp3an12i 1465 |
. . . . . 6
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β πΉ β (β βpm
β)) |
19 | | dvn0 25665 |
. . . . . 6
β’ ((β
β β β§ πΉ
β (β βpm β)) β ((β
Dπ πΉ)β0) = πΉ) |
20 | 13, 18, 19 | sylancr 587 |
. . . . 5
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β ((β Dπ
πΉ)β0) = πΉ) |
21 | | simpr 485 |
. . . . 5
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β πΉ β (Polyβπ)) |
22 | 20, 21 | eqeltrd 2833 |
. . . 4
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β ((β Dπ
πΉ)β0) β
(Polyβπ)) |
23 | | dvply2g 26022 |
. . . . . . . . 9
β’ ((π β
(SubRingββfld) β§ ((β Dπ
πΉ)βπ) β (Polyβπ)) β (β D ((β
Dπ πΉ)βπ)) β (Polyβπ)) |
24 | 23 | ex 413 |
. . . . . . . 8
β’ (π β
(SubRingββfld) β (((β Dπ
πΉ)βπ) β (Polyβπ) β (β D ((β
Dπ πΉ)βπ)) β (Polyβπ))) |
25 | 24 | ad2antrr 724 |
. . . . . . 7
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β0) β
(((β Dπ πΉ)βπ) β (Polyβπ) β (β D ((β
Dπ πΉ)βπ)) β (Polyβπ))) |
26 | | dvnp1 25666 |
. . . . . . . . . 10
β’ ((β
β β β§ πΉ
β (β βpm β) β§ π β β0) β ((β
Dπ πΉ)β(π + 1)) = (β D ((β
Dπ πΉ)βπ))) |
27 | 13, 26 | mp3an1 1448 |
. . . . . . . . 9
β’ ((πΉ β (β
βpm β) β§ π β β0) β ((β
Dπ πΉ)β(π + 1)) = (β D ((β
Dπ πΉ)βπ))) |
28 | 18, 27 | sylan 580 |
. . . . . . . 8
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β0) β ((β
Dπ πΉ)β(π + 1)) = (β D ((β
Dπ πΉ)βπ))) |
29 | 28 | eleq1d 2818 |
. . . . . . 7
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β0) β
(((β Dπ πΉ)β(π + 1)) β (Polyβπ) β (β D ((β
Dπ πΉ)βπ)) β (Polyβπ))) |
30 | 25, 29 | sylibrd 258 |
. . . . . 6
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β0) β
(((β Dπ πΉ)βπ) β (Polyβπ) β ((β Dπ
πΉ)β(π + 1)) β (Polyβπ))) |
31 | 30 | expcom 414 |
. . . . 5
β’ (π β β0
β ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β (((β Dπ
πΉ)βπ) β (Polyβπ) β ((β Dπ
πΉ)β(π + 1)) β (Polyβπ)))) |
32 | 31 | a2d 29 |
. . . 4
β’ (π β β0
β (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β ((β Dπ
πΉ)βπ) β (Polyβπ)) β ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β ((β Dπ
πΉ)β(π + 1)) β (Polyβπ)))) |
33 | 3, 6, 9, 12, 22, 32 | nn0ind 12661 |
. . 3
β’ (π β β0
β ((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β ((β Dπ
πΉ)βπ) β (Polyβπ))) |
34 | 33 | impcom 408 |
. 2
β’ (((π β
(SubRingββfld) β§ πΉ β (Polyβπ)) β§ π β β0) β
((β Dπ πΉ)βπ) β (Polyβπ)) |
35 | 34 | 3impa 1110 |
1
β’ ((π β
(SubRingββfld) β§ πΉ β (Polyβπ) β§ π β β0) β
((β Dπ πΉ)βπ) β (Polyβπ)) |