Theorem prdsvscacl

Description: Pointwise scalar multiplication is closed in products of modules. (Contributed by Stefan O'Rear, 10-Jan-2015)

	Ref	Expression
Hypotheses	prdsvscacl.y	$$⊢Y=S{⨉}_{𝑠}R$$
	prdsvscacl.b	$$⊢B={\mathrm{Base}}_Y$$
	prdsvscacl.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	prdsvscacl.k	$$⊢K={\mathrm{Base}}_S$$
	prdsvscacl.s	$$⊢\phi \to S\in \mathrm{Ring}$$
	prdsvscacl.i	$$⊢\phi \to I\in W$$
	prdsvscacl.r	$$⊢\phi \to R:I⟶\mathrm{LMod}$$
	prdsvscacl.f	$$⊢\phi \to F\in K$$
	prdsvscacl.g	$$⊢\phi \to G\in B$$
	prdsvscacl.sr	$$⊢\left(\phi \wedge x\in I\right)\to \mathrm{Scalar}\left(R\left(x\right)\right)=S$$
Assertion	prdsvscacl	$$⊢\phi \to F\underset{\dot{}}{·}G\in B$$

Proof

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