This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rngcl

Description: Closure of the multiplication operation of a non-unital 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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )