Theorem grpinv11

Description: The group inverse is one-to-one. (Contributed by NM, 22-Mar-2015)

	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	6	adantl	$$⊢\left(\phi \wedge N\left(X\right)=N\left(Y\right)\right)\to N\left(N\left(X\right)\right)=N\left(N\left(Y\right)\right)$$
8	1 2	grpinvinv	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(N\left(X\right)\right)=X$$
9	3 4 8	syl2anc	$$⊢\phi \to N\left(N\left(X\right)\right)=X$$
10	9	adantr	$$⊢\left(\phi \wedge N\left(X\right)=N\left(Y\right)\right)\to N\left(N\left(X\right)\right)=X$$
11	1 2	grpinvinv	$$⊢\left(G\in \mathrm{Grp}\wedge Y\in B\right)\to N\left(N\left(Y\right)\right)=Y$$
12	3 5 11	syl2anc	$$⊢\phi \to N\left(N\left(Y\right)\right)=Y$$
13	12	adantr	$$⊢\left(\phi \wedge N\left(X\right)=N\left(Y\right)\right)\to N\left(N\left(Y\right)\right)=Y$$
14	7 10 13	3eqtr3d	$$⊢\left(\phi \wedge N\left(X\right)=N\left(Y\right)\right)\to X=Y$$
15	14	ex	$$⊢\phi \to \left(N\left(X\right)=N\left(Y\right)\to X=Y\right)$$
16		fveq2	$$⊢X=Y\to N\left(X\right)=N\left(Y\right)$$
17	15 16	impbid1	$$⊢\phi \to \left(N\left(X\right)=N\left(Y\right)\leftrightarrow X=Y\right)$$