This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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