grpinv11

Description: The group inverse is one-to-one. (Contributed by NM, 22-Mar-2015) (Proof shortened by SN, 8-Jul-2025)

Step	Hyp	Ref	Expression
1		grpinvinv.b	$⊢ B = {Base}_{G}$
2		grpinvinv.n	$⊢ N = {inv}_{g} (G)$
3		grpinv11.g	$⊢ φ \to G \in Grp$
4		grpinv11.x	$⊢ φ \to X \in B$
5		grpinv11.y	$⊢ φ \to Y \in B$
6		fveq2	$⊢ N (X) = N (Y) \to N (N (X)) = N (N (Y))$
7	1 2	grpinvinv	$⊢ (G \in Grp \land X \in B) \to N (N (X)) = X$
8	3 4 7	syl2anc	$⊢ φ \to N (N (X)) = X$
9	1 2	grpinvinv	$⊢ (G \in Grp \land Y \in B) \to N (N (Y)) = Y$
10	3 5 9	syl2anc	$⊢ φ \to N (N (Y)) = Y$
11	8 10	eqeq12d	$⊢ φ \to (N (N (X)) = N (N (Y)) \leftrightarrow X = Y)$
12	6 11	imbitrid	$⊢ φ \to (N (X) = N (Y) \to X = Y)$
13		fveq2	$⊢ X = Y \to N (X) = N (Y)$
14	12 13	impbid1	$⊢ φ \to (N (X) = N (Y) \leftrightarrow X = Y)$

Metamath Proof Explorer