# 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}=\mathrm{ran}{G}$
Assertion grpolidinv ${⊢}{G}\in \mathrm{GrpOp}\to \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)$

### Proof

Step Hyp Ref Expression
1 grpfo.1 ${⊢}{X}=\mathrm{ran}{G}$
2 1 isgrpo ${⊢}{G}\in \mathrm{GrpOp}\to \left({G}\in \mathrm{GrpOp}↔\left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\right)$
3 2 ibi ${⊢}{G}\in \mathrm{GrpOp}\to \left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)$
4 3 simp3d ${⊢}{G}\in \mathrm{GrpOp}\to \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)$