Theorem 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	⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
	mhpind.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	mhpind.z	⊢ 0 = ( 0g ‘ 𝑅 )
	mhpind.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mhpind.a	⊢ + = ( +g ‘ 𝑃 )
	mhpind.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
	mhpind.s	⊢ 𝑆 = { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 }
	mhpind.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mhpind.r	⊢ ( 𝜑 → 𝑅 ∈ Grp )
	mhpind.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	mhpind.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) )
	mhpind.0	⊢ ( 𝜑 → ( 𝐷 × { 0 } ) ∈ 𝐺 )
	mhpind.1	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ 𝐺 )
	mhpind.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐺 )
Assertion	mhpind	⊢ ( 𝜑 → 𝑋 ∈ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		mhpind.h	⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
2		mhpind.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		mhpind.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		mhpind.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
5		mhpind.a	⊢ + = ( +g ‘ 𝑃 )
6		mhpind.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
7		mhpind.s	⊢ 𝑆 = { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 }
8		mhpind.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
9		mhpind.r	⊢ ( 𝜑 → 𝑅 ∈ Grp )
10		mhpind.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
11		mhpind.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) )
12		mhpind.0	⊢ ( 𝜑 → ( 𝐷 × { 0 } ) ∈ 𝐺 )
13		mhpind.1	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ 𝐺 )
14		mhpind.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐺 )
15		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
16		ovexd	⊢ ( 𝜑 → ( ℕ0 ↑m 𝐼 ) ∈ V )
17	6 16	rabexd	⊢ ( 𝜑 → 𝐷 ∈ V )
18		ssrab2	⊢ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ⊆ 𝐷
19	18	a1i	⊢ ( 𝜑 → { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ⊆ 𝐷 )
20	1 3 6 8 9 10	mhp0cl	⊢ ( 𝜑 → ( 𝐷 × { 0 } ) ∈ ( 𝐻 ‘ 𝑁 ) )
21	20 12	elind	⊢ ( 𝜑 → ( 𝐷 × { 0 } ) ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) )
22	7	eleq2i	⊢ ( 𝑎 ∈ 𝑆 ↔ 𝑎 ∈ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } )
23	22	biimpri	⊢ ( 𝑎 ∈ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } → 𝑎 ∈ 𝑆 )
24		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
25	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → 𝐼 ∈ 𝑉 )
26	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑅 ∈ Grp )
27	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑁 ∈ ℕ0 )
28		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑠 ∈ 𝐷 ) → 𝑏 ∈ 𝐵 )
29	2 3	grpidcl	⊢ ( 𝑅 ∈ Grp → 0 ∈ 𝐵 )
30	9 29	syl	⊢ ( 𝜑 → 0 ∈ 𝐵 )
31	30	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑠 ∈ 𝐷 ) → 0 ∈ 𝐵 )
32	28 31	ifcld	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑠 ∈ 𝐷 ) → if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ∈ 𝐵 )
33	32	fmpttd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) : 𝐷 ⟶ 𝐵 )
34	2	fvexi	⊢ 𝐵 ∈ V
35	34	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
36	35 17	elmapd	⊢ ( 𝜑 → ( ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( 𝐵 ↑m 𝐷 ) ↔ ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) : 𝐷 ⟶ 𝐵 ) )
37	36	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( 𝐵 ↑m 𝐷 ) ↔ ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) : 𝐷 ⟶ 𝐵 ) )
38	33 37	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( 𝐵 ↑m 𝐷 ) )
39		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
40		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
41	39 2 6 40 8	psrbas	⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 𝐵 ↑m 𝐷 ) )
42	41	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 𝐵 ↑m 𝐷 ) )
43	38 42	eleqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
44	3	fvexi	⊢ 0 ∈ V
45	44	a1i	⊢ ( 𝜑 → 0 ∈ V )
46		eqid	⊢ ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) = ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) )
47	17 45 46	sniffsupp	⊢ ( 𝜑 → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) finSupp 0 )
48	47	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) finSupp 0 )
49	4 39 40 3 24	mplelbas	⊢ ( ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( Base ‘ 𝑃 ) ↔ ( ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) finSupp 0 ) )
50	43 48 49	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( Base ‘ 𝑃 ) )
51		elneeldif	⊢ ( ( 𝑎 ∈ 𝑆 ∧ 𝑠 ∈ ( 𝐷 ∖ 𝑆 ) ) → 𝑎 ≠ 𝑠 )
52	51	necomd	⊢ ( ( 𝑎 ∈ 𝑆 ∧ 𝑠 ∈ ( 𝐷 ∖ 𝑆 ) ) → 𝑠 ≠ 𝑎 )
53	52	adantll	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑠 ∈ ( 𝐷 ∖ 𝑆 ) ) → 𝑠 ≠ 𝑎 )
54	53	adantlrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑠 ∈ ( 𝐷 ∖ 𝑆 ) ) → 𝑠 ≠ 𝑎 )
55	54	neneqd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑠 ∈ ( 𝐷 ∖ 𝑆 ) ) → ¬ 𝑠 = 𝑎 )
56	55	iffalsed	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑠 ∈ ( 𝐷 ∖ 𝑆 ) ) → if ( 𝑠 = 𝑎 , 𝑏 , 0 ) = 0 )
57	17	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → 𝐷 ∈ V )
58	56 57	suppss2	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) supp 0 ) ⊆ 𝑆 )
59	58 7	sseqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } )
60	1 4 24 3 6 25 26 27 50 59	ismhp2	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( 𝐻 ‘ 𝑁 ) )
61	60 13	elind	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) )
62	23 61	sylanr1	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) )
63	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → 𝐼 ∈ 𝑉 )
64	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → 𝑅 ∈ Grp )
65	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → 𝑁 ∈ ℕ0 )
66		elinel1	⊢ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) → 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) )
67	66	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) )
68	1 4 24 63 64 65 67	mhpmpl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑃 ) )
69		elinel1	⊢ ( 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) → 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) )
70	69	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) )
71	1 4 24 63 64 65 70	mhpmpl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑃 ) )
72	4 24 15 5 68 71	mpladd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) )
73	1 4 5 63 64 65 67 70	mhpaddcl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) )
74	73 14	elind	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) )
75	72 74	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) )
76	1 4 24 8 9 10 11	mhpmpl	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑃 ) )
77	4 2 24 6 76	mplelf	⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ 𝐵 )
78	4 24 3 76 9	mplelsfi	⊢ ( 𝜑 → 𝑋 finSupp 0 )
79	1 3 6 8 9 10 11	mhpdeg	⊢ ( 𝜑 → ( 𝑋 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } )
80	2 3 15 9 17 19 21 62 75 77 78 79	fsuppssind	⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) )
81	80	elin2d	⊢ ( 𝜑 → 𝑋 ∈ 𝐺 )