grpinvid2

Description: The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 24-Aug-2011)

	Ref	Expression
Hypotheses	grpinv.b	$⊢ B = {Base}_{G}$
	grpinv.p	$⊢ \underset{˙}{+} = +_{G}$
	grpinv.u	$⊢ \underset{˙}{0} = 0_{G}$
	grpinv.n	$⊢ N = {inv}_{g} (G)$
Assertion	grpinvid2	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (N (X) = Y \leftrightarrow Y \underset{˙}{+} X = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		grpinv.b	$⊢ B = {Base}_{G}$
2		grpinv.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpinv.u	$⊢ \underset{˙}{0} = 0_{G}$
4		grpinv.n	$⊢ N = {inv}_{g} (G)$
5		oveq1	$⊢ N (X) = Y \to N (X) \underset{˙}{+} X = Y \underset{˙}{+} X$
6	5	adantl	$⊢ ((G \in Grp \land X \in B \land Y \in B) \land N (X) = Y) \to N (X) \underset{˙}{+} X = Y \underset{˙}{+} X$
7	1 2 3 4	grplinv	$⊢ (G \in Grp \land X \in B) \to N (X) \underset{˙}{+} X = \underset{˙}{0}$
8	7	3adant3	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (X) \underset{˙}{+} X = \underset{˙}{0}$
9	8	adantr	$⊢ ((G \in Grp \land X \in B \land Y \in B) \land N (X) = Y) \to N (X) \underset{˙}{+} X = \underset{˙}{0}$
10	6 9	eqtr3d	$⊢ ((G \in Grp \land X \in B \land Y \in B) \land N (X) = Y) \to Y \underset{˙}{+} X = \underset{˙}{0}$
11	1 4	grpinvcl	$⊢ (G \in Grp \land X \in B) \to N (X) \in B$
12	1 2 3	grplid	$⊢ (G \in Grp \land N (X) \in B) \to \underset{˙}{0} \underset{˙}{+} N (X) = N (X)$
13	11 12	syldan	$⊢ (G \in Grp \land X \in B) \to \underset{˙}{0} \underset{˙}{+} N (X) = N (X)$
14	13	3adant3	$⊢ (G \in Grp \land X \in B \land Y \in B) \to \underset{˙}{0} \underset{˙}{+} N (X) = N (X)$
15	14	eqcomd	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (X) = \underset{˙}{0} \underset{˙}{+} N (X)$
16	15	adantr	$⊢ ((G \in Grp \land X \in B \land Y \in B) \land Y \underset{˙}{+} X = \underset{˙}{0}) \to N (X) = \underset{˙}{0} \underset{˙}{+} N (X)$
17		oveq1	$⊢ Y \underset{˙}{+} X = \underset{˙}{0} \to (Y \underset{˙}{+} X) \underset{˙}{+} N (X) = \underset{˙}{0} \underset{˙}{+} N (X)$
18	17	adantl	$⊢ ((G \in Grp \land X \in B \land Y \in B) \land Y \underset{˙}{+} X = \underset{˙}{0}) \to (Y \underset{˙}{+} X) \underset{˙}{+} N (X) = \underset{˙}{0} \underset{˙}{+} N (X)$
19		simprr	$⊢ (G \in Grp \land (X \in B \land Y \in B)) \to Y \in B$
20		simprl	$⊢ (G \in Grp \land (X \in B \land Y \in B)) \to X \in B$
21	11	adantrr	$⊢ (G \in Grp \land (X \in B \land Y \in B)) \to N (X) \in B$
22	19 20 21	3jca	$⊢ (G \in Grp \land (X \in B \land Y \in B)) \to (Y \in B \land X \in B \land N (X) \in B)$
23	1 2	grpass	$⊢ (G \in Grp \land (Y \in B \land X \in B \land N (X) \in B)) \to (Y \underset{˙}{+} X) \underset{˙}{+} N (X) = Y \underset{˙}{+} (X \underset{˙}{+} N (X))$
24	22 23	syldan	$⊢ (G \in Grp \land (X \in B \land Y \in B)) \to (Y \underset{˙}{+} X) \underset{˙}{+} N (X) = Y \underset{˙}{+} (X \underset{˙}{+} N (X))$
25	24	3impb	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (Y \underset{˙}{+} X) \underset{˙}{+} N (X) = Y \underset{˙}{+} (X \underset{˙}{+} N (X))$
26	1 2 3 4	grprinv	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{+} N (X) = \underset{˙}{0}$
27	26	oveq2d	$⊢ (G \in Grp \land X \in B) \to Y \underset{˙}{+} (X \underset{˙}{+} N (X)) = Y \underset{˙}{+} \underset{˙}{0}$
28	27	3adant3	$⊢ (G \in Grp \land X \in B \land Y \in B) \to Y \underset{˙}{+} (X \underset{˙}{+} N (X)) = Y \underset{˙}{+} \underset{˙}{0}$
29	1 2 3	grprid	$⊢ (G \in Grp \land Y \in B) \to Y \underset{˙}{+} \underset{˙}{0} = Y$
30	29	3adant2	$⊢ (G \in Grp \land X \in B \land Y \in B) \to Y \underset{˙}{+} \underset{˙}{0} = Y$
31	25 28 30	3eqtrd	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (Y \underset{˙}{+} X) \underset{˙}{+} N (X) = Y$
32	31	adantr	$⊢ ((G \in Grp \land X \in B \land Y \in B) \land Y \underset{˙}{+} X = \underset{˙}{0}) \to (Y \underset{˙}{+} X) \underset{˙}{+} N (X) = Y$
33	16 18 32	3eqtr2d	$⊢ ((G \in Grp \land X \in B \land Y \in B) \land Y \underset{˙}{+} X = \underset{˙}{0}) \to N (X) = Y$
34	10 33	impbida	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (N (X) = Y \leftrightarrow Y \underset{˙}{+} X = \underset{˙}{0})$

Metamath Proof Explorer

Theorem grpinvid2

Proof