# Metamath Proof Explorer

## Theorem grpoidinv

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

Ref Expression
Hypothesis grpfo.1 ${⊢}{X}=\mathrm{ran}{G}$
Assertion grpoidinv ${⊢}{G}\in \mathrm{GrpOp}\to \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)$

### Proof

Step Hyp Ref Expression
1 grpfo.1 ${⊢}{X}=\mathrm{ran}{G}$
2 simpl ${⊢}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\to {u}{G}{z}={z}$
3 2 ralimi ${⊢}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\to \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{z}={z}$
4 oveq2 ${⊢}{z}={x}\to {u}{G}{z}={u}{G}{x}$
5 id ${⊢}{z}={x}\to {z}={x}$
6 4 5 eqeq12d ${⊢}{z}={x}\to \left({u}{G}{z}={z}↔{u}{G}{x}={x}\right)$
7 6 rspccva ${⊢}\left(\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{z}={z}\wedge {x}\in {X}\right)\to {u}{G}{x}={x}$
8 3 7 sylan ${⊢}\left(\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\wedge {x}\in {X}\right)\to {u}{G}{x}={x}$
9 8 adantll ${⊢}\left(\left({u}\in {X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)\wedge {x}\in {X}\right)\to {u}{G}{x}={x}$
10 9 adantll ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge \left({u}\in {X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)\right)\wedge {x}\in {X}\right)\to {u}{G}{x}={x}$
11 simpl ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({u}\in {X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)\right)\to {G}\in \mathrm{GrpOp}$
12 11 anim1i ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge \left({u}\in {X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)\right)\wedge {x}\in {X}\right)\to \left({G}\in \mathrm{GrpOp}\wedge {x}\in {X}\right)$
13 id ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {u}\in {X}\right)\to \left({G}\in \mathrm{GrpOp}\wedge {u}\in {X}\right)$
14 13 adantrr ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({u}\in {X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)\right)\to \left({G}\in \mathrm{GrpOp}\wedge {u}\in {X}\right)$
15 14 adantr ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge \left({u}\in {X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)\right)\wedge {x}\in {X}\right)\to \left({G}\in \mathrm{GrpOp}\wedge {u}\in {X}\right)$
16 3 adantl ${⊢}\left({u}\in {X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)\to \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{z}={z}$
17 16 ad2antlr ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge \left({u}\in {X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)\right)\wedge {x}\in {X}\right)\to \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{z}={z}$
18 simpr ${⊢}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\to \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}$
19 18 ralimi ${⊢}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\to \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}$
20 19 adantl ${⊢}\left({u}\in {X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)\to \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}$
21 20 ad2antlr ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge \left({u}\in {X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)\right)\wedge {x}\in {X}\right)\to \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}$
22 15 17 21 jca32 ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge \left({u}\in {X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)\right)\wedge {x}\in {X}\right)\to \left(\left({G}\in \mathrm{GrpOp}\wedge {u}\in {X}\right)\wedge \left(\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{z}={z}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)$
23 biid ${⊢}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{z}={z}↔\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{z}={z}$
24 biid ${⊢}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}↔\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}$
25 1 23 24 grpoidinvlem3 ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {u}\in {X}\right)\wedge \left(\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{z}={z}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)\wedge {x}\in {X}\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)$
26 22 25 sylancom ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge \left({u}\in {X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)\right)\wedge {x}\in {X}\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)$
27 1 grpoidinvlem4 ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {x}\in {X}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)\to {x}{G}{u}={u}{G}{x}$
28 12 26 27 syl2anc ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge \left({u}\in {X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)\right)\wedge {x}\in {X}\right)\to {x}{G}{u}={u}{G}{x}$
29 28 10 eqtrd ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge \left({u}\in {X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)\right)\wedge {x}\in {X}\right)\to {x}{G}{u}={x}$
30 10 29 26 jca31 ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge \left({u}\in {X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)\right)\wedge {x}\in {X}\right)\to \left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)$
31 30 ralrimiva ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({u}\in {X}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)\right)\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)$
32 1 grpolidinv ${⊢}{G}\in \mathrm{GrpOp}\to \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{z}={z}\wedge \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{z}={u}\right)$
33 31 32 reximddv ${⊢}{G}\in \mathrm{GrpOp}\to \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)$