Theorem mhpinvcl

Description: Homogeneous polynomials are closed under taking the opposite. (Contributed by SN, 12-Sep-2023) Remove closure hypotheses. (Revised by SN, 4-Sep-2025)

	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.r	$$⊢\phi \to R\in \mathrm{Grp}$$
	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.r	$$⊢\phi \to R\in \mathrm{Grp}$$
5		mhpinvcl.x	$$⊢\phi \to X\in H\left(N\right)$$
6		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
7		eqid	$$⊢0_R=0_R$$
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		reldmmhp	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mHomP}$$
10	9 1 5	elfvov1	$$⊢\phi \to I\in \mathrm{V}$$
11	1 5	mhprcl	$$⊢\phi \to N\in {\mathbb{N}}_0$$
12	2	mplgrp	$$⊢\left(I\in \mathrm{V}\wedge R\in \mathrm{Grp}\right)\to P\in \mathrm{Grp}$$
13	10 4 12	syl2anc	$$⊢\phi \to P\in \mathrm{Grp}$$
14	1 2 6 5	mhpmpl	$$⊢\phi \to X\in {\mathrm{Base}}_P$$
15	6 3 13 14	grpinvcld	$$⊢\phi \to M\left(X\right)\in {\mathrm{Base}}_P$$
16		eqid	$$⊢{inv}_g\left(R\right)={inv}_g\left(R\right)$$
17	2 6 16 3 10 4 14	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 6 8 14	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	7 16	grpinvid	$$⊢R\in \mathrm{Grp}\to {inv}_g\left(R\right)\left(0_R\right)=0_R$$
28	4 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 7 8 5	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 6 7 8 10 4 11 15 32	ismhp2	$$⊢\phi \to M\left(X\right)\in H\left(N\right)$$