Metamath Proof Explorer

Theorem nghmcn

Description: A normed group homomorphism is a continuous function. (Contributed by Mario Carneiro, 20-Oct-2015)

Ref Expression
Hypotheses nghmcn.j 
|- J = ( TopOpen ` S )
nghmcn.k 
|- K = ( TopOpen ` T )
Assertion nghmcn 
|- ( F e. ( S NGHom T ) -> F e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 nghmcn.j 
 |-  J = ( TopOpen ` S )
2 nghmcn.k 
 |-  K = ( TopOpen ` T )
3 nghmghm 
 |-  ( F e. ( S NGHom T ) -> F e. ( S GrpHom T ) )
4 eqid 
 |-  ( Base ` S ) = ( Base ` S )
5 eqid 
 |-  ( Base ` T ) = ( Base ` T )
6 4 5 ghmf 
 |-  ( F e. ( S GrpHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
7 3 6 syl 
 |-  ( F e. ( S NGHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
8 simprr 
 |-  ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) -> r e. RR+ )
9 eqid 
 |-  ( S normOp T ) = ( S normOp T )
10 9 nghmcl 
 |-  ( F e. ( S NGHom T ) -> ( ( S normOp T ) ` F ) e. RR )
11 nghmrcl1 
 |-  ( F e. ( S NGHom T ) -> S e. NrmGrp )
12 nghmrcl2 
 |-  ( F e. ( S NGHom T ) -> T e. NrmGrp )
13 9 nmoge0 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> 0 <_ ( ( S normOp T ) ` F ) )
14 11 12 3 13 syl3anc 
 |-  ( F e. ( S NGHom T ) -> 0 <_ ( ( S normOp T ) ` F ) )
15 10 14 ge0p1rpd 
 |-  ( F e. ( S NGHom T ) -> ( ( ( S normOp T ) ` F ) + 1 ) e. RR+ )
16 15 adantr 
 |-  ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) -> ( ( ( S normOp T ) ` F ) + 1 ) e. RR+ )
17 8 16 rpdivcld 
 |-  ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) -> ( r / ( ( ( S normOp T ) ` F ) + 1 ) ) e. RR+ )
18 ngpms 
 |-  ( S e. NrmGrp -> S e. MetSp )
19 11 18 syl 
 |-  ( F e. ( S NGHom T ) -> S e. MetSp )
20 19 ad2antrr 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> S e. MetSp )
21 simplrl 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> x e. ( Base ` S ) )
22 simpr 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> y e. ( Base ` S ) )
23 eqid 
 |-  ( dist ` S ) = ( dist ` S )
24 4 23 mscl 
 |-  ( ( S e. MetSp /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( dist ` S ) y ) e. RR )
25 20 21 22 24 syl3anc 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( x ( dist ` S ) y ) e. RR )
26 8 adantr 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> r e. RR+ )
27 26 rpred 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> r e. RR )
28 15 ad2antrr 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( ( S normOp T ) ` F ) + 1 ) e. RR+ )
29 25 27 28 ltmuldiv2d 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( ( ( ( S normOp T ) ` F ) + 1 ) x. ( x ( dist ` S ) y ) ) < r <-> ( x ( dist ` S ) y ) < ( r / ( ( ( S normOp T ) ` F ) + 1 ) ) ) )
30 ngpms 
 |-  ( T e. NrmGrp -> T e. MetSp )
31 12 30 syl 
 |-  ( F e. ( S NGHom T ) -> T e. MetSp )
32 31 ad2antrr 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> T e. MetSp )
33 7 ad2antrr 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> F : ( Base ` S ) --> ( Base ` T ) )
34 33 21 ffvelrnd 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( F ` x ) e. ( Base ` T ) )
35 33 22 ffvelrnd 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( F ` y ) e. ( Base ` T ) )
36 eqid 
 |-  ( dist ` T ) = ( dist ` T )
37 5 36 mscl 
 |-  ( ( T e. MetSp /\ ( F ` x ) e. ( Base ` T ) /\ ( F ` y ) e. ( Base ` T ) ) -> ( ( F ` x ) ( dist ` T ) ( F ` y ) ) e. RR )
