Step | Hyp | Ref
| Expression |
1 | | inss1 3795 |
. . . . 5
⊢ (NrmMod
∩ ℂMod) ⊆ NrmMod |
2 | 1 | sseli 3564 |
. . . 4
⊢ (𝑆 ∈ (NrmMod ∩
ℂMod) → 𝑆 ∈
NrmMod) |
3 | 1 | sseli 3564 |
. . . 4
⊢ (𝑇 ∈ (NrmMod ∩
ℂMod) → 𝑇 ∈
NrmMod) |
4 | | isnmhm 22360 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod) ∧ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇)))) |
5 | 4 | baib 942 |
. . . 4
⊢ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇)))) |
6 | 2, 3, 5 | syl2an 493 |
. . 3
⊢ ((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod)) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇)))) |
7 | 6 | 3adant3 1074 |
. 2
⊢ ((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇)))) |
8 | | nmhmcn.j |
. . . . 5
⊢ 𝐽 = (TopOpen‘𝑆) |
9 | | nmhmcn.k |
. . . . 5
⊢ 𝐾 = (TopOpen‘𝑇) |
10 | 8, 9 | nghmcn 22359 |
. . . 4
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
11 | | simpll1 1093 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑆 ∈ (NrmMod ∩
ℂMod)) |
12 | 1, 11 | sseldi 3566 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑆 ∈ NrmMod) |
13 | | nlmngp 22291 |
. . . . . . . . 9
⊢ (𝑆 ∈ NrmMod → 𝑆 ∈ NrmGrp) |
14 | | ngpms 22214 |
. . . . . . . . 9
⊢ (𝑆 ∈ NrmGrp → 𝑆 ∈ MetSp) |
15 | 12, 13, 14 | 3syl 18 |
. . . . . . . 8
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑆 ∈ MetSp) |
16 | | msxms 22069 |
. . . . . . . 8
⊢ (𝑆 ∈ MetSp → 𝑆 ∈
∞MetSp) |
17 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝑆) =
(Base‘𝑆) |
18 | | eqid 2610 |
. . . . . . . . 9
⊢
((dist‘𝑆)
↾ ((Base‘𝑆)
× (Base‘𝑆))) =
((dist‘𝑆) ↾
((Base‘𝑆) ×
(Base‘𝑆))) |
19 | 17, 18 | xmsxmet 22071 |
. . . . . . . 8
⊢ (𝑆 ∈ ∞MetSp →
((dist‘𝑆) ↾
((Base‘𝑆) ×
(Base‘𝑆))) ∈
(∞Met‘(Base‘𝑆))) |
20 | 15, 16, 19 | 3syl 18 |
. . . . . . 7
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))) ∈
(∞Met‘(Base‘𝑆))) |
21 | | simpr 476 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
22 | | simpll2 1094 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑇 ∈ (NrmMod ∩
ℂMod)) |
23 | 1, 22 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑇 ∈ NrmMod) |
24 | | nlmngp 22291 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ NrmMod → 𝑇 ∈ NrmGrp) |
25 | | ngpms 22214 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ NrmGrp → 𝑇 ∈ MetSp) |
26 | 23, 24, 25 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑇 ∈ MetSp) |
27 | | msxms 22069 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ MetSp → 𝑇 ∈
∞MetSp) |
28 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑇) =
(Base‘𝑇) |
29 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
((dist‘𝑇)
↾ ((Base‘𝑇)
× (Base‘𝑇))) =
((dist‘𝑇) ↾
((Base‘𝑇) ×
(Base‘𝑇))) |
30 | 28, 29 | xmsxmet 22071 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ ∞MetSp →
((dist‘𝑇) ↾
((Base‘𝑇) ×
(Base‘𝑇))) ∈
(∞Met‘(Base‘𝑇))) |
31 | 26, 27, 30 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈
(∞Met‘(Base‘𝑇))) |
32 | | nlmlmod 22292 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ NrmMod → 𝑇 ∈ LMod) |
33 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑇) = (0g‘𝑇) |
34 | 28, 33 | lmod0vcl 18715 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ LMod →
(0g‘𝑇)
∈ (Base‘𝑇)) |
35 | 23, 32, 34 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (0g‘𝑇) ∈ (Base‘𝑇)) |
36 | | 1rp 11712 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ+ |
37 | | rpxr 11716 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℝ+ → 1 ∈ ℝ*) |
38 | 36, 37 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 1 ∈
ℝ*) |
39 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))) = (MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))) |
40 | 39 | blopn 22115 |
. . . . . . . . . . 11
⊢
((((dist‘𝑇)
↾ ((Base‘𝑇)
× (Base‘𝑇)))
∈ (∞Met‘(Base‘𝑇)) ∧ (0g‘𝑇) ∈ (Base‘𝑇) ∧ 1 ∈
ℝ*) → ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ∈
(MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))) |
41 | 31, 35, 38, 40 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ∈
(MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))) |
42 | 9, 28, 29 | mstopn 22067 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ MetSp → 𝐾 =
(MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))) |
43 | 23, 24, 25, 42 | 4syl 19 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 = (MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))) |
44 | 41, 43 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ∈ 𝐾) |
45 | | cnima 20879 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ∈ 𝐾) → (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ∈ 𝐽) |
46 | 21, 44, 45 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ∈ 𝐽) |
47 | 8, 17, 18 | mstopn 22067 |
. . . . . . . . 9
⊢ (𝑆 ∈ MetSp → 𝐽 =
(MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))) |
48 | 12, 13, 14, 47 | 4syl 19 |
. . . . . . . 8
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 = (MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))) |
49 | 46, 48 | eleqtrd 2690 |
. . . . . . 7
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ∈
(MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))) |
50 | | nlmlmod 22292 |
. . . . . . . . 9
⊢ (𝑆 ∈ NrmMod → 𝑆 ∈ LMod) |
51 | | eqid 2610 |
. . . . . . . . . 10
⊢
(0g‘𝑆) = (0g‘𝑆) |
52 | 17, 51 | lmod0vcl 18715 |
. . . . . . . . 9
⊢ (𝑆 ∈ LMod →
(0g‘𝑆)
∈ (Base‘𝑆)) |
53 | 12, 50, 52 | 3syl 18 |
. . . . . . . 8
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (0g‘𝑆) ∈ (Base‘𝑆)) |
54 | | lmghm 18852 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
55 | 54 | ad2antlr 759 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
56 | 51, 33 | ghmid 17489 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) |
57 | 55, 56 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) |
58 | 36 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 1 ∈
ℝ+) |
59 | | blcntr 22028 |
. . . . . . . . . 10
⊢
((((dist‘𝑇)
↾ ((Base‘𝑇)
× (Base‘𝑇)))
∈ (∞Met‘(Base‘𝑇)) ∧ (0g‘𝑇) ∈ (Base‘𝑇) ∧ 1 ∈
ℝ+) → (0g‘𝑇) ∈ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) |
60 | 31, 35, 58, 59 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (0g‘𝑇) ∈
((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) |
61 | 57, 60 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹‘(0g‘𝑆)) ∈
((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) |
62 | 17, 28 | lmhmf 18855 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
63 | 62 | ad2antlr 759 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
64 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → 𝐹 Fn (Base‘𝑆)) |
65 | | elpreima 6245 |
. . . . . . . . 9
⊢ (𝐹 Fn (Base‘𝑆) →
((0g‘𝑆)
∈ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ↔
((0g‘𝑆)
∈ (Base‘𝑆) ∧
(𝐹‘(0g‘𝑆)) ∈
((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)))) |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . . 8
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ((0g‘𝑆) ∈ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ↔
((0g‘𝑆)
∈ (Base‘𝑆) ∧
(𝐹‘(0g‘𝑆)) ∈
((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)))) |
67 | 53, 61, 66 | mpbir2and 959 |
. . . . . . 7
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (0g‘𝑆) ∈ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))) |
68 | | eqid 2610 |
. . . . . . . 8
⊢
(MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))) = (MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))) |
69 | 68 | mopni2 22108 |
. . . . . . 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))) |
70 | 20, 49, 67, 69 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ∃𝑥 ∈ ℝ+
((0g‘𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) ⊆ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))) |
71 | | simpl1 1057 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑆 ∈ (NrmMod ∩
ℂMod)) |
72 | 1, 71 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑆 ∈ NrmMod) |
73 | 72, 13 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑆 ∈ NrmGrp) |
74 | 73 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑆 ∈ NrmGrp) |
75 | 74 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑆 ∈ NrmGrp) |
76 | | ngpgrp 22213 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ∈ NrmGrp → 𝑆 ∈ Grp) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑆 ∈ Grp) |
78 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑦 ∈ (Base‘𝑆)) |
79 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(norm‘𝑆) =
(norm‘𝑆) |
80 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(dist‘𝑆) =
(dist‘𝑆) |
81 | 79, 17, 51, 80, 18 | nmval2 22206 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ Grp ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑆)‘𝑦) = (𝑦((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))(0g‘𝑆))) |
82 | 77, 78, 81 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑆)‘𝑦) = (𝑦((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))(0g‘𝑆))) |
83 | 20 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))) ∈
(∞Met‘(Base‘𝑆))) |
84 | 53 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) →
(0g‘𝑆)
∈ (Base‘𝑆)) |
85 | | xmetsym 21962 |
. . . . . . . . . . . . . . 15
⊢
((((dist‘𝑆)
↾ ((Base‘𝑆)
× (Base‘𝑆)))
∈ (∞Met‘(Base‘𝑆)) ∧ 𝑦 ∈ (Base‘𝑆) ∧ (0g‘𝑆) ∈ (Base‘𝑆)) → (𝑦((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))(0g‘𝑆)) = ((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦)) |
86 | 83, 78, 84, 85 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑦((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))(0g‘𝑆)) = ((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦)) |
87 | 82, 86 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑆)‘𝑦) = ((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦)) |
88 | 87 | breq1d 4593 |
. . . . . . . . . . . 12
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((norm‘𝑆)‘𝑦) < 𝑥 ↔ ((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥)) |
89 | 88 | biimpd 218 |
. . . . . . . . . . 11
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((norm‘𝑆)‘𝑦) < 𝑥 → ((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥)) |
90 | 63 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
91 | | elpreima 6245 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn (Base‘𝑆) → (𝑦 ∈ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ↔ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) ∈ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)))) |
92 | 90, 64, 91 | 3syl 18 |
. . . . . . . . . . . 12
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑦 ∈ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ↔ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) ∈ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)))) |
93 | 31 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈
(∞Met‘(Base‘𝑇))) |
94 | 35 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) →
(0g‘𝑇)
∈ (Base‘𝑇)) |
95 | 36, 37 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 1 ∈
ℝ*) |
96 | | elbl 22003 |
. . . . . . . . . . . . . . 15
⊢
((((dist‘𝑇)
↾ ((Base‘𝑇)
× (Base‘𝑇)))
∈ (∞Met‘(Base‘𝑇)) ∧ (0g‘𝑇) ∈ (Base‘𝑇) ∧ 1 ∈
ℝ*) → ((𝐹‘𝑦) ∈ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ↔ ((𝐹‘𝑦) ∈ (Base‘𝑇) ∧ ((0g‘𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 1))) |
97 | 93, 94, 95, 96 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹‘𝑦) ∈ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ↔ ((𝐹‘𝑦) ∈ (Base‘𝑇) ∧ ((0g‘𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 1))) |
98 | | simpl2 1058 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑇 ∈ (NrmMod ∩
ℂMod)) |
99 | 1, 98 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑇 ∈ NrmMod) |
100 | 99, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑇 ∈ NrmGrp) |
101 | 100 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑇 ∈ NrmGrp) |
102 | 101 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑇 ∈ NrmGrp) |
103 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
104 | 103 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
105 | 104, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
106 | 105 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘𝑦) ∈ (Base‘𝑇)) |
107 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(norm‘𝑇) =
(norm‘𝑇) |
108 | 28, 107 | nmcl 22230 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑇 ∈ NrmGrp ∧ (𝐹‘𝑦) ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝐹‘𝑦)) ∈ ℝ) |
109 | 102, 106,
108 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑇)‘(𝐹‘𝑦)) ∈ ℝ) |
110 | | 1re 9918 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ |
111 | | ltle 10005 |
. . . . . . . . . . . . . . . . 17
⊢
((((norm‘𝑇)‘(𝐹‘𝑦)) ∈ ℝ ∧ 1 ∈ ℝ)
→ (((norm‘𝑇)‘(𝐹‘𝑦)) < 1 → ((norm‘𝑇)‘(𝐹‘𝑦)) ≤ 1)) |
112 | 109, 110,
111 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((norm‘𝑇)‘(𝐹‘𝑦)) < 1 → ((norm‘𝑇)‘(𝐹‘𝑦)) ≤ 1)) |
113 | | ngpgrp 22213 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ NrmGrp → 𝑇 ∈ Grp) |
114 | 102, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑇 ∈ Grp) |
115 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(dist‘𝑇) =
(dist‘𝑇) |
116 | 107, 28, 33, 115, 29 | nmval2 22206 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑇 ∈ Grp ∧ (𝐹‘𝑦) ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝐹‘𝑦)) = ((𝐹‘𝑦)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(0g‘𝑇))) |
117 | 114, 106,
116 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑇)‘(𝐹‘𝑦)) = ((𝐹‘𝑦)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(0g‘𝑇))) |
118 | | xmetsym 21962 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((dist‘𝑇)
↾ ((Base‘𝑇)
× (Base‘𝑇)))
∈ (∞Met‘(Base‘𝑇)) ∧ (𝐹‘𝑦) ∈ (Base‘𝑇) ∧ (0g‘𝑇) ∈ (Base‘𝑇)) → ((𝐹‘𝑦)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(0g‘𝑇)) = ((0g‘𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦))) |
119 | 93, 106, 94, 118 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹‘𝑦)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(0g‘𝑇)) = ((0g‘𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦))) |
120 | 117, 119 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑇)‘(𝐹‘𝑦)) = ((0g‘𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦))) |
121 | 120 | breq1d 4593 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((norm‘𝑇)‘(𝐹‘𝑦)) < 1 ↔ ((0g‘𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 1)) |
122 | | 1red 9934 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 1 ∈
ℝ) |
123 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑥 ∈ ℝ+) |
124 | 109, 122,
123 | lediv1d 11794 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((norm‘𝑇)‘(𝐹‘𝑦)) ≤ 1 ↔ (((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥))) |
125 | 112, 121,
124 | 3imtr3d 281 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) →
(((0g‘𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 1 → (((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥))) |
126 | 125 | adantld 482 |
. . . . . . . . . . . . . 14
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((𝐹‘𝑦) ∈ (Base‘𝑇) ∧ ((0g‘𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 1) → (((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥))) |
127 | 97, 126 | sylbid 229 |
. . . . . . . . . . . . 13
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹‘𝑦) ∈ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) →
(((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥))) |
128 | 127 | adantld 482 |
. . . . . . . . . . . 12
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) ∈ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) →
(((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥))) |
129 | 92, 128 | sylbid 229 |
. . . . . . . . . . 11
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑦 ∈ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) →
(((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥))) |
130 | 89, 129 | imim12d 79 |
. . . . . . . . . 10
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) →
((((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥 → 𝑦 ∈ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))) →
(((norm‘𝑆)‘𝑦) < 𝑥 → (((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥)))) |
131 | 130 | ralimdva 2945 |
. . . . . . . . 9
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) →
(∀𝑦 ∈
(Base‘𝑆)(((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥 → 𝑦 ∈ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))) → ∀𝑦 ∈ (Base‘𝑆)(((norm‘𝑆)‘𝑦) < 𝑥 → (((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥)))) |
132 | 20 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) →
((dist‘𝑆) ↾
((Base‘𝑆) ×
(Base‘𝑆))) ∈
(∞Met‘(Base‘𝑆))) |
133 | 53 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) →
(0g‘𝑆)
∈ (Base‘𝑆)) |
134 | | rpxr 11716 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ*) |
135 | 134 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ*) |
136 | | blval 22001 |
. . . . . . . . . . . 12
⊢
((((dist‘𝑆)
↾ ((Base‘𝑆)
× (Base‘𝑆)))
∈ (∞Met‘(Base‘𝑆)) ∧ (0g‘𝑆) ∈ (Base‘𝑆) ∧ 𝑥 ∈ ℝ*) →
((0g‘𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) = {𝑦 ∈ (Base‘𝑆) ∣ ((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥}) |
137 | 132, 133,
135, 136 | syl3anc 1318 |
. . . . . . . . . . 11
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) →
((0g‘𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) = {𝑦 ∈ (Base‘𝑆) ∣ ((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥}) |
138 | 137 | sseq1d 3595 |
. . . . . . . . . 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)))) |
139 | | rabss 3642 |
. . . . . . . . . 10
⊢ ({𝑦 ∈ (Base‘𝑆) ∣
((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥} ⊆ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ↔ ∀𝑦 ∈ (Base‘𝑆)(((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥 → 𝑦 ∈ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)))) |
140 | 138, 139 | syl6bb 275 |
. . . . . . . . 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))))) |
141 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑆 normOp 𝑇) = (𝑆 normOp 𝑇) |
142 | | nmhmcn.g |
. . . . . . . . . 10
⊢ 𝐺 = (Scalar‘𝑆) |
143 | | nmhmcn.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐺) |
144 | 11 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → 𝑆 ∈ (NrmMod ∩
ℂMod)) |
145 | 22 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → 𝑇 ∈ (NrmMod ∩
ℂMod)) |
146 | | rpreccl 11733 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (1 / 𝑥) ∈
ℝ+) |
147 | 146 | adantl 481 |
. . . . . . . . . . 11
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℝ+) |
148 | 147 | rpxrd 11749 |
. . . . . . . . . 10
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℝ*) |
149 | | simpr 476 |
. . . . . . . . . 10
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
150 | | simpl3 1059 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → ℚ ⊆ 𝐵) |
151 | 150 | ad2antrr 758 |
. . . . . . . . . 10
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → ℚ
⊆ 𝐵) |
152 | 141, 17, 79, 107, 142, 143, 144, 145, 104, 148, 149, 151 | nmoleub2b 22726 |
. . . . . . . . 9
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → (((𝑆 normOp 𝑇)‘𝐹) ≤ (1 / 𝑥) ↔ ∀𝑦 ∈ (Base‘𝑆)(((norm‘𝑆)‘𝑦) < 𝑥 → (((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥)))) |
153 | 131, 140,
152 | 3imtr4d 282 |
. . . . . . . 8
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) →
(((0g‘𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) ⊆ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) → ((𝑆 normOp 𝑇)‘𝐹) ≤ (1 / 𝑥))) |
154 | 74, 101, 55 | 3jca 1235 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇))) |
155 | 146 | rpred 11748 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (1 / 𝑥) ∈
ℝ) |
156 | 141 | bddnghm 22340 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ ((1 / 𝑥) ∈ ℝ ∧ ((𝑆 normOp 𝑇)‘𝐹) ≤ (1 / 𝑥))) → 𝐹 ∈ (𝑆 NGHom 𝑇)) |
157 | 156 | expr 641 |
. . . . . . . . 9
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ (1 / 𝑥) ∈ ℝ) → (((𝑆 normOp 𝑇)‘𝐹) ≤ (1 / 𝑥) → 𝐹 ∈ (𝑆 NGHom 𝑇))) |
158 | 154, 155,
157 | syl2an 493 |
. . . . . . . 8
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → (((𝑆 normOp 𝑇)‘𝐹) ≤ (1 / 𝑥) → 𝐹 ∈ (𝑆 NGHom 𝑇))) |
159 | 153, 158 | syld 46 |
. . . . . . 7
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) →
(((0g‘𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) ⊆ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) → 𝐹 ∈ (𝑆 NGHom 𝑇))) |
160 | 159 | rexlimdva 3013 |
. . . . . 6
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (∃𝑥 ∈ ℝ+
((0g‘𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) ⊆ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) → 𝐹 ∈ (𝑆 NGHom 𝑇))) |
161 | 70, 160 | mpd 15 |
. . . . 5
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝑆 NGHom 𝑇)) |
162 | 161 | ex 449 |
. . . 4
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹 ∈ (𝑆 NGHom 𝑇))) |
163 | 10, 162 | impbid2 215 |
. . 3
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → (𝐹 ∈ (𝑆 NGHom 𝑇) ↔ 𝐹 ∈ (𝐽 Cn 𝐾))) |
164 | 163 | pm5.32da 671 |
. 2
⊢ ((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) → ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇)) ↔ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)))) |
165 | 7, 164 | bitrd 267 |
1
⊢ ((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)))) |