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