Metamath Proof Explorer


Theorem grpoeqdivid

Description: Two group elements are equal iff their quotient is the identity. (Contributed by Jeff Madsen, 6-Jan-2011)

Ref Expression
Hypotheses grpeqdivid.1
|- X = ran G
grpeqdivid.2
|- U = ( GId ` G )
grpeqdivid.3
|- D = ( /g ` G )
Assertion grpoeqdivid
|- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A = B <-> ( A D B ) = U ) )

Proof

Step Hyp Ref Expression
1 grpeqdivid.1
 |-  X = ran G
2 grpeqdivid.2
 |-  U = ( GId ` G )
3 grpeqdivid.3
 |-  D = ( /g ` G )
4 1 3 2 grpodivid
 |-  ( ( G e. GrpOp /\ B e. X ) -> ( B D B ) = U )
5 4 3adant2
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( B D B ) = U )
6 oveq1
 |-  ( A = B -> ( A D B ) = ( B D B ) )
7 6 eqeq1d
 |-  ( A = B -> ( ( A D B ) = U <-> ( B D B ) = U ) )
8 5 7 syl5ibrcom
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A = B -> ( A D B ) = U ) )
9 oveq1
 |-  ( ( A D B ) = U -> ( ( A D B ) G B ) = ( U G B ) )
10 1 3 grponpcan
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( A D B ) G B ) = A )
11 1 2 grpolid
 |-  ( ( G e. GrpOp /\ B e. X ) -> ( U G B ) = B )
12 11 3adant2
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( U G B ) = B )
13 10 12 eqeq12d
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( ( A D B ) G B ) = ( U G B ) <-> A = B ) )
14 9 13 syl5ib
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( A D B ) = U -> A = B ) )
15 8 14 impbid
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A = B <-> ( A D B ) = U ) )