Metamath Proof Explorer

Theorem dgrco

Description: The degree of a composition of two polynomials is the product of the degrees. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Hypotheses dgrco.1 
|- M = ( deg ` F )
dgrco.2 
|- N = ( deg ` G )
dgrco.3 
|- ( ph -> F e. ( Poly ` S ) )
dgrco.4 
|- ( ph -> G e. ( Poly ` S ) )
Assertion dgrco 
|- ( ph -> ( deg ` ( F o. G ) ) = ( M x. N ) )

Proof

Step Hyp Ref Expression
1 dgrco.1 
 |-  M = ( deg ` F )
2 dgrco.2 
 |-  N = ( deg ` G )
3 dgrco.3 
 |-  ( ph -> F e. ( Poly ` S ) )
4 dgrco.4 
 |-  ( ph -> G e. ( Poly ` S ) )
5 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
6 5 3 sselid 
 |-  ( ph -> F e. ( Poly ` CC ) )
7 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
8 3 7 syl 
 |-  ( ph -> ( deg ` F ) e. NN0 )
9 1 8 eqeltrid 
 |-  ( ph -> M e. NN0 )
10 breq2 
 |-  ( x = 0 -> ( ( deg ` f ) <_ x <-> ( deg ` f ) <_ 0 ) )
11 10 imbi1d 
 |-  ( x = 0 -> ( ( ( deg ` f ) <_ x -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) <-> ( ( deg ` f ) <_ 0 -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) )
12 11 ralbidv 
 |-  ( x = 0 -> ( A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ x -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) <-> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ 0 -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) )
13 12 imbi2d 
 |-  ( x = 0 -> ( ( ph -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ x -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) <-> ( ph -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ 0 -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) ) )
14 breq2 
 |-  ( x = d -> ( ( deg ` f ) <_ x <-> ( deg ` f ) <_ d ) )
15 14 imbi1d 
 |-  ( x = d -> ( ( ( deg ` f ) <_ x -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) <-> ( ( deg ` f ) <_ d -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) )
16 15 ralbidv 
 |-  ( x = d -> ( A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ x -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) <-> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ d -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) )
17 16 imbi2d 
 |-  ( x = d -> ( ( ph -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ x -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) <-> ( ph -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ d -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) ) )
18 breq2 
 |-  ( x = ( d + 1 ) -> ( ( deg ` f ) <_ x <-> ( deg ` f ) <_ ( d + 1 ) ) )
19 18 imbi1d 
 |-  ( x = ( d + 1 ) -> ( ( ( deg ` f ) <_ x -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) <-> ( ( deg ` f ) <_ ( d + 1 ) -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) )
20 19 ralbidv 
 |-  ( x = ( d + 1 ) -> ( A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ x -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) <-> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ ( d + 1 ) -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) )
21 20 imbi2d 
 |-  ( x = ( d + 1 ) -> ( ( ph -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ x -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) <-> ( ph -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ ( d + 1 ) -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) ) )
22 breq2 
 |-  ( x = M -> ( ( deg ` f ) <_ x <-> ( deg ` f ) <_ M ) )
23 22 imbi1d 
 |-  ( x = M -> ( ( ( deg ` f ) <_ x -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) <-> ( ( deg ` f ) <_ M -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) )
24 23 ralbidv 
 |-  ( x = M -> ( A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ x -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) <-> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ M -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) )
25 24 imbi2d 
 |-  ( x = M -> ( ( ph -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ x -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) <-> ( ph -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ M -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) ) )
26 dgrcl 
 |-  ( G e. ( Poly ` S ) -> ( deg ` G ) e. NN0 )
27 4 26 syl 
 |-  ( ph -> ( deg ` G ) e. NN0 )
28 2 27 eqeltrid 
 |-  ( ph -> N e. NN0 )
29 28 nn0cnd 
 |-  ( ph -> N e. CC )
