This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐻 = ( 𝐼 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 ⊢ ( 𝜑 → 𝑋 ∈ 𝐺 )