Theorem prdsmulrngcl

Description: Closure of the multiplication in a structure product of non-unital rings. (Contributed by Mario Carneiro, 11-Mar-2015) Generalization of prdsmulrcl . (Revised by AV, 21-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		prdsmulrngcl.y	$$⊢Y=S{⨉}_{𝑠}R$$
2		prdsmulrngcl.b	$$⊢B={\mathrm{Base}}_Y$$
3		prdsmulrngcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
4		prdsmulrngcl.s	$$⊢\phi \to S\in V$$
5		prdsmulrngcl.i	$$⊢\phi \to I\in W$$
6		prdsmulrngcl.r	$$⊢\phi \to R:I⟶\mathrm{Rng}$$
7		prdsmulrngcl.f	$$⊢\phi \to F\in B$$
8		prdsmulrngcl.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{Rng}$$
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	rngcl	$$⊢\left(R\left(x\right)\in \mathrm{Rng}\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$$