Metamath Proof Explorer

Theorem mulgnn0z

Description: A group multiple of the identity, for nonnegative multiple. (Contributed by Mario Carneiro, 13-Dec-2014)

Ref Expression
Hypotheses mulgnn0z.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgnn0z.t ⊢ · = ( .g ‘ 𝐺 )
mulgnn0z.o ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion mulgnn0z ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 · 0 ) = 0 )

Proof

Step Hyp Ref Expression
1 mulgnn0z.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgnn0z.t ⊢ · = ( .g ‘ 𝐺 )
3 mulgnn0z.o ⊢ 0 = ( 0g ‘ 𝐺 )
4 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
5 id ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ )
6 1 3 mndidcl ⊢ ( 𝐺 ∈ Mnd → 0 ∈ 𝐵 )
7 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
8 eqid ⊢ seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 0 } ) ) = seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 0 } ) )
9 1 7 2 8 mulgnn ⊢ ( ( 𝑁 ∈ ℕ ∧ 0 ∈ 𝐵 ) → ( 𝑁 · 0 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 0 } ) ) ‘ 𝑁 ) )
10 5 6 9 syl2anr ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 0 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 0 } ) ) ‘ 𝑁 ) )
11 1 7 3 mndlid ⊢ ( ( 𝐺 ∈ Mnd ∧ 0 ∈ 𝐵 ) → ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 )
12 6 11 mpdan ⊢ ( 𝐺 ∈ Mnd → ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 )
13 12 adantr ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ ) → ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 )
14 simpr ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
15 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
16 14 15 eleqtrdi ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
17 6 adantr ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ ) → 0 ∈ 𝐵 )
18 elfznn ⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → 𝑥 ∈ ℕ )
19 fvconst2g ⊢ ( ( 0 ∈ 𝐵 ∧ 𝑥 ∈ ℕ ) → ( ( ℕ × { 0 } ) ‘ 𝑥 ) = 0 )
20 17 18 19 syl2an ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( ( ℕ × { 0 } ) ‘ 𝑥 ) = 0 )
21 13 16 20 seqid3 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 0 } ) ) ‘ 𝑁 ) = 0 )
22 10 21 eqtrd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 0 ) = 0 )
23 oveq1 ⊢ ( 𝑁 = 0 → ( 𝑁 · 0 ) = ( 0 · 0 ) )
24 1 3 2 mulg0 ⊢ ( 0 ∈ 𝐵 → ( 0 · 0 ) = 0 )
25 6 24 syl ⊢ ( 𝐺 ∈ Mnd → ( 0 · 0 ) = 0 )
26 23 25 sylan9eqr ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 = 0 ) → ( 𝑁 · 0 ) = 0 )
27 22 26 jaodan ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ) → ( 𝑁 · 0 ) = 0 )
28 4 27 sylan2b ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 · 0 ) = 0 )