This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nmhmcn

Description: A linear operator over a normed subcomplex module is bounded iff it is continuous. (Contributed by Mario Carneiro, 22-Oct-2015)

Ref Expression
Hypotheses nmhmcn.j 
|- J = ( TopOpen ` S )
nmhmcn.k 
|- K = ( TopOpen ` T )
nmhmcn.g 
|- G = ( Scalar ` S )
nmhmcn.b 
|- B = ( Base ` G )
Assertion nmhmcn 
|- ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) -> ( F e. ( S NMHom T ) <-> ( F e. ( S LMHom T ) /\ F e. ( J Cn K ) ) ) )

Proof

Step Hyp Ref Expression
1 nmhmcn.j 
 |-  J = ( TopOpen ` S )
2 nmhmcn.k 
 |-  K = ( TopOpen ` T )
3 nmhmcn.g 
 |-  G = ( Scalar ` S )
4 nmhmcn.b 
 |-  B = ( Base ` G )
5 elinel1 
 |-  ( S e. ( NrmMod i^i CMod ) -> S e. NrmMod )
6 elinel1 
 |-  ( T e. ( NrmMod i^i CMod ) -> T e. NrmMod )
7 isnmhm 
 |-  ( F e. ( S NMHom T ) <-> ( ( S e. NrmMod /\ T e. NrmMod ) /\ ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) ) )
8 7 baib 
 |-  ( ( S e. NrmMod /\ T e. NrmMod ) -> ( F e. ( S NMHom T ) <-> ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) ) )
9 5 6 8 syl2an 
 |-  ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) ) -> ( F e. ( S NMHom T ) <-> ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) ) )
10 9 3adant3 
 |-  ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) -> ( F e. ( S NMHom T ) <-> ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) ) )
11 1 2 nghmcn 
 |-  ( F e. ( S NGHom T ) -> F e. ( J Cn K ) )
12 simpll1 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> S e. ( NrmMod i^i CMod ) )
13 12 elin1d 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> S e. NrmMod )
14 nlmngp 
 |-  ( S e. NrmMod -> S e. NrmGrp )
15 ngpms 
 |-  ( S e. NrmGrp -> S e. MetSp )
16 13 14 15 3syl 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> S e. MetSp )
17 msxms 
 |-  ( S e. MetSp -> S e. *MetSp )
18 eqid 
 |-  ( Base ` S ) = ( Base ` S )
19 eqid 
 |-  ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) = ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) )
20 18 19 xmsxmet 
 |-  ( S e. *MetSp -> ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) e. ( *Met ` ( Base ` S ) ) )
21 16 17 20 3syl 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) e. ( *Met ` ( Base ` S ) ) )
22 simpr 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> F e. ( J Cn K ) )
23 simpll2 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> T e. ( NrmMod i^i CMod ) )
24 23 elin1d 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> T e. NrmMod )
25 nlmngp 
 |-  ( T e. NrmMod -> T e. NrmGrp )
26 ngpms 
 |-  ( T e. NrmGrp -> T e. MetSp )
27 24 25 26 3syl 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> T e. MetSp )
28 msxms 
 |-  ( T e. MetSp -> T e. *MetSp )
29 eqid 
 |-  ( Base ` T ) = ( Base ` T )
30 eqid 
 |-  ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) = ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) )
31 29 30 xmsxmet 
 |-  ( T e. *MetSp -> ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) e. ( *Met ` ( Base ` T ) ) )
32 27 28 31 3syl 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) e. ( *Met ` ( Base ` T ) ) )
33 nlmlmod 
 |-  ( T e. NrmMod -> T e. LMod )
34 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
35 29 34 lmod0vcl 
 |-  ( T e. LMod -> ( 0g ` T ) e. ( Base ` T ) )
36 24 33 35 3syl 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> ( 0g ` T ) e. ( Base ` T ) )
37 1rp 
 |-  1 e. RR+
38 rpxr 
 |-  ( 1 e. RR+ -> 1 e. RR* )
39 37 38 mp1i 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> 1 e. RR* )
40 eqid 
 |-  ( MetOpen ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) = ( MetOpen ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) )
