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	$⊢ B = {Base}_{G}$
	mulgnncl.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	mulgneg.i	$⊢ I = {inv}_{g} (G)$
Assertion	mulgneg	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to -N \underset{˙}{\cdot} X = I (N \underset{˙}{\cdot} X)$

Proof

Step	Hyp	Ref	Expression
1		mulgnncl.b	$⊢ B = {Base}_{G}$
2		mulgnncl.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mulgneg.i	$⊢ I = {inv}_{g} (G)$
4		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
5		simpr	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land N \in ℕ) \to N \in ℕ$
6		simpl3	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land N \in ℕ) \to X \in B$
7	1 2 3	mulgnegnn	$⊢ (N \in ℕ \land X \in B) \to -N \underset{˙}{\cdot} X = I (N \underset{˙}{\cdot} X)$
8	5 6 7	syl2anc	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land N \in ℕ) \to -N \underset{˙}{\cdot} X = I (N \underset{˙}{\cdot} X)$
9		simpl1	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land N = 0) \to G \in Grp$
10		eqid	$⊢ 0_{G} = 0_{G}$
11	10 3	grpinvid	$⊢ G \in Grp \to I (0_{G}) = 0_{G}$
12	9 11	syl	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land N = 0) \to I (0_{G}) = 0_{G}$
13		simpr	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land N = 0) \to N = 0$
14	13	oveq1d	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land N = 0) \to N \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} X$
15		simpl3	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land N = 0) \to X \in B$
16	1 10 2	mulg0	$⊢ X \in B \to 0 \underset{˙}{\cdot} X = 0_{G}$
17	15 16	syl	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land N = 0) \to 0 \underset{˙}{\cdot} X = 0_{G}$
18	14 17	eqtrd	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land N = 0) \to N \underset{˙}{\cdot} X = 0_{G}$
19	18	fveq2d	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land N = 0) \to I (N \underset{˙}{\cdot} X) = I (0_{G})$
20	13	negeqd	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land N = 0) \to - N = - 0$
21		neg0	$⊢ - 0 = 0$
22	20 21	eqtrdi	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land N = 0) \to - N = 0$
23	22	oveq1d	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land N = 0) \to -N \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} X$
24	23 17	eqtrd	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land N = 0) \to -N \underset{˙}{\cdot} X = 0_{G}$
25	12 19 24	3eqtr4rd	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land N = 0) \to -N \underset{˙}{\cdot} X = I (N \underset{˙}{\cdot} X)$
26	8 25	jaodan	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land (N \in ℕ \lor N = 0)) \to -N \underset{˙}{\cdot} X = I (N \underset{˙}{\cdot} X)$
27	4 26	sylan2b	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land N \in ℕ_{0}) \to -N \underset{˙}{\cdot} X = I (N \underset{˙}{\cdot} X)$
28		simpl1	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to G \in Grp$
29		simprr	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to - N \in ℕ$
30	29	nnzd	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to - N \in ℤ$
31		simpl3	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to X \in B$
32	1 2	mulgcl	$⊢ (G \in Grp \land - N \in ℤ \land X \in B) \to -N \underset{˙}{\cdot} X \in B$
33	28 30 31 32	syl3anc	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to -N \underset{˙}{\cdot} X \in B$
34	1 3	grpinvinv	$⊢ (G \in Grp \land -N \underset{˙}{\cdot} X \in B) \to I (I (-N \underset{˙}{\cdot} X)) = -N \underset{˙}{\cdot} X$
35	28 33 34	syl2anc	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to I (I (-N \underset{˙}{\cdot} X)) = -N \underset{˙}{\cdot} X$
36	1 2 3	mulgnegnn	$⊢ (- N \in ℕ \land X \in B) \to (- -N) \underset{˙}{\cdot} X = I (-N \underset{˙}{\cdot} X)$
37	29 31 36	syl2anc	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to (- -N) \underset{˙}{\cdot} X = I (-N \underset{˙}{\cdot} X)$
38		simprl	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to N \in ℝ$
39	38	recnd	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to N \in ℂ$
40	39	negnegd	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to - -N = N$
41	40	oveq1d	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to (- -N) \underset{˙}{\cdot} X = N \underset{˙}{\cdot} X$
42	37 41	eqtr3d	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to I (-N \underset{˙}{\cdot} X) = N \underset{˙}{\cdot} X$
43	42	fveq2d	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to I (I (-N \underset{˙}{\cdot} X)) = I (N \underset{˙}{\cdot} X)$
44	35 43	eqtr3d	$⊢ ((G \in Grp \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to -N \underset{˙}{\cdot} X = I (N \underset{˙}{\cdot} X)$
45		simp2	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to N \in ℤ$
46		elznn0nn	$⊢ N \in ℤ \leftrightarrow (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ))$
47	45 46	sylib	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ))$
48	27 44 47	mpjaodan	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to -N \underset{˙}{\cdot} X = I (N \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem mulgneg

Proof