Metamath Proof Explorer

Theorem grpolidinv

Description: A group has a left identity element, and every member has a left inverse. (Contributed by NM, 2-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypothesis grpfo.1 ⊢ X = ran ⁡ G
Assertion grpolidinv ⊢ G ∈ GrpOp → ∃ u ∈ X ∀ x ∈ X u G x = x ∧ ∃ y ∈ X y G x = u

Proof

Step Hyp Ref Expression
1 grpfo.1 ⊢ X = ran ⁡ G
2 1 isgrpo ⊢ G ∈ GrpOp → G ∈ GrpOp ↔ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z ∧ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ ∃ y ∈ X y G x = u
3 2 ibi ⊢ G ∈ GrpOp → G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z ∧ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ ∃ y ∈ X y G x = u
4 3 simp3d ⊢ G ∈ GrpOp → ∃ u ∈ X ∀ x ∈ X u G x = x ∧ ∃ y ∈ X y G x = u