Metamath Proof Explorer


Theorem cringm4

Description: Commutative/associative law for commutative ring. (Contributed by Thierry Arnoux, 14-Jan-2024)

Ref Expression
Hypotheses cringm4.1 B = Base R
cringm4.2 · ˙ = R
Assertion cringm4 R CRing X B Y B Z B W B X · ˙ Y · ˙ Z · ˙ W = X · ˙ Z · ˙ Y · ˙ W

Proof

Step Hyp Ref Expression
1 cringm4.1 B = Base R
2 cringm4.2 · ˙ = R
3 eqid mulGrp R = mulGrp R
4 3 crngmgp R CRing mulGrp R CMnd
5 3 1 mgpbas B = Base mulGrp R
6 3 2 mgpplusg · ˙ = + mulGrp R
7 5 6 cmn4 mulGrp R CMnd X B Y B Z B W B X · ˙ Y · ˙ Z · ˙ W = X · ˙ Z · ˙ Y · ˙ W
8 4 7 syl3an1 R CRing X B Y B Z B W B X · ˙ Y · ˙ Z · ˙ W = X · ˙ Z · ˙ Y · ˙ W