grpinvid1

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	grpinvid1	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (N (X) = Y \leftrightarrow X \underset{˙}{+} Y = \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		oveq2	$⊢ N (X) = Y \to X \underset{˙}{+} N (X) = X \underset{˙}{+} Y$
6	5	adantl	$⊢ ((G \in Grp \land X \in B \land Y \in B) \land N (X) = Y) \to X \underset{˙}{+} N (X) = X \underset{˙}{+} Y$
7	1 2 3 4	grprinv	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{+} N (X) = \underset{˙}{0}$
8	7	3adant3	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} N (X) = \underset{˙}{0}$
9	8	adantr	$⊢ ((G \in Grp \land X \in B \land Y \in B) \land N (X) = Y) \to X \underset{˙}{+} N (X) = \underset{˙}{0}$
10	6 9	eqtr3d	$⊢ ((G \in Grp \land X \in B \land Y \in B) \land N (X) = Y) \to X \underset{˙}{+} Y = \underset{˙}{0}$
11		oveq2	$⊢ X \underset{˙}{+} Y = \underset{˙}{0} \to N (X) \underset{˙}{+} (X \underset{˙}{+} Y) = N (X) \underset{˙}{+} \underset{˙}{0}$
12	11	adantl	$⊢ ((G \in Grp \land X \in B \land Y \in B) \land X \underset{˙}{+} Y = \underset{˙}{0}) \to N (X) \underset{˙}{+} (X \underset{˙}{+} Y) = N (X) \underset{˙}{+} \underset{˙}{0}$
13	1 2 3 4	grplinv	$⊢ (G \in Grp \land X \in B) \to N (X) \underset{˙}{+} X = \underset{˙}{0}$
14	13	oveq1d	$⊢ (G \in Grp \land X \in B) \to (N (X) \underset{˙}{+} X) \underset{˙}{+} Y = \underset{˙}{0} \underset{˙}{+} Y$
15	14	3adant3	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (N (X) \underset{˙}{+} X) \underset{˙}{+} Y = \underset{˙}{0} \underset{˙}{+} Y$
16	1 4	grpinvcl	$⊢ (G \in Grp \land X \in B) \to N (X) \in B$
17	16	adantrr	$⊢ (G \in Grp \land (X \in B \land Y \in B)) \to N (X) \in B$
18		simprl	$⊢ (G \in Grp \land (X \in B \land Y \in B)) \to X \in B$
19		simprr	$⊢ (G \in Grp \land (X \in B \land Y \in B)) \to Y \in B$
20	17 18 19	3jca	$⊢ (G \in Grp \land (X \in B \land Y \in B)) \to (N (X) \in B \land X \in B \land Y \in B)$
21	1 2	grpass	$⊢ (G \in Grp \land (N (X) \in B \land X \in B \land Y \in B)) \to (N (X) \underset{˙}{+} X) \underset{˙}{+} Y = N (X) \underset{˙}{+} (X \underset{˙}{+} Y)$
22	20 21	syldan	$⊢ (G \in Grp \land (X \in B \land Y \in B)) \to (N (X) \underset{˙}{+} X) \underset{˙}{+} Y = N (X) \underset{˙}{+} (X \underset{˙}{+} Y)$
23	22	3impb	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (N (X) \underset{˙}{+} X) \underset{˙}{+} Y = N (X) \underset{˙}{+} (X \underset{˙}{+} Y)$
24	15 23	eqtr3d	$⊢ (G \in Grp \land X \in B \land Y \in B) \to \underset{˙}{0} \underset{˙}{+} Y = N (X) \underset{˙}{+} (X \underset{˙}{+} Y)$
25	1 2 3	grplid	$⊢ (G \in Grp \land Y \in B) \to \underset{˙}{0} \underset{˙}{+} Y = Y$
26	25	3adant2	$⊢ (G \in Grp \land X \in B \land Y \in B) \to \underset{˙}{0} \underset{˙}{+} Y = Y$
27	24 26	eqtr3d	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (X) \underset{˙}{+} (X \underset{˙}{+} Y) = Y$
28	27	adantr	$⊢ ((G \in Grp \land X \in B \land Y \in B) \land X \underset{˙}{+} Y = \underset{˙}{0}) \to N (X) \underset{˙}{+} (X \underset{˙}{+} Y) = Y$
29	1 2 3	grprid	$⊢ (G \in Grp \land N (X) \in B) \to N (X) \underset{˙}{+} \underset{˙}{0} = N (X)$
30	16 29	syldan	$⊢ (G \in Grp \land X \in B) \to N (X) \underset{˙}{+} \underset{˙}{0} = N (X)$
31	30	3adant3	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (X) \underset{˙}{+} \underset{˙}{0} = N (X)$
32	31	adantr	$⊢ ((G \in Grp \land X \in B \land Y \in B) \land X \underset{˙}{+} Y = \underset{˙}{0}) \to N (X) \underset{˙}{+} \underset{˙}{0} = N (X)$
33	12 28 32	3eqtr3rd	$⊢ ((G \in Grp \land X \in B \land Y \in B) \land X \underset{˙}{+} Y = \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 X \underset{˙}{+} Y = \underset{˙}{0})$

Metamath Proof Explorer

Theorem grpinvid1

Proof