mhpind

Description: The homogeneous polynomials of degree N are generated by the terms of degree N and addition. (Contributed by SN, 28-Jul-2024)

	Ref	Expression
Hypotheses	mhpind.h	$⊢ H = I mHomP R$
	mhpind.b	$⊢ B = {Base}_{R}$
	mhpind.z	$⊢ \underset{˙}{0} = 0_{R}$
	mhpind.p	$⊢ P = I mPoly R$
	mhpind.a	$⊢ \underset{˙}{+} = +_{P}$
	mhpind.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	mhpind.s	$⊢ S = \{g \in D \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}$
	mhpind.r	$⊢ φ \to R \in Grp$
	mhpind.x	$⊢ φ \to X \in H (N)$
	mhpind.0	$⊢ φ \to D \times \{\underset{˙}{0}\} \in G$
	mhpind.1	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in D ⟼ if (s = a, b, \underset{˙}{0})) \in G$
	mhpind.2	$⊢ (φ \land (x \in (H (N) \cap G) \land y \in (H (N) \cap G))) \to x \underset{˙}{+} y \in G$
Assertion	mhpind	$⊢ φ \to X \in G$

Proof

Step	Hyp	Ref	Expression
1		mhpind.h	$⊢ H = I mHomP R$
2		mhpind.b	$⊢ B = {Base}_{R}$
3		mhpind.z	$⊢ \underset{˙}{0} = 0_{R}$
4		mhpind.p	$⊢ P = I mPoly R$
5		mhpind.a	$⊢ \underset{˙}{+} = +_{P}$
6		mhpind.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
7		mhpind.s	$⊢ S = \{g \in D \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}$
8		mhpind.r	$⊢ φ \to R \in Grp$
9		mhpind.x	$⊢ φ \to X \in H (N)$
10		mhpind.0	$⊢ φ \to D \times \{\underset{˙}{0}\} \in G$
11		mhpind.1	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in D ⟼ if (s = a, b, \underset{˙}{0})) \in G$
12		mhpind.2	$⊢ (φ \land (x \in (H (N) \cap G) \land y \in (H (N) \cap G))) \to x \underset{˙}{+} y \in G$
13		eqid	$⊢ +_{R} = +_{R}$
14		ovexd	$⊢ φ \to {ℕ_{0}}^{I} \in V$
15	6 14	rabexd	$⊢ φ \to D \in V$
16		ssrab2	$⊢ \{g \in D \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \subseteq D$
17	16	a1i	$⊢ φ \to \{g \in D \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \subseteq D$
18		reldmmhp	$⊢ Rel dom mHomP$
19	18 1 9	elfvov1	$⊢ φ \to I \in V$
20	1 9	mhprcl	$⊢ φ \to N \in ℕ_{0}$
21	1 3 6 19 8 20	mhp0cl	$⊢ φ \to D \times \{\underset{˙}{0}\} \in H (N)$
22	21 10	elind	$⊢ φ \to D \times \{\underset{˙}{0}\} \in (H (N) \cap G)$
23	7	eleq2i	$⊢ a \in S \leftrightarrow a \in \{g \in D \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}$
24	23	biimpri	$⊢ a \in \{g \in D \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \to a \in S$
25		eqid	$⊢ {Base}_{P} = {Base}_{P}$
26	19	adantr	$⊢ (φ \land (a \in S \land b \in B)) \to I \in V$
27	8	adantr	$⊢ (φ \land (a \in S \land b \in B)) \to R \in Grp$
28	20	adantr	$⊢ (φ \land (a \in S \land b \in B)) \to N \in ℕ_{0}$
29		simplrr	$⊢ ((φ \land (a \in S \land b \in B)) \land s \in D) \to b \in B$
30	2 3	grpidcl	$⊢ R \in Grp \to \underset{˙}{0} \in B$
31	8 30	syl	$⊢ φ \to \underset{˙}{0} \in B$
32	31	ad2antrr	$⊢ ((φ \land (a \in S \land b \in B)) \land s \in D) \to \underset{˙}{0} \in B$
33	29 32	ifcld	$⊢ ((φ \land (a \in S \land b \in B)) \land s \in D) \to if (s = a, b, \underset{˙}{0}) \in B$
34	33	fmpttd	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in D ⟼ if (s = a, b, \underset{˙}{0})) : D ⟶ B$
35	2	fvexi	$⊢ B \in V$
36	35	a1i	$⊢ φ \to B \in V$
37	36 15	elmapd	$⊢ φ \to ((s \in D ⟼ if (s = a, b, \underset{˙}{0})) \in (B^{D}) \leftrightarrow (s \in D ⟼ if (s = a, b, \underset{˙}{0})) : D ⟶ B)$
38	37	adantr	$⊢ (φ \land (a \in S \land b \in B)) \to ((s \in D ⟼ if (s = a, b, \underset{˙}{0})) \in (B^{D}) \leftrightarrow (s \in D ⟼ if (s = a, b, \underset{˙}{0})) : D ⟶ B)$
39	34 38	mpbird	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in D ⟼ if (s = a, b, \underset{˙}{0})) \in (B^{D})$
40		eqid	$⊢ I mPwSer R = I mPwSer R$
41		eqid	$⊢ {Base}_{(I mPwSer R)} = {Base}_{(I mPwSer R)}$
42	40 2 6 41 19	psrbas	$⊢ φ \to {Base}_{(I mPwSer R)} = B^{D}$
43	42	adantr	$⊢ (φ \land (a \in S \land b \in B)) \to {Base}_{(I mPwSer R)} = B^{D}$
44	39 43	eleqtrrd	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in D ⟼ if (s = a, b, \underset{˙}{0})) \in {Base}_{(I mPwSer R)}$
45	3	fvexi	$⊢ \underset{˙}{0} \in V$
46	45	a1i	$⊢ φ \to \underset{˙}{0} \in V$
47		eqid	$⊢ (s \in D ⟼ if (s = a, b, \underset{˙}{0})) = (s \in D ⟼ if (s = a, b, \underset{˙}{0}))$
48	15 46 47	sniffsupp	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((s \in D ⟼ if (s = a, b, \underset{˙}{0})))$
49	48	adantr	$⊢ (φ \land (a \in S \land b \in B)) \to {finSupp}_{\underset{˙}{0}} ((s \in D ⟼ if (s = a, b, \underset{˙}{0})))$
50	4 40 41 3 25	mplelbas	$⊢ (s \in D ⟼ if (s = a, b, \underset{˙}{0})) \in {Base}_{P} \leftrightarrow ((s \in D ⟼ if (s = a, b, \underset{˙}{0})) \in {Base}_{(I mPwSer R)} \land {finSupp}_{\underset{˙}{0}} ((s \in D ⟼ if (s = a, b, \underset{˙}{0}))))$
51	44 49 50	sylanbrc	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in D ⟼ if (s = a, b, \underset{˙}{0})) \in {Base}_{P}$
52		elneeldif	$⊢ (a \in S \land s \in (D ∖ S)) \to a \neq s$
53	52	necomd	$⊢ (a \in S \land s \in (D ∖ S)) \to s \neq a$
54	53	adantll	$⊢ ((φ \land a \in S) \land s \in (D ∖ S)) \to s \neq a$
55	54	adantlrr	$⊢ ((φ \land (a \in S \land b \in B)) \land s \in (D ∖ S)) \to s \neq a$
56	55	neneqd	$⊢ ((φ \land (a \in S \land b \in B)) \land s \in (D ∖ S)) \to \neg s = a$
57	56	iffalsed	$⊢ ((φ \land (a \in S \land b \in B)) \land s \in (D ∖ S)) \to if (s = a, b, \underset{˙}{0}) = \underset{˙}{0}$
58	15	adantr	$⊢ (φ \land (a \in S \land b \in B)) \to D \in V$
59	57 58	suppss2	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in D ⟼ if (s = a, b, \underset{˙}{0})) supp \underset{˙}{0} \subseteq S$
60	59 7	sseqtrdi	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in D ⟼ if (s = a, b, \underset{˙}{0})) supp \underset{˙}{0} \subseteq \{g \in D \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}$
61	1 4 25 3 6 26 27 28 51 60	ismhp2	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in D ⟼ if (s = a, b, \underset{˙}{0})) \in H (N)$
62	61 11	elind	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in D ⟼ if (s = a, b, \underset{˙}{0})) \in (H (N) \cap G)$
63	24 62	sylanr1	$⊢ (φ \land (a \in \{g \in D \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\} \land b \in B)) \to (s \in D ⟼ if (s = a, b, \underset{˙}{0})) \in (H (N) \cap G)$
64		elinel1	$⊢ x \in (H (N) \cap G) \to x \in H (N)$
65	64	ad2antrl	$⊢ (φ \land (x \in (H (N) \cap G) \land y \in (H (N) \cap G))) \to x \in H (N)$
66	1 4 25 65	mhpmpl	$⊢ (φ \land (x \in (H (N) \cap G) \land y \in (H (N) \cap G))) \to x \in {Base}_{P}$
67		elinel1	$⊢ y \in (H (N) \cap G) \to y \in H (N)$
68	67	ad2antll	$⊢ (φ \land (x \in (H (N) \cap G) \land y \in (H (N) \cap G))) \to y \in H (N)$
69	1 4 25 68	mhpmpl	$⊢ (φ \land (x \in (H (N) \cap G) \land y \in (H (N) \cap G))) \to y \in {Base}_{P}$
70	4 25 13 5 66 69	mpladd	$⊢ (φ \land (x \in (H (N) \cap G) \land y \in (H (N) \cap G))) \to x \underset{˙}{+} y = x {+_{R}}_{f} y$
71	8	adantr	$⊢ (φ \land (x \in (H (N) \cap G) \land y \in (H (N) \cap G))) \to R \in Grp$
72	1 4 5 71 65 68	mhpaddcl	$⊢ (φ \land (x \in (H (N) \cap G) \land y \in (H (N) \cap G))) \to x \underset{˙}{+} y \in H (N)$
73	72 12	elind	$⊢ (φ \land (x \in (H (N) \cap G) \land y \in (H (N) \cap G))) \to x \underset{˙}{+} y \in (H (N) \cap G)$
74	70 73	eqeltrrd	$⊢ (φ \land (x \in (H (N) \cap G) \land y \in (H (N) \cap G))) \to x {+_{R}}_{f} y \in (H (N) \cap G)$
75	1 4 25 9	mhpmpl	$⊢ φ \to X \in {Base}_{P}$
76	4 2 25 6 75	mplelf	$⊢ φ \to X : D ⟶ B$
77	4 25 3 75 8	mplelsfi	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (X)$
78	1 3 6 9	mhpdeg	$⊢ φ \to X supp \underset{˙}{0} \subseteq \{g \in D \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}$
79	2 3 13 8 15 17 22 63 74 76 77 78	fsuppssind	$⊢ φ \to X \in (H (N) \cap G)$
80	79	elin2d	$⊢ φ \to X \in G$

Metamath Proof Explorer

Theorem mhpind

Proof