Metamath Proof Explorer

Theorem dgrmul

Description: The degree of a product of nonzero polynomials is the sum of degrees. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses dgradd.1 ⊢ 𝑀 = ( deg ‘ 𝐹 )
dgradd.2 ⊢ 𝑁 = ( deg ‘ 𝐺 )
Assertion dgrmul ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( deg ‘ ( 𝐹 ∘f · 𝐺 ) ) = ( 𝑀 + 𝑁 ) )

Proof

Step Hyp Ref Expression
1 dgradd.1 ⊢ 𝑀 = ( deg ‘ 𝐹 )
2 dgradd.2 ⊢ 𝑁 = ( deg ‘ 𝐺 )
3 1 2 dgrmul2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( 𝐹 ∘f · 𝐺 ) ) ≤ ( 𝑀 + 𝑁 ) )
4 3 ad2ant2r ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( deg ‘ ( 𝐹 ∘f · 𝐺 ) ) ≤ ( 𝑀 + 𝑁 ) )
5 plymulcl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ ℂ ) )
6 5 ad2ant2r ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ ℂ ) )
7 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
8 1 7 eqeltrid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑀 ∈ ℕ0 )
9 8 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → 𝑀 ∈ ℕ0 )
10 dgrcl ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐺 ) ∈ ℕ0 )
11 2 10 eqeltrid ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝑁 ∈ ℕ0 )
12 11 ad2antrl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → 𝑁 ∈ ℕ0 )
13 9 12 nn0addcld ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
14 eqid ⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 )
15 eqid ⊢ ( coeff ‘ 𝐺 ) = ( coeff ‘ 𝐺 )
16 14 15 1 2 coemulhi ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) ‘ ( 𝑀 + 𝑁 ) ) = ( ( ( coeff ‘ 𝐹 ) ‘ 𝑀 ) · ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) )
17 16 ad2ant2r ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) ‘ ( 𝑀 + 𝑁 ) ) = ( ( ( coeff ‘ 𝐹 ) ‘ 𝑀 ) · ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) )
18 14 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ )
19 18 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ )
20 19 9 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑀 ) ∈ ℂ )
21 15 coef3 ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℂ )
22 21 ad2antrl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℂ )
23 22 12 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ∈ ℂ )
24 1 14 dgreq0 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 = 0𝑝 ↔ ( ( coeff ‘ 𝐹 ) ‘ 𝑀 ) = 0 ) )
25 24 necon3bid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 ≠ 0𝑝 ↔ ( ( coeff ‘ 𝐹 ) ‘ 𝑀 ) ≠ 0 ) )
26 25 biimpa ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑀 ) ≠ 0 )
27 26 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑀 ) ≠ 0 )
28 2 15 dgreq0 ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( 𝐺 = 0𝑝 ↔ ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) = 0 ) )
29 28 necon3bid ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( 𝐺 ≠ 0𝑝 ↔ ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ≠ 0 ) )
30 29 biimpa ⊢ ( ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ≠ 0 )
31 30 adantl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ≠ 0 )
32 20 23 27 31 mulne0d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( ( ( coeff ‘ 𝐹 ) ‘ 𝑀 ) · ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ≠ 0 )
33 17 32 eqnetrd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) ‘ ( 𝑀 + 𝑁 ) ) ≠ 0 )
34 eqid ⊢ ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) = ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) )
35 eqid ⊢ ( deg ‘ ( 𝐹 ∘f · 𝐺 ) ) = ( deg ‘ ( 𝐹 ∘f · 𝐺 ) )
36 34 35 dgrub ⊢ ( ( ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ ℂ ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ∧ ( ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) ‘ ( 𝑀 + 𝑁 ) ) ≠ 0 ) → ( 𝑀 + 𝑁 ) ≤ ( deg ‘ ( 𝐹 ∘f · 𝐺 ) ) )
37 6 13 33 36 syl3anc ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( 𝑀 + 𝑁 ) ≤ ( deg ‘ ( 𝐹 ∘f · 𝐺 ) ) )
38 dgrcl ⊢ ( ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( 𝐹 ∘f · 𝐺 ) ) ∈ ℕ0 )
39 6 38 syl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( deg ‘ ( 𝐹 ∘f · 𝐺 ) ) ∈ ℕ0 )
40 39 nn0red ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( deg ‘ ( 𝐹 ∘f · 𝐺 ) ) ∈ ℝ )
41 13 nn0red ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
42 40 41 letri3d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( ( deg ‘ ( 𝐹 ∘f · 𝐺 ) ) = ( 𝑀 + 𝑁 ) ↔ ( ( deg ‘ ( 𝐹 ∘f · 𝐺 ) ) ≤ ( 𝑀 + 𝑁 ) ∧ ( 𝑀 + 𝑁 ) ≤ ( deg ‘ ( 𝐹 ∘f · 𝐺 ) ) ) ) )
43 4 37 42 mpbir2and ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( deg ‘ ( 𝐹 ∘f · 𝐺 ) ) = ( 𝑀 + 𝑁 ) )