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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgnngsum.t ⊢ · = ( .g ‘ 𝐺 )
mulgnngsum.f ⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ 𝑋 )
Assertion mulgnngsum ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) = ( 𝐺 Σg 𝐹 ) )

Proof

Step Hyp Ref Expression
1 mulgnngsum.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgnngsum.t ⊢ · = ( .g ‘ 𝐺 )
3 mulgnngsum.f ⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ 𝑋 )
4 elnnuz ⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
5 4 birani ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
6 3 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝐹 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ 𝑋 ) )
7 eqidd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑥 = 𝑖 ) → 𝑋 = 𝑋 )
8 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
9 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
10 9 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑋 ∈ 𝐵 )
11 6 7 8 10 fvmptd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑖 ) = 𝑋 )
12 elfznn ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → 𝑖 ∈ ℕ )
13 fvconst2g ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑖 ∈ ℕ ) → ( ( ℕ × { 𝑋 } ) ‘ 𝑖 ) = 𝑋 )
14 9 12 13 syl2an ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ℕ × { 𝑋 } ) ‘ 𝑖 ) = 𝑋 )
15 11 14 eqtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑖 ) = ( ( ℕ × { 𝑋 } ) ‘ 𝑖 ) )
16 5 15 seqfveq ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( seq 1 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑁 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
17 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
18 elfvex ⊢ ( 𝑋 ∈ ( Base ‘ 𝐺 ) → 𝐺 ∈ V )
19 18 1 eleq2s ⊢ ( 𝑋 ∈ 𝐵 → 𝐺 ∈ V )
20 19 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → 𝐺 ∈ V )
21 9 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → 𝑋 ∈ 𝐵 )
22 21 3 fmptd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → 𝐹 : ( 1 ... 𝑁 ) ⟶ 𝐵 )
23 1 17 20 5 22 gsumval2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑁 ) )
24 eqid ⊢ seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) )
25 1 17 2 24 mulgnn ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
26 16 23 25 3eqtr4rd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) = ( 𝐺 Σg 𝐹 ) )