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	|- Y = ( S Xs_ R )
	prdsmulrcl.b	|- B = ( Base ` Y )
	prdsmulrcl.t	|- .x. = ( .r ` Y )
	prdsmulrcl.s	|- ( ph -> S e. V )
	prdsmulrcl.i	|- ( ph -> I e. W )
	prdsmulrcl.r	|- ( ph -> R : I --> Ring )
	prdsmulrcl.f	|- ( ph -> F e. B )
	prdsmulrcl.g	|- ( ph -> G e. B )
Assertion	prdsmulrcl	|- ( ph -> ( F .x. G ) e. B )

Proof

Step	Hyp	Ref	Expression
1		prdsmulrcl.y	|- Y = ( S Xs_ R )
2		prdsmulrcl.b	|- B = ( Base ` Y )
3		prdsmulrcl.t	|- .x. = ( .r ` Y )
4		prdsmulrcl.s	|- ( ph -> S e. V )
5		prdsmulrcl.i	|- ( ph -> I e. W )
6		prdsmulrcl.r	|- ( ph -> R : I --> Ring )
7		prdsmulrcl.f	|- ( ph -> F e. B )
8		prdsmulrcl.g	|- ( ph -> G e. B )
9		ringssrng	|- Ring C_ Rng
10		fss	|- ( ( R : I --> Ring /\ Ring C_ Rng ) -> R : I --> Rng )
11	6 9 10	sylancl	|- ( ph -> R : I --> Rng )
12	1 2 3 4 5 11 7 8	prdsmulrngcl	|- ( ph -> ( F .x. G ) e. B )