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 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 𝐷 𝐵 ) = 𝑈 ) )