Theorem mhpsclcl

Description: A scalar (or constant) polynomial has degree 0. Compare deg1scl . In other contexts, there may be an exception for the zero polynomial, but under df-mhp the zero polynomial can be any degree (see mhp0cl ) so there is no exception. (Contributed by SN, 25-May-2024)

	Ref	Expression
Hypotheses	mhpsclcl.h	$$⊢H=I\mathrm{mHomP}R$$
	mhpsclcl.p	$$⊢P=I\mathrm{mPoly}R$$
	mhpsclcl.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
	mhpsclcl.k	$$⊢K={\mathrm{Base}}_R$$
	mhpsclcl.i	$$⊢\phi \to I\in V$$
	mhpsclcl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mhpsclcl.c	$$⊢\phi \to C\in K$$
Assertion	mhpsclcl	$$⊢\phi \to A\left(C\right)\in H\left(0\right)$$

Proof

Step	Hyp	Ref	Expression
1		mhpsclcl.h	$$⊢H=I\mathrm{mHomP}R$$
2		mhpsclcl.p	$$⊢P=I\mathrm{mPoly}R$$
3		mhpsclcl.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
4		mhpsclcl.k	$$⊢K={\mathrm{Base}}_R$$
5		mhpsclcl.i	$$⊢\phi \to I\in V$$
6		mhpsclcl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
7		mhpsclcl.c	$$⊢\phi \to C\in K$$
8		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
9		eqid	$$⊢0_R=0_R$$
10	5	adantr	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to I\in V$$
11	6	adantr	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to R\in \mathrm{Ring}$$
12	7	adantr	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to C\in K$$
13	2 8 9 4 3 10 11 12	mplascl	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to A\left(C\right)=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(y=I\times \left\{0\right\},C,0_R\right)\right)$$
14		eqeq1	$$⊢y=d\to \left(y=I\times \left\{0\right\}\leftrightarrow d=I\times \left\{0\right\}\right)$$
15	14	ifbid	$$⊢y=d\to if\left(y=I\times \left\{0\right\},C,0_R\right)=if\left(d=I\times \left\{0\right\},C,0_R\right)$$
16	15	adantl	$$⊢\left(\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge y=d\right)\to if\left(y=I\times \left\{0\right\},C,0_R\right)=if\left(d=I\times \left\{0\right\},C,0_R\right)$$
17		simpr	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
18		fvexd	$$⊢\phi \to 0_R\in \mathrm{V}$$
19	7 18	ifexd	$$⊢\phi \to if\left(d=I\times \left\{0\right\},C,0_R\right)\in \mathrm{V}$$
20	19	adantr	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to if\left(d=I\times \left\{0\right\},C,0_R\right)\in \mathrm{V}$$
21	13 16 17 20	fvmptd	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to A\left(C\right)\left(d\right)=if\left(d=I\times \left\{0\right\},C,0_R\right)$$
22	21	neeq1d	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(A\left(C\right)\left(d\right)\ne 0_R\leftrightarrow if\left(d=I\times \left\{0\right\},C,0_R\right)\ne 0_R\right)$$
23		iffalse	$$⊢\neg d=I\times \left\{0\right\}\to if\left(d=I\times \left\{0\right\},C,0_R\right)=0_R$$
24	23	necon1ai	$$⊢if\left(d=I\times \left\{0\right\},C,0_R\right)\ne 0_R\to d=I\times \left\{0\right\}$$
25		fconstmpt	$$⊢I\times \left\{0\right\}=\left(k\in I⟼0\right)$$
26	25	oveq2i	$$⊢{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(I\times \left\{0\right\}\right)=\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}}0$$
27		nn0subm	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
28		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
29	28	submmnd	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{Mnd}$$
30	27 29	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{Mnd}$$
31		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
32	28 31	subm0	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to 0=0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
33	27 32	ax-mp	$$⊢0=0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
34	33	gsumz	$$⊢\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{Mnd}\wedge I\in V\right)\to \underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}}0=0$$
35	30 10 34	sylancr	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}}0=0$$
36	26 35	syl5eq	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(I\times \left\{0\right\}\right)=0$$
37		oveq2	$$⊢d=I\times \left\{0\right\}\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d={\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(I\times \left\{0\right\}\right)$$
38	37	eqeq1d	$$⊢d=I\times \left\{0\right\}\to \left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=0\leftrightarrow {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(I\times \left\{0\right\}\right)=0\right)$$
39	36 38	syl5ibrcom	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(d=I\times \left\{0\right\}\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=0\right)$$
40	24 39	syl5	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(if\left(d=I\times \left\{0\right\},C,0_R\right)\ne 0_R\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=0\right)$$
41	22 40	sylbid	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(A\left(C\right)\left(d\right)\ne 0_R\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=0\right)$$
42	41	ralrimiva	$$⊢\phi \to \forall d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(A\left(C\right)\left(d\right)\ne 0_R\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=0\right)$$
43		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
44		0nn0	$$⊢0\in {\mathbb{N}}_0$$
45	44	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
46	2 43 4 3 5 6	mplasclf	$$⊢\phi \to A:K⟶{\mathrm{Base}}_P$$
47	46 7	ffvelrnd	$$⊢\phi \to A\left(C\right)\in {\mathrm{Base}}_P$$
48	1 2 43 9 8 5 6 45 47	ismhp3	$$⊢\phi \to \left(A\left(C\right)\in H\left(0\right)\leftrightarrow \forall d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(A\left(C\right)\left(d\right)\ne 0_R\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=0\right)\right)$$
49	42 48	mpbird	$$⊢\phi \to A\left(C\right)\in H\left(0\right)$$