Theorem grpinv11

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

	Ref	Expression
Hypotheses	grpinvinv.b	$$⊢B={\mathrm{Base}}_G$$
	grpinvinv.n	$$⊢N={inv}_g\left(G\right)$$
	grpinv11.g	$$⊢\phi \to G\in \mathrm{Grp}$$
	grpinv11.x	$$⊢\phi \to X\in B$$
	grpinv11.y	$$⊢\phi \to Y\in B$$
Assertion	grpinv11	$$⊢\phi \to \left(N\left(X\right)=N\left(Y\right)\leftrightarrow X=Y\right)$$

Proof

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