mulgneg2

Description: Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 13-Dec-2014)

	Ref	Expression
Hypotheses	mulgneg2.b	$⊢ B = {Base}_{G}$
	mulgneg2.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	mulgneg2.i	$⊢ I = {inv}_{g} (G)$
Assertion	mulgneg2	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to -N \underset{˙}{\cdot} X = N \underset{˙}{\cdot} I (X)$

Proof

Step	Hyp	Ref	Expression
1		mulgneg2.b	$⊢ B = {Base}_{G}$
2		mulgneg2.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mulgneg2.i	$⊢ I = {inv}_{g} (G)$
4		negeq	$⊢ x = 0 \to - x = - 0$
5		neg0	$⊢ - 0 = 0$
6	4 5	eqtrdi	$⊢ x = 0 \to - x = 0$
7	6	oveq1d	$⊢ x = 0 \to (- x) \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} X$
8		oveq1	$⊢ x = 0 \to x \underset{˙}{\cdot} I (X) = 0 \underset{˙}{\cdot} I (X)$
9	7 8	eqeq12d	$⊢ x = 0 \to ((- x) \underset{˙}{\cdot} X = x \underset{˙}{\cdot} I (X) \leftrightarrow 0 \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} I (X))$
10		negeq	$⊢ x = n \to - x = - n$
11	10	oveq1d	$⊢ x = n \to (- x) \underset{˙}{\cdot} X = (- n) \underset{˙}{\cdot} X$
12		oveq1	$⊢ x = n \to x \underset{˙}{\cdot} I (X) = n \underset{˙}{\cdot} I (X)$
13	11 12	eqeq12d	$⊢ x = n \to ((- x) \underset{˙}{\cdot} X = x \underset{˙}{\cdot} I (X) \leftrightarrow (- n) \underset{˙}{\cdot} X = n \underset{˙}{\cdot} I (X))$
14		negeq	$⊢ x = n + 1 \to - x = - (n + 1)$
15	14	oveq1d	$⊢ x = n + 1 \to (- x) \underset{˙}{\cdot} X = (- (n + 1)) \underset{˙}{\cdot} X$
16		oveq1	$⊢ x = n + 1 \to x \underset{˙}{\cdot} I (X) = (n + 1) \underset{˙}{\cdot} I (X)$
17	15 16	eqeq12d	$⊢ x = n + 1 \to ((- x) \underset{˙}{\cdot} X = x \underset{˙}{\cdot} I (X) \leftrightarrow (- (n + 1)) \underset{˙}{\cdot} X = (n + 1) \underset{˙}{\cdot} I (X))$
18		negeq	$⊢ x = - n \to - x = - (- n)$
19	18	oveq1d	$⊢ x = - n \to (- x) \underset{˙}{\cdot} X = (- (- n)) \underset{˙}{\cdot} X$
20		oveq1	$⊢ x = - n \to x \underset{˙}{\cdot} I (X) = (- n) \underset{˙}{\cdot} I (X)$
21	19 20	eqeq12d	$⊢ x = - n \to ((- x) \underset{˙}{\cdot} X = x \underset{˙}{\cdot} I (X) \leftrightarrow (- (- n)) \underset{˙}{\cdot} X = (- n) \underset{˙}{\cdot} I (X))$
22		negeq	$⊢ x = N \to - x = - N$
23	22	oveq1d	$⊢ x = N \to (- x) \underset{˙}{\cdot} X = -N \underset{˙}{\cdot} X$
24		oveq1	$⊢ x = N \to x \underset{˙}{\cdot} I (X) = N \underset{˙}{\cdot} I (X)$
25	23 24	eqeq12d	$⊢ x = N \to ((- x) \underset{˙}{\cdot} X = x \underset{˙}{\cdot} I (X) \leftrightarrow -N \underset{˙}{\cdot} X = N \underset{˙}{\cdot} I (X))$
26		eqid	$⊢ 0_{G} = 0_{G}$
27	1 26 2	mulg0	$⊢ X \in B \to 0 \underset{˙}{\cdot} X = 0_{G}$
28	27	adantl	$⊢ (G \in Grp \land X \in B) \to 0 \underset{˙}{\cdot} X = 0_{G}$
29	1 3	grpinvcl	$⊢ (G \in Grp \land X \in B) \to I (X) \in B$
30	1 26 2	mulg0	$⊢ I (X) \in B \to 0 \underset{˙}{\cdot} I (X) = 0_{G}$
31	29 30	syl	$⊢ (G \in Grp \land X \in B) \to 0 \underset{˙}{\cdot} I (X) = 0_{G}$
32	28 31	eqtr4d	$⊢ (G \in Grp \land X \in B) \to 0 \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} I (X)$
33		oveq1	$⊢ (- n) \underset{˙}{\cdot} X = n \underset{˙}{\cdot} I (X) \to ((- n) \underset{˙}{\cdot} X) +_{G} I (X) = (n \underset{˙}{\cdot} I (X)) +_{G} I (X)$
34		nn0cn	$⊢ n \in ℕ_{0} \to n \in ℂ$
35	34	adantl	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ_{0}) \to n \in ℂ$
36		ax-1cn	$⊢ 1 \in ℂ$
37		negdi	$⊢ (n \in ℂ \land 1 \in ℂ) \to - (n + 1) = - n + -1$
38	35 36 37	sylancl	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ_{0}) \to - (n + 1) = - n + -1$
39	38	oveq1d	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ_{0}) \to (- (n + 1)) \underset{˙}{\cdot} X = (- n + -1) \underset{˙}{\cdot} X$
40		simpll	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ_{0}) \to G \in Grp$
41		nn0negz	$⊢ n \in ℕ_{0} \to - n \in ℤ$
42	41	adantl	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ_{0}) \to - n \in ℤ$
43		1z	$⊢ 1 \in ℤ$
44		znegcl	$⊢ 1 \in ℤ \to - 1 \in ℤ$
45	43 44	mp1i	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ_{0}) \to - 1 \in ℤ$
46		simplr	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ_{0}) \to X \in B$
47		eqid	$⊢ +_{G} = +_{G}$
48	1 2 47	mulgdir	$⊢ (G \in Grp \land (- n \in ℤ \land - 1 \in ℤ \land X \in B)) \to (- n + -1) \underset{˙}{\cdot} X = ((- n) \underset{˙}{\cdot} X) +_{G} (-1 \underset{˙}{\cdot} X)$
49	40 42 45 46 48	syl13anc	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ_{0}) \to (- n + -1) \underset{˙}{\cdot} X = ((- n) \underset{˙}{\cdot} X) +_{G} (-1 \underset{˙}{\cdot} X)$
50	1 2 3	mulgm1	$⊢ (G \in Grp \land X \in B) \to -1 \underset{˙}{\cdot} X = I (X)$
51	50	adantr	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ_{0}) \to -1 \underset{˙}{\cdot} X = I (X)$
52	51	oveq2d	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ_{0}) \to ((- n) \underset{˙}{\cdot} X) +_{G} (-1 \underset{˙}{\cdot} X) = ((- n) \underset{˙}{\cdot} X) +_{G} I (X)$
53	39 49 52	3eqtrd	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ_{0}) \to (- (n + 1)) \underset{˙}{\cdot} X = ((- n) \underset{˙}{\cdot} X) +_{G} I (X)$
54		grpmnd	$⊢ G \in Grp \to G \in Mnd$
55	54	ad2antrr	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ_{0}) \to G \in Mnd$
56		simpr	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
57	29	adantr	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ_{0}) \to I (X) \in B$
58	1 2 47	mulgnn0p1	$⊢ (G \in Mnd \land n \in ℕ_{0} \land I (X) \in B) \to (n + 1) \underset{˙}{\cdot} I (X) = (n \underset{˙}{\cdot} I (X)) +_{G} I (X)$
59	55 56 57 58	syl3anc	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ_{0}) \to (n + 1) \underset{˙}{\cdot} I (X) = (n \underset{˙}{\cdot} I (X)) +_{G} I (X)$
60	53 59	eqeq12d	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ_{0}) \to ((- (n + 1)) \underset{˙}{\cdot} X = (n + 1) \underset{˙}{\cdot} I (X) \leftrightarrow ((- n) \underset{˙}{\cdot} X) +_{G} I (X) = (n \underset{˙}{\cdot} I (X)) +_{G} I (X))$
61	33 60	imbitrrid	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ_{0}) \to ((- n) \underset{˙}{\cdot} X = n \underset{˙}{\cdot} I (X) \to (- (n + 1)) \underset{˙}{\cdot} X = (n + 1) \underset{˙}{\cdot} I (X))$
62	61	ex	$⊢ (G \in Grp \land X \in B) \to (n \in ℕ_{0} \to ((- n) \underset{˙}{\cdot} X = n \underset{˙}{\cdot} I (X) \to (- (n + 1)) \underset{˙}{\cdot} X = (n + 1) \underset{˙}{\cdot} I (X)))$
63		fveq2	$⊢ (- n) \underset{˙}{\cdot} X = n \underset{˙}{\cdot} I (X) \to I ((- n) \underset{˙}{\cdot} X) = I (n \underset{˙}{\cdot} I (X))$
64		simpll	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ) \to G \in Grp$
65		nnnegz	$⊢ n \in ℕ \to - n \in ℤ$
66	65	adantl	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ) \to - n \in ℤ$
67		simplr	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ) \to X \in B$
68	1 2 3	mulgneg	$⊢ (G \in Grp \land - n \in ℤ \land X \in B) \to (- (- n)) \underset{˙}{\cdot} X = I ((- n) \underset{˙}{\cdot} X)$
69	64 66 67 68	syl3anc	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ) \to (- (- n)) \underset{˙}{\cdot} X = I ((- n) \underset{˙}{\cdot} X)$
70		id	$⊢ n \in ℕ \to n \in ℕ$
71	1 2 3	mulgnegnn	$⊢ (n \in ℕ \land I (X) \in B) \to (- n) \underset{˙}{\cdot} I (X) = I (n \underset{˙}{\cdot} I (X))$
72	70 29 71	syl2anr	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ) \to (- n) \underset{˙}{\cdot} I (X) = I (n \underset{˙}{\cdot} I (X))$
73	69 72	eqeq12d	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ) \to ((- (- n)) \underset{˙}{\cdot} X = (- n) \underset{˙}{\cdot} I (X) \leftrightarrow I ((- n) \underset{˙}{\cdot} X) = I (n \underset{˙}{\cdot} I (X)))$
74	63 73	imbitrrid	$⊢ ((G \in Grp \land X \in B) \land n \in ℕ) \to ((- n) \underset{˙}{\cdot} X = n \underset{˙}{\cdot} I (X) \to (- (- n)) \underset{˙}{\cdot} X = (- n) \underset{˙}{\cdot} I (X))$
75	74	ex	$⊢ (G \in Grp \land X \in B) \to (n \in ℕ \to ((- n) \underset{˙}{\cdot} X = n \underset{˙}{\cdot} I (X) \to (- (- n)) \underset{˙}{\cdot} X = (- n) \underset{˙}{\cdot} I (X)))$
76	9 13 17 21 25 32 62 75	zindd	$⊢ (G \in Grp \land X \in B) \to (N \in ℤ \to -N \underset{˙}{\cdot} X = N \underset{˙}{\cdot} I (X))$
77	76	3impia	$⊢ (G \in Grp \land X \in B \land N \in ℤ) \to -N \underset{˙}{\cdot} X = N \underset{˙}{\cdot} I (X)$
78	77	3com23	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to -N \underset{˙}{\cdot} X = N \underset{˙}{\cdot} I (X)$

Metamath Proof Explorer

Theorem mulgneg2

Proof