Theorem mhpinvcl

Description: Homogeneous polynomials are closed under taking the opposite. (Contributed by SN, 12-Sep-2023)

	Ref	Expression
Hypotheses	mhpinvcl.h	$$⊢H=I\mathrm{mHomP}R$$
	mhpinvcl.p	$$⊢P=I\mathrm{mPoly}R$$
	mhpinvcl.m	$$⊢M={inv}_g\left(P\right)$$
	mhpinvcl.i	$$⊢\phi \to I\in V$$
	mhpinvcl.r	$$⊢\phi \to R\in \mathrm{Grp}$$
	mhpinvcl.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	mhpinvcl.x	$$⊢\phi \to X\in H\left(N\right)$$
Assertion	mhpinvcl	$$⊢\phi \to M\left(X\right)\in H\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		mhpinvcl.h	$$⊢H=I\mathrm{mHomP}R$$
2		mhpinvcl.p	$$⊢P=I\mathrm{mPoly}R$$
3		mhpinvcl.m	$$⊢M={inv}_g\left(P\right)$$
4		mhpinvcl.i	$$⊢\phi \to I\in V$$
5		mhpinvcl.r	$$⊢\phi \to R\in \mathrm{Grp}$$
6		mhpinvcl.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		mhpinvcl.x	$$⊢\phi \to X\in H\left(N\right)$$
8		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
9		eqid	$$⊢0_R=0_R$$
10		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\}$$
11	2	mplgrp	$$⊢\left(I\in V\wedge R\in \mathrm{Grp}\right)\to P\in \mathrm{Grp}$$
12	4 5 11	syl2anc	$$⊢\phi \to P\in \mathrm{Grp}$$
13	1 2 8 4 5 6 7	mhpmpl	$$⊢\phi \to X\in {\mathrm{Base}}_P$$
14	8 3	grpinvcl	$$⊢\left(P\in \mathrm{Grp}\wedge X\in {\mathrm{Base}}_P\right)\to M\left(X\right)\in {\mathrm{Base}}_P$$
15	12 13 14	syl2anc	$$⊢\phi \to M\left(X\right)\in {\mathrm{Base}}_P$$
16		eqid	$$⊢{inv}_g\left(R\right)={inv}_g\left(R\right)$$
17	2 8 16 3 4 5 13	mplneg	$$⊢\phi \to M\left(X\right)={inv}_g\left(R\right)\circ X$$
18	17	oveq1d	$$⊢\phi \to M\left(X\right)\mathrm{supp}{0}_R=\left({inv}_g\left(R\right)\circ X\right)\mathrm{supp}{0}_R$$
19		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
20	19 16	grpinvfn	$$⊢{inv}_g\left(R\right)Fn{\mathrm{Base}}_R$$
21	20	a1i	$$⊢\phi \to {inv}_g\left(R\right)Fn{\mathrm{Base}}_R$$
22	2 19 8 10 13	mplelf	$$⊢\phi \to X:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
23		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
24	23	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
25	24	a1i	$$⊢\phi \to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
26		fvexd	$$⊢\phi \to 0_R\in \mathrm{V}$$
27	9 16	grpinvid	$$⊢R\in \mathrm{Grp}\to {inv}_g\left(R\right)\left(0_R\right)=0_R$$
28	5 27	syl	$$⊢\phi \to {inv}_g\left(R\right)\left(0_R\right)=0_R$$
29	21 22 25 26 28	suppcoss	$$⊢\phi \to \left({inv}_g\left(R\right)\circ X\right)\mathrm{supp}{0}_R\subseteq X\mathrm{supp}{0}_R$$
30	18 29	eqsstrd	$$⊢\phi \to M\left(X\right)\mathrm{supp}{0}_R\subseteq X\mathrm{supp}{0}_R$$
31	1 9 10 4 5 6 7	mhpdeg	$$⊢\phi \to X\mathrm{supp}{0}_R\subseteq \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$
32	30 31	sstrd	$$⊢\phi \to M\left(X\right)\mathrm{supp}{0}_R\subseteq \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$
33	1 2 8 9 10 4 5 6 15 32	ismhp2	$$⊢\phi \to M\left(X\right)\in H\left(N\right)$$