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 = ( Base ` G )
	grpinvinv.n	|- N = ( invg ` G )
	grpinv11.g	|- ( ph -> G e. Grp )
	grpinv11.x	|- ( ph -> X e. B )
	grpinv11.y	|- ( ph -> Y e. B )
Assertion	grpinv11	|- ( ph -> ( ( N ` X ) = ( N ` Y ) <-> X = Y ) )

Proof

Step	Hyp	Ref	Expression
1		grpinvinv.b	|- B = ( Base ` G )
2		grpinvinv.n	|- N = ( invg ` G )
3		grpinv11.g	|- ( ph -> G e. Grp )
4		grpinv11.x	|- ( ph -> X e. B )
5		grpinv11.y	|- ( ph -> Y e. B )
6		fveq2	|- ( ( N ` X ) = ( N ` Y ) -> ( N ` ( N ` X ) ) = ( N ` ( N ` Y ) ) )
7	1 2	grpinvinv	|- ( ( G e. Grp /\ X e. B ) -> ( N ` ( N ` X ) ) = X )
8	3 4 7	syl2anc	|- ( ph -> ( N ` ( N ` X ) ) = X )
9	1 2	grpinvinv	|- ( ( G e. Grp /\ Y e. B ) -> ( N ` ( N ` Y ) ) = Y )
10	3 5 9	syl2anc	|- ( ph -> ( N ` ( N ` Y ) ) = Y )
11	8 10	eqeq12d	|- ( ph -> ( ( N ` ( N ` X ) ) = ( N ` ( N ` Y ) ) <-> X = Y ) )
12	6 11	imbitrid	|- ( ph -> ( ( N ` X ) = ( N ` Y ) -> X = Y ) )
13		fveq2	|- ( X = Y -> ( N ` X ) = ( N ` Y ) )
14	12 13	impbid1	|- ( ph -> ( ( N ` X ) = ( N ` Y ) <-> X = Y ) )