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 ∈ GrpOp ∧ A ∈ X ∧ B ∈ 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 ∈ GrpOp ∧ B ∈ X → B D B = U
5 4 3adant2 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ 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 ∈ GrpOp ∧ A ∈ X ∧ B ∈ 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 ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A D B G B = A
11 1 2 grpolid ⊢ G ∈ GrpOp ∧ B ∈ X → U G B = B
12 11 3adant2 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → U G B = B
13 10 12 eqeq12d ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A D B G B = U G B ↔ A = B
14 9 13 syl5ib ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A D B = U → A = B
15 8 14 impbid ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A = B ↔ A D B = U