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

Metamath Proof Explorer

Theorem mhpind

Proof