# Metamath Proof Explorer

## Theorem grpomndo

Description: A group is a monoid. (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion grpomndo ${⊢}{G}\in \mathrm{GrpOp}\to {G}\in \mathrm{MndOp}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{ran}{G}=\mathrm{ran}{G}$
2 1 isgrpo ${⊢}{G}\in \mathrm{GrpOp}\to \left({G}\in \mathrm{GrpOp}↔\left({G}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {w}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({w}{G}{x}={x}\wedge \exists {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={w}\right)\right)\right)$
3 2 biimpd ${⊢}{G}\in \mathrm{GrpOp}\to \left({G}\in \mathrm{GrpOp}\to \left({G}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {w}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({w}{G}{x}={x}\wedge \exists {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={w}\right)\right)\right)$
4 1 grpoidinv ${⊢}{G}\in \mathrm{GrpOp}\to \exists {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left(\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\wedge \exists {w}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({w}{G}{y}={x}\wedge {y}{G}{w}={x}\right)\right)$
5 simpl ${⊢}\left(\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\wedge \exists {w}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({w}{G}{y}={x}\wedge {y}{G}{w}={x}\right)\right)\to \left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)$
6 5 ralimi ${⊢}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left(\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\wedge \exists {w}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({w}{G}{y}={x}\wedge {y}{G}{w}={x}\right)\right)\to \forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)$
7 6 reximi ${⊢}\exists {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left(\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\wedge \exists {w}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({w}{G}{y}={x}\wedge {y}{G}{w}={x}\right)\right)\to \exists {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)$
8 1 ismndo2 ${⊢}{G}\in \mathrm{GrpOp}\to \left({G}\in \mathrm{MndOp}↔\left({G}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)$
9 8 biimprcd ${⊢}\left({G}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\to \left({G}\in \mathrm{GrpOp}\to {G}\in \mathrm{MndOp}\right)$
10 9 3exp ${⊢}{G}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\to \left(\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\to \left(\exists {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\to \left({G}\in \mathrm{GrpOp}\to {G}\in \mathrm{MndOp}\right)\right)\right)$
11 10 impcom ${⊢}\left(\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge {G}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\right)\to \left(\exists {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\to \left({G}\in \mathrm{GrpOp}\to {G}\in \mathrm{MndOp}\right)\right)$
12 11 com3l ${⊢}\exists {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\to \left({G}\in \mathrm{GrpOp}\to \left(\left(\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge {G}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\right)\to {G}\in \mathrm{MndOp}\right)\right)$
13 7 12 syl ${⊢}\exists {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left(\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\wedge \exists {w}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({w}{G}{y}={x}\wedge {y}{G}{w}={x}\right)\right)\to \left({G}\in \mathrm{GrpOp}\to \left(\left(\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge {G}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\right)\to {G}\in \mathrm{MndOp}\right)\right)$
14 4 13 mpcom ${⊢}{G}\in \mathrm{GrpOp}\to \left(\left(\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge {G}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\right)\to {G}\in \mathrm{MndOp}\right)$
15 14 expdcom ${⊢}\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\to \left({G}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\to \left({G}\in \mathrm{GrpOp}\to {G}\in \mathrm{MndOp}\right)\right)$
16 15 a1i ${⊢}\exists {w}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({w}{G}{x}={x}\wedge \exists {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={w}\right)\to \left(\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\to \left({G}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\to \left({G}\in \mathrm{GrpOp}\to {G}\in \mathrm{MndOp}\right)\right)\right)$
17 16 com13 ${⊢}{G}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\to \left(\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\to \left(\exists {w}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({w}{G}{x}={x}\wedge \exists {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={w}\right)\to \left({G}\in \mathrm{GrpOp}\to {G}\in \mathrm{MndOp}\right)\right)\right)$
18 17 3imp ${⊢}\left({G}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {w}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({w}{G}{x}={x}\wedge \exists {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={w}\right)\right)\to \left({G}\in \mathrm{GrpOp}\to {G}\in \mathrm{MndOp}\right)$
19 3 18 syli ${⊢}{G}\in \mathrm{GrpOp}\to \left({G}\in \mathrm{GrpOp}\to {G}\in \mathrm{MndOp}\right)$
20 19 pm2.43i ${⊢}{G}\in \mathrm{GrpOp}\to {G}\in \mathrm{MndOp}$