Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nmhmcn Structured version   Visualization version   GIF version

Theorem nmhmcn 23716
 Description: A linear operator over a normed subcomplex module is bounded iff it is continuous. (Contributed by Mario Carneiro, 22-Oct-2015.)
Hypotheses
Ref Expression
nmhmcn.j 𝐽 = (TopOpen‘𝑆)
nmhmcn.k 𝐾 = (TopOpen‘𝑇)
nmhmcn.g 𝐺 = (Scalar‘𝑆)
nmhmcn.b 𝐵 = (Base‘𝐺)
Assertion
Ref Expression
nmhmcn ((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝐽 Cn 𝐾))))

Proof of Theorem nmhmcn
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elinel1 4170 . . . 4 (𝑆 ∈ (NrmMod ∩ ℂMod) → 𝑆 ∈ NrmMod)
2 elinel1 4170 . . . 4 (𝑇 ∈ (NrmMod ∩ ℂMod) → 𝑇 ∈ NrmMod)
3 isnmhm 23347 . . . . 5 (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod) ∧ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇))))
43baib 538 . . . 4 ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇))))
51, 2, 4syl2an 597 . . 3 ((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod)) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇))))
653adant3 1126 . 2 ((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇))))
7 nmhmcn.j . . . . 5 𝐽 = (TopOpen‘𝑆)
8 nmhmcn.k . . . . 5 𝐾 = (TopOpen‘𝑇)
97, 8nghmcn 23346 . . . 4 (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝐽 Cn 𝐾))
10 simpll1 1206 . . . . . . . . . 10 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑆 ∈ (NrmMod ∩ ℂMod))
1110elin1d 4173 . . . . . . . . 9 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑆 ∈ NrmMod)
12 nlmngp 23278 . . . . . . . . 9 (𝑆 ∈ NrmMod → 𝑆 ∈ NrmGrp)
13 ngpms 23201 . . . . . . . . 9 (𝑆 ∈ NrmGrp → 𝑆 ∈ MetSp)
1411, 12, 133syl 18 . . . . . . . 8 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑆 ∈ MetSp)
15 msxms 23056 . . . . . . . 8 (𝑆 ∈ MetSp → 𝑆 ∈ ∞MetSp)
16 eqid 2819 . . . . . . . . 9 (Base‘𝑆) = (Base‘𝑆)
17 eqid 2819 . . . . . . . . 9 ((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))) = ((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))
1816, 17xmsxmet 23058 . . . . . . . 8 (𝑆 ∈ ∞MetSp → ((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))) ∈ (∞Met‘(Base‘𝑆)))
1914, 15, 183syl 18 . . . . . . 7 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))) ∈ (∞Met‘(Base‘𝑆)))
20 simpr 487 . . . . . . . . 9 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝐽 Cn 𝐾))
21 simpll2 1207 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑇 ∈ (NrmMod ∩ ℂMod))
2221elin1d 4173 . . . . . . . . . . . . 13 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑇 ∈ NrmMod)
23 nlmngp 23278 . . . . . . . . . . . . 13 (𝑇 ∈ NrmMod → 𝑇 ∈ NrmGrp)
24 ngpms 23201 . . . . . . . . . . . . 13 (𝑇 ∈ NrmGrp → 𝑇 ∈ MetSp)
2522, 23, 243syl 18 . . . . . . . . . . . 12 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑇 ∈ MetSp)
26 msxms 23056 . . . . . . . . . . . 12 (𝑇 ∈ MetSp → 𝑇 ∈ ∞MetSp)
27 eqid 2819 . . . . . . . . . . . . 13 (Base‘𝑇) = (Base‘𝑇)
28 eqid 2819 . . . . . . . . . . . . 13 ((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))) = ((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))
2927, 28xmsxmet 23058 . . . . . . . . . . . 12 (𝑇 ∈ ∞MetSp → ((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈ (∞Met‘(Base‘𝑇)))
3025, 26, 293syl 18 . . . . . . . . . . 11 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈ (∞Met‘(Base‘𝑇)))
31 nlmlmod 23279 . . . . . . . . . . . 12 (𝑇 ∈ NrmMod → 𝑇 ∈ LMod)
32 eqid 2819 . . . . . . . . . . . . 13 (0g𝑇) = (0g𝑇)
3327, 32lmod0vcl 19655 . . . . . . . . . . . 12 (𝑇 ∈ LMod → (0g𝑇) ∈ (Base‘𝑇))
3422, 31, 333syl 18 . . . . . . . . . . 11 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (0g𝑇) ∈ (Base‘𝑇))
35 1rp 12385 . . . . . . . . . . . 12 1 ∈ ℝ+
36 rpxr 12390 . . . . . . . . . . . 12 (1 ∈ ℝ+ → 1 ∈ ℝ*)
3735, 36mp1i 13 . . . . . . . . . . 11 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 1 ∈ ℝ*)
38 eqid 2819 . . . . . . . . . . . 12 (MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))) = (MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))
3938blopn 23102 . . . . . . . . . . 11 ((((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈ (∞Met‘(Base‘𝑇)) ∧ (0g𝑇) ∈ (Base‘𝑇) ∧ 1 ∈ ℝ*) → ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ∈ (MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))))
4030, 34, 37, 39syl3anc 1365 . . . . . . . . . 10 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ∈ (MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))))
418, 27, 28mstopn 23054 . . . . . . . . . . 11 (𝑇 ∈ MetSp → 𝐾 = (MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))))
4222, 23, 24, 414syl 19 . . . . . . . . . 10 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 = (MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))))
4340, 42eleqtrrd 2914 . . . . . . . . 9 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ∈ 𝐾)
44 cnima 21865 . . . . . . . . 9 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ∈ 𝐾) → (𝐹 “ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ∈ 𝐽)
4520, 43, 44syl2anc 586 . . . . . . . 8 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 “ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ∈ 𝐽)
467, 16, 17mstopn 23054 . . . . . . . . 9 (𝑆 ∈ MetSp → 𝐽 = (MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))))
4711, 12, 13, 464syl 19 . . . . . . . 8 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 = (MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))))
4845, 47eleqtrd 2913 . . . . . . 7 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 “ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ∈ (MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))))
49 nlmlmod 23279 . . . . . . . . 9 (𝑆 ∈ NrmMod → 𝑆 ∈ LMod)
50 eqid 2819 . . . . . . . . . 10 (0g𝑆) = (0g𝑆)
5116, 50lmod0vcl 19655 . . . . . . . . 9 (𝑆 ∈ LMod → (0g𝑆) ∈ (Base‘𝑆))
5211, 49, 513syl 18 . . . . . . . 8 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (0g𝑆) ∈ (Base‘𝑆))
53 lmghm 19795 . . . . . . . . . . 11 (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
5453ad2antlr 725 . . . . . . . . . 10 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
5550, 32ghmid 18356 . . . . . . . . . 10 (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹‘(0g𝑆)) = (0g𝑇))
5654, 55syl 17 . . . . . . . . 9 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹‘(0g𝑆)) = (0g𝑇))
5735a1i 11 . . . . . . . . . 10 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 1 ∈ ℝ+)
58 blcntr 23015 . . . . . . . . . 10 ((((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈ (∞Met‘(Base‘𝑇)) ∧ (0g𝑇) ∈ (Base‘𝑇) ∧ 1 ∈ ℝ+) → (0g𝑇) ∈ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))
5930, 34, 57, 58syl3anc 1365 . . . . . . . . 9 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (0g𝑇) ∈ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))
6056, 59eqeltrd 2911 . . . . . . . 8 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹‘(0g𝑆)) ∈ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))
6116, 27lmhmf 19798 . . . . . . . . . 10 (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇))
6261ad2antlr 725 . . . . . . . . 9 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇))
63 ffn 6507 . . . . . . . . 9 (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → 𝐹 Fn (Base‘𝑆))
64 elpreima 6821 . . . . . . . . 9 (𝐹 Fn (Base‘𝑆) → ((0g𝑆) ∈ (𝐹 “ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ↔ ((0g𝑆) ∈ (Base‘𝑆) ∧ (𝐹‘(0g𝑆)) ∈ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))))
6562, 63, 643syl 18 . . . . . . . 8 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ((0g𝑆) ∈ (𝐹 “ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ↔ ((0g𝑆) ∈ (Base‘𝑆) ∧ (𝐹‘(0g𝑆)) ∈ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))))
6652, 60, 65mpbir2and 711 . . . . . . 7 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (0g𝑆) ∈ (𝐹 “ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)))
67 eqid 2819 . . . . . . . 8 (MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))) = (MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))
6867mopni2 23095 . . . . . . 7 ((((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)))
6919, 48, 66, 68syl3anc 1365 . . . . . 6 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ∃𝑥 ∈ ℝ+ ((0g𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) ⊆ (𝐹 “ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)))
70 simpl1 1185 . . . . . . . . . . . . . . . . . . . 20 (((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑆 ∈ (NrmMod ∩ ℂMod))
7170elin1d 4173 . . . . . . . . . . . . . . . . . . 19 (((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑆 ∈ NrmMod)
7271, 12syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑆 ∈ NrmGrp)
7372adantr 483 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑆 ∈ NrmGrp)
7473ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑆 ∈ NrmGrp)
75 ngpgrp 23200 . . . . . . . . . . . . . . . 16 (𝑆 ∈ NrmGrp → 𝑆 ∈ Grp)
7674, 75syl 17 . . . . . . . . . . . . . . 15 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑆 ∈ Grp)
77 simpr 487 . . . . . . . . . . . . . . 15 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑦 ∈ (Base‘𝑆))
78 eqid 2819 . . . . . . . . . . . . . . . 16 (norm‘𝑆) = (norm‘𝑆)
79 eqid 2819 . . . . . . . . . . . . . . . 16 (dist‘𝑆) = (dist‘𝑆)
8078, 16, 50, 79, 17nmval2 23193 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Grp ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑆)‘𝑦) = (𝑦((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))(0g𝑆)))
8176, 77, 80syl2anc 586 . . . . . . . . . . . . . 14 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑆)‘𝑦) = (𝑦((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))(0g𝑆)))
8219ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))) ∈ (∞Met‘(Base‘𝑆)))
8352ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (0g𝑆) ∈ (Base‘𝑆))
84 xmetsym 22949 . . . . . . . . . . . . . . 15 ((((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))) ∈ (∞Met‘(Base‘𝑆)) ∧ 𝑦 ∈ (Base‘𝑆) ∧ (0g𝑆) ∈ (Base‘𝑆)) → (𝑦((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))(0g𝑆)) = ((0g𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦))
8582, 77, 83, 84syl3anc 1365 . . . . . . . . . . . . . 14 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑦((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))(0g𝑆)) = ((0g𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦))
8681, 85eqtrd 2854 . . . . . . . . . . . . 13 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑆)‘𝑦) = ((0g𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦))
8786breq1d 5067 . . . . . . . . . . . 12 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((norm‘𝑆)‘𝑦) < 𝑥 ↔ ((0g𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥))
8887biimpd 231 . . . . . . . . . . 11 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((norm‘𝑆)‘𝑦) < 𝑥 → ((0g𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥))
8962ad2antrr 724 . . . . . . . . . . . . 13 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇))
90 elpreima 6821 . . . . . . . . . . . . 13 (𝐹 Fn (Base‘𝑆) → (𝑦 ∈ (𝐹 “ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ↔ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹𝑦) ∈ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))))
9189, 63, 903syl 18 . . . . . . . . . . . 12 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑦 ∈ (𝐹 “ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ↔ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹𝑦) ∈ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))))
9230ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈ (∞Met‘(Base‘𝑇)))
9334ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (0g𝑇) ∈ (Base‘𝑇))
9435, 36mp1i 13 . . . . . . . . . . . . . . 15 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 1 ∈ ℝ*)
95 elbl 22990 . . . . . . . . . . . . . . 15 ((((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈ (∞Met‘(Base‘𝑇)) ∧ (0g𝑇) ∈ (Base‘𝑇) ∧ 1 ∈ ℝ*) → ((𝐹𝑦) ∈ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ↔ ((𝐹𝑦) ∈ (Base‘𝑇) ∧ ((0g𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹𝑦)) < 1)))
9692, 93, 94, 95syl3anc 1365 . . . . . . . . . . . . . 14 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹𝑦) ∈ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ↔ ((𝐹𝑦) ∈ (Base‘𝑇) ∧ ((0g𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹𝑦)) < 1)))
97 simpl2 1186 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑇 ∈ (NrmMod ∩ ℂMod))
9897elin1d 4173 . . . . . . . . . . . . . . . . . . . . 21 (((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑇 ∈ NrmMod)
9998, 23syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑇 ∈ NrmGrp)
10099adantr 483 . . . . . . . . . . . . . . . . . . 19 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑇 ∈ NrmGrp)
101100ad2antrr 724 . . . . . . . . . . . . . . . . . 18 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑇 ∈ NrmGrp)
102 simplr 767 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝑆 LMHom 𝑇))
103102adantr 483 . . . . . . . . . . . . . . . . . . . 20 (((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → 𝐹 ∈ (𝑆 LMHom 𝑇))
104103, 61syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇))
105104ffvelrnda 6844 . . . . . . . . . . . . . . . . . 18 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹𝑦) ∈ (Base‘𝑇))
106 eqid 2819 . . . . . . . . . . . . . . . . . . 19 (norm‘𝑇) = (norm‘𝑇)
10727, 106nmcl 23217 . . . . . . . . . . . . . . . . . 18 ((𝑇 ∈ NrmGrp ∧ (𝐹𝑦) ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝐹𝑦)) ∈ ℝ)
108101, 105, 107syl2anc 586 . . . . . . . . . . . . . . . . 17 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑇)‘(𝐹𝑦)) ∈ ℝ)
109 1re 10633 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
110 ltle 10721 . . . . . . . . . . . . . . . . 17 ((((norm‘𝑇)‘(𝐹𝑦)) ∈ ℝ ∧ 1 ∈ ℝ) → (((norm‘𝑇)‘(𝐹𝑦)) < 1 → ((norm‘𝑇)‘(𝐹𝑦)) ≤ 1))
111108, 109, 110sylancl 588 . . . . . . . . . . . . . . . 16 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((norm‘𝑇)‘(𝐹𝑦)) < 1 → ((norm‘𝑇)‘(𝐹𝑦)) ≤ 1))
112 ngpgrp 23200 . . . . . . . . . . . . . . . . . . . 20 (𝑇 ∈ NrmGrp → 𝑇 ∈ Grp)
113101, 112syl 17 . . . . . . . . . . . . . . . . . . 19 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑇 ∈ Grp)
114 eqid 2819 . . . . . . . . . . . . . . . . . . . 20 (dist‘𝑇) = (dist‘𝑇)
115106, 27, 32, 114, 28nmval2 23193 . . . . . . . . . . . . . . . . . . 19 ((𝑇 ∈ Grp ∧ (𝐹𝑦) ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝐹𝑦)) = ((𝐹𝑦)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(0g𝑇)))
116113, 105, 115syl2anc 586 . . . . . . . . . . . . . . . . . 18 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑇)‘(𝐹𝑦)) = ((𝐹𝑦)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(0g𝑇)))
117 xmetsym 22949 . . . . . . . . . . . . . . . . . . 19 ((((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈ (∞Met‘(Base‘𝑇)) ∧ (𝐹𝑦) ∈ (Base‘𝑇) ∧ (0g𝑇) ∈ (Base‘𝑇)) → ((𝐹𝑦)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(0g𝑇)) = ((0g𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹𝑦)))
11892, 105, 93, 117syl3anc 1365 . . . . . . . . . . . . . . . . . 18 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹𝑦)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(0g𝑇)) = ((0g𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹𝑦)))
119116, 118eqtrd 2854 . . . . . . . . . . . . . . . . 17 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑇)‘(𝐹𝑦)) = ((0g𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹𝑦)))
120119breq1d 5067 . . . . . . . . . . . . . . . 16 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((norm‘𝑇)‘(𝐹𝑦)) < 1 ↔ ((0g𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹𝑦)) < 1))
121 1red 10634 . . . . . . . . . . . . . . . . 17 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 1 ∈ ℝ)
122 simplr 767 . . . . . . . . . . . . . . . . 17 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑥 ∈ ℝ+)
123108, 121, 122lediv1d 12469 . . . . . . . . . . . . . . . 16 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((norm‘𝑇)‘(𝐹𝑦)) ≤ 1 ↔ (((norm‘𝑇)‘(𝐹𝑦)) / 𝑥) ≤ (1 / 𝑥)))
124111, 120, 1233imtr3d 295 . . . . . . . . . . . . . . 15 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((0g𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹𝑦)) < 1 → (((norm‘𝑇)‘(𝐹𝑦)) / 𝑥) ≤ (1 / 𝑥)))
125124adantld 493 . . . . . . . . . . . . . 14 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((𝐹𝑦) ∈ (Base‘𝑇) ∧ ((0g𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹𝑦)) < 1) → (((norm‘𝑇)‘(𝐹𝑦)) / 𝑥) ≤ (1 / 𝑥)))
12696, 125sylbid 242 . . . . . . . . . . . . 13 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹𝑦) ∈ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) → (((norm‘𝑇)‘(𝐹𝑦)) / 𝑥) ≤ (1 / 𝑥)))
127126adantld 493 . . . . . . . . . . . 12 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝑦 ∈ (Base‘𝑆) ∧ (𝐹𝑦) ∈ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) → (((norm‘𝑇)‘(𝐹𝑦)) / 𝑥) ≤ (1 / 𝑥)))
12891, 127sylbid 242 . . . . . . . . . . 11 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑦 ∈ (𝐹 “ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) → (((norm‘𝑇)‘(𝐹𝑦)) / 𝑥) ≤ (1 / 𝑥)))
12988, 128imim12d 81 . . . . . . . . . 10 ((((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((((0g𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥𝑦 ∈ (𝐹 “ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))) → (((norm‘𝑆)‘𝑦) < 𝑥 → (((norm‘𝑇)‘(𝐹𝑦)) / 𝑥) ≤ (1 / 𝑥))))
130129ralimdva 3175 . . . . . . . . 9 (((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → (∀𝑦 ∈ (Base‘𝑆)(((0g𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥𝑦 ∈ (𝐹 “ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))) → ∀𝑦 ∈ (Base‘𝑆)(((norm‘𝑆)‘𝑦) < 𝑥 → (((norm‘𝑇)‘(𝐹𝑦)) / 𝑥) ≤ (1 / 𝑥))))
131 rpxr 12390 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ∈ ℝ*)
132 blval 22988 . . . . . . . . . . . 12 ((((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))) ∈ (∞Met‘(Base‘𝑆)) ∧ (0g𝑆) ∈ (Base‘𝑆) ∧ 𝑥 ∈ ℝ*) → ((0g𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) = {𝑦 ∈ (Base‘𝑆) ∣ ((0g𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥})
13319, 52, 131, 132syl2an3an 1416 . . . . . . . . . . 11 (((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → ((0g𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) = {𝑦 ∈ (Base‘𝑆) ∣ ((0g𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥})
134133sseq1d 3996 . . . . . . . . . 10 (((((𝑆 ∈ (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))))
135 rabss 4046 . . . . . . . . . 10 ({𝑦 ∈ (Base‘𝑆) ∣ ((0g𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥} ⊆ (𝐹 “ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ↔ ∀𝑦 ∈ (Base‘𝑆)(((0g𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥𝑦 ∈ (𝐹 “ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))))
136134, 135syl6bb 289 . . . . . . . . 9 (((((𝑆 ∈ (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 eqid 2819 . . . . . . . . . 10 (𝑆 normOp 𝑇) = (𝑆 normOp 𝑇)
138 nmhmcn.g . . . . . . . . . 10 𝐺 = (Scalar‘𝑆)
139 nmhmcn.b . . . . . . . . . 10 𝐵 = (Base‘𝐺)
14010adantr 483 . . . . . . . . . 10 (((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → 𝑆 ∈ (NrmMod ∩ ℂMod))
14121adantr 483 . . . . . . . . . 10 (((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → 𝑇 ∈ (NrmMod ∩ ℂMod))
142 rpreccl 12407 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ → (1 / 𝑥) ∈ ℝ+)
143142adantl 484 . . . . . . . . . . 11 (((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℝ+)
144143rpxrd 12424 . . . . . . . . . 10 (((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℝ*)
145 simpr 487 . . . . . . . . . 10 (((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
146 simpl3 1187 . . . . . . . . . . 11 (((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → ℚ ⊆ 𝐵)
147146ad2antrr 724 . . . . . . . . . 10 (((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → ℚ ⊆ 𝐵)
148137, 16, 78, 106, 138, 139, 140, 141, 103, 144, 145, 147nmoleub2b 23714 . . . . . . . . 9 (((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → (((𝑆 normOp 𝑇)‘𝐹) ≤ (1 / 𝑥) ↔ ∀𝑦 ∈ (Base‘𝑆)(((norm‘𝑆)‘𝑦) < 𝑥 → (((norm‘𝑇)‘(𝐹𝑦)) / 𝑥) ≤ (1 / 𝑥))))
149130, 136, 1483imtr4d 296 . . . . . . . 8 (((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → (((0g𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) ⊆ (𝐹 “ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) → ((𝑆 normOp 𝑇)‘𝐹) ≤ (1 / 𝑥)))
15073, 100, 543jca 1122 . . . . . . . . 9 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)))
151142rpred 12423 . . . . . . . . 9 (𝑥 ∈ ℝ+ → (1 / 𝑥) ∈ ℝ)
152137bddnghm 23327 . . . . . . . . . 10 (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ ((1 / 𝑥) ∈ ℝ ∧ ((𝑆 normOp 𝑇)‘𝐹) ≤ (1 / 𝑥))) → 𝐹 ∈ (𝑆 NGHom 𝑇))
153152expr 459 . . . . . . . . 9 (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ (1 / 𝑥) ∈ ℝ) → (((𝑆 normOp 𝑇)‘𝐹) ≤ (1 / 𝑥) → 𝐹 ∈ (𝑆 NGHom 𝑇)))
154150, 151, 153syl2an 597 . . . . . . . 8 (((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → (((𝑆 normOp 𝑇)‘𝐹) ≤ (1 / 𝑥) → 𝐹 ∈ (𝑆 NGHom 𝑇)))
155149, 154syld 47 . . . . . . 7 (((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → (((0g𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) ⊆ (𝐹 “ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) → 𝐹 ∈ (𝑆 NGHom 𝑇)))
156155rexlimdva 3282 . . . . . 6 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (∃𝑥 ∈ ℝ+ ((0g𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) ⊆ (𝐹 “ ((0g𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) → 𝐹 ∈ (𝑆 NGHom 𝑇)))
15769, 156mpd 15 . . . . 5 ((((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝑆 NGHom 𝑇))
158157ex 415 . . . 4 (((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹 ∈ (𝑆 NGHom 𝑇)))
1599, 158impbid2 228 . . 3 (((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → (𝐹 ∈ (𝑆 NGHom 𝑇) ↔ 𝐹 ∈ (𝐽 Cn 𝐾)))
160159pm5.32da 581 . 2 ((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) → ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇)) ↔ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝐽 Cn 𝐾))))
1616, 160bitrd 281 1 ((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝐽 Cn 𝐾))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1081   = wceq 1530   ∈ wcel 2107  ∀wral 3136  ∃wrex 3137  {crab 3140   ∩ cin 3933   ⊆ wss 3934   class class class wbr 5057   × cxp 5546  ◡ccnv 5547   ↾ cres 5550   “ cima 5551   Fn wfn 6343  ⟶wf 6344  ‘cfv 6348  (class class class)co 7148  ℝcr 10528  1c1 10530  ℝ*cxr 10666   < clt 10667   ≤ cle 10668   / cdiv 11289  ℚcq 12340  ℝ+crp 12381  Basecbs 16475  Scalarcsca 16560  distcds 16566  TopOpenctopn 16687  0gc0g 16705  Grpcgrp 18095   GrpHom cghm 18347  LModclmod 19626   LMHom clmhm 19783  ∞Metcxmet 20522  ballcbl 20524  MetOpencmopn 20527   Cn ccn 21824  ∞MetSpcxms 22919  MetSpcms 22920  normcnm 23178  NrmGrpcngp 23179  NrmModcnlm 23182   normOp cnmo 23306   NGHom cnghm 23307   NMHom cnmhm 23308  ℂModcclm 23658 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-oadd 8098  df-er 8281  df-map 8400  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-sup 8898  df-inf 8899  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ico 12736  df-fz 12885  df-seq 13362  df-exp 13422  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-0g 16707  df-topgen 16709  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-grp 18098  df-minusg 18099  df-sbg 18100  df-subg 18268  df-ghm 18348  df-cmn 18900  df-mgp 19232  df-ring 19291  df-cring 19292  df-subrg 19525  df-lmod 19628  df-lmhm 19786  df-psmet 20529  df-xmet 20530  df-met 20531  df-bl 20532  df-mopn 20533  df-cnfld 20538  df-top 21494  df-topon 21511  df-topsp 21533  df-bases 21546  df-cn 21827  df-cnp 21828  df-xms 22922  df-ms 22923  df-nm 23184  df-ngp 23185  df-nlm 23188  df-nmo 23309  df-nghm 23310  df-nmhm 23311  df-clm 23659 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator