This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrid 
 |-  ( ( 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 ) )