rngmgp

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

		Ref	Expression
	Hypothesis	rngmgp.g	$⊢ G = {mulGrp}_{R}$
	Assertion	rngmgp	$⊢ R \in Rng \to G \in Smgrp$

Step	Hyp	Ref	Expression
1		rngmgp.g	$⊢ G = {mulGrp}_{R}$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3		eqid	$⊢ +_{R} = +_{R}$
4		eqid	$⊢ \cdot_{R} = \cdot_{R}$
5	2 1 3 4	isrng	$⊢ R \in Rng \leftrightarrow (R \in Abel \land G \in Smgrp \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} \forall z \in {Base}_{R} (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z)))$
6	5	simp2bi	$⊢ R \in Rng \to G \in Smgrp$

Metamath Proof Explorer