Theorem rngcl

Description: Closure of the multiplication operation of a nonunital ring. (Contributed by AV, 17-Apr-2020)

	Ref	Expression
Hypotheses	rngcl.b	$$⊢B={\mathrm{Base}}_R$$
	rngcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	rngcl	$$⊢\left(R\in \mathrm{Rng}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{·}Y\in B$$

Proof

Step	Hyp	Ref	Expression
1		rngcl.b	$$⊢B={\mathrm{Base}}_R$$
2		rngcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
4	3	rngmgp	Could not format ( R e. Rng -> ( mulGrp ` R ) e. Smgrp ) : No typesetting found for |- ( R e. Rng -> ( mulGrp ` R ) e. Smgrp ) with typecode |-
5		sgrpmgm	Could not format ( ( mulGrp ` R ) e. Smgrp -> ( mulGrp ` R ) e. Mgm ) : No typesetting found for |- ( ( mulGrp ` R ) e. Smgrp -> ( mulGrp ` R ) e. Mgm ) with typecode |-
6	4 5	syl	$$⊢R\in \mathrm{Rng}\to {\mathrm{mulGrp}}_R\in \mathrm{Mgm}$$
7	3 1	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
8	3 2	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_{{\mathrm{mulGrp}}_R}$$
9	7 8	mgmcl	$$⊢\left({\mathrm{mulGrp}}_R\in \mathrm{Mgm}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{·}Y\in B$$
10	6 9	syl3an1	$$⊢\left(R\in \mathrm{Rng}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{·}Y\in B$$