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 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) )