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	$⊢ M = \deg (F)$
	dgradd.2	$⊢ N = \deg (G)$
Assertion	dgrmul	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to \deg (F \times_{f} G) = M + N$

Proof

Step	Hyp	Ref	Expression
1		dgradd.1	$⊢ M = \deg (F)$
2		dgradd.2	$⊢ N = \deg (G)$
3	1 2	dgrmul2	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to \deg (F \times_{f} G) \leq M + N$
4	3	ad2ant2r	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to \deg (F \times_{f} G) \leq M + N$
5		plymulcl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F \times_{f} G \in Poly (ℂ)$
6	5	ad2ant2r	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to F \times_{f} G \in Poly (ℂ)$
7		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
8	1 7	eqeltrid	$⊢ F \in Poly (S) \to M \in ℕ_{0}$
9	8	ad2antrr	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to M \in ℕ_{0}$
10		dgrcl	$⊢ G \in Poly (S) \to \deg (G) \in ℕ_{0}$
11	2 10	eqeltrid	$⊢ G \in Poly (S) \to N \in ℕ_{0}$
12	11	ad2antrl	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to N \in ℕ_{0}$
13	9 12	nn0addcld	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to M + N \in ℕ_{0}$
14		eqid	$⊢ coeff (F) = coeff (F)$
15		eqid	$⊢ coeff (G) = coeff (G)$
16	14 15 1 2	coemulhi	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to coeff (F \times_{f} G) (M + N) = coeff (F) (M) coeff (G) (N)$
17	16	ad2ant2r	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to coeff (F \times_{f} G) (M + N) = coeff (F) (M) coeff (G) (N)$
18	14	coef3	$⊢ F \in Poly (S) \to coeff (F) : ℕ_{0} ⟶ ℂ$
19	18	ad2antrr	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to coeff (F) : ℕ_{0} ⟶ ℂ$
20	19 9	ffvelcdmd	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to coeff (F) (M) \in ℂ$
21	15	coef3	$⊢ G \in Poly (S) \to coeff (G) : ℕ_{0} ⟶ ℂ$
22	21	ad2antrl	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to coeff (G) : ℕ_{0} ⟶ ℂ$
23	22 12	ffvelcdmd	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to coeff (G) (N) \in ℂ$
24	1 14	dgreq0	$⊢ F \in Poly (S) \to (F = 0_{𝑝} \leftrightarrow coeff (F) (M) = 0)$
25	24	necon3bid	$⊢ F \in Poly (S) \to (F \neq 0_{𝑝} \leftrightarrow coeff (F) (M) \neq 0)$
26	25	biimpa	$⊢ (F \in Poly (S) \land F \neq 0_{𝑝}) \to coeff (F) (M) \neq 0$
27	26	adantr	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to coeff (F) (M) \neq 0$
28	2 15	dgreq0	$⊢ G \in Poly (S) \to (G = 0_{𝑝} \leftrightarrow coeff (G) (N) = 0)$
29	28	necon3bid	$⊢ G \in Poly (S) \to (G \neq 0_{𝑝} \leftrightarrow coeff (G) (N) \neq 0)$
30	29	biimpa	$⊢ (G \in Poly (S) \land G \neq 0_{𝑝}) \to coeff (G) (N) \neq 0$
31	30	adantl	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to coeff (G) (N) \neq 0$
32	20 23 27 31	mulne0d	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to coeff (F) (M) coeff (G) (N) \neq 0$
33	17 32	eqnetrd	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to coeff (F \times_{f} G) (M + N) \neq 0$
34		eqid	$⊢ coeff (F \times_{f} G) = coeff (F \times_{f} G)$
35		eqid	$⊢ \deg (F \times_{f} G) = \deg (F \times_{f} G)$
36	34 35	dgrub	$⊢ (F \times_{f} G \in Poly (ℂ) \land M + N \in ℕ_{0} \land coeff (F \times_{f} G) (M + N) \neq 0) \to M + N \leq \deg (F \times_{f} G)$
37	6 13 33 36	syl3anc	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to M + N \leq \deg (F \times_{f} G)$
38		dgrcl	$⊢ F \times_{f} G \in Poly (ℂ) \to \deg (F \times_{f} G) \in ℕ_{0}$
39	6 38	syl	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to \deg (F \times_{f} G) \in ℕ_{0}$
40	39	nn0red	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to \deg (F \times_{f} G) \in ℝ$
41	13	nn0red	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to M + N \in ℝ$
42	40 41	letri3d	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to (\deg (F \times_{f} G) = M + N \leftrightarrow (\deg (F \times_{f} G) \leq M + N \land M + N \leq \deg (F \times_{f} G)))$
43	4 37 42	mpbir2and	$⊢ ((F \in Poly (S) \land F \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to \deg (F \times_{f} G) = M + N$

Metamath Proof Explorer

Theorem dgrmul

Proof