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 ⊢ 𝑋 = 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 imbitrid ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) = 𝑈 → 𝐴 = 𝐵 ) )
15 8 14 impbid ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 𝐷 𝐵 ) = 𝑈 ) )