Theorem cringm4

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

	Ref	Expression
Hypotheses	cringm4.1	$$⊢B={\mathrm{Base}}_R$$
	cringm4.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	cringm4	$$⊢\left(R\in \mathrm{CRing}\wedge \left(X\in B\wedge Y\in B\right)\wedge \left(Z\in B\wedge W\in B\right)\right)\to \left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}W\right)=\left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}\left(Y\underset{\dot{}}{·}W\right)$$

Proof

Step	Hyp	Ref	Expression
1		cringm4.1	$$⊢B={\mathrm{Base}}_R$$
2		cringm4.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
4	3	crngmgp	$$⊢R\in \mathrm{CRing}\to {\mathrm{mulGrp}}_R\in \mathrm{CMnd}$$
5	3 1	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
6	3 2	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_{{\mathrm{mulGrp}}_R}$$
7	5 6	cmn4	$$⊢\left({\mathrm{mulGrp}}_R\in \mathrm{CMnd}\wedge \left(X\in B\wedge Y\in B\right)\wedge \left(Z\in B\wedge W\in B\right)\right)\to \left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}W\right)=\left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}\left(Y\underset{\dot{}}{·}W\right)$$
8	4 7	syl3an1	$$⊢\left(R\in \mathrm{CRing}\wedge \left(X\in B\wedge Y\in B\right)\wedge \left(Z\in B\wedge W\in B\right)\right)\to \left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}W\right)=\left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}\left(Y\underset{\dot{}}{·}W\right)$$