Theorem mhpaddcl

Description: Homogeneous polynomials are closed under addition. (Contributed by SN, 26-Aug-2023) Remove sethood hypothesis. (Revised by SN, 18-May-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.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	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.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
6		mhpaddcl.x	$$⊢\phi \to X\in H\left(N\right)$$
7		mhpaddcl.y	$$⊢\phi \to Y\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		reldmmhp	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mHomP}$$
12	11 1 6	elfvov1	$$⊢\phi \to I\in \mathrm{V}$$
13	2	mplgrp	$$⊢\left(I\in \mathrm{V}\wedge R\in \mathrm{Grp}\right)\to P\in \mathrm{Grp}$$
14	12 4 13	syl2anc	$$⊢\phi \to P\in \mathrm{Grp}$$
15	1 2 8 12 4 5 6	mhpmpl	$$⊢\phi \to X\in {\mathrm{Base}}_P$$
16	1 2 8 12 4 5 7	mhpmpl	$$⊢\phi \to Y\in {\mathrm{Base}}_P$$
17	8 3	grpcl	$$⊢\left(P\in \mathrm{Grp}\wedge X\in {\mathrm{Base}}_P\wedge Y\in {\mathrm{Base}}_P\right)\to X\underset{\dot{}}{+}Y\in {\mathrm{Base}}_P$$
18	14 15 16 17	syl3anc	$$⊢\phi \to X\underset{\dot{}}{+}Y\in {\mathrm{Base}}_P$$
19		eqid	$$⊢{+}_R={+}_R$$
20	2 8 19 3 15 16	mpladd	$$⊢\phi \to X\underset{\dot{}}{+}Y=X{{+}_R}_{f}Y$$
21	20	oveq1d	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\mathrm{supp}{0}_R=\left(X{{+}_R}_{f}Y\right)\mathrm{supp}{0}_R$$
22		ovexd	$$⊢\phi \to {{\mathbb{N}}_0}^I\in \mathrm{V}$$
23	10 22	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}$$
24		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
25	24 9	grpidcl	$$⊢R\in \mathrm{Grp}\to 0_R\in {\mathrm{Base}}_R$$
26	4 25	syl	$$⊢\phi \to 0_R\in {\mathrm{Base}}_R$$
27	2 24 8 10 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$$
28	2 24 8 10 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$$
29	24 19 9	grplid	$$⊢\left(R\in \mathrm{Grp}\wedge 0_R\in {\mathrm{Base}}_R\right)\to 0_R{+}_R{0}_R=0_R$$
30	4 26 29	syl2anc	$$⊢\phi \to 0_R{+}_R{0}_R=0_R$$
31	23 26 27 28 30	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)$$
32	21 31	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)$$
33	1 9 10 12 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\}$$
34	1 9 10 12 4 5 7	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\}$$
35	33 34	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\}$$
36	32 35	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\}$$
37	1 2 8 9 10 12 4 5 18 36	ismhp2	$$⊢\phi \to X\underset{\dot{}}{+}Y\in H\left(N\right)$$