Metamath Proof Explorer

Theorem cringm4

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

Ref Expression
Hypotheses cringm4.1 โŠข ๐ต = ( Base โ€˜ ๐‘… )
cringm4.2 โŠข ยท = ( .r โ€˜ ๐‘… )
Assertion cringm4 ( ( ๐‘… โˆˆ CRing โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โˆง ( ๐‘ โˆˆ ๐ต โˆง ๐‘Š โˆˆ ๐ต ) ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) ยท ( ๐‘ ยท ๐‘Š ) ) = ( ( ๐‘‹ ยท ๐‘ ) ยท ( ๐‘Œ ยท ๐‘Š ) ) )

Proof

Step Hyp Ref Expression
1 cringm4.1 โŠข ๐ต = ( Base โ€˜ ๐‘… )
2 cringm4.2 โŠข ยท = ( .r โ€˜ ๐‘… )
3 eqid โŠข ( mulGrp โ€˜ ๐‘… ) = ( mulGrp โ€˜ ๐‘… )
4 3 crngmgp โŠข ( ๐‘… โˆˆ CRing โ†’ ( mulGrp โ€˜ ๐‘… ) โˆˆ CMnd )
5 3 1 mgpbas โŠข ๐ต = ( Base โ€˜ ( mulGrp โ€˜ ๐‘… ) )
6 3 2 mgpplusg โŠข ยท = ( +g โ€˜ ( mulGrp โ€˜ ๐‘… ) )
7 5 6 cmn4 โŠข ( ( ( mulGrp โ€˜ ๐‘… ) โˆˆ CMnd โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โˆง ( ๐‘ โˆˆ ๐ต โˆง ๐‘Š โˆˆ ๐ต ) ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) ยท ( ๐‘ ยท ๐‘Š ) ) = ( ( ๐‘‹ ยท ๐‘ ) ยท ( ๐‘Œ ยท ๐‘Š ) ) )
8 4 7 syl3an1 โŠข ( ( ๐‘… โˆˆ CRing โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โˆง ( ๐‘ โˆˆ ๐ต โˆง ๐‘Š โˆˆ ๐ต ) ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) ยท ( ๐‘ ยท ๐‘Š ) ) = ( ( ๐‘‹ ยท ๐‘ ) ยท ( ๐‘Œ ยท ๐‘Š ) ) )