# 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 𝑋 = ran 𝐺
grpeqdivid.2 𝑈 = ( GId ‘ 𝐺 )
grpeqdivid.3 𝐷 = ( /𝑔𝐺 )
Assertion grpoeqdivid ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 𝐷 𝐵 ) = 𝑈 ) )

### Proof

Step Hyp Ref Expression
1 grpeqdivid.1 𝑋 = ran 𝐺
2 grpeqdivid.2 𝑈 = ( GId ‘ 𝐺 )
3 grpeqdivid.3 𝐷 = ( /𝑔𝐺 )
4 1 3 2 grpodivid ( ( 𝐺 ∈ GrpOp ∧ 𝐵𝑋 ) → ( 𝐵 𝐷 𝐵 ) = 𝑈 )
5 4 3adant2 ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐵 𝐷 𝐵 ) = 𝑈 )
6 oveq1 ( 𝐴 = 𝐵 → ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐵 ) )
7 6 eqeq1d ( 𝐴 = 𝐵 → ( ( 𝐴 𝐷 𝐵 ) = 𝑈 ↔ ( 𝐵 𝐷 𝐵 ) = 𝑈 ) )
8 5 7 syl5ibrcom ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 = 𝐵 → ( 𝐴 𝐷 𝐵 ) = 𝑈 ) )
9 oveq1 ( ( 𝐴 𝐷 𝐵 ) = 𝑈 → ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐵 ) = ( 𝑈 𝐺 𝐵 ) )
10 1 3 grponpcan ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋𝐵𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐵 ) = 𝐴 )
11 1 2 grpolid ( ( 𝐺 ∈ GrpOp ∧ 𝐵𝑋 ) → ( 𝑈 𝐺 𝐵 ) = 𝐵 )
12 11 3adant2 ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝑈 𝐺 𝐵 ) = 𝐵 )
13 10 12 eqeq12d ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋𝐵𝑋 ) → ( ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐵 ) = ( 𝑈 𝐺 𝐵 ) ↔ 𝐴 = 𝐵 ) )
14 9 13 syl5ib ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋𝐵𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) = 𝑈𝐴 = 𝐵 ) )
15 8 14 impbid ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 𝐷 𝐵 ) = 𝑈 ) )