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 = ran G
Assertion ismndo2 G A G MndOp G : X × X X x X y X z X x G y G z = x G y G z x X y X x G y = y y G x = y

Proof

Step Hyp Ref Expression
1 ismndo2.1 X = ran G
2 mndomgmid G MndOp G Magma ExId
3 rngopidOLD G Magma ExId ran G = dom dom G
4 2 3 syl G MndOp ran G = dom dom G
5 1 4 syl5eq G MndOp X = dom dom G
6 5 a1i G A G MndOp X = dom dom G
7 fdm G : X × X X dom G = X × X
8 7 dmeqd G : X × X X dom dom G = dom X × X
9 dmxpid dom X × X = X
10 8 9 syl6req G : X × X X X = dom dom G
11 10 3ad2ant1 G : X × X X x X y X z X x G y G z = x G y G z x X y X x G y = y y G x = y X = dom dom G
12 11 a1i G A G : X × X X x X y X z X x G y G z = x G y G z x X y X x G y = y y G x = y X = dom dom G
13 eqid dom dom G = dom dom G
14 13 ismndo1 G A G MndOp G : dom dom G × dom dom G dom dom G x dom dom G y dom dom G z dom dom G x G y G z = x G y G z x dom dom G y dom dom G x G y = y y G x = y
15 xpid11 X × X = dom dom G × dom dom G X = dom dom G
16 15 biimpri X = dom dom G X × X = dom dom G × dom dom G
17 feq23 X × X = dom dom G × dom dom G X = dom dom G G : X × X X G : dom dom G × dom dom G dom dom G
18 16 17 mpancom X = dom dom G G : X × X X G : dom dom G × dom dom G dom dom G
19 raleq X = dom dom G z X x G y G z = x G y G z z dom dom G x G y G z = x G y G z
20 19 raleqbi1dv X = dom dom G y X z X x G y G z = x G y G z y dom dom G z dom dom G x G y G z = x G y G z
21 20 raleqbi1dv X = dom dom G x X y X z X x G y G z = x G y G z x dom dom G y dom dom G z dom dom G x G y G z = x G y G z
22 raleq X = dom dom G y X x G y = y y G x = y y dom dom G x G y = y y G x = y
23 22 rexeqbi1dv X = dom dom G x X y X x G y = y y G x = y x dom dom G y dom dom G x G y = y y G x = y
24 18 21 23 3anbi123d X = dom dom G G : X × X X x X y X z X x G y G z = x G y G z x X y X x G y = y y G x = y G : dom dom G × dom dom G dom dom G x dom dom G y dom dom G z dom dom G x G y G z = x G y G z x dom dom G y dom dom G x G y = y y G x = y
25 24 bibi2d X = dom dom G G MndOp G : X × X X x X y X z X x G y G z = x G y G z x X y X x G y = y y G x = y G MndOp G : dom dom G × dom dom G dom dom G x dom dom G y dom dom G z dom dom G x G y G z = x G y G z x dom dom G y dom dom G x G y = y y G x = y
26 14 25 syl5ibrcom G A X = dom dom G G MndOp G : X × X X x X y X z X x G y G z = x G y G z x X y X x G y = y y G x = y
27 6 12 26 pm5.21ndd G A G MndOp G : X × X X x X y X z X x G y G z = x G y G z x X y X x G y = y y G x = y