Metamath Proof Explorer

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 ⊢ H = I mHomP R
mhpind.b ⊢ B = Base R
mhpind.z ⊢ 0 ˙ = 0 R
mhpind.p ⊢ P = I mPoly R
mhpind.a ⊢ + ˙ = + P
mhpind.d ⊢ D = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
mhpind.s ⊢ S = g ∈ D | ∑ ℂ fld ↾ 𝑠 ℕ 0 g = N
mhpind.i ⊢ φ → I ∈ V
mhpind.r ⊢ φ → R ∈ Grp
mhpind.n ⊢ φ → N ∈ ℕ 0
mhpind.x ⊢ φ → X ∈ H ⁡ N
mhpind.0 ⊢ φ → D × 0 ˙ ∈ G
mhpind.1 ⊢ φ ∧ a ∈ S ∧ b ∈ B → s ∈ D ⟼ if s = a b 0 ˙ ∈ G
mhpind.2 ⊢ φ ∧ x ∈ H ⁡ N ∩ G ∧ y ∈ H ⁡ N ∩ G → x + ˙ y ∈ G
Assertion mhpind ⊢ φ → X ∈ G

Proof

Step Hyp Ref Expression
1 mhpind.h ⊢ H = I mHomP R
2 mhpind.b ⊢ B = Base R
3 mhpind.z ⊢ 0 ˙ = 0 R
4 mhpind.p ⊢ P = I mPoly R
5 mhpind.a ⊢ + ˙ = + P
6 mhpind.d ⊢ D = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
7 mhpind.s ⊢ S = g ∈ D | ∑ ℂ fld ↾ 𝑠 ℕ 0 g = N
8 mhpind.i ⊢ φ → I ∈ V
9 mhpind.r ⊢ φ → R ∈ Grp
10 mhpind.n ⊢ φ → N ∈ ℕ 0
11 mhpind.x ⊢ φ → X ∈ H ⁡ N
12 mhpind.0 ⊢ φ → D × 0 ˙ ∈ G
13 mhpind.1 ⊢ φ ∧ a ∈ S ∧ b ∈ B → s ∈ D ⟼ if s = a b 0 ˙ ∈ G
14 mhpind.2 ⊢ φ ∧ x ∈ H ⁡ N ∩ G ∧ y ∈ H ⁡ N ∩ G → x + ˙ y ∈ G
15 eqid ⊢ + R = + R
16 ovexd ⊢ φ → ℕ 0 I ∈ V
17 6 16 rabexd ⊢ φ → D ∈ V
18 ssrab2 ⊢ g ∈ D | ∑ ℂ fld ↾ 𝑠 ℕ 0 g = N ⊆ D
19 18 a1i ⊢ φ → g ∈ D | ∑ ℂ fld ↾ 𝑠 ℕ 0 g = N ⊆ D
20 1 3 6 8 9 10 mhp0cl ⊢ φ → D × 0 ˙ ∈ H ⁡ N
21 20 12 elind ⊢ φ → D × 0 ˙ ∈ H ⁡ N ∩ G
22 7 eleq2i ⊢ a ∈ S ↔ a ∈ g ∈ D | ∑ ℂ fld ↾ 𝑠 ℕ 0 g = N
23 22 biimpri ⊢ a ∈ g ∈ D | ∑ ℂ fld ↾ 𝑠 ℕ 0 g = N → a ∈ S
24 eqid ⊢ Base P = Base P
25 8 adantr ⊢ φ ∧ a ∈ S ∧ b ∈ B → I ∈ V
26 9 adantr ⊢ φ ∧ a ∈ S ∧ b ∈ B → R ∈ Grp
27 10 adantr ⊢ φ ∧ a ∈ S ∧ b ∈ B → N ∈ ℕ 0
28 simplrr ⊢ φ ∧ a ∈ S ∧ b ∈ B ∧ s ∈ D → b ∈ B
29 2 3 grpidcl ⊢ R ∈ Grp → 0 ˙ ∈ B
30 9 29 syl ⊢ φ → 0 ˙ ∈ B
31 30 ad2antrr ⊢ φ ∧ a ∈ S ∧ b ∈ B ∧ s ∈ D → 0 ˙ ∈ B
32 28 31 ifcld ⊢ φ ∧ a ∈ S ∧ b ∈ B ∧ s ∈ D → if s = a b 0 ˙ ∈ B
33 32 fmpttd ⊢ φ ∧ a ∈ S ∧ b ∈ B → s ∈ D ⟼ if s = a b 0 ˙ : D ⟶ B
34 2 fvexi ⊢ B ∈ V
35 34 a1i ⊢ φ → B ∈ V
36 35 17 elmapd ⊢ φ → s ∈ D ⟼ if s = a b 0 ˙ ∈ B D ↔ s ∈ D ⟼ if s = a b 0 ˙ : D ⟶ B
37 36 adantr ⊢ φ ∧ a ∈ S ∧ b ∈ B → s ∈ D ⟼ if s = a b 0 ˙ ∈ B D ↔ s ∈ D ⟼ if s = a b 0 ˙ : D ⟶ B
38 33 37 mpbird ⊢ φ ∧ a ∈ S ∧ b ∈ B → s ∈ D ⟼ if s = a b 0 ˙ ∈ 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 ⊢ φ → Base I mPwSer R = B D
42 41 adantr ⊢ φ ∧ a ∈ S ∧ b ∈ B → Base I mPwSer R = B D
43 38 42 eleqtrrd ⊢ φ ∧ a ∈ S ∧ b ∈ B → s ∈ D ⟼ if s = a b 0 ˙ ∈ Base I mPwSer R
44 3 fvexi ⊢ 0 ˙ ∈ V
45 44 a1i ⊢ φ → 0 ˙ ∈ V
46 eqid ⊢ s ∈ D ⟼ if s = a b 0 ˙ = s ∈ D ⟼ if s = a b 0 ˙
47 17 45 46 sniffsupp ⊢ φ → finSupp 0 ˙⁡ s ∈ D ⟼ if s = a b 0 ˙
48 47 adantr ⊢ φ ∧ a ∈ S ∧ b ∈ B → finSupp 0 ˙⁡ s ∈ D ⟼ if s = a b 0 ˙
49 4 39 40 3 24 mplelbas ⊢ s ∈ D ⟼ if s = a b 0 ˙ ∈ Base P ↔ s ∈ D ⟼ if s = a b 0 ˙ ∈ Base I mPwSer R ∧ finSupp 0 ˙⁡ s ∈ D ⟼ if s = a b 0 ˙
50 43 48 49 sylanbrc ⊢ φ ∧ a ∈ S ∧ b ∈ B → s ∈ D ⟼ if s = a b 0 ˙ ∈ Base P
51 elneeldif ⊢ a ∈ S ∧ s ∈ D ∖ S → a ≠ s
52 51 necomd ⊢ a ∈ S ∧ s ∈ D ∖ S → s ≠ a
53 52 adantll ⊢ φ ∧ a ∈ S ∧ s ∈ D ∖ S → s ≠ a
54 53 adantlrr ⊢ φ ∧ a ∈ S ∧ b ∈ B ∧ s ∈ D ∖ S → s ≠ a
55 54 neneqd ⊢ φ ∧ a ∈ S ∧ b ∈ B ∧ s ∈ D ∖ S → ¬ s = a
56 55 iffalsed ⊢ φ ∧ a ∈ S ∧ b ∈ B ∧ s ∈ D ∖ S → if s = a b 0 ˙ = 0 ˙
57 17 adantr ⊢ φ ∧ a ∈ S ∧ b ∈ B → D ∈ V
58 56 57 suppss2 ⊢ φ ∧ a ∈ S ∧ b ∈ B → s ∈ D ⟼ if s = a b 0 ˙ supp 0 ˙ ⊆ S
59 58 7 sseqtrdi ⊢ φ ∧ a ∈ S ∧ b ∈ B → s ∈ D ⟼ if s = a b 0 ˙ supp 0 ˙ ⊆ g ∈ D | ∑ ℂ fld ↾ 𝑠 ℕ 0 g = N
60 1 4 24 3 6 25 26 27 50 59 ismhp2 ⊢ φ ∧ a ∈ S ∧ b ∈ B → s ∈ D ⟼ if s = a b 0 ˙ ∈ H ⁡ N
61 60 13 elind ⊢ φ ∧ a ∈ S ∧ b ∈ B → s ∈ D ⟼ if s = a b 0 ˙ ∈ H ⁡ N ∩ G
62 23 61 sylanr1 ⊢ φ ∧ a ∈ g ∈ D | ∑ ℂ fld ↾ 𝑠 ℕ 0 g = N ∧ b ∈ B → s ∈ D ⟼ if s = a b 0 ˙ ∈ H ⁡ N ∩ G
63 8 adantr ⊢ φ ∧ x ∈ H ⁡ N ∩ G ∧ y ∈ H ⁡ N ∩ G → I ∈ V
64 9 adantr ⊢ φ ∧ x ∈ H ⁡ N ∩ G ∧ y ∈ H ⁡ N ∩ G → R ∈ Grp
65 10 adantr ⊢ φ ∧ x ∈ H ⁡ N ∩ G ∧ y ∈ H ⁡ N ∩ G → N ∈ ℕ 0
66 elinel1 ⊢ x ∈ H ⁡ N ∩ G → x ∈ H ⁡ N
67 66 ad2antrl ⊢ φ ∧ x ∈ H ⁡ N ∩ G ∧ y ∈ H ⁡ N ∩ G → x ∈ H ⁡ N
68 1 4 24 63 64 65 67 mhpmpl ⊢ φ ∧ x ∈ H ⁡ N ∩ G ∧ y ∈ H ⁡ N ∩ G → x ∈ Base P
69 elinel1 ⊢ y ∈ H ⁡ N ∩ G → y ∈ H ⁡ N
70 69 ad2antll ⊢ φ ∧ x ∈ H ⁡ N ∩ G ∧ y ∈ H ⁡ N ∩ G → y ∈ H ⁡ N
71 1 4 24 63 64 65 70 mhpmpl ⊢ φ ∧ x ∈ H ⁡ N ∩ G ∧ y ∈ H ⁡ N ∩ G → y ∈ Base P
72 4 24 15 5 68 71 mpladd ⊢ φ ∧ x ∈ H ⁡ N ∩ G ∧ y ∈ H ⁡ N ∩ G → x + ˙ y = x + R f y
73 1 4 5 63 64 65 67 70 mhpaddcl ⊢ φ ∧ x ∈ H ⁡ N ∩ G ∧ y ∈ H ⁡ N ∩ G → x + ˙ y ∈ H ⁡ N
74 73 14 elind ⊢ φ ∧ x ∈ H ⁡ N ∩ G ∧ y ∈ H ⁡ N ∩ G → x + ˙ y ∈ H ⁡ N ∩ G
75 72 74 eqeltrrd ⊢ φ ∧ x ∈ H ⁡ N ∩ G ∧ y ∈ H ⁡ N ∩ G → x + R f y ∈ H ⁡ N ∩ G
76 1 4 24 8 9 10 11 mhpmpl ⊢ φ → X ∈ Base P
77 4 2 24 6 76 mplelf ⊢ φ → X : D ⟶ B
78 4 24 3 76 9 mplelsfi ⊢ φ → finSupp 0 ˙⁡ X
79 1 3 6 8 9 10 11 mhpdeg ⊢ φ → X supp 0 ˙ ⊆ g ∈ D | ∑ ℂ fld ↾ 𝑠 ℕ 0 g = N
80 2 3 15 9 17 19 21 62 75 77 78 79 fsuppssind ⊢ φ → X ∈ H ⁡ N ∩ G
81 80 elin2d ⊢ φ → X ∈ G