30 29 adantr 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> N e. CC )
31 30 mul02d 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> ( 0 x. N ) = 0 )
32 simprr 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> ( deg ` f ) <_ 0 )
33 dgrcl 
 |-  ( f e. ( Poly ` CC ) -> ( deg ` f ) e. NN0 )
34 33 ad2antrl 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> ( deg ` f ) e. NN0 )
35 34 nn0ge0d 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> 0 <_ ( deg ` f ) )
36 34 nn0red 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> ( deg ` f ) e. RR )
37 0re 
 |-  0 e. RR
38 letri3 
 |-  ( ( ( deg ` f ) e. RR /\ 0 e. RR ) -> ( ( deg ` f ) = 0 <-> ( ( deg ` f ) <_ 0 /\ 0 <_ ( deg ` f ) ) ) )
39 36 37 38 sylancl 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> ( ( deg ` f ) = 0 <-> ( ( deg ` f ) <_ 0 /\ 0 <_ ( deg ` f ) ) ) )
40 32 35 39 mpbir2and 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> ( deg ` f ) = 0 )
41 40 oveq1d 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> ( ( deg ` f ) x. N ) = ( 0 x. N ) )
42 31 41 40 3eqtr4d 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> ( ( deg ` f ) x. N ) = ( deg ` f ) )
43 fconstmpt 
 |-  ( CC X. { ( f ` 0 ) } ) = ( y e. CC |-> ( f ` 0 ) )
44 0dgrb 
 |-  ( f e. ( Poly ` CC ) -> ( ( deg ` f ) = 0 <-> f = ( CC X. { ( f ` 0 ) } ) ) )
45 44 ad2antrl 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> ( ( deg ` f ) = 0 <-> f = ( CC X. { ( f ` 0 ) } ) ) )
46 40 45 mpbid 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> f = ( CC X. { ( f ` 0 ) } ) )
47 4 adantr 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> G e. ( Poly ` S ) )
48 plyf 
 |-  ( G e. ( Poly ` S ) -> G : CC --> CC )
49 47 48 syl 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> G : CC --> CC )
50 49 ffvelrnda 
 |-  ( ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) /\ y e. CC ) -> ( G ` y ) e. CC )
51 49 feqmptd 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> G = ( y e. CC |-> ( G ` y ) ) )
52 fconstmpt 
 |-  ( CC X. { ( f ` 0 ) } ) = ( x e. CC |-> ( f ` 0 ) )
53 46 52 eqtrdi 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> f = ( x e. CC |-> ( f ` 0 ) ) )
54 eqidd 
 |-  ( x = ( G ` y ) -> ( f ` 0 ) = ( f ` 0 ) )
55 50 51 53 54 fmptco 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> ( f o. G ) = ( y e. CC |-> ( f ` 0 ) ) )
56 43 46 55 3eqtr4a 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> f = ( f o. G ) )
57 56 fveq2d 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> ( deg ` f ) = ( deg ` ( f o. G ) ) )
58 42 57 eqtr2d 
 |-  ( ( ph /\ ( f e. ( Poly ` CC ) /\ ( deg ` f ) <_ 0 ) ) -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) )
59 58 expr 
 |-  ( ( ph /\ f e. ( Poly ` CC ) ) -> ( ( deg ` f ) <_ 0 -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) )
60 59 ralrimiva 
 |-  ( ph -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ 0 -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) )
61 fveq2 
 |-  ( f = g -> ( deg ` f ) = ( deg ` g ) )
62 61 breq1d 
 |-  ( f = g -> ( ( deg ` f ) <_ d <-> ( deg ` g ) <_ d ) )
63 coeq1 
 |-  ( f = g -> ( f o. G ) = ( g o. G ) )
64 63 fveq2d 
 |-  ( f = g -> ( deg ` ( f o. G ) ) = ( deg ` ( g o. G ) ) )
65 61 oveq1d 
 |-  ( f = g -> ( ( deg ` f ) x. N ) = ( ( deg ` g ) x. N ) )
66 64 65 eqeq12d 
 |-  ( f = g -> ( ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) <-> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) )
