Theorem prdsmulrcl

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

	Ref	Expression
Hypotheses	prdsmulrcl.y	$$⊢Y=S{⨉}_{𝑠}R$$
	prdsmulrcl.b	$$⊢B={\mathrm{Base}}_Y$$
	prdsmulrcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	prdsmulrcl.s	$$⊢\phi \to S\in V$$
	prdsmulrcl.i	$$⊢\phi \to I\in W$$
	prdsmulrcl.r	$$⊢\phi \to R:I⟶\mathrm{Ring}$$
	prdsmulrcl.f	$$⊢\phi \to F\in B$$
	prdsmulrcl.g	$$⊢\phi \to G\in B$$
Assertion	prdsmulrcl	$$⊢\phi \to F\underset{\dot{}}{·}G\in B$$

Proof

Step	Hyp	Ref	Expression
1		prdsmulrcl.y	$$⊢Y=S{⨉}_{𝑠}R$$
2		prdsmulrcl.b	$$⊢B={\mathrm{Base}}_Y$$
3		prdsmulrcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
4		prdsmulrcl.s	$$⊢\phi \to S\in V$$
5		prdsmulrcl.i	$$⊢\phi \to I\in W$$
6		prdsmulrcl.r	$$⊢\phi \to R:I⟶\mathrm{Ring}$$
7		prdsmulrcl.f	$$⊢\phi \to F\in B$$
8		prdsmulrcl.g	$$⊢\phi \to G\in B$$
9	6	ffnd	$$⊢\phi \to RFnI$$
10	1 2 4 5 9 7 8 3	prdsmulrval	$$⊢\phi \to F\underset{\dot{}}{·}G=\left(x\in I⟼F\left(x\right){\cdot }_{R\left(x\right)}G\left(x\right)\right)$$
11	6	ffvelcdmda	$$⊢\left(\phi \wedge x\in I\right)\to R\left(x\right)\in \mathrm{Ring}$$
12	4	adantr	$$⊢\left(\phi \wedge x\in I\right)\to S\in V$$
13	5	adantr	$$⊢\left(\phi \wedge x\in I\right)\to I\in W$$
14	9	adantr	$$⊢\left(\phi \wedge x\in I\right)\to RFnI$$
15	7	adantr	$$⊢\left(\phi \wedge x\in I\right)\to F\in B$$
16		simpr	$$⊢\left(\phi \wedge x\in I\right)\to x\in I$$
17	1 2 12 13 14 15 16	prdsbasprj	$$⊢\left(\phi \wedge x\in I\right)\to F\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}$$
18	8	adantr	$$⊢\left(\phi \wedge x\in I\right)\to G\in B$$
19	1 2 12 13 14 18 16	prdsbasprj	$$⊢\left(\phi \wedge x\in I\right)\to G\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}$$
20		eqid	$$⊢{\mathrm{Base}}_{R\left(x\right)}={\mathrm{Base}}_{R\left(x\right)}$$
21		eqid	$$⊢{\cdot }_{R\left(x\right)}={\cdot }_{R\left(x\right)}$$
22	20 21	ringcl	$$⊢\left(R\left(x\right)\in \mathrm{Ring}\wedge F\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}\wedge G\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}\right)\to F\left(x\right){\cdot }_{R\left(x\right)}G\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}$$
23	11 17 19 22	syl3anc	$$⊢\left(\phi \wedge x\in I\right)\to F\left(x\right){\cdot }_{R\left(x\right)}G\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}$$
24	23	ralrimiva	$$⊢\phi \to \forall x\in IF\left(x\right){\cdot }_{R\left(x\right)}G\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}$$
25	1 2 4 5 9	prdsbasmpt	$$⊢\phi \to \left(\left(x\in I⟼F\left(x\right){\cdot }_{R\left(x\right)}G\left(x\right)\right)\in B\leftrightarrow \forall x\in IF\left(x\right){\cdot }_{R\left(x\right)}G\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}\right)$$
26	24 25	mpbird	$$⊢\phi \to \left(x\in I⟼F\left(x\right){\cdot }_{R\left(x\right)}G\left(x\right)\right)\in B$$
27	10 26	eqeltrd	$$⊢\phi \to F\underset{\dot{}}{·}G\in B$$