Metamath Proof Explorer

Theorem cnmpt2ip

Description: Continuity of inner product; analogue of cnmpt22f which cannot be used directly because .i is not a function. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses cnmpt1ip.j 
|- J = ( TopOpen ` W )
cnmpt1ip.c 
|- C = ( TopOpen ` CCfld )
cnmpt1ip.h 
|- ., = ( .i ` W )
cnmpt1ip.r 
|- ( ph -> W e. CPreHil )
cnmpt1ip.k 
|- ( ph -> K e. ( TopOn ` X ) )
cnmpt2ip.l 
|- ( ph -> L e. ( TopOn ` Y ) )
cnmpt2ip.a 
|- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( K tX L ) Cn J ) )
cnmpt2ip.b 
|- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( K tX L ) Cn J ) )
Assertion cnmpt2ip 
|- ( ph -> ( x e. X , y e. Y |-> ( A ., B ) ) e. ( ( K tX L ) Cn C ) )

Proof

Step Hyp Ref Expression
1 cnmpt1ip.j 
 |-  J = ( TopOpen ` W )
2 cnmpt1ip.c 
 |-  C = ( TopOpen ` CCfld )
3 cnmpt1ip.h 
 |-  ., = ( .i ` W )
4 cnmpt1ip.r 
 |-  ( ph -> W e. CPreHil )
5 cnmpt1ip.k 
 |-  ( ph -> K e. ( TopOn ` X ) )
6 cnmpt2ip.l 
 |-  ( ph -> L e. ( TopOn ` Y ) )
7 cnmpt2ip.a 
 |-  ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( K tX L ) Cn J ) )
8 cnmpt2ip.b 
 |-  ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( K tX L ) Cn J ) )
9 txtopon 
 |-  ( ( K e. ( TopOn ` X ) /\ L e. ( TopOn ` Y ) ) -> ( K tX L ) e. ( TopOn ` ( X X. Y ) ) )
10 5 6 9 syl2anc 
 |-  ( ph -> ( K tX L ) e. ( TopOn ` ( X X. Y ) ) )
11 cphngp 
 |-  ( W e. CPreHil -> W e. NrmGrp )
12 ngptps 
 |-  ( W e. NrmGrp -> W e. TopSp )
13 4 11 12 3syl 
 |-  ( ph -> W e. TopSp )
14 eqid 
 |-  ( Base ` W ) = ( Base ` W )
15 14 1 istps 
 |-  ( W e. TopSp <-> J e. ( TopOn ` ( Base ` W ) ) )
16 13 15 sylib 
 |-  ( ph -> J e. ( TopOn ` ( Base ` W ) ) )
17 cnf2 
 |-  ( ( ( K tX L ) e. ( TopOn ` ( X X. Y ) ) /\ J e. ( TopOn ` ( Base ` W ) ) /\ ( x e. X , y e. Y |-> A ) e. ( ( K tX L ) Cn J ) ) -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> ( Base ` W ) )
18 10 16 7 17 syl3anc 
 |-  ( ph -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> ( Base ` W ) )
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 ` W ) <-> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> ( Base ` W ) )
21 18 20 sylibr 
 |-  ( ph -> A. x e. X A. y e. Y A e. ( Base ` W ) )
22 21 r19.21bi 
 |-  ( ( ph /\ x e. X ) -> A. y e. Y A e. ( Base ` W ) )
23 22 r19.21bi 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> A e. ( Base ` W ) )
24 cnf2 
 |-  ( ( ( K tX L ) e. ( TopOn ` ( X X. Y ) ) /\ J e. ( TopOn ` ( Base ` W ) ) /\ ( x e. X , y e. Y |-> B ) e. ( ( K tX L ) Cn J ) ) -> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> ( Base ` W ) )
25 10 16 8 24 syl3anc 
 |-  ( ph -> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> ( Base ` W ) )
26 eqid 
 |-  ( x e. X , y e. Y |-> B ) = ( x e. X , y e. Y |-> B )
27 26 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 ) )
28 25 27 sylibr 
 |-  ( ph -> A. x e. X A. y e. Y B e. ( Base ` W ) )
29 28 r19.21bi 
 |-  ( ( ph /\ x e. X ) -> A. y e. Y B e. ( Base ` W ) )
30 29 r19.21bi 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> B e. ( Base ` W ) )
31 eqid 
 |-  ( .if ` W ) = ( .if ` W )
32 14 3 31 ipfval 
 |-  ( ( A e. ( Base ` W ) /\ B e. ( Base ` W ) ) -> ( A ( .if ` W ) B ) = ( A ., B ) )
33 23 30 32 syl2anc 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> ( A ( .if ` W ) B ) = ( A ., B ) )
34 33 3impa 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> ( A ( .if ` W ) B ) = ( A ., B ) )
35 34 mpoeq3dva 
 |-  ( ph -> ( x e. X , y e. Y |-> ( A ( .if ` W ) B ) ) = ( x e. X , y e. Y |-> ( A ., B ) ) )
36 31 1 2 ipcn 
 |-  ( W e. CPreHil -> ( .if ` W ) e. ( ( J tX J ) Cn C ) )
37 4 36 syl 
 |-  ( ph -> ( .if ` W ) e. ( ( J tX J ) Cn C ) )
38 5 6 7 8 37 cnmpt22f 
 |-  ( ph -> ( x e. X , y e. Y |-> ( A ( .if ` W ) B ) ) e. ( ( K tX L ) Cn C ) )
39 35 38 eqeltrrd 
 |-  ( ph -> ( x e. X , y e. Y |-> ( A ., B ) ) e. ( ( K tX L ) Cn C ) )