Theorem deg1mul

Description: Degree of multiplication of two nonzero polynomials in a domain. (Contributed by metakunt, 6-May-2025)

	Ref	Expression
Hypotheses	deg1mul.1	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	deg1mul.2	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	deg1mul.3	$$⊢B={\mathrm{Base}}_P$$
	deg1mul.4	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	deg1mul.5	$$⊢\underset{\dot{}}{0}=0_P$$
	deg1mul.6	$$⊢\phi \to R\in \mathrm{Domn}$$
	deg1mul.7	$$⊢\phi \to F\in B$$
	deg1mul.8	$$⊢\phi \to F\ne \underset{\dot{}}{0}$$
	deg1mul.9	$$⊢\phi \to G\in B$$
	deg1mul.10	$$⊢\phi \to G\ne \underset{\dot{}}{0}$$
Assertion	deg1mul	$$⊢\phi \to D\left(F\underset{\dot{}}{·}G\right)=D\left(F\right)+D\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		deg1mul.1	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		deg1mul.2	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		deg1mul.3	$$⊢B={\mathrm{Base}}_P$$
4		deg1mul.4	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
5		deg1mul.5	$$⊢\underset{\dot{}}{0}=0_P$$
6		deg1mul.6	$$⊢\phi \to R\in \mathrm{Domn}$$
7		deg1mul.7	$$⊢\phi \to F\in B$$
8		deg1mul.8	$$⊢\phi \to F\ne \underset{\dot{}}{0}$$
9		deg1mul.9	$$⊢\phi \to G\in B$$
10		deg1mul.10	$$⊢\phi \to G\ne \underset{\dot{}}{0}$$
11		eqid	$$⊢\mathrm{RLReg}\left(R\right)=\mathrm{RLReg}\left(R\right)$$
12		domnring	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{Ring}$$
13	6 12	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
14	1 2 5 3	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$$
15	13 7 8 14	syl3anc	$$⊢\phi \to D\left(F\right)\in {\mathbb{N}}_0$$
16		eqid	$$⊢{\mathrm{coe}}_1\left(F\right)={\mathrm{coe}}_1\left(F\right)$$
17		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
18	16 3 2 17	coe1fvalcl	$$⊢\left(F\in B\wedge D\left(F\right)\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\in {\mathrm{Base}}_R$$
19	7 15 18	syl2anc	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\in {\mathrm{Base}}_R$$
20		eqid	$$⊢0_R=0_R$$
21	1 2 5 3 20 16	deg1ldg	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\ne 0_R$$
22	13 7 8 21	syl3anc	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\ne 0_R$$
23	17 11 20	domnrrg	$$⊢\left(R\in \mathrm{Domn}\wedge {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\in {\mathrm{Base}}_R\wedge {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\ne 0_R\right)\to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\in \mathrm{RLReg}\left(R\right)$$
24	6 19 22 23	syl3anc	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\in \mathrm{RLReg}\left(R\right)$$
25	1 2 11 3 4 5 13 7 8 24 9 10	deg1mul2	$$⊢\phi \to D\left(F\underset{\dot{}}{·}G\right)=D\left(F\right)+D\left(G\right)$$