Metamath Proof Explorer


Theorem prdsmulrcl

Description: A structure product of rings has closed binary operation. (Contributed by Mario Carneiro, 11-Mar-2015) (Proof shortened by AV, 30-Mar-2025)

Ref Expression
Hypotheses prdsmulrcl.y 𝑌 = ( 𝑆 Xs 𝑅 )
prdsmulrcl.b 𝐵 = ( Base ‘ 𝑌 )
prdsmulrcl.t · = ( .r𝑌 )
prdsmulrcl.s ( 𝜑𝑆𝑉 )
prdsmulrcl.i ( 𝜑𝐼𝑊 )
prdsmulrcl.r ( 𝜑𝑅 : 𝐼 ⟶ Ring )
prdsmulrcl.f ( 𝜑𝐹𝐵 )
prdsmulrcl.g ( 𝜑𝐺𝐵 )
Assertion prdsmulrcl ( 𝜑 → ( 𝐹 · 𝐺 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 prdsmulrcl.y 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdsmulrcl.b 𝐵 = ( Base ‘ 𝑌 )
3 prdsmulrcl.t · = ( .r𝑌 )
4 prdsmulrcl.s ( 𝜑𝑆𝑉 )
5 prdsmulrcl.i ( 𝜑𝐼𝑊 )
6 prdsmulrcl.r ( 𝜑𝑅 : 𝐼 ⟶ Ring )
7 prdsmulrcl.f ( 𝜑𝐹𝐵 )
8 prdsmulrcl.g ( 𝜑𝐺𝐵 )
9 ringssrng Ring ⊆ Rng
10 fss ( ( 𝑅 : 𝐼 ⟶ Ring ∧ Ring ⊆ Rng ) → 𝑅 : 𝐼 ⟶ Rng )
11 6 9 10 sylancl ( 𝜑𝑅 : 𝐼 ⟶ Rng )
12 1 2 3 4 5 11 7 8 prdsmulrngcl ( 𝜑 → ( 𝐹 · 𝐺 ) ∈ 𝐵 )