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	ffvelcdmd	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑀 ) ∈ ℂ )
21	15	coef3	⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℂ )
22	21	ad2antrl	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℂ )
23	22 12	ffvelcdmd	⊢ ( ( ( 𝐹 ∈ ( 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 · 𝐺 ) ) = ( 𝑀 + 𝑁 ) )