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	2	mplgrp	$$⊢\left(I\in V\wedge R\in \mathrm{Grp}\right)\to P\in \mathrm{Grp}$$
10	4 5 9	syl2anc	$$⊢\phi \to P\in \mathrm{Grp}$$
11		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
12	1 2 11 4 5 6 7	mhpmpl	$$⊢\phi \to X\in {\mathrm{Base}}_P$$
13	1 2 11 4 5 6 8	mhpmpl	$$⊢\phi \to Y\in {\mathrm{Base}}_P$$
14	11 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$$
15	10 12 13 14	syl3anc	$$⊢\phi \to X\underset{\dot{}}{+}Y\in {\mathrm{Base}}_P$$
16		eqid	$$⊢{+}_R={+}_R$$
17	2 11 16 3 12 13	mpladd	$$⊢\phi \to X\underset{\dot{}}{+}Y=X{{+}_R}_{f}Y$$
18	17	oveq1d	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\mathrm{supp}{0}_R=\left(X{{+}_R}_{f}Y\right)\mathrm{supp}{0}_R$$
19		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\}$$
20		ovexd	$$⊢\phi \to {{\mathbb{N}}_0}^I\in \mathrm{V}$$
21	19 20	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}$$
22		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
23		eqid	$$⊢0_R=0_R$$
24	22 23	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 22 11 19 12	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 22 11 19 13	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	22 16 23	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	21 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	18 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 23 19 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 _{j\in {\mathbb{N}}_0}g\left(j\right)=N\right\}$$
33	1 23 19 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 _{j\in {\mathbb{N}}_0}g\left(j\right)=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 _{j\in {\mathbb{N}}_0}g\left(j\right)=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 _{j\in {\mathbb{N}}_0}g\left(j\right)=N\right\}$$
36	1 2 11 23 19 4 5 6	ismhp	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\in H\left(N\right)\leftrightarrow \left(X\underset{\dot{}}{+}Y\in {\mathrm{Base}}_P\wedge \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 _{j\in {\mathbb{N}}_0}g\left(j\right)=N\right\}\right)\right)$$
37	15 35 36	mpbir2and	$$⊢\phi \to X\underset{\dot{}}{+}Y\in H\left(N\right)$$