38 32 34 35 37 syl3anc 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( F ` x ) ( dist ` T ) ( F ` y ) ) e. RR )
39 10 ad2antrr 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( S normOp T ) ` F ) e. RR )
40 39 25 remulcld 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( ( S normOp T ) ` F ) x. ( x ( dist ` S ) y ) ) e. RR )
41 28 rpred 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( ( S normOp T ) ` F ) + 1 ) e. RR )
42 41 25 remulcld 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( ( ( S normOp T ) ` F ) + 1 ) x. ( x ( dist ` S ) y ) ) e. RR )
43 9 4 23 36 nmods 
 |-  ( ( F e. ( S NGHom T ) /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( ( F ` x ) ( dist ` T ) ( F ` y ) ) <_ ( ( ( S normOp T ) ` F ) x. ( x ( dist ` S ) y ) ) )
44 43 3expa 
 |-  ( ( ( F e. ( S NGHom T ) /\ x e. ( Base ` S ) ) /\ y e. ( Base ` S ) ) -> ( ( F ` x ) ( dist ` T ) ( F ` y ) ) <_ ( ( ( S normOp T ) ` F ) x. ( x ( dist ` S ) y ) ) )
45 44 adantlrr 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( F ` x ) ( dist ` T ) ( F ` y ) ) <_ ( ( ( S normOp T ) ` F ) x. ( x ( dist ` S ) y ) ) )
46 msxms 
 |-  ( S e. MetSp -> S e. *MetSp )
47 20 46 syl 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> S e. *MetSp )
48 4 23 xmsge0 
 |-  ( ( S e. *MetSp /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> 0 <_ ( x ( dist ` S ) y ) )
49 47 21 22 48 syl3anc 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> 0 <_ ( x ( dist ` S ) y ) )
50 39 lep1d 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( S normOp T ) ` F ) <_ ( ( ( S normOp T ) ` F ) + 1 ) )
51 39 41 25 49 50 lemul1ad 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( ( S normOp T ) ` F ) x. ( x ( dist ` S ) y ) ) <_ ( ( ( ( S normOp T ) ` F ) + 1 ) x. ( x ( dist ` S ) y ) ) )
52 38 40 42 45 51 letrd 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( F ` x ) ( dist ` T ) ( F ` y ) ) <_ ( ( ( ( S normOp T ) ` F ) + 1 ) x. ( x ( dist ` S ) y ) ) )
53 lelttr 
 |-  ( ( ( ( F ` x ) ( dist ` T ) ( F ` y ) ) e. RR /\ ( ( ( ( S normOp T ) ` F ) + 1 ) x. ( x ( dist ` S ) y ) ) e. RR /\ r e. RR ) -> ( ( ( ( F ` x ) ( dist ` T ) ( F ` y ) ) <_ ( ( ( ( S normOp T ) ` F ) + 1 ) x. ( x ( dist ` S ) y ) ) /\ ( ( ( ( S normOp T ) ` F ) + 1 ) x. ( x ( dist ` S ) y ) ) < r ) -> ( ( F ` x ) ( dist ` T ) ( F ` y ) ) < r ) )