41 40 blopn 
 |-  ( ( ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) e. ( *Met ` ( Base ` T ) ) /\ ( 0g ` T ) e. ( Base ` T ) /\ 1 e. RR* ) -> ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) e. ( MetOpen ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) )
42 32 36 39 41 syl3anc 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) e. ( MetOpen ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) )
43 2 29 30 mstopn 
 |-  ( T e. MetSp -> K = ( MetOpen ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) )
44 24 25 26 43 4syl 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> K = ( MetOpen ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) )
45 42 44 eleqtrrd 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) e. K )
46 cnima 
 |-  ( ( F e. ( J Cn K ) /\ ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) e. K ) -> ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) e. J )
47 22 45 46 syl2anc 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) e. J )
48 1 18 19 mstopn 
 |-  ( S e. MetSp -> J = ( MetOpen ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) )
49 13 14 15 48 4syl 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> J = ( MetOpen ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) )
50 47 49 eleqtrd 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) e. ( MetOpen ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) )
51 nlmlmod 
 |-  ( S e. NrmMod -> S e. LMod )
52 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
53 18 52 lmod0vcl 
 |-  ( S e. LMod -> ( 0g ` S ) e. ( Base ` S ) )
54 13 51 53 3syl 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> ( 0g ` S ) e. ( Base ` S ) )
55 lmghm 
 |-  ( F e. ( S LMHom T ) -> F e. ( S GrpHom T ) )
56 55 ad2antlr 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> F e. ( S GrpHom T ) )
57 52 34 ghmid 
 |-  ( F e. ( S GrpHom T ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
58 56 57 syl 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
59 37 a1i 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> 1 e. RR+ )
60 blcntr 
 |-  ( ( ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) e. ( *Met ` ( Base ` T ) ) /\ ( 0g ` T ) e. ( Base ` T ) /\ 1 e. RR+ ) -> ( 0g ` T ) e. ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) )
61 32 36 59 60 syl3anc 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> ( 0g ` T ) e. ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) )
62 58 61 eqeltrd 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> ( F ` ( 0g ` S ) ) e. ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) )
63 18 29 lmhmf 
 |-  ( F e. ( S LMHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
64 63 ad2antlr 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> F : ( Base ` S ) --> ( Base ` T ) )
65 ffn 
 |-  ( F : ( Base ` S ) --> ( Base ` T ) -> F Fn ( Base ` S ) )
66 elpreima 
 |-  ( F Fn ( Base ` S ) -> ( ( 0g ` S ) e. ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) <-> ( ( 0g ` S ) e. ( Base ` S ) /\ ( F ` ( 0g ` S ) ) e. ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) ) )
67 64 65 66 3syl 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> ( ( 0g ` S ) e. ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) <-> ( ( 0g ` S ) e. ( Base ` S ) /\ ( F ` ( 0g ` S ) ) e. ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) ) )
68 54 62 67 mpbir2and 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> ( 0g ` S ) e. ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) )
69 eqid 
 |-  ( MetOpen ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) = ( MetOpen ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) )
70 69 mopni2 
 |-  ( ( ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) e. ( *Met ` ( Base ` S ) ) /\ ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) e. ( MetOpen ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) /\ ( 0g ` S ) e. ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) ) -> E. x e. RR+ ( ( 0g ` S ) ( ball ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) x ) C_ ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) )
71 21 50 68 70 syl3anc 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> E. x e. RR+ ( ( 0g ` S ) ( ball ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) x ) C_ ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) )
72 simpl1 
 |-  ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) -> S e. ( NrmMod i^i CMod ) )
73 72 elin1d 
 |-  ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) -> S e. NrmMod )
74 73 14 syl 
 |-  ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) -> S e. NrmGrp )
75 74 adantr 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> S e. NrmGrp )
76 75 ad2antrr 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> S e. NrmGrp )
77 ngpgrp 
 |-  ( S e. NrmGrp -> S e. Grp )
78 76 77 syl 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> S e. Grp )
79 simpr 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> y e. ( Base ` S ) )
80 eqid 
 |-  ( norm ` S ) = ( norm ` S )
81 eqid 
 |-  ( dist ` S ) = ( dist ` S )
82 80 18 52 81 19 nmval2 
 |-  ( ( S e. Grp /\ y e. ( Base ` S ) ) -> ( ( norm ` S ) ` y ) = ( y ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ( 0g ` S ) ) )
83 78 79 82 syl2anc 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( norm ` S ) ` y ) = ( y ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ( 0g ` S ) ) )
84 21 ad2antrr 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) e. ( *Met ` ( Base ` S ) ) )
85 54 ad2antrr 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( 0g ` S ) e. ( Base ` S ) )
86 xmetsym 
 |-  ( ( ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) e. ( *Met ` ( Base ` S ) ) /\ y e. ( Base ` S ) /\ ( 0g ` S ) e. ( Base ` S ) ) -> ( y ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ( 0g ` S ) ) = ( ( 0g ` S ) ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) )
87 84 79 85 86 syl3anc 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( y ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ( 0g ` S ) ) = ( ( 0g ` S ) ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) )
88 83 87 eqtrd 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( norm ` S ) ` y ) = ( ( 0g ` S ) ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) )
89 88 breq1d 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( ( norm ` S ) ` y ) < x <-> ( ( 0g ` S ) ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < x ) )
90 89 biimpd 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( ( norm ` S ) ` y ) < x -> ( ( 0g ` S ) ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < x ) )
91 64 ad2antrr 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> F : ( Base ` S ) --> ( Base ` T ) )
92 elpreima 
 |-  ( F Fn ( Base ` S ) -> ( y e. ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) <-> ( y e. ( Base ` S ) /\ ( F ` y ) e. ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) ) )
93 91 65 92 3syl 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( y e. ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) <-> ( y e. ( Base ` S ) /\ ( F ` y ) e. ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) ) )
94 32 ad2antrr 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) e. ( *Met ` ( Base ` T ) ) )
95 36 ad2antrr 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( 0g ` T ) e. ( Base ` T ) )
96 37 38 mp1i 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> 1 e. RR* )
97 elbl 
 |-  ( ( ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) e. ( *Met ` ( Base ` T ) ) /\ ( 0g ` T ) e. ( Base ` T ) /\ 1 e. RR* ) -> ( ( F ` y ) e. ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) <-> ( ( F ` y ) e. ( Base ` T ) /\ ( ( 0g ` T ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) < 1 ) ) )
98 94 95 96 97 syl3anc 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( F ` y ) e. ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) <-> ( ( F ` y ) e. ( Base ` T ) /\ ( ( 0g ` T ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) < 1 ) ) )
99 simpl2 
 |-  ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) -> T e. ( NrmMod i^i CMod ) )
100 99 elin1d 
 |-  ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) -> T e. NrmMod )
101 100 25 syl 
 |-  ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) -> T e. NrmGrp )
102 101 adantr 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> T e. NrmGrp )
103 102 ad2antrr 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> T e. NrmGrp )
104 simplr 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> F e. ( S LMHom T ) )
105 104 adantr 
 |-  ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) -> F e. ( S LMHom T ) )
106 105 63 syl 
 |-  ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) -> F : ( Base ` S ) --> ( Base ` T ) )
107 106 ffvelcdmda 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( F ` y ) e. ( Base ` T ) )
108 eqid 
 |-  ( norm ` T ) = ( norm ` T )
109 29 108 nmcl 
 |-  ( ( T e. NrmGrp /\ ( F ` y ) e. ( Base ` T ) ) -> ( ( norm ` T ) ` ( F ` y ) ) e. RR )
110 103 107 109 syl2anc 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( norm ` T ) ` ( F ` y ) ) e. RR )
111 1re 
 |-  1 e. RR
112 ltle 
 |-  ( ( ( ( norm ` T ) ` ( F ` y ) ) e. RR /\ 1 e. RR ) -> ( ( ( norm ` T ) ` ( F ` y ) ) < 1 -> ( ( norm ` T ) ` ( F ` y ) ) <_ 1 ) )
113 110 111 112 sylancl 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( ( norm ` T ) ` ( F ` y ) ) < 1 -> ( ( norm ` T ) ` ( F ` y ) ) <_ 1 ) )
114 ngpgrp 
 |-  ( T e. NrmGrp -> T e. Grp )
