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

Metamath Proof Explorer

Theorem mhphflem

Description: Lemma for mhphf . Add several multiples of L together, in a case where the total amount of multiplies is N . (Contributed by SN, 30-Jul-2024)

Ref Expression
Hypotheses mhphflem.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
mhphflem.h ⊢ 𝐻 = { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 }
mhphflem.k ⊢ 𝐵 = ( Base ‘ 𝐺 )
mhphflem.e ⊢ · = ( .g ‘ 𝐺 )
mhphflem.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
mhphflem.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
mhphflem.l ⊢ ( 𝜑 → 𝐿 ∈ 𝐵 )
mhphflem.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion mhphflem ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝐺 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝐿 ) ) ) = ( 𝑁 · 𝐿 ) )

Proof

Step Hyp Ref Expression
1 mhphflem.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
2 mhphflem.h ⊢ 𝐻 = { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 }
3 mhphflem.k ⊢ 𝐵 = ( Base ‘ 𝐺 )
4 mhphflem.e ⊢ · = ( .g ‘ 𝐺 )
5 mhphflem.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 mhphflem.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
7 mhphflem.l ⊢ ( 𝜑 → 𝐿 ∈ 𝐵 )
8 mhphflem.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
9 nn0subm ⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
10 eqid ⊢ ( ℂfld ↾s ℕ0 ) = ( ℂfld ↾s ℕ0 )
11 10 submbas ⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → ℕ0 = ( Base ‘ ( ℂfld ↾s ℕ0 ) ) )
12 9 11 ax-mp ⊢ ℕ0 = ( Base ‘ ( ℂfld ↾s ℕ0 ) )
13 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
14 10 13 subm0 ⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → 0 = ( 0g ‘ ( ℂfld ↾s ℕ0 ) ) )
15 9 14 ax-mp ⊢ 0 = ( 0g ‘ ( ℂfld ↾s ℕ0 ) )
16 cnring ⊢ ℂfld ∈ Ring
17 ringcmn ⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
18 16 17 ax-mp ⊢ ℂfld ∈ CMnd
19 10 submcmn ⊢ ( ( ℂfld ∈ CMnd ∧ ℕ0 ∈ ( SubMnd ‘ ℂfld ) ) → ( ℂfld ↾s ℕ0 ) ∈ CMnd )
20 18 9 19 mp2an ⊢ ( ℂfld ↾s ℕ0 ) ∈ CMnd
21 20 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ℂfld ↾s ℕ0 ) ∈ CMnd )
22 6 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝐺 ∈ Mnd )
23 5 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝐼 ∈ 𝑉 )
24 cnfldadd ⊢ + = ( +g ‘ ℂfld )
25 10 24 ressplusg ⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → + = ( +g ‘ ( ℂfld ↾s ℕ0 ) ) )
26 9 25 ax-mp ⊢ + = ( +g ‘ ( ℂfld ↾s ℕ0 ) )
27 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
28 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
29 10 submmnd ⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → ( ℂfld ↾s ℕ0 ) ∈ Mnd )
30 9 29 mp1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ℂfld ↾s ℕ0 ) ∈ Mnd )
31 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐺 ∈ Mnd )
32 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
33 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐿 ∈ 𝐵 )
34 3 4 31 32 33 mulgnn0cld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 · 𝐿 ) ∈ 𝐵 )
35 34 fmpttd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) : ℕ0 ⟶ 𝐵 )
36 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → 𝐺 ∈ Mnd )
37 simprl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → 𝑥 ∈ ℕ0 )
38 simprr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → 𝑦 ∈ ℕ0 )
39 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → 𝐿 ∈ 𝐵 )
40 3 4 27 mulgnn0dir ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ∧ 𝐿 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) · 𝐿 ) = ( ( 𝑥 · 𝐿 ) ( +g ‘ 𝐺 ) ( 𝑦 · 𝐿 ) ) )
41 36 37 38 39 40 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑥 + 𝑦 ) · 𝐿 ) = ( ( 𝑥 · 𝐿 ) ( +g ‘ 𝐺 ) ( 𝑦 · 𝐿 ) ) )
42 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) )
43 oveq1 ⊢ ( 𝑛 = ( 𝑥 + 𝑦 ) → ( 𝑛 · 𝐿 ) = ( ( 𝑥 + 𝑦 ) · 𝐿 ) )
44 nn0addcl ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 + 𝑦 ) ∈ ℕ0 )
45 44 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( 𝑥 + 𝑦 ) ∈ ℕ0 )
46 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑥 + 𝑦 ) · 𝐿 ) ∈ V )
47 42 43 45 46 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑥 + 𝑦 ) · 𝐿 ) )
48 oveq1 ⊢ ( 𝑛 = 𝑥 → ( 𝑛 · 𝐿 ) = ( 𝑥 · 𝐿 ) )
49 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( 𝑥 · 𝐿 ) ∈ V )
50 42 48 37 49 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑥 ) = ( 𝑥 · 𝐿 ) )
51 oveq1 ⊢ ( 𝑛 = 𝑦 → ( 𝑛 · 𝐿 ) = ( 𝑦 · 𝐿 ) )
52 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( 𝑦 · 𝐿 ) ∈ V )
53 42 51 38 52 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑦 ) = ( 𝑦 · 𝐿 ) )
54 50 53 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑦 ) ) = ( ( 𝑥 · 𝐿 ) ( +g ‘ 𝐺 ) ( 𝑦 · 𝐿 ) ) )
55 41 47 54 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ ( 𝑥 + 𝑦 ) ) = ( ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑦 ) ) )
56 oveq1 ⊢ ( 𝑛 = 0 → ( 𝑛 · 𝐿 ) = ( 0 · 𝐿 ) )
57 0nn0 ⊢ 0 ∈ ℕ0
58 57 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 0 ∈ ℕ0 )
59 ovexd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 0 · 𝐿 ) ∈ V )
60 42 56 58 59 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 0 ) = ( 0 · 𝐿 ) )
61 7 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝐿 ∈ 𝐵 )
62 3 28 4 mulg0 ⊢ ( 𝐿 ∈ 𝐵 → ( 0 · 𝐿 ) = ( 0g ‘ 𝐺 ) )
63 61 62 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 0 · 𝐿 ) = ( 0g ‘ 𝐺 ) )
64 60 63 eqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 0 ) = ( 0g ‘ 𝐺 ) )
65 12 3 26 27 15 28 30 22 35 55 64 ismhmd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ∈ ( ( ℂfld ↾s ℕ0 ) MndHom 𝐺 ) )
66 elrabi ⊢ ( 𝑎 ∈ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } → 𝑎 ∈ 𝐷 )
67 66 2 eleq2s ⊢ ( 𝑎 ∈ 𝐻 → 𝑎 ∈ 𝐷 )
68 67 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑎 ∈ 𝐷 )
69 1 psrbagf ⊢ ( 𝑎 ∈ 𝐷 → 𝑎 : 𝐼 ⟶ ℕ0 )
70 68 69 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑎 : 𝐼 ⟶ ℕ0 )
71 70 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑣 ∈ 𝐼 ) → ( 𝑎 ‘ 𝑣 ) ∈ ℕ0 )
72 70 feqmptd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑎 = ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) )
73 1 psrbagfsupp ⊢ ( 𝑎 ∈ 𝐷 → 𝑎 finSupp 0 )
74 68 73 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑎 finSupp 0 )
75 72 74 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) finSupp 0 )
76 oveq1 ⊢ ( 𝑛 = ( 𝑎 ‘ 𝑣 ) → ( 𝑛 · 𝐿 ) = ( ( 𝑎 ‘ 𝑣 ) · 𝐿 ) )
77 oveq1 ⊢ ( 𝑛 = ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) → ( 𝑛 · 𝐿 ) = ( ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) · 𝐿 ) )
78 12 15 21 22 23 65 71 75 76 77 gsummhm2 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝐺 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝐿 ) ) ) = ( ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) · 𝐿 ) )
79 72 oveq2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) = ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) )
80 oveq2 ⊢ ( 𝑔 = 𝑎 → ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) )
81 80 eqeq1d ⊢ ( 𝑔 = 𝑎 → ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 ↔ ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) = 𝑁 ) )
82 81 2 elrab2 ⊢ ( 𝑎 ∈ 𝐻 ↔ ( 𝑎 ∈ 𝐷 ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) = 𝑁 ) )
83 82 simprbi ⊢ ( 𝑎 ∈ 𝐻 → ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) = 𝑁 )
84 83 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) = 𝑁 )
85 79 84 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) = 𝑁 )
86 85 oveq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) · 𝐿 ) = ( 𝑁 · 𝐿 ) )
87 78 86 eqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝐺 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝐿 ) ) ) = ( 𝑁 · 𝐿 ) )