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

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	⊢ 𝑌 = ( 𝑆 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	⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) ∈ 𝐵 )