Step | Hyp | Ref
| Expression |
1 | | dgrcolem1.2 |
. 2
β’ (π β π β β) |
2 | | oveq2 7417 |
. . . . . . 7
β’ (π¦ = 1 β ((πΊβπ₯)βπ¦) = ((πΊβπ₯)β1)) |
3 | 2 | mpteq2dv 5251 |
. . . . . 6
β’ (π¦ = 1 β (π₯ β β β¦ ((πΊβπ₯)βπ¦)) = (π₯ β β β¦ ((πΊβπ₯)β1))) |
4 | 3 | fveq2d 6896 |
. . . . 5
β’ (π¦ = 1 β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ¦))) = (degβ(π₯ β β β¦ ((πΊβπ₯)β1)))) |
5 | | oveq1 7416 |
. . . . 5
β’ (π¦ = 1 β (π¦ Β· π) = (1 Β· π)) |
6 | 4, 5 | eqeq12d 2749 |
. . . 4
β’ (π¦ = 1 β ((degβ(π₯ β β β¦ ((πΊβπ₯)βπ¦))) = (π¦ Β· π) β (degβ(π₯ β β β¦ ((πΊβπ₯)β1))) = (1 Β· π))) |
7 | 6 | imbi2d 341 |
. . 3
β’ (π¦ = 1 β ((π β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ¦))) = (π¦ Β· π)) β (π β (degβ(π₯ β β β¦ ((πΊβπ₯)β1))) = (1 Β· π)))) |
8 | | oveq2 7417 |
. . . . . . 7
β’ (π¦ = π β ((πΊβπ₯)βπ¦) = ((πΊβπ₯)βπ)) |
9 | 8 | mpteq2dv 5251 |
. . . . . 6
β’ (π¦ = π β (π₯ β β β¦ ((πΊβπ₯)βπ¦)) = (π₯ β β β¦ ((πΊβπ₯)βπ))) |
10 | 9 | fveq2d 6896 |
. . . . 5
β’ (π¦ = π β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ¦))) = (degβ(π₯ β β β¦ ((πΊβπ₯)βπ)))) |
11 | | oveq1 7416 |
. . . . 5
β’ (π¦ = π β (π¦ Β· π) = (π Β· π)) |
12 | 10, 11 | eqeq12d 2749 |
. . . 4
β’ (π¦ = π β ((degβ(π₯ β β β¦ ((πΊβπ₯)βπ¦))) = (π¦ Β· π) β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π))) |
13 | 12 | imbi2d 341 |
. . 3
β’ (π¦ = π β ((π β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ¦))) = (π¦ Β· π)) β (π β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)))) |
14 | | oveq2 7417 |
. . . . . . 7
β’ (π¦ = (π + 1) β ((πΊβπ₯)βπ¦) = ((πΊβπ₯)β(π + 1))) |
15 | 14 | mpteq2dv 5251 |
. . . . . 6
β’ (π¦ = (π + 1) β (π₯ β β β¦ ((πΊβπ₯)βπ¦)) = (π₯ β β β¦ ((πΊβπ₯)β(π + 1)))) |
16 | 15 | fveq2d 6896 |
. . . . 5
β’ (π¦ = (π + 1) β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ¦))) = (degβ(π₯ β β β¦ ((πΊβπ₯)β(π + 1))))) |
17 | | oveq1 7416 |
. . . . 5
β’ (π¦ = (π + 1) β (π¦ Β· π) = ((π + 1) Β· π)) |
18 | 16, 17 | eqeq12d 2749 |
. . . 4
β’ (π¦ = (π + 1) β ((degβ(π₯ β β β¦ ((πΊβπ₯)βπ¦))) = (π¦ Β· π) β (degβ(π₯ β β β¦ ((πΊβπ₯)β(π + 1)))) = ((π + 1) Β· π))) |
19 | 18 | imbi2d 341 |
. . 3
β’ (π¦ = (π + 1) β ((π β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ¦))) = (π¦ Β· π)) β (π β (degβ(π₯ β β β¦ ((πΊβπ₯)β(π + 1)))) = ((π + 1) Β· π)))) |
20 | | oveq2 7417 |
. . . . . . 7
β’ (π¦ = π β ((πΊβπ₯)βπ¦) = ((πΊβπ₯)βπ)) |
21 | 20 | mpteq2dv 5251 |
. . . . . 6
β’ (π¦ = π β (π₯ β β β¦ ((πΊβπ₯)βπ¦)) = (π₯ β β β¦ ((πΊβπ₯)βπ))) |
22 | 21 | fveq2d 6896 |
. . . . 5
β’ (π¦ = π β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ¦))) = (degβ(π₯ β β β¦ ((πΊβπ₯)βπ)))) |
23 | | oveq1 7416 |
. . . . 5
β’ (π¦ = π β (π¦ Β· π) = (π Β· π)) |
24 | 22, 23 | eqeq12d 2749 |
. . . 4
β’ (π¦ = π β ((degβ(π₯ β β β¦ ((πΊβπ₯)βπ¦))) = (π¦ Β· π) β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π))) |
25 | 24 | imbi2d 341 |
. . 3
β’ (π¦ = π β ((π β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ¦))) = (π¦ Β· π)) β (π β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)))) |
26 | | dgrcolem1.4 |
. . . . . . . . . . 11
β’ (π β πΊ β (Polyβπ)) |
27 | | plyf 25712 |
. . . . . . . . . . 11
β’ (πΊ β (Polyβπ) β πΊ:ββΆβ) |
28 | 26, 27 | syl 17 |
. . . . . . . . . 10
β’ (π β πΊ:ββΆβ) |
29 | 28 | ffvelcdmda 7087 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (πΊβπ₯) β β) |
30 | 29 | exp1d 14106 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β ((πΊβπ₯)β1) = (πΊβπ₯)) |
31 | 30 | mpteq2dva 5249 |
. . . . . . 7
β’ (π β (π₯ β β β¦ ((πΊβπ₯)β1)) = (π₯ β β β¦ (πΊβπ₯))) |
32 | 28 | feqmptd 6961 |
. . . . . . 7
β’ (π β πΊ = (π₯ β β β¦ (πΊβπ₯))) |
33 | 31, 32 | eqtr4d 2776 |
. . . . . 6
β’ (π β (π₯ β β β¦ ((πΊβπ₯)β1)) = πΊ) |
34 | 33 | fveq2d 6896 |
. . . . 5
β’ (π β (degβ(π₯ β β β¦ ((πΊβπ₯)β1))) = (degβπΊ)) |
35 | | dgrcolem1.1 |
. . . . 5
β’ π = (degβπΊ) |
36 | 34, 35 | eqtr4di 2791 |
. . . 4
β’ (π β (degβ(π₯ β β β¦ ((πΊβπ₯)β1))) = π) |
37 | | dgrcolem1.3 |
. . . . . 6
β’ (π β π β β) |
38 | 37 | nncnd 12228 |
. . . . 5
β’ (π β π β β) |
39 | 38 | mullidd 11232 |
. . . 4
β’ (π β (1 Β· π) = π) |
40 | 36, 39 | eqtr4d 2776 |
. . 3
β’ (π β (degβ(π₯ β β β¦ ((πΊβπ₯)β1))) = (1 Β· π)) |
41 | 29 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β β) β (πΊβπ₯) β β) |
42 | | nnnn0 12479 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β0) |
43 | 42 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β β0) |
44 | 43 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β β) β π β β0) |
45 | 41, 44 | expp1d 14112 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β ((πΊβπ₯)β(π + 1)) = (((πΊβπ₯)βπ) Β· (πΊβπ₯))) |
46 | 45 | mpteq2dva 5249 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (π₯ β β β¦ ((πΊβπ₯)β(π + 1))) = (π₯ β β β¦ (((πΊβπ₯)βπ) Β· (πΊβπ₯)))) |
47 | | cnex 11191 |
. . . . . . . . . . . 12
β’ β
β V |
48 | 47 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β β β
V) |
49 | | ovexd 7444 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β ((πΊβπ₯)βπ) β V) |
50 | | eqidd 2734 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π₯ β β β¦ ((πΊβπ₯)βπ)) = (π₯ β β β¦ ((πΊβπ₯)βπ))) |
51 | 32 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β πΊ = (π₯ β β β¦ (πΊβπ₯))) |
52 | 48, 49, 41, 50, 51 | offval2 7690 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((π₯ β β β¦ ((πΊβπ₯)βπ)) βf Β· πΊ) = (π₯ β β β¦ (((πΊβπ₯)βπ) Β· (πΊβπ₯)))) |
53 | 46, 52 | eqtr4d 2776 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π₯ β β β¦ ((πΊβπ₯)β(π + 1))) = ((π₯ β β β¦ ((πΊβπ₯)βπ)) βf Β· πΊ)) |
54 | 53 | fveq2d 6896 |
. . . . . . . 8
β’ ((π β§ π β β) β (degβ(π₯ β β β¦ ((πΊβπ₯)β(π + 1)))) = (degβ((π₯ β β β¦ ((πΊβπ₯)βπ)) βf Β· πΊ))) |
55 | 54 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β β) β§ (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) β (degβ(π₯ β β β¦ ((πΊβπ₯)β(π + 1)))) = (degβ((π₯ β β β¦ ((πΊβπ₯)βπ)) βf Β· πΊ))) |
56 | | oveq1 7416 |
. . . . . . . . 9
β’
((degβ(π₯
β β β¦ ((πΊβπ₯)βπ))) = (π Β· π) β ((degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) + π) = ((π Β· π) + π)) |
57 | 56 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) β ((degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) + π) = ((π Β· π) + π)) |
58 | | eqidd 2734 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π¦ β β β¦ (π¦βπ)) = (π¦ β β β¦ (π¦βπ))) |
59 | | oveq1 7416 |
. . . . . . . . . . . 12
β’ (π¦ = (πΊβπ₯) β (π¦βπ) = ((πΊβπ₯)βπ)) |
60 | 41, 51, 58, 59 | fmptco 7127 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((π¦ β β β¦ (π¦βπ)) β πΊ) = (π₯ β β β¦ ((πΊβπ₯)βπ))) |
61 | | ssidd 4006 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β β β
β) |
62 | | 1cnd 11209 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β 1 β
β) |
63 | | plypow 25719 |
. . . . . . . . . . . . 13
β’ ((β
β β β§ 1 β β β§ π β β0) β (π¦ β β β¦ (π¦βπ)) β
(Polyββ)) |
64 | 61, 62, 43, 63 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π¦ β β β¦ (π¦βπ)) β
(Polyββ)) |
65 | | plyssc 25714 |
. . . . . . . . . . . . 13
β’
(Polyβπ)
β (Polyββ) |
66 | 26 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β πΊ β (Polyβπ)) |
67 | 65, 66 | sselid 3981 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β πΊ β
(Polyββ)) |
68 | | addcl 11192 |
. . . . . . . . . . . . 13
β’ ((π§ β β β§ π€ β β) β (π§ + π€) β β) |
69 | 68 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (π§ β β β§ π€ β β)) β (π§ + π€) β β) |
70 | | mulcl 11194 |
. . . . . . . . . . . . 13
β’ ((π§ β β β§ π€ β β) β (π§ Β· π€) β β) |
71 | 70 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (π§ β β β§ π€ β β)) β (π§ Β· π€) β β) |
72 | 64, 67, 69, 71 | plyco 25755 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((π¦ β β β¦ (π¦βπ)) β πΊ) β
(Polyββ)) |
73 | 60, 72 | eqeltrrd 2835 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (π₯ β β β¦ ((πΊβπ₯)βπ)) β
(Polyββ)) |
74 | 73 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) β (π₯ β β β¦ ((πΊβπ₯)βπ)) β
(Polyββ)) |
75 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) |
76 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β β) |
77 | 37 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β β) |
78 | 76, 77 | nnmulcld 12265 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (π Β· π) β β) |
79 | 78 | nnne0d 12262 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π Β· π) β 0) |
80 | 79 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) β (π Β· π) β 0) |
81 | 75, 80 | eqnetrd 3009 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) β 0) |
82 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ ((π₯ β β β¦ ((πΊβπ₯)βπ)) = 0π β
(degβ(π₯ β
β β¦ ((πΊβπ₯)βπ))) =
(degβ0π)) |
83 | | dgr0 25776 |
. . . . . . . . . . . 12
β’
(degβ0π) = 0 |
84 | 82, 83 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ ((π₯ β β β¦ ((πΊβπ₯)βπ)) = 0π β
(degβ(π₯ β
β β¦ ((πΊβπ₯)βπ))) = 0) |
85 | 84 | necon3i 2974 |
. . . . . . . . . 10
β’
((degβ(π₯
β β β¦ ((πΊβπ₯)βπ))) β 0 β (π₯ β β β¦ ((πΊβπ₯)βπ)) β
0π) |
86 | 81, 85 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) β (π₯ β β β¦ ((πΊβπ₯)βπ)) β
0π) |
87 | 67 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) β πΊ β
(Polyββ)) |
88 | 37 | nnne0d 12262 |
. . . . . . . . . . . 12
β’ (π β π β 0) |
89 | | fveq2 6892 |
. . . . . . . . . . . . . . 15
β’ (πΊ = 0π β
(degβπΊ) =
(degβ0π)) |
90 | 89, 83 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
β’ (πΊ = 0π β
(degβπΊ) =
0) |
91 | 35, 90 | eqtrid 2785 |
. . . . . . . . . . . . 13
β’ (πΊ = 0π β
π = 0) |
92 | 91 | necon3i 2974 |
. . . . . . . . . . . 12
β’ (π β 0 β πΊ β
0π) |
93 | 88, 92 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΊ β
0π) |
94 | 93 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β πΊ β
0π) |
95 | 94 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) β πΊ β
0π) |
96 | | eqid 2733 |
. . . . . . . . . 10
β’
(degβ(π₯ β
β β¦ ((πΊβπ₯)βπ))) = (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) |
97 | 96, 35 | dgrmul 25784 |
. . . . . . . . 9
β’ ((((π₯ β β β¦ ((πΊβπ₯)βπ)) β (Polyββ) β§ (π₯ β β β¦ ((πΊβπ₯)βπ)) β 0π) β§ (πΊ β (Polyββ)
β§ πΊ β
0π)) β (degβ((π₯ β β β¦ ((πΊβπ₯)βπ)) βf Β· πΊ)) = ((degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) + π)) |
98 | 74, 86, 87, 95, 97 | syl22anc 838 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) β (degβ((π₯ β β β¦ ((πΊβπ₯)βπ)) βf Β· πΊ)) = ((degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) + π)) |
99 | | nncn 12220 |
. . . . . . . . . . 11
β’ (π β β β π β
β) |
100 | 99 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β) |
101 | 38 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β) |
102 | 100, 101 | adddirp1d 11240 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((π + 1) Β· π) = ((π Β· π) + π)) |
103 | 102 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) β ((π + 1) Β· π) = ((π Β· π) + π)) |
104 | 57, 98, 103 | 3eqtr4rd 2784 |
. . . . . . 7
β’ (((π β§ π β β) β§ (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) β ((π + 1) Β· π) = (degβ((π₯ β β β¦ ((πΊβπ₯)βπ)) βf Β· πΊ))) |
105 | 55, 104 | eqtr4d 2776 |
. . . . . 6
β’ (((π β§ π β β) β§ (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) β (degβ(π₯ β β β¦ ((πΊβπ₯)β(π + 1)))) = ((π + 1) Β· π)) |
106 | 105 | ex 414 |
. . . . 5
β’ ((π β§ π β β) β ((degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π) β (degβ(π₯ β β β¦ ((πΊβπ₯)β(π + 1)))) = ((π + 1) Β· π))) |
107 | 106 | expcom 415 |
. . . 4
β’ (π β β β (π β ((degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π) β (degβ(π₯ β β β¦ ((πΊβπ₯)β(π + 1)))) = ((π + 1) Β· π)))) |
108 | 107 | a2d 29 |
. . 3
β’ (π β β β ((π β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) β (π β (degβ(π₯ β β β¦ ((πΊβπ₯)β(π + 1)))) = ((π + 1) Β· π)))) |
109 | 7, 13, 19, 25, 40, 108 | nnind 12230 |
. 2
β’ (π β β β (π β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π))) |
110 | 1, 109 | mpcom 38 |
1
β’ (π β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) |