Metamath Proof Explorer

Theorem dipcn

Description: Inner product is jointly continuous in both arguments. (Contributed by NM, 21-Aug-2007) (Revised by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

Ref Expression
Hypotheses dipcn.p 
|- P = ( .iOLD ` U )
dipcn.c 
|- C = ( IndMet ` U )
dipcn.j 
|- J = ( MetOpen ` C )
dipcn.k 
|- K = ( TopOpen ` CCfld )
Assertion dipcn 
|- ( U e. NrmCVec -> P e. ( ( J tX J ) Cn K ) )

Proof

Step Hyp Ref Expression
1 dipcn.p 
 |-  P = ( .iOLD ` U )
2 dipcn.c 
 |-  C = ( IndMet ` U )
3 dipcn.j 
 |-  J = ( MetOpen ` C )
4 dipcn.k 
 |-  K = ( TopOpen ` CCfld )
5 eqid 
 |-  ( BaseSet ` U ) = ( BaseSet ` U )
6 eqid 
 |-  ( +v ` U ) = ( +v ` U )
7 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
8 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
9 5 6 7 8 1 dipfval 
 |-  ( U e. NrmCVec -> P = ( x e. ( BaseSet ` U ) , y e. ( BaseSet ` U ) |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) / 4 ) ) )
10 5 2 imsxmet 
 |-  ( U e. NrmCVec -> C e. ( *Met ` ( BaseSet ` U ) ) )
11 3 mopntopon 
 |-  ( C e. ( *Met ` ( BaseSet ` U ) ) -> J e. ( TopOn ` ( BaseSet ` U ) ) )
12 10 11 syl 
 |-  ( U e. NrmCVec -> J e. ( TopOn ` ( BaseSet ` U ) ) )
13 fzfid 
 |-  ( U e. NrmCVec -> ( 1 ... 4 ) e. Fin )
14 12 adantr 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> J e. ( TopOn ` ( BaseSet ` U ) ) )
15 4 cnfldtopon 
 |-  K e. ( TopOn ` CC )
16 15 a1i 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> K e. ( TopOn ` CC ) )
17 ax-icn 
 |-  _i e. CC
18 elfznn 
 |-  ( k e. ( 1 ... 4 ) -> k e. NN )
19 18 adantl 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> k e. NN )
20 19 nnnn0d 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> k e. NN0 )
21 expcl 
 |-  ( ( _i e. CC /\ k e. NN0 ) -> ( _i ^ k ) e. CC )
22 17 20 21 sylancr 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> ( _i ^ k ) e. CC )
23 14 14 16 22 cnmpt2c 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> ( x e. ( BaseSet ` U ) , y e. ( BaseSet ` U ) |-> ( _i ^ k ) ) e. ( ( J tX J ) Cn K ) )
24 14 14 cnmpt1st 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> ( x e. ( BaseSet ` U ) , y e. ( BaseSet ` U ) |-> x ) e. ( ( J tX J ) Cn J ) )
25 14 14 cnmpt2nd 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> ( x e. ( BaseSet ` U ) , y e. ( BaseSet ` U ) |-> y ) e. ( ( J tX J ) Cn J ) )
26 2 3 7 4 smcn 
 |-  ( U e. NrmCVec -> ( .sOLD ` U ) e. ( ( K tX J ) Cn J ) )
27 26 adantr 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> ( .sOLD ` U ) e. ( ( K tX J ) Cn J ) )
28 14 14 23 25 27 cnmpt22f 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> ( x e. ( BaseSet ` U ) , y e. ( BaseSet ` U ) |-> ( ( _i ^ k ) ( .sOLD ` U ) y ) ) e. ( ( J tX J ) Cn J ) )
29 2 3 6 vacn 
 |-  ( U e. NrmCVec -> ( +v ` U ) e. ( ( J tX J ) Cn J ) )
30 29 adantr 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> ( +v ` U ) e. ( ( J tX J ) Cn J ) )
31 14 14 24 28 30 cnmpt22f 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> ( x e. ( BaseSet ` U ) , y e. ( BaseSet ` U ) |-> ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) e. ( ( J tX J ) Cn J ) )
32 8 2 3 4 nmcnc 
 |-  ( U e. NrmCVec -> ( normCV ` U ) e. ( J Cn K ) )
33 32 adantr 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> ( normCV ` U ) e. ( J Cn K ) )
34 14 14 31 33 cnmpt21f 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> ( x e. ( BaseSet ` U ) , y e. ( BaseSet ` U ) |-> ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ) e. ( ( J tX J ) Cn K ) )
35 4 sqcn 
 |-  ( z e. CC |-> ( z ^ 2 ) ) e. ( K Cn K )
36 35 a1i 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> ( z e. CC |-> ( z ^ 2 ) ) e. ( K Cn K ) )
37 oveq1 
 |-  ( z = ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) -> ( z ^ 2 ) = ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) )
38 14 14 34 16 36 37 cnmpt21 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> ( x e. ( BaseSet ` U ) , y e. ( BaseSet ` U ) |-> ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) e. ( ( J tX J ) Cn K ) )
39 4 mulcn 
 |-  x. e. ( ( K tX K ) Cn K )
40 39 a1i 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> x. e. ( ( K tX K ) Cn K ) )
41 14 14 23 38 40 cnmpt22f 
 |-  ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> ( x e. ( BaseSet ` U ) , y e. ( BaseSet ` U ) |-> ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) ) e. ( ( J tX J ) Cn K ) )
42 4 12 13 12 41 fsum2cn 
 |-  ( U e. NrmCVec -> ( x e. ( BaseSet ` U ) , y e. ( BaseSet ` U ) |-> sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) ) e. ( ( J tX J ) Cn K ) )
43 15 a1i 
 |-  ( U e. NrmCVec -> K e. ( TopOn ` CC ) )
44 4cn 
 |-  4 e. CC
45 4ne0 
 |-  4 =/= 0
46 4 divccn 
 |-  ( ( 4 e. CC /\ 4 =/= 0 ) -> ( z e. CC |-> ( z / 4 ) ) e. ( K Cn K ) )
47 44 45 46 mp2an 
 |-  ( z e. CC |-> ( z / 4 ) ) e. ( K Cn K )
48 47 a1i 
 |-  ( U e. NrmCVec -> ( z e. CC |-> ( z / 4 ) ) e. ( K Cn K ) )
49 oveq1 
 |-  ( z = sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) -> ( z / 4 ) = ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) / 4 ) )
50 12 12 42 43 48 49 cnmpt21 
 |-  ( U e. NrmCVec -> ( x e. ( BaseSet ` U ) , y e. ( BaseSet ` U ) |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) / 4 ) ) e. ( ( J tX J ) Cn K ) )
51 9 50 eqeltrd 
 |-  ( U e. NrmCVec -> P e. ( ( J tX J ) Cn K ) )