Theorem rngcl

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

	Ref	Expression
Hypotheses	rngcl.b	|- B = ( Base ` R )
	rngcl.t	|- .x. = ( .r ` R )
Assertion	rngcl	|- ( ( R e. Rng /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )

Proof

Step	Hyp	Ref	Expression
1		rngcl.b	|- B = ( Base ` R )
2		rngcl.t	|- .x. = ( .r ` R )
3		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
4	3	rngmgp	|- ( R e. Rng -> ( mulGrp ` R ) e. Smgrp )
5		sgrpmgm	|- ( ( mulGrp ` R ) e. Smgrp -> ( mulGrp ` R ) e. Mgm )
6	4 5	syl	|- ( R e. Rng -> ( mulGrp ` R ) e. Mgm )
7	3 1	mgpbas	|- B = ( Base ` ( mulGrp ` R ) )
8	3 2	mgpplusg	|- .x. = ( +g ` ( mulGrp ` R ) )
9	7 8	mgmcl	|- ( ( ( mulGrp ` R ) e. Mgm /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )
10	6 9	syl3an1	|- ( ( R e. Rng /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )