Theorem mhpvarcl

Description: A power series variable is a polynomial of degree 1. (Contributed by SN, 25-May-2024)

	Ref	Expression
Hypotheses	mhpvarcl.h	$$⊢H=I\mathrm{mHomP}R$$
	mhpvarcl.v	$$⊢V=I\mathrm{mVar}R$$
	mhpvarcl.i	$$⊢\phi \to I\in W$$
	mhpvarcl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mhpvarcl.x	$$⊢\phi \to X\in I$$
Assertion	mhpvarcl	$$⊢\phi \to V\left(X\right)\in H\left(1\right)$$

Proof

Step	Hyp	Ref	Expression
1		mhpvarcl.h	$$⊢H=I\mathrm{mHomP}R$$
2		mhpvarcl.v	$$⊢V=I\mathrm{mVar}R$$
3		mhpvarcl.i	$$⊢\phi \to I\in W$$
4		mhpvarcl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
5		mhpvarcl.x	$$⊢\phi \to X\in I$$
6		iffalse	$$⊢\neg d=\left(y\in I⟼if\left(y=X,1,0\right)\right)\to if\left(d=\left(y\in I⟼if\left(y=X,1,0\right)\right),1_R,0_R\right)=0_R$$
7		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\}$$
8		eqid	$$⊢0_R=0_R$$
9		eqid	$$⊢1_R=1_R$$
10	3	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 W$$
11	4	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	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 X\in I$$
13		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\}$$
14	2 7 8 9 10 11 12 13	mvrval2	$$⊢\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 V\left(X\right)\left(d\right)=if\left(d=\left(y\in I⟼if\left(y=X,1,0\right)\right),1_R,0_R\right)$$
15	14	eqeq1d	$$⊢\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(V\left(X\right)\left(d\right)=0_R\leftrightarrow if\left(d=\left(y\in I⟼if\left(y=X,1,0\right)\right),1_R,0_R\right)=0_R\right)$$
16	6 15	imbitrrid	$$⊢\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(\neg d=\left(y\in I⟼if\left(y=X,1,0\right)\right)\to V\left(X\right)\left(d\right)=0_R\right)$$
17	16	necon1ad	$$⊢\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(V\left(X\right)\left(d\right)\ne 0_R\to d=\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$
18		nn0subm	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
19		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
20		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
21	19 20	subm0	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to 0=0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
22	18 21	ax-mp	$$⊢0=0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
23	19	submmnd	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{Mnd}$$
24	18 23	mp1i	$$⊢\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 {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{Mnd}$$
25		eqid	$$⊢\left(y\in I⟼if\left(y=X,1,0\right)\right)=\left(y\in I⟼if\left(y=X,1,0\right)\right)$$
26		1nn0	$$⊢1\in {\mathbb{N}}_0$$
27	19	submbas	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to {\mathbb{N}}_0={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
28	18 27	ax-mp	$$⊢{\mathbb{N}}_0={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
29	26 28	eleqtri	$$⊢1\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
30	29	a1i	$$⊢\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 1\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
31	22 24 10 12 25 30	gsummptif1n0	$$⊢\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{y\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}}if\left(y=X,1,0\right)=1$$
32		oveq2	$$⊢d=\left(y\in I⟼if\left(y=X,1,0\right)\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=\underset{y\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}}if\left(y=X,1,0\right)$$
33	32	eqeq1d	$$⊢d=\left(y\in I⟼if\left(y=X,1,0\right)\right)\to \left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=1\leftrightarrow \underset{y\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}}if\left(y=X,1,0\right)=1\right)$$
34	31 33	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=\left(y\in I⟼if\left(y=X,1,0\right)\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=1\right)$$
35	17 34	syld	$$⊢\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(V\left(X\right)\left(d\right)\ne 0_R\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=1\right)$$
36	35	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(V\left(X\right)\left(d\right)\ne 0_R\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=1\right)$$
37		eqid	$$⊢I\mathrm{mPoly}R=I\mathrm{mPoly}R$$
38		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
39	26	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
40	37 2 38 3 4 5	mvrcl	$$⊢\phi \to V\left(X\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
41	1 37 38 8 7 3 4 39 40	ismhp3	$$⊢\phi \to \left(V\left(X\right)\in H\left(1\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(V\left(X\right)\left(d\right)\ne 0_R\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=1\right)\right)$$
42	36 41	mpbird	$$⊢\phi \to V\left(X\right)\in H\left(1\right)$$