Metamath Proof Explorer

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 ⊢ X = ran ⁡ G
grpoinveu.2 ⊢ U = GId ⁡ G
Assertion grpoid ⊢ G ∈ GrpOp ∧ A ∈ X → A = U ↔ A G A = A

Proof

Step Hyp Ref Expression
1 grpoinveu.1 ⊢ X = ran ⁡ G
2 grpoinveu.2 ⊢ U = GId ⁡ G
3 1 2 grpoidcl ⊢ G ∈ GrpOp → U ∈ X
4 1 grporcan ⊢ G ∈ GrpOp ∧ A ∈ X ∧ U ∈ X ∧ A ∈ X → A G A = U G A ↔ A = U
5 4 3exp2 ⊢ G ∈ GrpOp → A ∈ X → U ∈ X → A ∈ X → A G A = U G A ↔ A = U
6 3 5 mpid ⊢ G ∈ GrpOp → A ∈ X → A ∈ X → A G A = U G A ↔ A = U
7 6 pm2.43d ⊢ G ∈ GrpOp → A ∈ X → A G A = U G A ↔ A = U
8 7 imp ⊢ G ∈ GrpOp ∧ A ∈ X → A G A = U G A ↔ A = U
9 1 2 grpolid ⊢ G ∈ GrpOp ∧ A ∈ X → U G A = A
10 9 eqeq2d ⊢ G ∈ GrpOp ∧ A ∈ X → A G A = U G A ↔ A G A = A
11 8 10 bitr3d ⊢ G ∈ GrpOp ∧ A ∈ X → A = U ↔ A G A = A