Theorem deg1mul2

Description: Degree of multiplication of two nonzero polynomials when the first leads with a nonzero-divisor coefficient. (Contributed by Stefan O'Rear, 26-Mar-2015)

	Ref	Expression
Hypotheses	deg1mul2.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	deg1mul2.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	deg1mul2.e	$$⊢E=\mathrm{RLReg}\left(R\right)$$
	deg1mul2.b	$$⊢B={\mathrm{Base}}_P$$
	deg1mul2.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	deg1mul2.z	$$⊢\underset{\dot{}}{0}=0_P$$
	deg1mul2.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	deg1mul2.fb	$$⊢\phi \to F\in B$$
	deg1mul2.fz	$$⊢\phi \to F\ne \underset{\dot{}}{0}$$
	deg1mul2.fc	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\in E$$
	deg1mul2.gb	$$⊢\phi \to G\in B$$
	deg1mul2.gz	$$⊢\phi \to G\ne \underset{\dot{}}{0}$$
Assertion	deg1mul2	$$⊢\phi \to D\left(F\underset{\dot{}}{·}G\right)=D\left(F\right)+D\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		deg1mul2.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		deg1mul2.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		deg1mul2.e	$$⊢E=\mathrm{RLReg}\left(R\right)$$
4		deg1mul2.b	$$⊢B={\mathrm{Base}}_P$$
5		deg1mul2.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
6		deg1mul2.z	$$⊢\underset{\dot{}}{0}=0_P$$
7		deg1mul2.r	$$⊢\phi \to R\in \mathrm{Ring}$$
8		deg1mul2.fb	$$⊢\phi \to F\in B$$
9		deg1mul2.fz	$$⊢\phi \to F\ne \underset{\dot{}}{0}$$
10		deg1mul2.fc	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\in E$$
11		deg1mul2.gb	$$⊢\phi \to G\in B$$
12		deg1mul2.gz	$$⊢\phi \to G\ne \underset{\dot{}}{0}$$
13	2	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
14	7 13	syl	$$⊢\phi \to P\in \mathrm{Ring}$$
15	4 5	ringcl	$$⊢\left(P\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to F\underset{\dot{}}{·}G\in B$$
16	14 8 11 15	syl3anc	$$⊢\phi \to F\underset{\dot{}}{·}G\in B$$
17	1 2 4	deg1xrcl	$$⊢F\underset{\dot{}}{·}G\in B\to D\left(F\underset{\dot{}}{·}G\right)\in {ℝ}^{*}$$
18	16 17	syl	$$⊢\phi \to D\left(F\underset{\dot{}}{·}G\right)\in {ℝ}^{*}$$
19	1 2 6 4	deg1nn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to D\left(F\right)\in {\mathbb{N}}_0$$
20	7 8 9 19	syl3anc	$$⊢\phi \to D\left(F\right)\in {\mathbb{N}}_0$$
21	1 2 6 4	deg1nn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge G\in B\wedge G\ne \underset{\dot{}}{0}\right)\to D\left(G\right)\in {\mathbb{N}}_0$$
22	7 11 12 21	syl3anc	$$⊢\phi \to D\left(G\right)\in {\mathbb{N}}_0$$
23	20 22	nn0addcld	$$⊢\phi \to D\left(F\right)+D\left(G\right)\in {\mathbb{N}}_0$$
24	23	nn0red	$$⊢\phi \to D\left(F\right)+D\left(G\right)\in ℝ$$
25	24	rexrd	$$⊢\phi \to D\left(F\right)+D\left(G\right)\in {ℝ}^{*}$$
26	20	nn0red	$$⊢\phi \to D\left(F\right)\in ℝ$$
27	26	leidd	$$⊢\phi \to D\left(F\right)\le D\left(F\right)$$
28	22	nn0red	$$⊢\phi \to D\left(G\right)\in ℝ$$
29	28	leidd	$$⊢\phi \to D\left(G\right)\le D\left(G\right)$$
30	2 1 7 4 5 8 11 20 22 27 29	deg1mulle2	$$⊢\phi \to D\left(F\underset{\dot{}}{·}G\right)\le D\left(F\right)+D\left(G\right)$$
31		eqid	$$⊢{\cdot }_R={\cdot }_R$$
32	2 5 31 4 1 6 7 8 9 11 12	coe1mul4	$$⊢\phi \to {\mathrm{coe}}_1\left(F\underset{\dot{}}{·}G\right)\left(D\left(F\right)+D\left(G\right)\right)={\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right){\cdot }_R{\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)$$
33		eqid	$$⊢0_R=0_R$$
34		eqid	$$⊢{\mathrm{coe}}_1\left(G\right)={\mathrm{coe}}_1\left(G\right)$$
35	1 2 6 4 33 34	deg1ldg	$$⊢\left(R\in \mathrm{Ring}\wedge G\in B\wedge G\ne \underset{\dot{}}{0}\right)\to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\ne 0_R$$
36	7 11 12 35	syl3anc	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\ne 0_R$$
37		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
38	34 4 2 37	coe1f	$$⊢G\in B\to {\mathrm{coe}}_1\left(G\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R$$
39	11 38	syl	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R$$
40	39 22	ffvelcdmd	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\in {\mathrm{Base}}_R$$
41	3 37 31 33	rrgeq0i	$$⊢\left({\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\in E\wedge {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\in {\mathrm{Base}}_R\right)\to \left({\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right){\cdot }_R{\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)=0_R\to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)=0_R\right)$$
42	10 40 41	syl2anc	$$⊢\phi \to \left({\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right){\cdot }_R{\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)=0_R\to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)=0_R\right)$$
43	42	necon3d	$$⊢\phi \to \left({\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\ne 0_R\to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right){\cdot }_R{\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\ne 0_R\right)$$
44	36 43	mpd	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right){\cdot }_R{\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\ne 0_R$$
45	32 44	eqnetrd	$$⊢\phi \to {\mathrm{coe}}_1\left(F\underset{\dot{}}{·}G\right)\left(D\left(F\right)+D\left(G\right)\right)\ne 0_R$$
46		eqid	$$⊢{\mathrm{coe}}_1\left(F\underset{\dot{}}{·}G\right)={\mathrm{coe}}_1\left(F\underset{\dot{}}{·}G\right)$$
47	1 2 4 33 46	deg1ge	$$⊢\left(F\underset{\dot{}}{·}G\in B\wedge D\left(F\right)+D\left(G\right)\in {\mathbb{N}}_0\wedge {\mathrm{coe}}_1\left(F\underset{\dot{}}{·}G\right)\left(D\left(F\right)+D\left(G\right)\right)\ne 0_R\right)\to D\left(F\right)+D\left(G\right)\le D\left(F\underset{\dot{}}{·}G\right)$$
48	16 23 45 47	syl3anc	$$⊢\phi \to D\left(F\right)+D\left(G\right)\le D\left(F\underset{\dot{}}{·}G\right)$$
49	18 25 30 48	xrletrid	$$⊢\phi \to D\left(F\underset{\dot{}}{·}G\right)=D\left(F\right)+D\left(G\right)$$