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 ⊢ 𝐽 = ( TopOpen ‘ 𝑆 )
nmhmcn.k ⊢ 𝐾 = ( TopOpen ‘ 𝑇 )
nmhmcn.g ⊢ 𝐺 = ( Scalar ‘ 𝑆 )
nmhmcn.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion nmhmcn ( ( 𝑆 ∈ ( NrmMod ∩ ℂMod ) ∧ 𝑇 ∈ ( NrmMod ∩ ℂMod ) ∧ ℚ ⊆ 𝐵 ) → ( 𝐹 ∈ ( 𝑆 NMHom 𝑇 ) ↔ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ) )

Proof

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