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 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 → seq 1 + G F ⁡ N = seq 1 + G ℕ × X ⁡ N
18 eqid ⊢ + G = + G
19 elfvex ⊢ X ∈ Base G → 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 → ∑ G F = seq 1 + G F ⁡ N
25 eqid ⊢ seq 1 + G ℕ × X = seq 1 + G ℕ × X
26 1 18 2 25 mulgnn ⊢ N ∈ ℕ ∧ X ∈ B → N · ˙ X = seq 1 + G ℕ × X ⁡ N
27 17 24 26 3eqtr4rd ⊢ N ∈ ℕ ∧ X ∈ B → N · ˙ X = ∑ G F