Theorem mdegvsca

Description: The degree of a scalar multiple of a polynomial is exactly the degree of the original polynomial when the multiple is a nonzero-divisor. (Contributed by Stefan O'Rear, 28-Mar-2015) (Proof shortened by AV, 27-Jul-2019)

	Ref	Expression
Hypotheses	mdegaddle.y	$$⊢Y=I\mathrm{mPoly}R$$
	mdegaddle.d	$$⊢D=I\mathrm{mDeg}R$$
	mdegaddle.i	$$⊢\phi \to I\in V$$
	mdegaddle.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mdegvsca.b	$$⊢B={\mathrm{Base}}_Y$$
	mdegvsca.e	$$⊢E=\mathrm{RLReg}\left(R\right)$$
	mdegvsca.p	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	mdegvsca.f	$$⊢\phi \to F\in E$$
	mdegvsca.g	$$⊢\phi \to G\in B$$
Assertion	mdegvsca	$$⊢\phi \to D\left(F\underset{\dot{}}{·}G\right)=D\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		mdegaddle.y	$$⊢Y=I\mathrm{mPoly}R$$
2		mdegaddle.d	$$⊢D=I\mathrm{mDeg}R$$
3		mdegaddle.i	$$⊢\phi \to I\in V$$
4		mdegaddle.r	$$⊢\phi \to R\in \mathrm{Ring}$$
5		mdegvsca.b	$$⊢B={\mathrm{Base}}_Y$$
6		mdegvsca.e	$$⊢E=\mathrm{RLReg}\left(R\right)$$
7		mdegvsca.p	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
8		mdegvsca.f	$$⊢\phi \to F\in E$$
9		mdegvsca.g	$$⊢\phi \to G\in B$$
10		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
11		eqid	$$⊢{\cdot }_R={\cdot }_R$$
12		eqid	$$⊢\left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
13	6 10	rrgss	$$⊢E\subseteq {\mathrm{Base}}_R$$
14	13 8	sseldi	$$⊢\phi \to F\in {\mathrm{Base}}_R$$
15	1 7 10 5 11 12 14 9	mplvsca	$$⊢\phi \to F\underset{\dot{}}{·}G=\left(\left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{F\right\}\right){{\cdot }_R}_{f}G$$
16	15	oveq1d	$$⊢\phi \to \left(F\underset{\dot{}}{·}G\right)\mathrm{supp}{0}_R=\left(\left(\left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{F\right\}\right){{\cdot }_R}_{f}G\right)\mathrm{supp}{0}_R$$
17		eqid	$$⊢0_R=0_R$$
18		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
19	18	rabex	$$⊢\left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
20	19	a1i	$$⊢\phi \to \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
21	1 10 5 12 9	mplelf	$$⊢\phi \to G:\left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
22	6 10 11 17 20 4 8 21	rrgsupp	$$⊢\phi \to \left(\left(\left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{F\right\}\right){{\cdot }_R}_{f}G\right)\mathrm{supp}{0}_R=G\mathrm{supp}{0}_R$$
23	16 22	eqtrd	$$⊢\phi \to \left(F\underset{\dot{}}{·}G\right)\mathrm{supp}{0}_R=G\mathrm{supp}{0}_R$$
24	23	imaeq2d	$$⊢\phi \to \left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)\left[\left(F\underset{\dot{}}{·}G\right)\mathrm{supp}{0}_R\right]=\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)\left[G\mathrm{supp}{0}_R\right]$$
25	24	supeq1d	$$⊢\phi \to sup\left(\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)\left[\left(F\underset{\dot{}}{·}G\right)\mathrm{supp}{0}_R\right],{ℝ}^{*},<\right)=sup\left(\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)\left[G\mathrm{supp}{0}_R\right],{ℝ}^{*},<\right)$$
26	1	mpllmod	$$⊢\left(I\in V\wedge R\in \mathrm{Ring}\right)\to Y\in \mathrm{LMod}$$
27	3 4 26	syl2anc	$$⊢\phi \to Y\in \mathrm{LMod}$$
28	1 3 4	mplsca	$$⊢\phi \to R=\mathrm{Scalar}\left(Y\right)$$
29	28	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(Y\right)}$$
30	14 29	eleqtrd	$$⊢\phi \to F\in {\mathrm{Base}}_{\mathrm{Scalar}\left(Y\right)}$$
31		eqid	$$⊢\mathrm{Scalar}\left(Y\right)=\mathrm{Scalar}\left(Y\right)$$
32		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(Y\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(Y\right)}$$
33	5 31 7 32	lmodvscl	$$⊢\left(Y\in \mathrm{LMod}\wedge F\in {\mathrm{Base}}_{\mathrm{Scalar}\left(Y\right)}\wedge G\in B\right)\to F\underset{\dot{}}{·}G\in B$$
34	27 30 9 33	syl3anc	$$⊢\phi \to F\underset{\dot{}}{·}G\in B$$
35		eqid	$$⊢\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)=\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)$$
36	2 1 5 17 12 35	mdegval	$$⊢F\underset{\dot{}}{·}G\in B\to D\left(F\underset{\dot{}}{·}G\right)=sup\left(\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)\left[\left(F\underset{\dot{}}{·}G\right)\mathrm{supp}{0}_R\right],{ℝ}^{*},<\right)$$
37	34 36	syl	$$⊢\phi \to D\left(F\underset{\dot{}}{·}G\right)=sup\left(\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)\left[\left(F\underset{\dot{}}{·}G\right)\mathrm{supp}{0}_R\right],{ℝ}^{*},<\right)$$
38	2 1 5 17 12 35	mdegval	$$⊢G\in B\to D\left(G\right)=sup\left(\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)\left[G\mathrm{supp}{0}_R\right],{ℝ}^{*},<\right)$$
39	9 38	syl	$$⊢\phi \to D\left(G\right)=sup\left(\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)\left[G\mathrm{supp}{0}_R\right],{ℝ}^{*},<\right)$$
40	25 37 39	3eqtr4d	$$⊢\phi \to D\left(F\underset{\dot{}}{·}G\right)=D\left(G\right)$$