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=ranG
Assertion ismndo2 GAGMndOpG:X×XXxXyXzXxGyGz=xGyGzxXyXxGy=yyGx=y

Proof

Step Hyp Ref Expression
1 ismndo2.1 X=ranG
2 mndomgmid GMndOpGMagmaExId
3 rngopidOLD GMagmaExIdranG=domdomG
4 2 3 syl GMndOpranG=domdomG
5 1 4 eqtrid GMndOpX=domdomG
6 5 a1i GAGMndOpX=domdomG
7 fdm G:X×XXdomG=X×X
8 7 dmeqd G:X×XXdomdomG=domX×X
9 dmxpid domX×X=X
10 8 9 eqtr2di G:X×XXX=domdomG
11 10 3ad2ant1 G:X×XXxXyXzXxGyGz=xGyGzxXyXxGy=yyGx=yX=domdomG
12 11 a1i GAG:X×XXxXyXzXxGyGz=xGyGzxXyXxGy=yyGx=yX=domdomG
13 eqid domdomG=domdomG
14 13 ismndo1 GAGMndOpG:domdomG×domdomGdomdomGxdomdomGydomdomGzdomdomGxGyGz=xGyGzxdomdomGydomdomGxGy=yyGx=y
15 xpid11 X×X=domdomG×domdomGX=domdomG
16 15 biimpri X=domdomGX×X=domdomG×domdomG
17 feq23 X×X=domdomG×domdomGX=domdomGG:X×XXG:domdomG×domdomGdomdomG
18 16 17 mpancom X=domdomGG:X×XXG:domdomG×domdomGdomdomG
19 raleq X=domdomGzXxGyGz=xGyGzzdomdomGxGyGz=xGyGz
20 19 raleqbi1dv X=domdomGyXzXxGyGz=xGyGzydomdomGzdomdomGxGyGz=xGyGz
21 20 raleqbi1dv X=domdomGxXyXzXxGyGz=xGyGzxdomdomGydomdomGzdomdomGxGyGz=xGyGz
22 raleq X=domdomGyXxGy=yyGx=yydomdomGxGy=yyGx=y
23 22 rexeqbi1dv X=domdomGxXyXxGy=yyGx=yxdomdomGydomdomGxGy=yyGx=y
24 18 21 23 3anbi123d X=domdomGG:X×XXxXyXzXxGyGz=xGyGzxXyXxGy=yyGx=yG:domdomG×domdomGdomdomGxdomdomGydomdomGzdomdomGxGyGz=xGyGzxdomdomGydomdomGxGy=yyGx=y
25 24 bibi2d X=domdomGGMndOpG:X×XXxXyXzXxGyGz=xGyGzxXyXxGy=yyGx=yGMndOpG:domdomG×domdomGdomdomGxdomdomGydomdomGzdomdomGxGyGz=xGyGzxdomdomGydomdomGxGy=yyGx=y
26 14 25 syl5ibrcom GAX=domdomGGMndOpG:X×XXxXyXzXxGyGz=xGyGzxXyXxGy=yyGx=y
27 6 12 26 pm5.21ndd GAGMndOpG:X×XXxXyXzXxGyGz=xGyGzxXyXxGy=yyGx=y