Metamath Proof Explorer

Theorem mulgnngsum

Description: Group multiple (exponentiation) operation at a positive integer expressed by a group sum. (Contributed by AV, 28-Dec-2023)

Ref Expression
Hypotheses mulgnngsum.b ⊢B=BaseG
mulgnngsum.t ⊢·˙=⋅G
mulgnngsum.f ⊢F=x∈1…N⟼X
Assertion mulgnngsum ⊢N∈ℕ∧X∈B→N·˙X=∑GF

Proof

Step Hyp Ref Expression
1 mulgnngsum.b ⊢B=BaseG
2 mulgnngsum.t ⊢·˙=⋅G
3 mulgnngsum.f ⊢F=x∈1…N⟼X
4 elnnuz ⊢N∈ℕ↔N∈ℤ≥1
5 4 biimpi ⊢N∈ℕ→N∈ℤ≥1
6 5 adantr ⊢N∈ℕ∧X∈B→N∈ℤ≥1
7 3 a1i ⊢N∈ℕ∧X∈B∧i∈1…N→F=x∈1…N⟼X
8 eqidd ⊢N∈ℕ∧X∈B∧i∈1…N∧x=i→X=X
9 simpr ⊢N∈ℕ∧X∈B∧i∈1…N→i∈1…N
10 simpr ⊢N∈ℕ∧X∈B→X∈B
11 10 adantr ⊢N∈ℕ∧X∈B∧i∈1…N→X∈B
12 7 8 9 11 fvmptd ⊢N∈ℕ∧X∈B∧i∈1…N→F⁡i=X
13 elfznn ⊢i∈1…N→i∈ℕ
14 fvconst2g ⊢X∈B∧i∈ℕ→ℕ×X⁡i=X
15 10 13 14 syl2an ⊢N∈ℕ∧X∈B∧i∈1…N→ℕ×X⁡i=X
16 12 15 eqtr4d ⊢N∈ℕ∧X∈B∧i∈1…N→F⁡i=ℕ×X⁡i
17 6 16 seqfveq ⊢N∈ℕ∧X∈B→seq1+GF⁡N=seq1+Gℕ×X⁡N
18 eqid ⊢+G=+G
19 elfvex ⊢X∈BaseG→G∈V
20 19 1 eleq2s ⊢X∈B→G∈V
21 20 adantl ⊢N∈ℕ∧X∈B→G∈V
22 10 adantr ⊢N∈ℕ∧X∈B∧x∈1…N→X∈B
23 22 3 fmptd ⊢N∈ℕ∧X∈B→F:1…N⟶B
24 1 18 21 6 23 gsumval2 ⊢N∈ℕ∧X∈B→∑GF=seq1+GF⁡N
25 eqid ⊢seq1+Gℕ×X=seq1+Gℕ×X
26 1 18 2 25 mulgnn ⊢N∈ℕ∧X∈B→N·˙X=seq1+Gℕ×X⁡N
27 17 24 26 3eqtr4rd ⊢N∈ℕ∧X∈B→N·˙X=∑GF