Metamath Proof Explorer


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 = Base Y
prdsvscacl.t · ˙ = Y
prdsvscacl.k K = Base S
prdsvscacl.s φ S Ring
prdsvscacl.i φ I W
prdsvscacl.r φ R : I LMod
prdsvscacl.f φ F K
prdsvscacl.g φ G B
prdsvscacl.sr φ x I Scalar R x = S
Assertion prdsvscacl φ F · ˙ G B

Proof

Step Hyp Ref Expression
1 prdsvscacl.y Y = S 𝑠 R
2 prdsvscacl.b B = Base Y
3 prdsvscacl.t · ˙ = Y
4 prdsvscacl.k K = Base S
5 prdsvscacl.s φ S Ring
6 prdsvscacl.i φ I W
7 prdsvscacl.r φ R : I LMod
8 prdsvscacl.f φ F K
9 prdsvscacl.g φ G B
10 prdsvscacl.sr φ x I Scalar R x = S
11 7 ffnd φ R Fn I
12 1 2 3 4 5 6 11 8 9 prdsvscaval φ F · ˙ G = x I F R x G x
13 7 ffvelrnda φ x I R x LMod
14 8 adantr φ x I F K
15 10 fveq2d φ x I Base Scalar R x = Base S
16 15 4 eqtr4di φ x I Base Scalar R x = K
17 14 16 eleqtrrd φ x I F Base Scalar R x
18 5 adantr φ x I S Ring
19 6 adantr φ x I I W
20 11 adantr φ x I R Fn I
21 9 adantr φ x I G B
22 simpr φ x I x I
23 1 2 18 19 20 21 22 prdsbasprj φ x I G x Base R x
24 eqid Base R x = Base R x
25 eqid Scalar R x = Scalar R x
26 eqid R x = R x
27 eqid Base Scalar R x = Base Scalar R x
28 24 25 26 27 lmodvscl R x LMod F Base Scalar R x G x Base R x F R x G x Base R x
29 13 17 23 28 syl3anc φ x I F R x G x Base R x
30 29 ralrimiva φ x I F R x G x Base R x
31 1 2 5 6 11 prdsbasmpt φ x I F R x G x B x I F R x G x Base R x
32 30 31 mpbird φ x I F R x G x B
33 12 32 eqeltrd φ F · ˙ G B