67 62 66 imbi12d 
 |-  ( f = g -> ( ( ( deg ` f ) <_ d -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) <-> ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) )
68 67 cbvralvw 
 |-  ( A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ d -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) <-> A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) )
69 33 ad2antrl 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) ) -> ( deg ` f ) e. NN0 )
70 69 nn0red 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) ) -> ( deg ` f ) e. RR )
71 nn0p1nn 
 |-  ( d e. NN0 -> ( d + 1 ) e. NN )
72 71 ad2antlr 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) ) -> ( d + 1 ) e. NN )
73 72 nnred 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) ) -> ( d + 1 ) e. RR )
74 70 73 leloed 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) ) -> ( ( deg ` f ) <_ ( d + 1 ) <-> ( ( deg ` f ) < ( d + 1 ) \/ ( deg ` f ) = ( d + 1 ) ) ) )
75 simplr 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) ) -> d e. NN0 )
76 nn0leltp1 
 |-  ( ( ( deg ` f ) e. NN0 /\ d e. NN0 ) -> ( ( deg ` f ) <_ d <-> ( deg ` f ) < ( d + 1 ) ) )
77 69 75 76 syl2anc 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) ) -> ( ( deg ` f ) <_ d <-> ( deg ` f ) < ( d + 1 ) ) )
78 fveq2 
 |-  ( g = f -> ( deg ` g ) = ( deg ` f ) )
79 78 breq1d 
 |-  ( g = f -> ( ( deg ` g ) <_ d <-> ( deg ` f ) <_ d ) )
80 coeq1 
 |-  ( g = f -> ( g o. G ) = ( f o. G ) )
81 80 fveq2d 
 |-  ( g = f -> ( deg ` ( g o. G ) ) = ( deg ` ( f o. G ) ) )
82 78 oveq1d 
 |-  ( g = f -> ( ( deg ` g ) x. N ) = ( ( deg ` f ) x. N ) )
83 81 82 eqeq12d 
 |-  ( g = f -> ( ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) <-> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) )
84 79 83 imbi12d 
 |-  ( g = f -> ( ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) <-> ( ( deg ` f ) <_ d -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) )
85 84 rspcva 
 |-  ( ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) -> ( ( deg ` f ) <_ d -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) )
86 85 adantl 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) ) -> ( ( deg ` f ) <_ d -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) )
87 77 86 sylbird 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) ) -> ( ( deg ` f ) < ( d + 1 ) -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) )
88 eqid 
 |-  ( deg ` f ) = ( deg ` f )
89 simprll 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) /\ ( deg ` f ) = ( d + 1 ) ) ) -> f e. ( Poly ` CC ) )
90 5 4 sselid 
 |-  ( ph -> G e. ( Poly ` CC ) )
91 90 ad2antrr 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) /\ ( deg ` f ) = ( d + 1 ) ) ) -> G e. ( Poly ` CC ) )
92 eqid 
 |-  ( coeff ` f ) = ( coeff ` f )
93 simplr 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) /\ ( deg ` f ) = ( d + 1 ) ) ) -> d e. NN0 )
94 simprr 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) /\ ( deg ` f ) = ( d + 1 ) ) ) -> ( deg ` f ) = ( d + 1 ) )
95 simprlr 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) /\ ( deg ` f ) = ( d + 1 ) ) ) -> A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) )
96 fveq2 
 |-  ( g = h -> ( deg ` g ) = ( deg ` h ) )
97 96 breq1d 
 |-  ( g = h -> ( ( deg ` g ) <_ d <-> ( deg ` h ) <_ d ) )
98 coeq1 
 |-  ( g = h -> ( g o. G ) = ( h o. G ) )
99 98 fveq2d 
 |-  ( g = h -> ( deg ` ( g o. G ) ) = ( deg ` ( h o. G ) ) )
100 96 oveq1d 
 |-  ( g = h -> ( ( deg ` g ) x. N ) = ( ( deg ` h ) x. N ) )
101 99 100 eqeq12d 
 |-  ( g = h -> ( ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) <-> ( deg ` ( h o. G ) ) = ( ( deg ` h ) x. N ) ) )
102 97 101 imbi12d 
 |-  ( g = h -> ( ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) <-> ( ( deg ` h ) <_ d -> ( deg ` ( h o. G ) ) = ( ( deg ` h ) x. N ) ) ) )
103 102 cbvralvw 
 |-  ( A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) <-> A. h e. ( Poly ` CC ) ( ( deg ` h ) <_ d -> ( deg ` ( h o. G ) ) = ( ( deg ` h ) x. N ) ) )
104 95 103 sylib 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) /\ ( deg ` f ) = ( d + 1 ) ) ) -> A. h e. ( Poly ` CC ) ( ( deg ` h ) <_ d -> ( deg ` ( h o. G ) ) = ( ( deg ` h ) x. N ) ) )
105 88 2 89 91 92 93 94 104 dgrcolem2 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) /\ ( deg ` f ) = ( d + 1 ) ) ) -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) )
106 105 expr 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) ) -> ( ( deg ` f ) = ( d + 1 ) -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) )
107 87 106 jaod 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) ) -> ( ( ( deg ` f ) < ( d + 1 ) \/ ( deg ` f ) = ( d + 1 ) ) -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) )
108 74 107 sylbid 
 |-  ( ( ( ph /\ d e. NN0 ) /\ ( f e. ( Poly ` CC ) /\ A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) ) ) -> ( ( deg ` f ) <_ ( d + 1 ) -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) )
109 108 expr 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` CC ) ) -> ( A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) -> ( ( deg ` f ) <_ ( d + 1 ) -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) )
110 109 ralrimdva 
 |-  ( ( ph /\ d e. NN0 ) -> ( A. g e. ( Poly ` CC ) ( ( deg ` g ) <_ d -> ( deg ` ( g o. G ) ) = ( ( deg ` g ) x. N ) ) -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ ( d + 1 ) -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) )
111 68 110 syl5bi 
 |-  ( ( ph /\ d e. NN0 ) -> ( A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ d -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ ( d + 1 ) -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) )
112 111 expcom 
 |-  ( d e. NN0 -> ( ph -> ( A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ d -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ ( d + 1 ) -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) ) )
113 112 a2d 
 |-  ( d e. NN0 -> ( ( ph -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ d -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) -> ( ph -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ ( d + 1 ) -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) ) )
114 13 17 21 25 60 113 nn0ind 
 |-  ( M e. NN0 -> ( ph -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ M -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) ) )
115 9 114 mpcom 
 |-  ( ph -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ M -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) )
116 9 nn0red 
 |-  ( ph -> M e. RR )
117 116 leidd 
 |-  ( ph -> M <_ M )
118 fveq2 
 |-  ( f = F -> ( deg ` f ) = ( deg ` F ) )
119 118 1 eqtr4di 
 |-  ( f = F -> ( deg ` f ) = M )
120 119 breq1d 
 |-  ( f = F -> ( ( deg ` f ) <_ M <-> M <_ M ) )
121 coeq1 
 |-  ( f = F -> ( f o. G ) = ( F o. G ) )
122 121 fveq2d 
 |-  ( f = F -> ( deg ` ( f o. G ) ) = ( deg ` ( F o. G ) ) )
123 119 oveq1d 
 |-  ( f = F -> ( ( deg ` f ) x. N ) = ( M x. N ) )
124 122 123 eqeq12d 
 |-  ( f = F -> ( ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) <-> ( deg ` ( F o. G ) ) = ( M x. N ) ) )
125 120 124 imbi12d 
 |-  ( f = F -> ( ( ( deg ` f ) <_ M -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) <-> ( M <_ M -> ( deg ` ( F o. G ) ) = ( M x. N ) ) ) )
126 125 rspcv 
 |-  ( F e. ( Poly ` CC ) -> ( A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ M -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) -> ( M <_ M -> ( deg ` ( F o. G ) ) = ( M x. N ) ) ) )
127 6 115 117 126 syl3c 
 |-  ( ph -> ( deg ` ( F o. G ) ) = ( M x. N ) )