Theorem mhpaddcl

Description: Homogeneous polynomials are closed under addition. (Contributed by SN, 26-Aug-2023) Remove closure hypotheses. (Revised by SN, 4-Sep-2025)

	Ref	Expression
Hypotheses	mhpaddcl.h	$$⊢H=I\mathrm{mHomP}R$$
	mhpaddcl.p	$$⊢P=I\mathrm{mPoly}R$$
	mhpaddcl.a	$$⊢\underset{\dot{}}{+}={+}_P$$
	mhpaddcl.r	$$⊢\phi \to R\in \mathrm{Grp}$$
	mhpaddcl.x	$$⊢\phi \to X\in H\left(N\right)$$
	mhpaddcl.y	$$⊢\phi \to Y\in H\left(N\right)$$
Assertion	mhpaddcl	$$⊢\phi \to X\underset{\dot{}}{+}Y\in H\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		mhpaddcl.h	$$⊢H=I\mathrm{mHomP}R$$
2		mhpaddcl.p	$$⊢P=I\mathrm{mPoly}R$$
3		mhpaddcl.a	$$⊢\underset{\dot{}}{+}={+}_P$$
4		mhpaddcl.r	$$⊢\phi \to R\in \mathrm{Grp}$$
5		mhpaddcl.x	$$⊢\phi \to X\in H\left(N\right)$$
6		mhpaddcl.y	$$⊢\phi \to Y\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 5	elfvov1	$$⊢\phi \to I\in \mathrm{V}$$
12	1 5	mhprcl	$$⊢\phi \to N\in {\mathbb{N}}_0$$
13	2	mplgrp	$$⊢\left(I\in \mathrm{V}\wedge R\in \mathrm{Grp}\right)\to P\in \mathrm{Grp}$$
14	11 4 13	syl2anc	$$⊢\phi \to P\in \mathrm{Grp}$$
15	1 2 7 5	mhpmpl	$$⊢\phi \to X\in {\mathrm{Base}}_P$$
16	1 2 7 6	mhpmpl	$$⊢\phi \to Y\in {\mathrm{Base}}_P$$
17	7 3 14 15 16	grpcld	$$⊢\phi \to X\underset{\dot{}}{+}Y\in {\mathrm{Base}}_P$$
18		eqid	$$⊢{+}_R={+}_R$$
19	2 7 18 3 15 16	mpladd	$$⊢\phi \to X\underset{\dot{}}{+}Y=X{{+}_R}_{f}Y$$
20	19	oveq1d	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\mathrm{supp}{0}_R=\left(X{{+}_R}_{f}Y\right)\mathrm{supp}{0}_R$$
21		ovexd	$$⊢\phi \to {{\mathbb{N}}_0}^I\in \mathrm{V}$$
22	9 21	rabexd	$$⊢\phi \to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
23		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
24	23 8	grpidcl	$$⊢R\in \mathrm{Grp}\to 0_R\in {\mathrm{Base}}_R$$
25	4 24	syl	$$⊢\phi \to 0_R\in {\mathrm{Base}}_R$$
26	2 23 7 9 15	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$$
27	2 23 7 9 16	mplelf	$$⊢\phi \to Y:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
28	23 18 8 4 25	grplidd	$$⊢\phi \to 0_R{+}_R{0}_R=0_R$$
29	22 25 26 27 28	suppofssd	$$⊢\phi \to \left(X{{+}_R}_{f}Y\right)\mathrm{supp}{0}_R\subseteq {supp}_{0_R}\left(X\right)\cup {supp}_{0_R}\left(Y\right)$$
30	20 29	eqsstrd	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\mathrm{supp}{0}_R\subseteq {supp}_{0_R}\left(X\right)\cup {supp}_{0_R}\left(Y\right)$$
31	1 8 9 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	1 8 9 6	mhpdeg	$$⊢\phi \to Y\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	unssd	$$⊢\phi \to {supp}_{0_R}\left(X\right)\cup {supp}_{0_R}\left(Y\right)\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	30 33	sstrd	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\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\}$$
35	1 2 7 8 9 11 4 12 17 34	ismhp2	$$⊢\phi \to X\underset{\dot{}}{+}Y\in H\left(N\right)$$