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 = Base G
mulgnngsum.t ⊢ · ˙ = ⋅ G
mulgnngsum.f ⊢ F = x ∈ 1 … N ⟼ X
Assertion mulgnngsum ⊢ N ∈ ℕ ∧ X ∈ B → N · ˙ X = ∑ G F

Proof

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