Theorem mplneg

Description: The negative function on multivariate polynomials. (Contributed by SN, 25-May-2024)

	Ref	Expression
Hypotheses	mplneg.p	$$⊢P=I\mathrm{mPoly}R$$
	mplneg.b	$$⊢B={\mathrm{Base}}_P$$
	mplneg.n	$$⊢N={inv}_g\left(R\right)$$
	mplneg.m	$$⊢M={inv}_g\left(P\right)$$
	mplneg.i	$$⊢\phi \to I\in V$$
	mplneg.r	$$⊢\phi \to R\in \mathrm{Grp}$$
	mplneg.x	$$⊢\phi \to X\in B$$
Assertion	mplneg	$$⊢\phi \to M\left(X\right)=N\circ X$$

Proof

Step	Hyp	Ref	Expression
1		mplneg.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplneg.b	$$⊢B={\mathrm{Base}}_P$$
3		mplneg.n	$$⊢N={inv}_g\left(R\right)$$
4		mplneg.m	$$⊢M={inv}_g\left(P\right)$$
5		mplneg.i	$$⊢\phi \to I\in V$$
6		mplneg.r	$$⊢\phi \to R\in \mathrm{Grp}$$
7		mplneg.x	$$⊢\phi \to X\in B$$
8		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
9	8 1 2 5 6	mplsubg	$$⊢\phi \to B\in \mathrm{SubGrp}\left(I\mathrm{mPwSer}R\right)$$
10	1 8 2	mplval2	$$⊢P=\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}B$$
11		eqid	$$⊢{inv}_g\left(I\mathrm{mPwSer}R\right)={inv}_g\left(I\mathrm{mPwSer}R\right)$$
12	10 11 4	subginv	$$⊢\left(B\in \mathrm{SubGrp}\left(I\mathrm{mPwSer}R\right)\wedge X\in B\right)\to {inv}_g\left(I\mathrm{mPwSer}R\right)\left(X\right)=M\left(X\right)$$
13	9 7 12	syl2anc	$$⊢\phi \to {inv}_g\left(I\mathrm{mPwSer}R\right)\left(X\right)=M\left(X\right)$$
14		eqid	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
15		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
16	1 8 2 15	mplbasss	$$⊢B\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
17	16	sseli	$$⊢X\in B\to X\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
18	7 17	syl	$$⊢\phi \to X\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
19	8 5 6 14 3 15 11 18	psrneg	$$⊢\phi \to {inv}_g\left(I\mathrm{mPwSer}R\right)\left(X\right)=N\circ X$$
20	13 19	eqtr3d	$$⊢\phi \to M\left(X\right)=N\circ X$$