Theorem grpinv11

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

	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	6	adantl	|- ( ( ph /\ ( N ` X ) = ( N ` Y ) ) -> ( N ` ( N ` X ) ) = ( N ` ( N ` Y ) ) )
8	1 2	grpinvinv	|- ( ( G e. Grp /\ X e. B ) -> ( N ` ( N ` X ) ) = X )
9	3 4 8	syl2anc	|- ( ph -> ( N ` ( N ` X ) ) = X )
10	9	adantr	|- ( ( ph /\ ( N ` X ) = ( N ` Y ) ) -> ( N ` ( N ` X ) ) = X )
11	1 2	grpinvinv	|- ( ( G e. Grp /\ Y e. B ) -> ( N ` ( N ` Y ) ) = Y )
12	3 5 11	syl2anc	|- ( ph -> ( N ` ( N ` Y ) ) = Y )
13	12	adantr	|- ( ( ph /\ ( N ` X ) = ( N ` Y ) ) -> ( N ` ( N ` Y ) ) = Y )
14	7 10 13	3eqtr3d	|- ( ( ph /\ ( N ` X ) = ( N ` Y ) ) -> X = Y )
15	14	ex	|- ( ph -> ( ( N ` X ) = ( N ` Y ) -> X = Y ) )
16		fveq2	|- ( X = Y -> ( N ` X ) = ( N ` Y ) )
17	15 16	impbid1	|- ( ph -> ( ( N ` X ) = ( N ` Y ) <-> X = Y ) )