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