Metamath Proof Explorer

Theorem mulgz

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

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

Proof

Step Hyp Ref Expression
1 mulgnn0z.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgnn0z.t ⊢ · = ( .g ‘ 𝐺 )
3 mulgnn0z.o ⊢ 0 = ( 0g ‘ 𝐺 )
4 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
5 4 adantr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) → 𝐺 ∈ Mnd )
6 1 2 3 mulgnn0z ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 · 0 ) = 0 )
7 5 6 sylan ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 · 0 ) = 0 )
8 simpll ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ0 ) → 𝐺 ∈ Grp )
9 nn0z ⊢ ( - 𝑁 ∈ ℕ0 → - 𝑁 ∈ ℤ )
10 9 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ0 ) → - 𝑁 ∈ ℤ )
11 1 3 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝐵 )
12 11 ad2antrr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ0 ) → 0 ∈ 𝐵 )
13 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
14 1 2 13 mulgneg ⊢ ( ( 𝐺 ∈ Grp ∧ - 𝑁 ∈ ℤ ∧ 0 ∈ 𝐵 ) → ( - - 𝑁 · 0 ) = ( ( invg ‘ 𝐺 ) ‘ ( - 𝑁 · 0 ) ) )
15 8 10 12 14 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ0 ) → ( - - 𝑁 · 0 ) = ( ( invg ‘ 𝐺 ) ‘ ( - 𝑁 · 0 ) ) )
16 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
17 16 ad2antlr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
18 17 negnegd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ0 ) → - - 𝑁 = 𝑁 )
19 18 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ0 ) → ( - - 𝑁 · 0 ) = ( 𝑁 · 0 ) )
20 1 2 3 mulgnn0z ⊢ ( ( 𝐺 ∈ Mnd ∧ - 𝑁 ∈ ℕ0 ) → ( - 𝑁 · 0 ) = 0 )
21 5 20 sylan ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ0 ) → ( - 𝑁 · 0 ) = 0 )
22 21 fveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ0 ) → ( ( invg ‘ 𝐺 ) ‘ ( - 𝑁 · 0 ) ) = ( ( invg ‘ 𝐺 ) ‘ 0 ) )
23 3 13 grpinvid ⊢ ( 𝐺 ∈ Grp → ( ( invg ‘ 𝐺 ) ‘ 0 ) = 0 )
24 23 ad2antrr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ0 ) → ( ( invg ‘ 𝐺 ) ‘ 0 ) = 0 )
25 22 24 eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ0 ) → ( ( invg ‘ 𝐺 ) ‘ ( - 𝑁 · 0 ) ) = 0 )
26 15 19 25 3eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ0 ) → ( 𝑁 · 0 ) = 0 )
27 elznn0 ⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) ) )
28 27 simprbi ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) )
29 28 adantl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) )
30 7 26 29 mpjaodan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) → ( 𝑁 · 0 ) = 0 )