115 103 114 syl 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> T e. Grp )
116 eqid 
 |-  ( dist ` T ) = ( dist ` T )
117 108 29 34 116 30 nmval2 
 |-  ( ( T e. Grp /\ ( F ` y ) e. ( Base ` T ) ) -> ( ( norm ` T ) ` ( F ` y ) ) = ( ( F ` y ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( 0g ` T ) ) )
118 115 107 117 syl2anc 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( norm ` T ) ` ( F ` y ) ) = ( ( F ` y ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( 0g ` T ) ) )
119 xmetsym 
 |-  ( ( ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) e. ( *Met ` ( Base ` T ) ) /\ ( F ` y ) e. ( Base ` T ) /\ ( 0g ` T ) e. ( Base ` T ) ) -> ( ( F ` y ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( 0g ` T ) ) = ( ( 0g ` T ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) )
120 94 107 95 119 syl3anc 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( F ` y ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( 0g ` T ) ) = ( ( 0g ` T ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) )
121 118 120 eqtrd 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( norm ` T ) ` ( F ` y ) ) = ( ( 0g ` T ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) )
122 121 breq1d 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( ( norm ` T ) ` ( F ` y ) ) < 1 <-> ( ( 0g ` T ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) < 1 ) )
123 1red 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> 1 e. RR )
124 simplr 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> x e. RR+ )
125 110 123 124 lediv1d 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( ( norm ` T ) ` ( F ` y ) ) <_ 1 <-> ( ( ( norm ` T ) ` ( F ` y ) ) / x ) <_ ( 1 / x ) ) )
126 113 122 125 3imtr3d 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( ( 0g ` T ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) < 1 -> ( ( ( norm ` T ) ` ( F ` y ) ) / x ) <_ ( 1 / x ) ) )
127 126 adantld 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( ( F ` y ) e. ( Base ` T ) /\ ( ( 0g ` T ) ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ( F ` y ) ) < 1 ) -> ( ( ( norm ` T ) ` ( F ` y ) ) / x ) <_ ( 1 / x ) ) )
128 98 127 sylbid 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( F ` y ) e. ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) -> ( ( ( norm ` T ) ` ( F ` y ) ) / x ) <_ ( 1 / x ) ) )
129 128 adantld 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( y e. ( Base ` S ) /\ ( F ` y ) e. ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) -> ( ( ( norm ` T ) ` ( F ` y ) ) / x ) <_ ( 1 / x ) ) )
130 93 129 sylbid 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( y e. ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) -> ( ( ( norm ` T ) ` ( F ` y ) ) / x ) <_ ( 1 / x ) ) )
131 90 130 imim12d 
 |-  ( ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) /\ y e. ( Base ` S ) ) -> ( ( ( ( 0g ` S ) ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < x -> y e. ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) ) -> ( ( ( norm ` S ) ` y ) < x -> ( ( ( norm ` T ) ` ( F ` y ) ) / x ) <_ ( 1 / x ) ) ) )
132 131 ralimdva 
 |-  ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) -> ( A. y e. ( Base ` S ) ( ( ( 0g ` S ) ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < x -> y e. ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) ) -> A. y e. ( Base ` S ) ( ( ( norm ` S ) ` y ) < x -> ( ( ( norm ` T ) ` ( F ` y ) ) / x ) <_ ( 1 / x ) ) ) )
133 rpxr 
 |-  ( x e. RR+ -> x e. RR* )
134 blval 
 |-  ( ( ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) e. ( *Met ` ( Base ` S ) ) /\ ( 0g ` S ) e. ( Base ` S ) /\ x e. RR* ) -> ( ( 0g ` S ) ( ball ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) x ) = { y e. ( Base ` S ) | ( ( 0g ` S ) ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < x } )
135 21 54 133 134 syl2an3an 
 |-  ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) -> ( ( 0g ` S ) ( ball ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) x ) = { y e. ( Base ` S ) | ( ( 0g ` S ) ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < x } )
