Metamath Proof Explorer

Theorem dgrmulc

Description: Scalar multiplication by a nonzero constant does not change the degree of a function. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Assertion dgrmulc 
|- ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) -> ( deg ` ( ( CC X. { A } ) oF x. F ) ) = ( deg ` F ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( F = 0p -> ( ( CC X. { A } ) oF x. F ) = ( ( CC X. { A } ) oF x. 0p ) )
2 1 fveq2d 
 |-  ( F = 0p -> ( deg ` ( ( CC X. { A } ) oF x. F ) ) = ( deg ` ( ( CC X. { A } ) oF x. 0p ) ) )
3 fveq2 
 |-  ( F = 0p -> ( deg ` F ) = ( deg ` 0p ) )
4 dgr0 
 |-  ( deg ` 0p ) = 0
5 3 4 eqtrdi 
 |-  ( F = 0p -> ( deg ` F ) = 0 )
6 2 5 eqeq12d 
 |-  ( F = 0p -> ( ( deg ` ( ( CC X. { A } ) oF x. F ) ) = ( deg ` F ) <-> ( deg ` ( ( CC X. { A } ) oF x. 0p ) ) = 0 ) )
7 ssid 
 |-  CC C_ CC
8 simpl1 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) /\ F =/= 0p ) -> A e. CC )
9 plyconst 
 |-  ( ( CC C_ CC /\ A e. CC ) -> ( CC X. { A } ) e. ( Poly ` CC ) )
10 7 8 9 sylancr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) /\ F =/= 0p ) -> ( CC X. { A } ) e. ( Poly ` CC ) )
11 0cn 
 |-  0 e. CC
12 fvconst2g 
 |-  ( ( A e. CC /\ 0 e. CC ) -> ( ( CC X. { A } ) ` 0 ) = A )
13 8 11 12 sylancl 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) /\ F =/= 0p ) -> ( ( CC X. { A } ) ` 0 ) = A )
14 simpl2 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) /\ F =/= 0p ) -> A =/= 0 )
15 13 14 eqnetrd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) /\ F =/= 0p ) -> ( ( CC X. { A } ) ` 0 ) =/= 0 )
16 ne0p 
 |-  ( ( 0 e. CC /\ ( ( CC X. { A } ) ` 0 ) =/= 0 ) -> ( CC X. { A } ) =/= 0p )
17 11 15 16 sylancr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) /\ F =/= 0p ) -> ( CC X. { A } ) =/= 0p )
18 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
19 simpl3 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) /\ F =/= 0p ) -> F e. ( Poly ` S ) )
20 18 19 sselid 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) /\ F =/= 0p ) -> F e. ( Poly ` CC ) )
21 simpr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) /\ F =/= 0p ) -> F =/= 0p )
22 eqid 
 |-  ( deg ` ( CC X. { A } ) ) = ( deg ` ( CC X. { A } ) )
23 eqid 
 |-  ( deg ` F ) = ( deg ` F )
24 22 23 dgrmul 
 |-  ( ( ( ( CC X. { A } ) e. ( Poly ` CC ) /\ ( CC X. { A } ) =/= 0p ) /\ ( F e. ( Poly ` CC ) /\ F =/= 0p ) ) -> ( deg ` ( ( CC X. { A } ) oF x. F ) ) = ( ( deg ` ( CC X. { A } ) ) + ( deg ` F ) ) )
25 10 17 20 21 24 syl22anc 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) /\ F =/= 0p ) -> ( deg ` ( ( CC X. { A } ) oF x. F ) ) = ( ( deg ` ( CC X. { A } ) ) + ( deg ` F ) ) )
26 0dgr 
 |-  ( A e. CC -> ( deg ` ( CC X. { A } ) ) = 0 )
27 8 26 syl 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) /\ F =/= 0p ) -> ( deg ` ( CC X. { A } ) ) = 0 )
28 27 oveq1d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) /\ F =/= 0p ) -> ( ( deg ` ( CC X. { A } ) ) + ( deg ` F ) ) = ( 0 + ( deg ` F ) ) )
29 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
30 19 29 syl 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) /\ F =/= 0p ) -> ( deg ` F ) e. NN0 )
31 30 nn0cnd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) /\ F =/= 0p ) -> ( deg ` F ) e. CC )
32 31 addlidd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) /\ F =/= 0p ) -> ( 0 + ( deg ` F ) ) = ( deg ` F ) )
33 25 28 32 3eqtrd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) /\ F =/= 0p ) -> ( deg ` ( ( CC X. { A } ) oF x. F ) ) = ( deg ` F ) )
34 cnex 
 |-  CC e. _V
35 34 a1i 
 |-  ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) -> CC e. _V )
36 simp1 
 |-  ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) -> A e. CC )
37 11 a1i 
 |-  ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) -> 0 e. CC )
38 35 36 37 ofc12 
 |-  ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) -> ( ( CC X. { A } ) oF x. ( CC X. { 0 } ) ) = ( CC X. { ( A x. 0 ) } ) )
39 36 mul01d 
 |-  ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) -> ( A x. 0 ) = 0 )
40 39 sneqd 
 |-  ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) -> { ( A x. 0 ) } = { 0 } )
41 40 xpeq2d 
 |-  ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) -> ( CC X. { ( A x. 0 ) } ) = ( CC X. { 0 } ) )
42 38 41 eqtrd 
 |-  ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) -> ( ( CC X. { A } ) oF x. ( CC X. { 0 } ) ) = ( CC X. { 0 } ) )
43 df-0p 
 |-  0p = ( CC X. { 0 } )
44 43 oveq2i 
 |-  ( ( CC X. { A } ) oF x. 0p ) = ( ( CC X. { A } ) oF x. ( CC X. { 0 } ) )
45 42 44 43 3eqtr4g 
 |-  ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) -> ( ( CC X. { A } ) oF x. 0p ) = 0p )
46 45 fveq2d 
 |-  ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) -> ( deg ` ( ( CC X. { A } ) oF x. 0p ) ) = ( deg ` 0p ) )
47 46 4 eqtrdi 
 |-  ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) -> ( deg ` ( ( CC X. { A } ) oF x. 0p ) ) = 0 )
48 6 33 47 pm2.61ne 
 |-  ( ( A e. CC /\ A =/= 0 /\ F e. ( Poly ` S ) ) -> ( deg ` ( ( CC X. { A } ) oF x. F ) ) = ( deg ` F ) )