Theorem rngmgp

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

	Ref	Expression
Hypothesis	rngmgp.g	$$⊢G={\mathrm{mulGrp}}_R$$
Assertion	rngmgp	Could not format assertion : No typesetting found for |- ( R e. Rng -> G e. Smgrp ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rngmgp.g	$$⊢G={\mathrm{mulGrp}}_R$$
2		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
3		eqid	$$⊢{+}_R={+}_R$$
4		eqid	$$⊢{\cdot }_R={\cdot }_R$$
5	2 1 3 4	isrng	Could not format ( R e. Rng <-> ( R e. Abel /\ G e. Smgrp /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) ) ) : No typesetting found for |- ( R e. Rng <-> ( R e. Abel /\ G e. Smgrp /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) ) ) with typecode |-
6	5	simp2bi	Could not format ( R e. Rng -> G e. Smgrp ) : No typesetting found for |- ( R e. Rng -> G e. Smgrp ) with typecode |-