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 biimpi ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
6 5 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
7 3 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝐹 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ 𝑋 ) )
8 eqidd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑥 = 𝑖 ) → 𝑋 = 𝑋 )
9 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
10 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
11 10 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑋 ∈ 𝐵 )
12 7 8 9 11 fvmptd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑖 ) = 𝑋 )
13 elfznn ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → 𝑖 ∈ ℕ )
14 fvconst2g ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑖 ∈ ℕ ) → ( ( ℕ × { 𝑋 } ) ‘ 𝑖 ) = 𝑋 )
15 10 13 14 syl2an ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ℕ × { 𝑋 } ) ‘ 𝑖 ) = 𝑋 )
16 12 15 eqtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑖 ) = ( ( ℕ × { 𝑋 } ) ‘ 𝑖 ) )
17 6 16 seqfveq ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( seq 1 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑁 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
18 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
19 elfvex ⊢ ( 𝑋 ∈ ( Base ‘ 𝐺 ) → 𝐺 ∈ V )
20 19 1 eleq2s ⊢ ( 𝑋 ∈ 𝐵 → 𝐺 ∈ V )
21 20 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → 𝐺 ∈ V )
22 10 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → 𝑋 ∈ 𝐵 )
23 22 3 fmptd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → 𝐹 : ( 1 ... 𝑁 ) ⟶ 𝐵 )
24 1 18 21 6 23 gsumval2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑁 ) )
25 eqid ⊢ seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) )
26 1 18 2 25 mulgnn ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
27 17 24 26 3eqtr4rd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) = ( 𝐺 Σg 𝐹 ) )