Metamath Proof Explorer


Theorem crngcom

Description: A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Hypotheses ringcl.b B=BaseR
ringcl.t ·˙=R
Assertion crngcom RCRingXBYBX·˙Y=Y·˙X

Proof

Step Hyp Ref Expression
1 ringcl.b B=BaseR
2 ringcl.t ·˙=R
3 eqid mulGrpR=mulGrpR
4 3 crngmgp RCRingmulGrpRCMnd
5 3 1 mgpbas B=BasemulGrpR
6 3 2 mgpplusg ·˙=+mulGrpR
7 5 6 cmncom mulGrpRCMndXBYBX·˙Y=Y·˙X
8 4 7 syl3an1 RCRingXBYBX·˙Y=Y·˙X