Metamath Proof Explorer

Theorem cnmpt2vsca

Description: Continuity of scalar multiplication; analogue of cnmpt22f which cannot be used directly because .s is not a function. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses tlmtrg.f 
|- F = ( Scalar ` W )
cnmpt1vsca.t 
|- .x. = ( .s ` W )
cnmpt1vsca.j 
|- J = ( TopOpen ` W )
cnmpt1vsca.k 
|- K = ( TopOpen ` F )
cnmpt1vsca.w 
|- ( ph -> W e. TopMod )
cnmpt1vsca.l 
|- ( ph -> L e. ( TopOn ` X ) )
cnmpt2vsca.m 
|- ( ph -> M e. ( TopOn ` Y ) )
cnmpt2vsca.a 
|- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( L tX M ) Cn K ) )
cnmpt2vsca.b 
|- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( L tX M ) Cn J ) )
Assertion cnmpt2vsca 
|- ( ph -> ( x e. X , y e. Y |-> ( A .x. B ) ) e. ( ( L tX M ) Cn J ) )

Proof

Step Hyp Ref Expression
1 tlmtrg.f 
 |-  F = ( Scalar ` W )
2 cnmpt1vsca.t 
 |-  .x. = ( .s ` W )
3 cnmpt1vsca.j 
 |-  J = ( TopOpen ` W )
4 cnmpt1vsca.k 
 |-  K = ( TopOpen ` F )
5 cnmpt1vsca.w 
 |-  ( ph -> W e. TopMod )
6 cnmpt1vsca.l 
 |-  ( ph -> L e. ( TopOn ` X ) )
7 cnmpt2vsca.m 
 |-  ( ph -> M e. ( TopOn ` Y ) )
8 cnmpt2vsca.a 
 |-  ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( L tX M ) Cn K ) )
9 cnmpt2vsca.b 
 |-  ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( L tX M ) Cn J ) )
10 txtopon 
 |-  ( ( L e. ( TopOn ` X ) /\ M e. ( TopOn ` Y ) ) -> ( L tX M ) e. ( TopOn ` ( X X. Y ) ) )
11 6 7 10 syl2anc 
 |-  ( ph -> ( L tX M ) e. ( TopOn ` ( X X. Y ) ) )
12 1 tlmscatps 
 |-  ( W e. TopMod -> F e. TopSp )
13 5 12 syl 
 |-  ( ph -> F e. TopSp )
14 eqid 
 |-  ( Base ` F ) = ( Base ` F )
15 14 4 istps 
 |-  ( F e. TopSp <-> K e. ( TopOn ` ( Base ` F ) ) )
16 13 15 sylib 
 |-  ( ph -> K e. ( TopOn ` ( Base ` F ) ) )
17 cnf2 
 |-  ( ( ( L tX M ) e. ( TopOn ` ( X X. Y ) ) /\ K e. ( TopOn ` ( Base ` F ) ) /\ ( x e. X , y e. Y |-> A ) e. ( ( L tX M ) Cn K ) ) -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> ( Base ` F ) )
18 11 16 8 17 syl3anc 
 |-  ( ph -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> ( Base ` F ) )
19 eqid 
 |-  ( x e. X , y e. Y |-> A ) = ( x e. X , y e. Y |-> A )
20 19 fmpo 
 |-  ( A. x e. X A. y e. Y A e. ( Base ` F ) <-> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> ( Base ` F ) )
21 18 20 sylibr 
 |-  ( ph -> A. x e. X A. y e. Y A e. ( Base ` F ) )
22 21 r19.21bi 
 |-  ( ( ph /\ x e. X ) -> A. y e. Y A e. ( Base ` F ) )
23 22 r19.21bi 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> A e. ( Base ` F ) )
24 tlmtps 
 |-  ( W e. TopMod -> W e. TopSp )
25 5 24 syl 
 |-  ( ph -> W e. TopSp )
26 eqid 
 |-  ( Base ` W ) = ( Base ` W )
27 26 3 istps 
 |-  ( W e. TopSp <-> J e. ( TopOn ` ( Base ` W ) ) )
28 25 27 sylib 
 |-  ( ph -> J e. ( TopOn ` ( Base ` W ) ) )
29 cnf2 
 |-  ( ( ( L tX M ) e. ( TopOn ` ( X X. Y ) ) /\ J e. ( TopOn ` ( Base ` W ) ) /\ ( x e. X , y e. Y |-> B ) e. ( ( L tX M ) Cn J ) ) -> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> ( Base ` W ) )
30 11 28 9 29 syl3anc 
 |-  ( ph -> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> ( Base ` W ) )
31 eqid 
 |-  ( x e. X , y e. Y |-> B ) = ( x e. X , y e. Y |-> B )
32 31 fmpo 
 |-  ( A. x e. X A. y e. Y B e. ( Base ` W ) <-> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> ( Base ` W ) )
33 30 32 sylibr 
 |-  ( ph -> A. x e. X A. y e. Y B e. ( Base ` W ) )
34 33 r19.21bi 
 |-  ( ( ph /\ x e. X ) -> A. y e. Y B e. ( Base ` W ) )
35 34 r19.21bi 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> B e. ( Base ` W ) )
36 eqid 
 |-  ( .sf ` W ) = ( .sf ` W )
37 26 1 14 36 2 scafval 
 |-  ( ( A e. ( Base ` F ) /\ B e. ( Base ` W ) ) -> ( A ( .sf ` W ) B ) = ( A .x. B ) )
38 23 35 37 syl2anc 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> ( A ( .sf ` W ) B ) = ( A .x. B ) )
39 38 3impa 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> ( A ( .sf ` W ) B ) = ( A .x. B ) )
40 39 mpoeq3dva 
 |-  ( ph -> ( x e. X , y e. Y |-> ( A ( .sf ` W ) B ) ) = ( x e. X , y e. Y |-> ( A .x. B ) ) )
41 36 3 1 4 vscacn 
 |-  ( W e. TopMod -> ( .sf ` W ) e. ( ( K tX J ) Cn J ) )
42 5 41 syl 
 |-  ( ph -> ( .sf ` W ) e. ( ( K tX J ) Cn J ) )
43 6 7 8 9 42 cnmpt22f 
 |-  ( ph -> ( x e. X , y e. Y |-> ( A ( .sf ` W ) B ) ) e. ( ( L tX M ) Cn J ) )
44 40 43 eqeltrrd 
 |-  ( ph -> ( x e. X , y e. Y |-> ( A .x. B ) ) e. ( ( L tX M ) Cn J ) )