Theorem rngmgp

Description: A non-unital ring is a semigroup under multiplication. (Contributed by AV, 17-Feb-2020)

	Ref	Expression
Hypothesis	rngmgp.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
Assertion	rngmgp	⊢ ( 𝑅 ∈ Rng → 𝐺 ∈ Smgrp )

Proof

Step	Hyp	Ref	Expression
1		rngmgp.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
2		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
4		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
5	2 1 3 4	isrng	⊢ ( 𝑅 ∈ Rng ↔ ( 𝑅 ∈ Abel ∧ 𝐺 ∈ Smgrp ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑧 ) ) ∧ ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑧 ) ( +g ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ) ) )
6	5	simp2bi	⊢ ( 𝑅 ∈ Rng → 𝐺 ∈ Smgrp )