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

Metamath Proof Explorer

Theorem mhpind

Proof