Metamath Proof Explorer


Theorem iscmn

Description: The predicate "is a commutative monoid". (Contributed by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses iscmn.b B=BaseG
iscmn.p +˙=+G
Assertion iscmn GCMndGMndxByBx+˙y=y+˙x

Proof

Step Hyp Ref Expression
1 iscmn.b B=BaseG
2 iscmn.p +˙=+G
3 fveq2 g=GBaseg=BaseG
4 3 1 eqtr4di g=GBaseg=B
5 raleq Baseg=ByBasegx+gy=y+gxyBx+gy=y+gx
6 5 raleqbi1dv Baseg=BxBasegyBasegx+gy=y+gxxByBx+gy=y+gx
7 4 6 syl g=GxBasegyBasegx+gy=y+gxxByBx+gy=y+gx
8 fveq2 g=G+g=+G
9 8 2 eqtr4di g=G+g=+˙
10 9 oveqd g=Gx+gy=x+˙y
11 9 oveqd g=Gy+gx=y+˙x
12 10 11 eqeq12d g=Gx+gy=y+gxx+˙y=y+˙x
13 12 2ralbidv g=GxByBx+gy=y+gxxByBx+˙y=y+˙x
14 7 13 bitrd g=GxBasegyBasegx+gy=y+gxxByBx+˙y=y+˙x
15 df-cmn CMnd=gMnd|xBasegyBasegx+gy=y+gx
16 14 15 elrab2 GCMndGMndxByBx+˙y=y+˙x