136 135 sseq1d 
 |-  ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) -> ( ( ( 0g ` S ) ( ball ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) x ) C_ ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) <-> { y e. ( Base ` S ) | ( ( 0g ` S ) ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < x } C_ ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) ) )
137 rabss 
 |-  ( { y e. ( Base ` S ) | ( ( 0g ` S ) ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < x } C_ ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) <-> A. y e. ( Base ` S ) ( ( ( 0g ` S ) ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < x -> y e. ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) ) )
138 136 137 bitrdi 
 |-  ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) -> ( ( ( 0g ` S ) ( ball ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) x ) C_ ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) <-> A. y e. ( Base ` S ) ( ( ( 0g ` S ) ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) y ) < x -> y e. ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) ) ) )
139 eqid 
 |-  ( S normOp T ) = ( S normOp T )
140 12 adantr 
 |-  ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) -> S e. ( NrmMod i^i CMod ) )
141 23 adantr 
 |-  ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) -> T e. ( NrmMod i^i CMod ) )
142 rpreccl 
 |-  ( x e. RR+ -> ( 1 / x ) e. RR+ )
143 142 adantl 
 |-  ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) -> ( 1 / x ) e. RR+ )
144 143 rpxrd 
 |-  ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) -> ( 1 / x ) e. RR* )
145 simpr 
 |-  ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) -> x e. RR+ )
146 simpl3 
 |-  ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) -> QQ C_ B )
147 146 ad2antrr 
 |-  ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) -> QQ C_ B )
148 139 18 80 108 3 4 140 141 105 144 145 147 nmoleub2b 
 |-  ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) -> ( ( ( S normOp T ) ` F ) <_ ( 1 / x ) <-> A. y e. ( Base ` S ) ( ( ( norm ` S ) ` y ) < x -> ( ( ( norm ` T ) ` ( F ` y ) ) / x ) <_ ( 1 / x ) ) ) )
149 132 138 148 3imtr4d 
 |-  ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) -> ( ( ( 0g ` S ) ( ball ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) x ) C_ ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) -> ( ( S normOp T ) ` F ) <_ ( 1 / x ) ) )
150 75 102 56 3jca 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) )
151 142 rpred 
 |-  ( x e. RR+ -> ( 1 / x ) e. RR )
152 139 bddnghm 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( ( 1 / x ) e. RR /\ ( ( S normOp T ) ` F ) <_ ( 1 / x ) ) ) -> F e. ( S NGHom T ) )
153 152 expr 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( 1 / x ) e. RR ) -> ( ( ( S normOp T ) ` F ) <_ ( 1 / x ) -> F e. ( S NGHom T ) ) )
154 150 151 153 syl2an 
 |-  ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) -> ( ( ( S normOp T ) ` F ) <_ ( 1 / x ) -> F e. ( S NGHom T ) ) )
155 149 154 syld 
 |-  ( ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) /\ x e. RR+ ) -> ( ( ( 0g ` S ) ( ball ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) x ) C_ ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) -> F e. ( S NGHom T ) ) )
156 155 rexlimdva 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> ( E. x e. RR+ ( ( 0g ` S ) ( ball ` ( ( dist ` S ) |` ( ( Base ` S ) X. ( Base ` S ) ) ) ) x ) C_ ( `' F " ( ( 0g ` T ) ( ball ` ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) 1 ) ) -> F e. ( S NGHom T ) ) )
157 71 156 mpd 
 |-  ( ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) /\ F e. ( J Cn K ) ) -> F e. ( S NGHom T ) )
158 157 ex 
 |-  ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) -> ( F e. ( J Cn K ) -> F e. ( S NGHom T ) ) )
159 11 158 impbid2 
 |-  ( ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) /\ F e. ( S LMHom T ) ) -> ( F e. ( S NGHom T ) <-> F e. ( J Cn K ) ) )
160 159 pm5.32da 
 |-  ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) -> ( ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) <-> ( F e. ( S LMHom T ) /\ F e. ( J Cn K ) ) ) )
161 10 160 bitrd 
 |-  ( ( S e. ( NrmMod i^i CMod ) /\ T e. ( NrmMod i^i CMod ) /\ QQ C_ B ) -> ( F e. ( S NMHom T ) <-> ( F e. ( S LMHom T ) /\ F e. ( J Cn K ) ) ) )