grpoinvid2

Description: The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 27-Oct-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpinv.1	$⊢ X = ran G$
	grpinv.2	$⊢ U = GId (G)$
	grpinv.3	$⊢ N = inv (G)$
Assertion	grpoinvid2	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (N (A) = B \leftrightarrow B G A = U)$

Proof

Step	Hyp	Ref	Expression
1		grpinv.1	$⊢ X = ran G$
2		grpinv.2	$⊢ U = GId (G)$
3		grpinv.3	$⊢ N = inv (G)$
4		oveq1	$⊢ N (A) = B \to N (A) G A = B G A$
5	4	adantl	$⊢ ((G \in GrpOp \land A \in X \land B \in X) \land N (A) = B) \to N (A) G A = B G A$
6	1 2 3	grpolinv	$⊢ (G \in GrpOp \land A \in X) \to N (A) G A = U$
7	6	3adant3	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to N (A) G A = U$
8	7	adantr	$⊢ ((G \in GrpOp \land A \in X \land B \in X) \land N (A) = B) \to N (A) G A = U$
9	5 8	eqtr3d	$⊢ ((G \in GrpOp \land A \in X \land B \in X) \land N (A) = B) \to B G A = U$
10	1 3	grpoinvcl	$⊢ (G \in GrpOp \land A \in X) \to N (A) \in X$
11	1 2	grpolid	$⊢ (G \in GrpOp \land N (A) \in X) \to U G N (A) = N (A)$
12	10 11	syldan	$⊢ (G \in GrpOp \land A \in X) \to U G N (A) = N (A)$
13	12	3adant3	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to U G N (A) = N (A)$
14	13	eqcomd	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to N (A) = U G N (A)$
15	14	adantr	$⊢ ((G \in GrpOp \land A \in X \land B \in X) \land B G A = U) \to N (A) = U G N (A)$
16		oveq1	$⊢ B G A = U \to (B G A) G N (A) = U G N (A)$
17	16	adantl	$⊢ ((G \in GrpOp \land A \in X \land B \in X) \land B G A = U) \to (B G A) G N (A) = U G N (A)$
18		simprr	$⊢ (G \in GrpOp \land (A \in X \land B \in X)) \to B \in X$
19		simprl	$⊢ (G \in GrpOp \land (A \in X \land B \in X)) \to A \in X$
20	10	adantrr	$⊢ (G \in GrpOp \land (A \in X \land B \in X)) \to N (A) \in X$
21	18 19 20	3jca	$⊢ (G \in GrpOp \land (A \in X \land B \in X)) \to (B \in X \land A \in X \land N (A) \in X)$
22	1	grpoass	$⊢ (G \in GrpOp \land (B \in X \land A \in X \land N (A) \in X)) \to (B G A) G N (A) = B G (A G N (A))$
23	21 22	syldan	$⊢ (G \in GrpOp \land (A \in X \land B \in X)) \to (B G A) G N (A) = B G (A G N (A))$
24	23	3impb	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (B G A) G N (A) = B G (A G N (A))$
25	1 2 3	grporinv	$⊢ (G \in GrpOp \land A \in X) \to A G N (A) = U$
26	25	oveq2d	$⊢ (G \in GrpOp \land A \in X) \to B G (A G N (A)) = B G U$
27	26	3adant3	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to B G (A G N (A)) = B G U$
28	1 2	grporid	$⊢ (G \in GrpOp \land B \in X) \to B G U = B$
29	28	3adant2	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to B G U = B$
30	24 27 29	3eqtrd	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (B G A) G N (A) = B$
31	30	adantr	$⊢ ((G \in GrpOp \land A \in X \land B \in X) \land B G A = U) \to (B G A) G N (A) = B$
32	15 17 31	3eqtr2d	$⊢ ((G \in GrpOp \land A \in X \land B \in X) \land B G A = U) \to N (A) = B$
33	9 32	impbida	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (N (A) = B \leftrightarrow B G A = U)$

Metamath Proof Explorer

Theorem grpoinvid2

Proof