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