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

Metamath Proof Explorer

Theorem ringlsmss

Description: Closure of the product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024)

Ref Expression
Hypotheses ringlsmss.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
ringlsmss.2 ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
ringlsmss.3 ⊢ × = ( LSSum ‘ 𝐺 )
ringlsmss.4 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
ringlsmss.5 ⊢ ( 𝜑 → 𝐸 ⊆ 𝐵 )
ringlsmss.6 ⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 )
Assertion ringlsmss ( 𝜑 → ( 𝐸 × 𝐹 ) ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 ringlsmss.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ringlsmss.2 ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
3 ringlsmss.3 ⊢ × = ( LSSum ‘ 𝐺 )
4 ringlsmss.4 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 ringlsmss.5 ⊢ ( 𝜑 → 𝐸 ⊆ 𝐵 )
6 ringlsmss.6 ⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 )
7 2 ringmgp ⊢ ( 𝑅 ∈ Ring → 𝐺 ∈ Mnd )
8 4 7 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
9 2 1 mgpbas ⊢ 𝐵 = ( Base ‘ 𝐺 )
10 9 3 lsmssv ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐸 ⊆ 𝐵 ∧ 𝐹 ⊆ 𝐵 ) → ( 𝐸 × 𝐹 ) ⊆ 𝐵 )
11 8 5 6 10 syl3anc ⊢ ( 𝜑 → ( 𝐸 × 𝐹 ) ⊆ 𝐵 )