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 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( deg ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝐹 = 0𝑝 → ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) = ( ( ℂ × { 𝐴 } ) ∘f · 0𝑝 ) )
2 1 fveq2d ⊢ ( 𝐹 = 0𝑝 → ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 0𝑝 ) ) )
3 fveq2 ⊢ ( 𝐹 = 0𝑝 → ( deg ‘ 𝐹 ) = ( deg ‘ 0𝑝 ) )
4 dgr0 ⊢ ( deg ‘ 0𝑝 ) = 0
5 3 4 eqtrdi ⊢ ( 𝐹 = 0𝑝 → ( deg ‘ 𝐹 ) = 0 )
6 2 5 eqeq12d ⊢ ( 𝐹 = 0𝑝 → ( ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( deg ‘ 𝐹 ) ↔ ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 0𝑝 ) ) = 0 ) )
7 ssid ⊢ ℂ ⊆ ℂ
8 simpl1 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → 𝐴 ∈ ℂ )
9 plyconst ⊢ ( ( ℂ ⊆ ℂ ∧ 𝐴 ∈ ℂ ) → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
10 7 8 9 sylancr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
11 0cn ⊢ 0 ∈ ℂ
12 fvconst2g ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → ( ( ℂ × { 𝐴 } ) ‘ 0 ) = 𝐴 )
13 8 11 12 sylancl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( ( ℂ × { 𝐴 } ) ‘ 0 ) = 𝐴 )
14 simpl2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → 𝐴 ≠ 0 )
15 13 14 eqnetrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( ( ℂ × { 𝐴 } ) ‘ 0 ) ≠ 0 )
16 ne0p ⊢ ( ( 0 ∈ ℂ ∧ ( ( ℂ × { 𝐴 } ) ‘ 0 ) ≠ 0 ) → ( ℂ × { 𝐴 } ) ≠ 0𝑝 )
17 11 15 16 sylancr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( ℂ × { 𝐴 } ) ≠ 0𝑝 )
18 plyssc ⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
19 simpl3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
20 18 19 sselid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
21 simpr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → 𝐹 ≠ 0𝑝 )
22 eqid ⊢ ( deg ‘ ( ℂ × { 𝐴 } ) ) = ( deg ‘ ( ℂ × { 𝐴 } ) )
23 eqid ⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 )
24 22 23 dgrmul ⊢ ( ( ( ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) ∧ ( ℂ × { 𝐴 } ) ≠ 0𝑝 ) ∧ ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐹 ≠ 0𝑝 ) ) → ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( ( deg ‘ ( ℂ × { 𝐴 } ) ) + ( deg ‘ 𝐹 ) ) )
25 10 17 20 21 24 syl22anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( ( deg ‘ ( ℂ × { 𝐴 } ) ) + ( deg ‘ 𝐹 ) ) )
26 0dgr ⊢ ( 𝐴 ∈ ℂ → ( deg ‘ ( ℂ × { 𝐴 } ) ) = 0 )
27 8 26 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( deg ‘ ( ℂ × { 𝐴 } ) ) = 0 )
28 27 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( ( deg ‘ ( ℂ × { 𝐴 } ) ) + ( deg ‘ 𝐹 ) ) = ( 0 + ( deg ‘ 𝐹 ) ) )
29 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
30 19 29 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
31 30 nn0cnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( deg ‘ 𝐹 ) ∈ ℂ )
32 31 addid2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( 0 + ( deg ‘ 𝐹 ) ) = ( deg ‘ 𝐹 ) )
33 25 28 32 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( deg ‘ 𝐹 ) )
34 cnex ⊢ ℂ ∈ V
35 34 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ℂ ∈ V )
36 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → 𝐴 ∈ ℂ )
37 11 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → 0 ∈ ℂ )
38 35 36 37 ofc12 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ × { 𝐴 } ) ∘f · ( ℂ × { 0 } ) ) = ( ℂ × { ( 𝐴 · 0 ) } ) )
39 36 mul01d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐴 · 0 ) = 0 )
40 39 sneqd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → { ( 𝐴 · 0 ) } = { 0 } )
41 40 xpeq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ℂ × { ( 𝐴 · 0 ) } ) = ( ℂ × { 0 } ) )
42 38 41 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ × { 𝐴 } ) ∘f · ( ℂ × { 0 } ) ) = ( ℂ × { 0 } ) )
43 df-0p ⊢ 0𝑝 = ( ℂ × { 0 } )
44 43 oveq2i ⊢ ( ( ℂ × { 𝐴 } ) ∘f · 0𝑝 ) = ( ( ℂ × { 𝐴 } ) ∘f · ( ℂ × { 0 } ) )
45 42 44 43 3eqtr4g ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ × { 𝐴 } ) ∘f · 0𝑝 ) = 0𝑝 )
46 45 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 0𝑝 ) ) = ( deg ‘ 0𝑝 ) )
47 46 4 eqtrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 0𝑝 ) ) = 0 )
48 6 33 47 pm2.61ne ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( deg ‘ 𝐹 ) )