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 Xs_ R )
prdsvscacl.b 
|- B = ( Base ` Y )
prdsvscacl.t 
|- .x. = ( .s ` Y )
prdsvscacl.k 
|- K = ( Base ` S )
prdsvscacl.s 
|- ( ph -> S e. Ring )
prdsvscacl.i 
|- ( ph -> I e. W )
prdsvscacl.r 
|- ( ph -> R : I --> LMod )
prdsvscacl.f 
|- ( ph -> F e. K )
prdsvscacl.g 
|- ( ph -> G e. B )
prdsvscacl.sr 
|- ( ( ph /\ x e. I ) -> ( Scalar ` ( R ` x ) ) = S )
Assertion prdsvscacl 
|- ( ph -> ( F .x. G ) e. B )

Proof

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