Theorem mhpaddcl

Description: Homogeneous polynomials are closed under addition. (Contributed by SN, 26-Aug-2023)

	Ref	Expression
Hypotheses	mhpaddcl.h	$$⊢H=I\mathrm{mHomP}R$$
	mhpaddcl.p	$$⊢P=I\mathrm{mPoly}R$$
	mhpaddcl.a	$$⊢\underset{\dot{}}{+}={+}_P$$
	mhpaddcl.i	$$⊢\phi \to I\in V$$
	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.i	$$⊢\phi \to I\in V$$
5		mhpaddcl.r	$$⊢\phi \to R\in \mathrm{Grp}$$
6		mhpaddcl.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		mhpaddcl.x	$$⊢\phi \to X\in H\left(N\right)$$
8		mhpaddcl.y	$$⊢\phi \to Y\in H\left(N\right)$$
9		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
10		eqid	$$⊢0_R=0_R$$
11		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\}$$
12	2	mplgrp	$$⊢\left(I\in V\wedge R\in \mathrm{Grp}\right)\to P\in \mathrm{Grp}$$
13	4 5 12	syl2anc	$$⊢\phi \to P\in \mathrm{Grp}$$
14	1 2 9 4 5 6 7	mhpmpl	$$⊢\phi \to X\in {\mathrm{Base}}_P$$
15	1 2 9 4 5 6 8	mhpmpl	$$⊢\phi \to Y\in {\mathrm{Base}}_P$$
16	9 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$$
17	13 14 15 16	syl3anc	$$⊢\phi \to X\underset{\dot{}}{+}Y\in {\mathrm{Base}}_P$$
18		eqid	$$⊢{+}_R={+}_R$$
19	2 9 18 3 14 15	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	11 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 10	grpidcl	$$⊢R\in \mathrm{Grp}\to 0_R\in {\mathrm{Base}}_R$$
25	5 24	syl	$$⊢\phi \to 0_R\in {\mathrm{Base}}_R$$
26	2 23 9 11 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$$
27	2 23 9 11 15	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 10	grplid	$$⊢\left(R\in \mathrm{Grp}\wedge 0_R\in {\mathrm{Base}}_R\right)\to 0_R{+}_R{0}_R=0_R$$
29	5 25 28	syl2anc	$$⊢\phi \to 0_R{+}_R{0}_R=0_R$$
30	22 25 26 27 29	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)$$
31	20 30	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)$$
32	1 10 11 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\}$$
33	1 10 11 4 5 6 8	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\}$$
34	32 33	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\}$$
35	31 34	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\}$$
36	1 2 9 10 11 4 5 6 17 35	ismhp2	$$⊢\phi \to X\underset{\dot{}}{+}Y\in H\left(N\right)$$