Database
BASIC ALGEBRAIC STRUCTURES
Rings
Unital rings
prdsmulrcl
Metamath Proof Explorer
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
⊢ 𝑌 = ( 𝑆 X s 𝑅 )
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
⊢ 𝑌 = ( 𝑆 X s 𝑅 )
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
⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) ∈ 𝐵 )