Metamath Proof Explorer


Theorem mulgneg

Description: Group multiple (exponentiation) operation at a negative integer. (Contributed by Paul Chapman, 17-Apr-2009) (Revised by Mario Carneiro, 11-Dec-2014)

Ref Expression
Hypotheses mulgnncl.b 𝐵 = ( Base ‘ 𝐺 )
mulgnncl.t · = ( .g𝐺 )
mulgneg.i 𝐼 = ( invg𝐺 )
Assertion mulgneg ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) → ( - 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 mulgnncl.b 𝐵 = ( Base ‘ 𝐺 )
2 mulgnncl.t · = ( .g𝐺 )
3 mulgneg.i 𝐼 = ( invg𝐺 )
4 elnn0 ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
5 simpr ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
6 simpl3 ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ 𝑁 ∈ ℕ ) → 𝑋𝐵 )
7 1 2 3 mulgnegnn ( ( 𝑁 ∈ ℕ ∧ 𝑋𝐵 ) → ( - 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) )
8 5 6 7 syl2anc ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ 𝑁 ∈ ℕ ) → ( - 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) )
9 simpl1 ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ 𝑁 = 0 ) → 𝐺 ∈ Grp )
10 eqid ( 0g𝐺 ) = ( 0g𝐺 )
11 10 3 grpinvid ( 𝐺 ∈ Grp → ( 𝐼 ‘ ( 0g𝐺 ) ) = ( 0g𝐺 ) )
12 9 11 syl ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ 𝑁 = 0 ) → ( 𝐼 ‘ ( 0g𝐺 ) ) = ( 0g𝐺 ) )
13 simpr ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ 𝑁 = 0 ) → 𝑁 = 0 )
14 13 oveq1d ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ 𝑁 = 0 ) → ( 𝑁 · 𝑋 ) = ( 0 · 𝑋 ) )
15 simpl3 ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ 𝑁 = 0 ) → 𝑋𝐵 )
16 1 10 2 mulg0 ( 𝑋𝐵 → ( 0 · 𝑋 ) = ( 0g𝐺 ) )
17 15 16 syl ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ 𝑁 = 0 ) → ( 0 · 𝑋 ) = ( 0g𝐺 ) )
18 14 17 eqtrd ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ 𝑁 = 0 ) → ( 𝑁 · 𝑋 ) = ( 0g𝐺 ) )
19 18 fveq2d ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ 𝑁 = 0 ) → ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝐼 ‘ ( 0g𝐺 ) ) )
20 13 negeqd ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ 𝑁 = 0 ) → - 𝑁 = - 0 )
21 neg0 - 0 = 0
22 20 21 eqtrdi ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ 𝑁 = 0 ) → - 𝑁 = 0 )
23 22 oveq1d ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ 𝑁 = 0 ) → ( - 𝑁 · 𝑋 ) = ( 0 · 𝑋 ) )
24 23 17 eqtrd ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ 𝑁 = 0 ) → ( - 𝑁 · 𝑋 ) = ( 0g𝐺 ) )
25 12 19 24 3eqtr4rd ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ 𝑁 = 0 ) → ( - 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) )
26 8 25 jaodan ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ) → ( - 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) )
27 4 26 sylan2b ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ 𝑁 ∈ ℕ0 ) → ( - 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) )
28 simpl1 ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐺 ∈ Grp )
29 simprr ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑁 ∈ ℕ )
30 29 nnzd ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑁 ∈ ℤ )
31 simpl3 ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑋𝐵 )
32 1 2 mulgcl ( ( 𝐺 ∈ Grp ∧ - 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) → ( - 𝑁 · 𝑋 ) ∈ 𝐵 )
33 28 30 31 32 syl3anc ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( - 𝑁 · 𝑋 ) ∈ 𝐵 )
34 1 3 grpinvinv ( ( 𝐺 ∈ Grp ∧ ( - 𝑁 · 𝑋 ) ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝐼 ‘ ( - 𝑁 · 𝑋 ) ) ) = ( - 𝑁 · 𝑋 ) )
35 28 33 34 syl2anc ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐼 ‘ ( 𝐼 ‘ ( - 𝑁 · 𝑋 ) ) ) = ( - 𝑁 · 𝑋 ) )
36 1 2 3 mulgnegnn ( ( - 𝑁 ∈ ℕ ∧ 𝑋𝐵 ) → ( - - 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( - 𝑁 · 𝑋 ) ) )
37 29 31 36 syl2anc ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( - - 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( - 𝑁 · 𝑋 ) ) )
38 simprl ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑁 ∈ ℝ )
39 38 recnd ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑁 ∈ ℂ )
40 39 negnegd ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - - 𝑁 = 𝑁 )
41 40 oveq1d ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( - - 𝑁 · 𝑋 ) = ( 𝑁 · 𝑋 ) )
42 37 41 eqtr3d ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐼 ‘ ( - 𝑁 · 𝑋 ) ) = ( 𝑁 · 𝑋 ) )
43 42 fveq2d ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐼 ‘ ( 𝐼 ‘ ( - 𝑁 · 𝑋 ) ) ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) )
44 35 43 eqtr3d ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( - 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) )
45 simp2 ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) → 𝑁 ∈ ℤ )
46 elznn0nn ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
47 45 46 sylib ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) → ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
48 27 44 47 mpjaodan ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) → ( - 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) )