Theorem rngcl

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

	Ref	Expression
Hypotheses	rngcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rngcl.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	rngcl	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		rngcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rngcl.t	⊢ · = ( .r ‘ 𝑅 )
3		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
4	3	rngmgp	⊢ ( 𝑅 ∈ Rng → ( mulGrp ‘ 𝑅 ) ∈ Smgrp )
5		sgrpmgm	⊢ ( ( mulGrp ‘ 𝑅 ) ∈ Smgrp → ( mulGrp ‘ 𝑅 ) ∈ Mgm )
6	4 5	syl	⊢ ( 𝑅 ∈ Rng → ( mulGrp ‘ 𝑅 ) ∈ Mgm )
7	3 1	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
8	3 2	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
9	7 8	mgmcl	⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mgm ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
10	6 9	syl3an1	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )