Metamath Proof Explorer

Theorem nmcvcn

Description: The norm of a normed complex vector space is a continuous function. (Contributed by NM, 16-May-2007) (Proof shortened by Mario Carneiro, 10-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses nmcvcn.1 
|- N = ( normCV ` U )
nmcvcn.2 
|- C = ( IndMet ` U )
nmcvcn.j 
|- J = ( MetOpen ` C )
nmcvcn.k 
|- K = ( topGen ` ran (,) )
Assertion nmcvcn 
|- ( U e. NrmCVec -> N e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 nmcvcn.1 
 |-  N = ( normCV ` U )
2 nmcvcn.2 
 |-  C = ( IndMet ` U )
3 nmcvcn.j 
 |-  J = ( MetOpen ` C )
4 nmcvcn.k 
 |-  K = ( topGen ` ran (,) )
5 eqid 
 |-  ( BaseSet ` U ) = ( BaseSet ` U )
6 5 1 nvf 
 |-  ( U e. NrmCVec -> N : ( BaseSet ` U ) --> RR )
7 simprr 
 |-  ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ e e. RR+ ) ) -> e e. RR+ )
8 5 1 nvcl 
 |-  ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) ) -> ( N ` x ) e. RR )
9 8 ex 
 |-  ( U e. NrmCVec -> ( x e. ( BaseSet ` U ) -> ( N ` x ) e. RR ) )
10 5 1 nvcl 
 |-  ( ( U e. NrmCVec /\ y e. ( BaseSet ` U ) ) -> ( N ` y ) e. RR )
11 10 ex 
 |-  ( U e. NrmCVec -> ( y e. ( BaseSet ` U ) -> ( N ` y ) e. RR ) )
12 9 11 anim12d 
 |-  ( U e. NrmCVec -> ( ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) -> ( ( N ` x ) e. RR /\ ( N ` y ) e. RR ) ) )
13 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
14 13 remet 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( Met ` RR )
15 metcl 
 |-  ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( Met ` RR ) /\ ( N ` x ) e. RR /\ ( N ` y ) e. RR ) -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) e. RR )
16 14 15 mp3an1 
 |-  ( ( ( N ` x ) e. RR /\ ( N ` y ) e. RR ) -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) e. RR )
17 12 16 syl6 
 |-  ( U e. NrmCVec -> ( ( x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) e. RR ) )
18 17 3impib 
 |-  ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) e. RR )
19 5 2 imsmet 
 |-  ( U e. NrmCVec -> C e. ( Met ` ( BaseSet ` U ) ) )
20 metcl 
 |-  ( ( C e. ( Met ` ( BaseSet ` U ) ) /\ x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) -> ( x C y ) e. RR )
21 19 20 syl3an1 
 |-  ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) -> ( x C y ) e. RR )
22 eqid 
 |-  ( +v ` U ) = ( +v ` U )
23 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
24 5 22 23 1 nvabs 
 |-  ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) -> ( abs ` ( ( N ` x ) - ( N ` y ) ) ) <_ ( N ` ( x ( +v ` U ) ( -u 1 ( .sOLD ` U ) y ) ) ) )
25 12 3impib 
 |-  ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) -> ( ( N ` x ) e. RR /\ ( N ` y ) e. RR ) )
26 13 remetdval 
 |-  ( ( ( N ` x ) e. RR /\ ( N ` y ) e. RR ) -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) = ( abs ` ( ( N ` x ) - ( N ` y ) ) ) )
27 25 26 syl 
 |-  ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) = ( abs ` ( ( N ` x ) - ( N ` y ) ) ) )
28 5 22 23 1 2 imsdval2 
 |-  ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) -> ( x C y ) = ( N ` ( x ( +v ` U ) ( -u 1 ( .sOLD ` U ) y ) ) ) )
29 24 27 28 3brtr4d 
 |-  ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) <_ ( x C y ) )
30 18 21 29 jca31 
 |-  ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) /\ y e. ( BaseSet ` U ) ) -> ( ( ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) e. RR /\ ( x C y ) e. RR ) /\ ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) <_ ( x C y ) ) )
