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 𝐹 ) )