This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cmncom

Description: A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses ablcom.b 
|- B = ( Base ` G )
ablcom.p 
|- .+ = ( +g ` G )
Assertion cmncom 
|- ( ( G e. CMnd /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )

Proof

Step Hyp Ref Expression
1 ablcom.b 
 |-  B = ( Base ` G )
2 ablcom.p 
 |-  .+ = ( +g ` G )
3 1 2 iscmn 
 |-  ( G e. CMnd <-> ( G e. Mnd /\ A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )
4 3 simprbi 
 |-  ( G e. CMnd -> A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) )
5 rsp2 
 |-  ( A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) -> ( ( x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) ) )
6 5 imp 
 |-  ( ( A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) = ( y .+ x ) )
7 4 6 sylan 
 |-  ( ( G e. CMnd /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) = ( y .+ x ) )
8 7 caovcomg 
 |-  ( ( G e. CMnd /\ ( X e. B /\ Y e. B ) ) -> ( X .+ Y ) = ( Y .+ X ) )
9 8 3impb 
 |-  ( ( G e. CMnd /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )