Theorem mhpinvcl

Description: Homogeneous polynomials are closed under taking the opposite. (Contributed by SN, 12-Sep-2023) Remove sethood hypothesis. (Revised by SN, 18-May-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.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.r	$$⊢\phi \to R\in \mathrm{Grp}$$
5		mhpinvcl.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
6		mhpinvcl.x	$$⊢\phi \to X\in H\left(N\right)$$
7		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
8		eqid	$$⊢0_R=0_R$$
9		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\}$$
10		reldmmhp	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mHomP}$$
11	10 1 6	elfvov1	$$⊢\phi \to I\in \mathrm{V}$$
12	2	mplgrp	$$⊢\left(I\in \mathrm{V}\wedge R\in \mathrm{Grp}\right)\to P\in \mathrm{Grp}$$
13	11 4 12	syl2anc	$$⊢\phi \to P\in \mathrm{Grp}$$
14	1 2 7 11 4 5 6	mhpmpl	$$⊢\phi \to X\in {\mathrm{Base}}_P$$
15	7 3	grpinvcl	$$⊢\left(P\in \mathrm{Grp}\wedge X\in {\mathrm{Base}}_P\right)\to M\left(X\right)\in {\mathrm{Base}}_P$$
16	13 14 15	syl2anc	$$⊢\phi \to M\left(X\right)\in {\mathrm{Base}}_P$$
17		eqid	$$⊢{inv}_g\left(R\right)={inv}_g\left(R\right)$$
18	2 7 17 3 11 4 14	mplneg	$$⊢\phi \to M\left(X\right)={inv}_g\left(R\right)\circ X$$
19	18	oveq1d	$$⊢\phi \to M\left(X\right)\mathrm{supp}{0}_R=\left({inv}_g\left(R\right)\circ X\right)\mathrm{supp}{0}_R$$
20		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
21	20 17	grpinvfn	$$⊢{inv}_g\left(R\right)Fn{\mathrm{Base}}_R$$
22	21	a1i	$$⊢\phi \to {inv}_g\left(R\right)Fn{\mathrm{Base}}_R$$
23	2 20 7 9 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$$
24		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
25	24	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
26	25	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}$$
27		fvexd	$$⊢\phi \to 0_R\in \mathrm{V}$$
28	8 17	grpinvid	$$⊢R\in \mathrm{Grp}\to {inv}_g\left(R\right)\left(0_R\right)=0_R$$
29	4 28	syl	$$⊢\phi \to {inv}_g\left(R\right)\left(0_R\right)=0_R$$
30	22 23 26 27 29	suppcoss	$$⊢\phi \to \left({inv}_g\left(R\right)\circ X\right)\mathrm{supp}{0}_R\subseteq X\mathrm{supp}{0}_R$$
31	19 30	eqsstrd	$$⊢\phi \to M\left(X\right)\mathrm{supp}{0}_R\subseteq X\mathrm{supp}{0}_R$$
32	1 8 9 11 4 5 6	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\}$$
33	31 32	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\}$$
34	1 2 7 8 9 11 4 5 16 33	ismhp2	$$⊢\phi \to M\left(X\right)\in H\left(N\right)$$