Theorem mulgnn0gsum

Description: Group multiple (exponentiation) operation at a nonnegative integer expressed by a group sum. This corresponds to the definition in Lang p. 6, second formula. (Contributed by AV, 28-Dec-2023)

	Ref	Expression
Hypotheses	mulgnngsum.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	mulgnngsum.t	⊢ · = ( .g ‘ 𝐺 )
	mulgnngsum.f	⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ 𝑋 )
Assertion	mulgnn0gsum	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) = ( 𝐺 Σg 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		mulgnngsum.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mulgnngsum.t	⊢ · = ( .g ‘ 𝐺 )
3		mulgnngsum.f	⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ 𝑋 )
4		elnn0	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
5	1 2 3	mulgnngsum	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) = ( 𝐺 Σg 𝐹 ) )
6	5	ex	⊢ ( 𝑁 ∈ ℕ → ( 𝑋 ∈ 𝐵 → ( 𝑁 · 𝑋 ) = ( 𝐺 Σg 𝐹 ) ) )
7		oveq1	⊢ ( 𝑁 = 0 → ( 𝑁 · 𝑋 ) = ( 0 · 𝑋 ) )
8		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
9	1 8 2	mulg0	⊢ ( 𝑋 ∈ 𝐵 → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
10	7 9	sylan9eq	⊢ ( ( 𝑁 = 0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
11		oveq2	⊢ ( 𝑁 = 0 → ( 1 ... 𝑁 ) = ( 1 ... 0 ) )
12		fz10	⊢ ( 1 ... 0 ) = ∅
13	11 12	eqtrdi	⊢ ( 𝑁 = 0 → ( 1 ... 𝑁 ) = ∅ )
14		eqidd	⊢ ( 𝑁 = 0 → 𝑋 = 𝑋 )
15	13 14	mpteq12dv	⊢ ( 𝑁 = 0 → ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ 𝑋 ) = ( 𝑥 ∈ ∅ ↦ 𝑋 ) )
16		mpt0	⊢ ( 𝑥 ∈ ∅ ↦ 𝑋 ) = ∅
17	15 16	eqtrdi	⊢ ( 𝑁 = 0 → ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ 𝑋 ) = ∅ )
18	3 17	eqtrid	⊢ ( 𝑁 = 0 → 𝐹 = ∅ )
19	18	adantr	⊢ ( ( 𝑁 = 0 ∧ 𝑋 ∈ 𝐵 ) → 𝐹 = ∅ )
20	19	oveq2d	⊢ ( ( 𝑁 = 0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ∅ ) )
21	8	gsum0	⊢ ( 𝐺 Σg ∅ ) = ( 0g ‘ 𝐺 )
22	20 21	eqtrdi	⊢ ( ( 𝑁 = 0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐺 Σg 𝐹 ) = ( 0g ‘ 𝐺 ) )
23	10 22	eqtr4d	⊢ ( ( 𝑁 = 0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) = ( 𝐺 Σg 𝐹 ) )
24	23	ex	⊢ ( 𝑁 = 0 → ( 𝑋 ∈ 𝐵 → ( 𝑁 · 𝑋 ) = ( 𝐺 Σg 𝐹 ) ) )
25	6 24	jaoi	⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( 𝑋 ∈ 𝐵 → ( 𝑁 · 𝑋 ) = ( 𝐺 Σg 𝐹 ) ) )
26	4 25	sylbi	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑋 ∈ 𝐵 → ( 𝑁 · 𝑋 ) = ( 𝐺 Σg 𝐹 ) ) )
27	26	imp	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) = ( 𝐺 Σg 𝐹 ) )