Metamath Proof Explorer


Theorem srgmgp

Description: A semiring is a monoid under multiplication. (Contributed by Thierry Arnoux, 21-Mar-2018)

Ref Expression
Hypothesis srgmgp.g 𝐺 = ( mulGrp ‘ 𝑅 )
Assertion srgmgp ( 𝑅 ∈ SRing → 𝐺 ∈ Mnd )

Proof

Step Hyp Ref Expression
1 srgmgp.g 𝐺 = ( mulGrp ‘ 𝑅 )
2 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3 eqid ( +g𝑅 ) = ( +g𝑅 )
4 eqid ( .r𝑅 ) = ( .r𝑅 )
5 eqid ( 0g𝑅 ) = ( 0g𝑅 )
6 2 1 3 4 5 issrg ( 𝑅 ∈ SRing ↔ ( 𝑅 ∈ CMnd ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r𝑅 ) ( 𝑦 ( +g𝑅 ) 𝑧 ) ) = ( ( 𝑥 ( .r𝑅 ) 𝑦 ) ( +g𝑅 ) ( 𝑥 ( .r𝑅 ) 𝑧 ) ) ∧ ( ( 𝑥 ( +g𝑅 ) 𝑦 ) ( .r𝑅 ) 𝑧 ) = ( ( 𝑥 ( .r𝑅 ) 𝑧 ) ( +g𝑅 ) ( 𝑦 ( .r𝑅 ) 𝑧 ) ) ) ∧ ( ( ( 0g𝑅 ) ( .r𝑅 ) 𝑥 ) = ( 0g𝑅 ) ∧ ( 𝑥 ( .r𝑅 ) ( 0g𝑅 ) ) = ( 0g𝑅 ) ) ) ) )
7 6 simp2bi ( 𝑅 ∈ SRing → 𝐺 ∈ Mnd )