31 30 3expa 
 |-  ( ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) ) /\ y e. ( BaseSet ` U ) ) -> ( ( ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) e. RR /\ ( x C y ) e. RR ) /\ ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) <_ ( x C y ) ) )
32 rpre 
 |-  ( e e. RR+ -> e e. RR )
33 lelttr 
 |-  ( ( ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) e. RR /\ ( x C y ) e. RR /\ e e. RR ) -> ( ( ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) <_ ( x C y ) /\ ( x C y ) < e ) -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) < e ) )
34 33 3expa 
 |-  ( ( ( ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) e. RR /\ ( x C y ) e. RR ) /\ e e. RR ) -> ( ( ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) <_ ( x C y ) /\ ( x C y ) < e ) -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) < e ) )
35 34 expdimp 
 |-  ( ( ( ( ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) e. RR /\ ( x C y ) e. RR ) /\ e e. RR ) /\ ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) <_ ( x C y ) ) -> ( ( x C y ) < e -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) < e ) )
36 35 an32s 
 |-  ( ( ( ( ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) e. RR /\ ( x C y ) e. RR ) /\ ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) <_ ( x C y ) ) /\ e e. RR ) -> ( ( x C y ) < e -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) < e ) )
37 31 32 36 syl2an 
 |-  ( ( ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) ) /\ y e. ( BaseSet ` U ) ) /\ e e. RR+ ) -> ( ( x C y ) < e -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) < e ) )
38 37 ex 
 |-  ( ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) ) /\ y e. ( BaseSet ` U ) ) -> ( e e. RR+ -> ( ( x C y ) < e -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) < e ) ) )
39 38 ralrimdva 
 |-  ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) ) -> ( e e. RR+ -> A. y e. ( BaseSet ` U ) ( ( x C y ) < e -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) < e ) ) )
40 39 impr 
 |-  ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ e e. RR+ ) ) -> A. y e. ( BaseSet ` U ) ( ( x C y ) < e -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) < e ) )
41 breq2 
 |-  ( d = e -> ( ( x C y ) < d <-> ( x C y ) < e ) )
42 41 rspceaimv 
 |-  ( ( e e. RR+ /\ A. y e. ( BaseSet ` U ) ( ( x C y ) < e -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) < e ) ) -> E. d e. RR+ A. y e. ( BaseSet ` U ) ( ( x C y ) < d -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) < e ) )
43 7 40 42 syl2anc 
 |-  ( ( U e. NrmCVec /\ ( x e. ( BaseSet ` U ) /\ e e. RR+ ) ) -> E. d e. RR+ A. y e. ( BaseSet ` U ) ( ( x C y ) < d -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) < e ) )
44 43 ralrimivva 
 |-  ( U e. NrmCVec -> A. x e. ( BaseSet ` U ) A. e e. RR+ E. d e. RR+ A. y e. ( BaseSet ` U ) ( ( x C y ) < d -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) < e ) )
45 5 2 imsxmet 
 |-  ( U e. NrmCVec -> C e. ( *Met ` ( BaseSet ` U ) ) )
46 13 rexmet 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )
47 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
48 13 47 tgioo 
 |-  ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
49 4 48 eqtri 
 |-  K = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
50 3 49 metcn 
 |-  ( ( C e. ( *Met ` ( BaseSet ` U ) ) /\ ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) ) -> ( N e. ( J Cn K ) <-> ( N : ( BaseSet ` U ) --> RR /\ A. x e. ( BaseSet ` U ) A. e e. RR+ E. d e. RR+ A. y e. ( BaseSet ` U ) ( ( x C y ) < d -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) < e ) ) ) )
51 45 46 50 sylancl 
 |-  ( U e. NrmCVec -> ( N e. ( J Cn K ) <-> ( N : ( BaseSet ` U ) --> RR /\ A. x e. ( BaseSet ` U ) A. e e. RR+ E. d e. RR+ A. y e. ( BaseSet ` U ) ( ( x C y ) < d -> ( ( N ` x ) ( ( abs o. - ) |` ( RR X. RR ) ) ( N ` y ) ) < e ) ) ) )
52 6 44 51 mpbir2and 
 |-  ( U e. NrmCVec -> N e. ( J Cn K ) )