# Metamath Proof Explorer

## Theorem ismndo2

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

Ref Expression
Hypothesis ismndo2.1 ${⊢}{X}=\mathrm{ran}{G}$
Assertion ismndo2 ${⊢}{G}\in {A}\to \left({G}\in \mathrm{MndOp}↔\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 {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 ismndo2.1 ${⊢}{X}=\mathrm{ran}{G}$
2 mndomgmid ${⊢}{G}\in \mathrm{MndOp}\to {G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)$
3 rngopidOLD ${⊢}{G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\to \mathrm{ran}{G}=\mathrm{dom}\mathrm{dom}{G}$
4 2 3 syl ${⊢}{G}\in \mathrm{MndOp}\to \mathrm{ran}{G}=\mathrm{dom}\mathrm{dom}{G}$
5 1 4 syl5eq ${⊢}{G}\in \mathrm{MndOp}\to {X}=\mathrm{dom}\mathrm{dom}{G}$
6 5 a1i ${⊢}{G}\in {A}\to \left({G}\in \mathrm{MndOp}\to {X}=\mathrm{dom}\mathrm{dom}{G}\right)$
7 fdm ${⊢}{G}:{X}×{X}⟶{X}\to \mathrm{dom}{G}={X}×{X}$
8 7 dmeqd ${⊢}{G}:{X}×{X}⟶{X}\to \mathrm{dom}\mathrm{dom}{G}=\mathrm{dom}\left({X}×{X}\right)$
9 dmxpid ${⊢}\mathrm{dom}\left({X}×{X}\right)={X}$
10 8 9 syl6req ${⊢}{G}:{X}×{X}⟶{X}\to {X}=\mathrm{dom}\mathrm{dom}{G}$
11 10 3ad2ant1 ${⊢}\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 {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\to {X}=\mathrm{dom}\mathrm{dom}{G}$
12 11 a1i ${⊢}{G}\in {A}\to \left(\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 {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\to {X}=\mathrm{dom}\mathrm{dom}{G}\right)$
13 eqid ${⊢}\mathrm{dom}\mathrm{dom}{G}=\mathrm{dom}\mathrm{dom}{G}$
14 13 ismndo1 ${⊢}{G}\in {A}\to \left({G}\in \mathrm{MndOp}↔\left({G}:\mathrm{dom}\mathrm{dom}{G}×\mathrm{dom}\mathrm{dom}{G}⟶\mathrm{dom}\mathrm{dom}{G}\wedge \forall {x}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {x}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)$
15 xpid11 ${⊢}{X}×{X}=\mathrm{dom}\mathrm{dom}{G}×\mathrm{dom}\mathrm{dom}{G}↔{X}=\mathrm{dom}\mathrm{dom}{G}$
16 15 biimpri ${⊢}{X}=\mathrm{dom}\mathrm{dom}{G}\to {X}×{X}=\mathrm{dom}\mathrm{dom}{G}×\mathrm{dom}\mathrm{dom}{G}$
17 feq23 ${⊢}\left({X}×{X}=\mathrm{dom}\mathrm{dom}{G}×\mathrm{dom}\mathrm{dom}{G}\wedge {X}=\mathrm{dom}\mathrm{dom}{G}\right)\to \left({G}:{X}×{X}⟶{X}↔{G}:\mathrm{dom}\mathrm{dom}{G}×\mathrm{dom}\mathrm{dom}{G}⟶\mathrm{dom}\mathrm{dom}{G}\right)$
18 16 17 mpancom ${⊢}{X}=\mathrm{dom}\mathrm{dom}{G}\to \left({G}:{X}×{X}⟶{X}↔{G}:\mathrm{dom}\mathrm{dom}{G}×\mathrm{dom}\mathrm{dom}{G}⟶\mathrm{dom}\mathrm{dom}{G}\right)$
19 raleq ${⊢}{X}=\mathrm{dom}\mathrm{dom}{G}\to \left(\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)↔\forall {z}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\right)$
20 19 raleqbi1dv ${⊢}{X}=\mathrm{dom}\mathrm{dom}{G}\to \left(\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)↔\forall {y}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\right)$
21 20 raleqbi1dv ${⊢}{X}=\mathrm{dom}\mathrm{dom}{G}\to \left(\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)↔\forall {x}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\right)$
22 raleq ${⊢}{X}=\mathrm{dom}\mathrm{dom}{G}\to \left(\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)↔\forall {y}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)$
23 22 rexeqbi1dv ${⊢}{X}=\mathrm{dom}\mathrm{dom}{G}\to \left(\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)↔\exists {x}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)$
24 18 21 23 3anbi123d ${⊢}{X}=\mathrm{dom}\mathrm{dom}{G}\to \left(\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 {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)↔\left({G}:\mathrm{dom}\mathrm{dom}{G}×\mathrm{dom}\mathrm{dom}{G}⟶\mathrm{dom}\mathrm{dom}{G}\wedge \forall {x}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {x}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)$
25 24 bibi2d ${⊢}{X}=\mathrm{dom}\mathrm{dom}{G}\to \left(\left({G}\in \mathrm{MndOp}↔\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 {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)↔\left({G}\in \mathrm{MndOp}↔\left({G}:\mathrm{dom}\mathrm{dom}{G}×\mathrm{dom}\mathrm{dom}{G}⟶\mathrm{dom}\mathrm{dom}{G}\wedge \forall {x}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {x}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{dom}\mathrm{dom}{G}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)\right)$
26 14 25 syl5ibrcom ${⊢}{G}\in {A}\to \left({X}=\mathrm{dom}\mathrm{dom}{G}\to \left({G}\in \mathrm{MndOp}↔\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 {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)\right)$
27 6 12 26 pm5.21ndd ${⊢}{G}\in {A}\to \left({G}\in \mathrm{MndOp}↔\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 {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)$