Theorem grpoid

Description: Two ways of saying that an element of a group is the identity element. (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpoinveu.1	⊢ 𝑋 = ran 𝐺
	grpoinveu.2	⊢ 𝑈 = ( GId ‘ 𝐺 )
Assertion	grpoid	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 = 𝑈 ↔ ( 𝐴 𝐺 𝐴 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		grpoinveu.1	⊢ 𝑋 = ran 𝐺
2		grpoinveu.2	⊢ 𝑈 = ( GId ‘ 𝐺 )
3	1 2	grpoidcl	⊢ ( 𝐺 ∈ GrpOp → 𝑈 ∈ 𝑋 )
4	1	grporcan	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑈 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐴 ) = ( 𝑈 𝐺 𝐴 ) ↔ 𝐴 = 𝑈 ) )
5	4	3exp2	⊢ ( 𝐺 ∈ GrpOp → ( 𝐴 ∈ 𝑋 → ( 𝑈 ∈ 𝑋 → ( 𝐴 ∈ 𝑋 → ( ( 𝐴 𝐺 𝐴 ) = ( 𝑈 𝐺 𝐴 ) ↔ 𝐴 = 𝑈 ) ) ) ) )
6	3 5	mpid	⊢ ( 𝐺 ∈ GrpOp → ( 𝐴 ∈ 𝑋 → ( 𝐴 ∈ 𝑋 → ( ( 𝐴 𝐺 𝐴 ) = ( 𝑈 𝐺 𝐴 ) ↔ 𝐴 = 𝑈 ) ) ) )
7	6	pm2.43d	⊢ ( 𝐺 ∈ GrpOp → ( 𝐴 ∈ 𝑋 → ( ( 𝐴 𝐺 𝐴 ) = ( 𝑈 𝐺 𝐴 ) ↔ 𝐴 = 𝑈 ) ) )
8	7	imp	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐴 ) = ( 𝑈 𝐺 𝐴 ) ↔ 𝐴 = 𝑈 ) )
9	1 2	grpolid	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑈 𝐺 𝐴 ) = 𝐴 )
10	9	eqeq2d	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐴 ) = ( 𝑈 𝐺 𝐴 ) ↔ ( 𝐴 𝐺 𝐴 ) = 𝐴 ) )
11	8 10	bitr3d	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 = 𝑈 ↔ ( 𝐴 𝐺 𝐴 ) = 𝐴 ) )