54 38 42 27 53 syl3anc 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( ( ( F ` x ) ( dist ` T ) ( F ` y ) ) <_ ( ( ( ( S normOp T ) ` F ) + 1 ) x. ( x ( dist ` S ) y ) ) /\ ( ( ( ( S normOp T ) ` F ) + 1 ) x. ( x ( dist ` S ) y ) ) < r ) -> ( ( F ` x ) ( dist ` T ) ( F ` y ) ) < r ) )
55 52 54 mpand 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( ( ( ( S normOp T ) ` F ) + 1 ) x. ( x ( dist ` S ) y ) ) < r -> ( ( F ` x ) ( dist ` T ) ( F ` y ) ) < r ) )
56 29 55 sylbird 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( x ( dist ` S ) y ) < ( r / ( ( ( S normOp T ) ` F ) + 1 ) ) -> ( ( F ` x ) ( dist ` T ) ( F ` y ) ) < r ) )
57 21 22 ovresd 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( x ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) = ( x ( dist ` S ) y ) )
58 57 breq1d 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( x ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < ( r / ( ( ( S normOp T ) ` F ) + 1 ) ) <-> ( x ( dist ` S ) y ) < ( r / ( ( ( S normOp T ) ` F ) + 1 ) ) ) )
59 34 35 ovresd 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( F ` x ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) = ( ( F ` x ) ( dist ` T ) ( F ` y ) ) )
60 59 breq1d 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( ( F ` x ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) < r <-> ( ( F ` x ) ( dist ` T ) ( F ` y ) ) < r ) )
61 56 58 60 3imtr4d 
 |-  ( ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) /\ y e. ( Base ` S ) ) -> ( ( x ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < ( r / ( ( ( S normOp T ) ` F ) + 1 ) ) -> ( ( F ` x ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) < r ) )
62 61 ralrimiva 
 |-  ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) -> A. y e. ( Base ` S ) ( ( x ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < ( r / ( ( ( S normOp T ) ` F ) + 1 ) ) -> ( ( F ` x ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) < r ) )
63 breq2 
 |-  ( s = ( r / ( ( ( S normOp T ) ` F ) + 1 ) ) -> ( ( x ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < s <-> ( x ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < ( r / ( ( ( S normOp T ) ` F ) + 1 ) ) ) )
64 63 rspceaimv 
 |-  ( ( ( r / ( ( ( S normOp T ) ` F ) + 1 ) ) e. RR+ /\ A. y e. ( Base ` S ) ( ( x ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < ( r / ( ( ( S normOp T ) ` F ) + 1 ) ) -> ( ( F ` x ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) < r ) ) -> E. s e. RR+ A. y e. ( Base ` S ) ( ( x ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < s -> ( ( F ` x ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) < r ) )
65 17 62 64 syl2anc 
 |-  ( ( F e. ( S NGHom T ) /\ ( x e. ( Base ` S ) /\ r e. RR+ ) ) -> E. s e. RR+ A. y e. ( Base ` S ) ( ( x ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < s -> ( ( F ` x ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) < r ) )
66 65 ralrimivva 
 |-  ( F e. ( S NGHom T ) -> A. x e. ( Base ` S ) A. r e. RR+ E. s e. RR+ A. y e. ( Base ` S ) ( ( x ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < s -> ( ( F ` x ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) < r ) )
67 eqid 
 |-  ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) = ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) )
68 4 67 xmsxmet 
 |-  ( S e. *MetSp -> ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) e. ( *Met ` ( Base ` S ) ) )
69 19 46 68 3syl 
 |-  ( F e. ( S NGHom T ) -> ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) e. ( *Met ` ( Base ` S ) ) )
70 msxms 
 |-  ( T e. MetSp -> T e. *MetSp )
71 eqid 
 |-  ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) = ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) )
72 5 71 xmsxmet 
 |-  ( T e. *MetSp -> ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) e. ( *Met ` ( Base ` T ) ) )
73 31 70 72 3syl 
 |-  ( F e. ( S NGHom T ) -> ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) e. ( *Met ` ( Base ` T ) ) )
74 eqid 
 |-  ( MetOpen ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) = ( MetOpen ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) )
75 eqid 
 |-  ( MetOpen ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) = ( MetOpen ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) )
76 74 75 metcn 
 |-  ( ( ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) e. ( *Met ` ( Base ` S ) ) /\ ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) e. ( *Met ` ( Base ` T ) ) ) -> ( F e. ( ( MetOpen ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) Cn ( MetOpen ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) ) <-> ( F : ( Base ` S ) --> ( Base ` T ) /\ A. x e. ( Base ` S ) A. r e. RR+ E. s e. RR+ A. y e. ( Base ` S ) ( ( x ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < s -> ( ( F ` x ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) < r ) ) ) )
77 69 73 76 syl2anc 
 |-  ( F e. ( S NGHom T ) -> ( F e. ( ( MetOpen ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) Cn ( MetOpen ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) ) <-> ( F : ( Base ` S ) --> ( Base ` T ) /\ A. x e. ( Base ` S ) A. r e. RR+ E. s e. RR+ A. y e. ( Base ` S ) ( ( x ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < s -> ( ( F ` x ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) < r ) ) ) )
78 7 66 77 mpbir2and 
 |-  ( F e. ( S NGHom T ) -> F e. ( ( MetOpen ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) Cn ( MetOpen ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) ) )
79 1 4 67 mstopn 
 |-  ( S e. MetSp -> J = ( MetOpen ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) )
80 19 79 syl 
 |-  ( F e. ( S NGHom T ) -> J = ( MetOpen ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) )
81 2 5 71 mstopn 
 |-  ( T e. MetSp -> K = ( MetOpen ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) )
82 31 81 syl 
 |-  ( F e. ( S NGHom T ) -> K = ( MetOpen ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) )
83 80 82 oveq12d 
 |-  ( F e. ( S NGHom T ) -> ( J Cn K ) = ( ( MetOpen ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) Cn ( MetOpen ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) ) )
84 78 83 eleqtrrd 
 |-  ( F e. ( S NGHom T ) -> F e. ( J Cn K ) )