| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elinel1 4201 | . . . 4
⊢ (𝑆 ∈ (NrmMod ∩
ℂMod) → 𝑆 ∈
NrmMod) | 
| 2 |  | elinel1 4201 | . . . 4
⊢ (𝑇 ∈ (NrmMod ∩
ℂMod) → 𝑇 ∈
NrmMod) | 
| 3 |  | isnmhm 24767 | . . . . 5
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod) ∧ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇)))) | 
| 4 | 3 | baib 535 | . . . 4
⊢ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇)))) | 
| 5 | 1, 2, 4 | syl2an 596 | . . 3
⊢ ((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod)) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇)))) | 
| 6 | 5 | 3adant3 1133 | . 2
⊢ ((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇)))) | 
| 7 |  | nmhmcn.j | . . . . 5
⊢ 𝐽 = (TopOpen‘𝑆) | 
| 8 |  | nmhmcn.k | . . . . 5
⊢ 𝐾 = (TopOpen‘𝑇) | 
| 9 | 7, 8 | nghmcn 24766 | . . . 4
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝐽 Cn 𝐾)) | 
| 10 |  | simpll1 1213 | . . . . . . . . . 10
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑆 ∈ (NrmMod ∩
ℂMod)) | 
| 11 | 10 | elin1d 4204 | . . . . . . . . 9
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑆 ∈ NrmMod) | 
| 12 |  | nlmngp 24698 | . . . . . . . . 9
⊢ (𝑆 ∈ NrmMod → 𝑆 ∈ NrmGrp) | 
| 13 |  | ngpms 24613 | . . . . . . . . 9
⊢ (𝑆 ∈ NrmGrp → 𝑆 ∈ MetSp) | 
| 14 | 11, 12, 13 | 3syl 18 | . . . . . . . 8
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑆 ∈ MetSp) | 
| 15 |  | msxms 24464 | . . . . . . . 8
⊢ (𝑆 ∈ MetSp → 𝑆 ∈
∞MetSp) | 
| 16 |  | eqid 2737 | . . . . . . . . 9
⊢
(Base‘𝑆) =
(Base‘𝑆) | 
| 17 |  | eqid 2737 | . . . . . . . . 9
⊢
((dist‘𝑆)
↾ ((Base‘𝑆)
× (Base‘𝑆))) =
((dist‘𝑆) ↾
((Base‘𝑆) ×
(Base‘𝑆))) | 
| 18 | 16, 17 | xmsxmet 24466 | . . . . . . . 8
⊢ (𝑆 ∈ ∞MetSp →
((dist‘𝑆) ↾
((Base‘𝑆) ×
(Base‘𝑆))) ∈
(∞Met‘(Base‘𝑆))) | 
| 19 | 14, 15, 18 | 3syl 18 | . . . . . . 7
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))) ∈
(∞Met‘(Base‘𝑆))) | 
| 20 |  | simpr 484 | . . . . . . . . 9
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝐽 Cn 𝐾)) | 
| 21 |  | simpll2 1214 | . . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑇 ∈ (NrmMod ∩
ℂMod)) | 
| 22 | 21 | elin1d 4204 | . . . . . . . . . . . . 13
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑇 ∈ NrmMod) | 
| 23 |  | nlmngp 24698 | . . . . . . . . . . . . 13
⊢ (𝑇 ∈ NrmMod → 𝑇 ∈ NrmGrp) | 
| 24 |  | ngpms 24613 | . . . . . . . . . . . . 13
⊢ (𝑇 ∈ NrmGrp → 𝑇 ∈ MetSp) | 
| 25 | 22, 23, 24 | 3syl 18 | . . . . . . . . . . . 12
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑇 ∈ MetSp) | 
| 26 |  | msxms 24464 | . . . . . . . . . . . 12
⊢ (𝑇 ∈ MetSp → 𝑇 ∈
∞MetSp) | 
| 27 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
(Base‘𝑇) =
(Base‘𝑇) | 
| 28 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
((dist‘𝑇)
↾ ((Base‘𝑇)
× (Base‘𝑇))) =
((dist‘𝑇) ↾
((Base‘𝑇) ×
(Base‘𝑇))) | 
| 29 | 27, 28 | xmsxmet 24466 | . . . . . . . . . . . 12
⊢ (𝑇 ∈ ∞MetSp →
((dist‘𝑇) ↾
((Base‘𝑇) ×
(Base‘𝑇))) ∈
(∞Met‘(Base‘𝑇))) | 
| 30 | 25, 26, 29 | 3syl 18 | . . . . . . . . . . 11
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈
(∞Met‘(Base‘𝑇))) | 
| 31 |  | nlmlmod 24699 | . . . . . . . . . . . 12
⊢ (𝑇 ∈ NrmMod → 𝑇 ∈ LMod) | 
| 32 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
(0g‘𝑇) = (0g‘𝑇) | 
| 33 | 27, 32 | lmod0vcl 20889 | . . . . . . . . . . . 12
⊢ (𝑇 ∈ LMod →
(0g‘𝑇)
∈ (Base‘𝑇)) | 
| 34 | 22, 31, 33 | 3syl 18 | . . . . . . . . . . 11
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (0g‘𝑇) ∈ (Base‘𝑇)) | 
| 35 |  | 1rp 13038 | . . . . . . . . . . . 12
⊢ 1 ∈
ℝ+ | 
| 36 |  | rpxr 13044 | . . . . . . . . . . . 12
⊢ (1 ∈
ℝ+ → 1 ∈ ℝ*) | 
| 37 | 35, 36 | mp1i 13 | . . . . . . . . . . 11
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 1 ∈
ℝ*) | 
| 38 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))) = (MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))) | 
| 39 | 38 | blopn 24513 | . . . . . . . . . . 11
⊢
((((dist‘𝑇)
↾ ((Base‘𝑇)
× (Base‘𝑇)))
∈ (∞Met‘(Base‘𝑇)) ∧ (0g‘𝑇) ∈ (Base‘𝑇) ∧ 1 ∈
ℝ*) → ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ∈
(MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))) | 
| 40 | 30, 34, 37, 39 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ∈
(MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))) | 
| 41 | 8, 27, 28 | mstopn 24462 | . . . . . . . . . . 11
⊢ (𝑇 ∈ MetSp → 𝐾 =
(MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))) | 
| 42 | 22, 23, 24, 41 | 4syl 19 | . . . . . . . . . 10
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 = (MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))) | 
| 43 | 40, 42 | eleqtrrd 2844 | . . . . . . . . 9
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ∈ 𝐾) | 
| 44 |  | cnima 23273 | . . . . . . . . 9
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ∈ 𝐾) → (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ∈ 𝐽) | 
| 45 | 20, 43, 44 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ∈ 𝐽) | 
| 46 | 7, 16, 17 | mstopn 24462 | . . . . . . . . 9
⊢ (𝑆 ∈ MetSp → 𝐽 =
(MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))) | 
| 47 | 11, 12, 13, 46 | 4syl 19 | . . . . . . . 8
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 = (MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))) | 
| 48 | 45, 47 | eleqtrd 2843 | . . . . . . 7
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ∈
(MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))) | 
| 49 |  | nlmlmod 24699 | . . . . . . . . 9
⊢ (𝑆 ∈ NrmMod → 𝑆 ∈ LMod) | 
| 50 |  | eqid 2737 | . . . . . . . . . 10
⊢
(0g‘𝑆) = (0g‘𝑆) | 
| 51 | 16, 50 | lmod0vcl 20889 | . . . . . . . . 9
⊢ (𝑆 ∈ LMod →
(0g‘𝑆)
∈ (Base‘𝑆)) | 
| 52 | 11, 49, 51 | 3syl 18 | . . . . . . . 8
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (0g‘𝑆) ∈ (Base‘𝑆)) | 
| 53 |  | lmghm 21030 | . . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | 
| 54 | 53 | ad2antlr 727 | . . . . . . . . . 10
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | 
| 55 | 50, 32 | ghmid 19240 | . . . . . . . . . 10
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) | 
| 56 | 54, 55 | syl 17 | . . . . . . . . 9
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) | 
| 57 | 35 | a1i 11 | . . . . . . . . . 10
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 1 ∈
ℝ+) | 
| 58 |  | blcntr 24423 | . . . . . . . . . 10
⊢
((((dist‘𝑇)
↾ ((Base‘𝑇)
× (Base‘𝑇)))
∈ (∞Met‘(Base‘𝑇)) ∧ (0g‘𝑇) ∈ (Base‘𝑇) ∧ 1 ∈
ℝ+) → (0g‘𝑇) ∈ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) | 
| 59 | 30, 34, 57, 58 | syl3anc 1373 | . . . . . . . . 9
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (0g‘𝑇) ∈
((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) | 
| 60 | 56, 59 | eqeltrd 2841 | . . . . . . . 8
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹‘(0g‘𝑆)) ∈
((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) | 
| 61 | 16, 27 | lmhmf 21033 | . . . . . . . . . 10
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) | 
| 62 | 61 | ad2antlr 727 | . . . . . . . . 9
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) | 
| 63 |  | ffn 6736 | . . . . . . . . 9
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → 𝐹 Fn (Base‘𝑆)) | 
| 64 |  | elpreima 7078 | . . . . . . . . 9
⊢ (𝐹 Fn (Base‘𝑆) →
((0g‘𝑆)
∈ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ↔
((0g‘𝑆)
∈ (Base‘𝑆) ∧
(𝐹‘(0g‘𝑆)) ∈
((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)))) | 
| 65 | 62, 63, 64 | 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)))) | 
| 66 | 52, 60, 65 | mpbir2and 713 | . . . . . . 7
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (0g‘𝑆) ∈ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))) | 
| 67 |  | eqid 2737 | . . . . . . . 8
⊢
(MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))) = (MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))) | 
| 68 | 67 | mopni2 24506 | . . . . . . 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))) | 
| 69 | 19, 48, 66, 68 | syl3anc 1373 | . . . . . 6
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ∃𝑥 ∈ ℝ+
((0g‘𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) ⊆ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))) | 
| 70 |  | simpl1 1192 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑆 ∈ (NrmMod ∩
ℂMod)) | 
| 71 | 70 | elin1d 4204 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑆 ∈ NrmMod) | 
| 72 | 71, 12 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑆 ∈ NrmGrp) | 
| 73 | 72 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑆 ∈ NrmGrp) | 
| 74 | 73 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑆 ∈ NrmGrp) | 
| 75 |  | ngpgrp 24612 | . . . . . . . . . . . . . . . 16
⊢ (𝑆 ∈ NrmGrp → 𝑆 ∈ Grp) | 
| 76 | 74, 75 | syl 17 | . . . . . . . . . . . . . . 15
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑆 ∈ Grp) | 
| 77 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑦 ∈ (Base‘𝑆)) | 
| 78 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢
(norm‘𝑆) =
(norm‘𝑆) | 
| 79 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢
(dist‘𝑆) =
(dist‘𝑆) | 
| 80 | 78, 16, 50, 79, 17 | nmval2 24605 | . . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ Grp ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑆)‘𝑦) = (𝑦((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))(0g‘𝑆))) | 
| 81 | 76, 77, 80 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑆)‘𝑦) = (𝑦((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))(0g‘𝑆))) | 
| 82 | 19 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))) ∈
(∞Met‘(Base‘𝑆))) | 
| 83 | 52 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) →
(0g‘𝑆)
∈ (Base‘𝑆)) | 
| 84 |  | xmetsym 24357 | . . . . . . . . . . . . . . 15
⊢
((((dist‘𝑆)
↾ ((Base‘𝑆)
× (Base‘𝑆)))
∈ (∞Met‘(Base‘𝑆)) ∧ 𝑦 ∈ (Base‘𝑆) ∧ (0g‘𝑆) ∈ (Base‘𝑆)) → (𝑦((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))(0g‘𝑆)) = ((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦)) | 
| 85 | 82, 77, 83, 84 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑦((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))(0g‘𝑆)) = ((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦)) | 
| 86 | 81, 85 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑆)‘𝑦) = ((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦)) | 
| 87 | 86 | breq1d 5153 | . . . . . . . . . . . 12
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((norm‘𝑆)‘𝑦) < 𝑥 ↔ ((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥)) | 
| 88 | 87 | biimpd 229 | . . . . . . . . . . 11
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((norm‘𝑆)‘𝑦) < 𝑥 → ((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥)) | 
| 89 | 62 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) | 
| 90 |  | elpreima 7078 | . . . . . . . . . . . . 13
⊢ (𝐹 Fn (Base‘𝑆) → (𝑦 ∈ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ↔ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) ∈ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)))) | 
| 91 | 89, 63, 90 | 3syl 18 | . . . . . . . . . . . 12
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑦 ∈ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ↔ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) ∈ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)))) | 
| 92 | 30 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈
(∞Met‘(Base‘𝑇))) | 
| 93 | 34 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) →
(0g‘𝑇)
∈ (Base‘𝑇)) | 
| 94 | 35, 36 | mp1i 13 | . . . . . . . . . . . . . . 15
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 1 ∈
ℝ*) | 
| 95 |  | elbl 24398 | . . . . . . . . . . . . . . 15
⊢
((((dist‘𝑇)
↾ ((Base‘𝑇)
× (Base‘𝑇)))
∈ (∞Met‘(Base‘𝑇)) ∧ (0g‘𝑇) ∈ (Base‘𝑇) ∧ 1 ∈
ℝ*) → ((𝐹‘𝑦) ∈ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ↔ ((𝐹‘𝑦) ∈ (Base‘𝑇) ∧ ((0g‘𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 1))) | 
| 96 | 92, 93, 94, 95 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹‘𝑦) ∈ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) ↔ ((𝐹‘𝑦) ∈ (Base‘𝑇) ∧ ((0g‘𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 1))) | 
| 97 |  | simpl2 1193 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑇 ∈ (NrmMod ∩
ℂMod)) | 
| 98 | 97 | elin1d 4204 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑇 ∈ NrmMod) | 
| 99 | 98, 23 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → 𝑇 ∈ NrmGrp) | 
| 100 | 99 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑇 ∈ NrmGrp) | 
| 101 | 100 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑇 ∈ NrmGrp) | 
| 102 |  | simplr 769 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝑆 LMHom 𝑇)) | 
| 103 | 102 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → 𝐹 ∈ (𝑆 LMHom 𝑇)) | 
| 104 | 103, 61 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) | 
| 105 | 104 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘𝑦) ∈ (Base‘𝑇)) | 
| 106 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . 19
⊢
(norm‘𝑇) =
(norm‘𝑇) | 
| 107 | 27, 106 | nmcl 24629 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑇 ∈ NrmGrp ∧ (𝐹‘𝑦) ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝐹‘𝑦)) ∈ ℝ) | 
| 108 | 101, 105,
107 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑇)‘(𝐹‘𝑦)) ∈ ℝ) | 
| 109 |  | 1re 11261 | . . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ | 
| 110 |  | ltle 11349 | . . . . . . . . . . . . . . . . 17
⊢
((((norm‘𝑇)‘(𝐹‘𝑦)) ∈ ℝ ∧ 1 ∈ ℝ)
→ (((norm‘𝑇)‘(𝐹‘𝑦)) < 1 → ((norm‘𝑇)‘(𝐹‘𝑦)) ≤ 1)) | 
| 111 | 108, 109,
110 | sylancl 586 | . . . . . . . . . . . . . . . 16
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((norm‘𝑇)‘(𝐹‘𝑦)) < 1 → ((norm‘𝑇)‘(𝐹‘𝑦)) ≤ 1)) | 
| 112 |  | ngpgrp 24612 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ NrmGrp → 𝑇 ∈ Grp) | 
| 113 | 101, 112 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑇 ∈ Grp) | 
| 114 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . 20
⊢
(dist‘𝑇) =
(dist‘𝑇) | 
| 115 | 106, 27, 32, 114, 28 | nmval2 24605 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑇 ∈ Grp ∧ (𝐹‘𝑦) ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝐹‘𝑦)) = ((𝐹‘𝑦)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(0g‘𝑇))) | 
| 116 | 113, 105,
115 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑇)‘(𝐹‘𝑦)) = ((𝐹‘𝑦)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(0g‘𝑇))) | 
| 117 |  | xmetsym 24357 | . . . . . . . . . . . . . . . . . . 19
⊢
((((dist‘𝑇)
↾ ((Base‘𝑇)
× (Base‘𝑇)))
∈ (∞Met‘(Base‘𝑇)) ∧ (𝐹‘𝑦) ∈ (Base‘𝑇) ∧ (0g‘𝑇) ∈ (Base‘𝑇)) → ((𝐹‘𝑦)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(0g‘𝑇)) = ((0g‘𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦))) | 
| 118 | 92, 105, 93, 117 | syl3anc 1373 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹‘𝑦)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(0g‘𝑇)) = ((0g‘𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦))) | 
| 119 | 116, 118 | eqtrd 2777 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((norm‘𝑇)‘(𝐹‘𝑦)) = ((0g‘𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦))) | 
| 120 | 119 | breq1d 5153 | . . . . . . . . . . . . . . . 16
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((norm‘𝑇)‘(𝐹‘𝑦)) < 1 ↔ ((0g‘𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 1)) | 
| 121 |  | 1red 11262 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 1 ∈
ℝ) | 
| 122 |  | simplr 769 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑥 ∈ ℝ+) | 
| 123 | 108, 121,
122 | lediv1d 13123 | . . . . . . . . . . . . . . . 16
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((norm‘𝑇)‘(𝐹‘𝑦)) ≤ 1 ↔ (((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥))) | 
| 124 | 111, 120,
123 | 3imtr3d 293 | . . . . . . . . . . . . . . 15
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) →
(((0g‘𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 1 → (((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥))) | 
| 125 | 124 | adantld 490 | . . . . . . . . . . . . . 14
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (((𝐹‘𝑦) ∈ (Base‘𝑇) ∧ ((0g‘𝑇)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 1) → (((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥))) | 
| 126 | 96, 125 | sylbid 240 | . . . . . . . . . . . . 13
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹‘𝑦) ∈ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1) →
(((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥))) | 
| 127 | 126 | adantld 490 | . . . . . . . . . . . 12
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) ∈ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) →
(((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥))) | 
| 128 | 91, 127 | sylbid 240 | . . . . . . . . . . 11
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑦 ∈ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) →
(((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥))) | 
| 129 | 88, 128 | imim12d 81 | . . . . . . . . . 10
⊢
((((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ (Base‘𝑆)) →
((((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥 → 𝑦 ∈ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))) →
(((norm‘𝑆)‘𝑦) < 𝑥 → (((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥)))) | 
| 130 | 129 | ralimdva 3167 | . . . . . . . . 9
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) →
(∀𝑦 ∈
(Base‘𝑆)(((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥 → 𝑦 ∈ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1))) → ∀𝑦 ∈ (Base‘𝑆)(((norm‘𝑆)‘𝑦) < 𝑥 → (((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥)))) | 
| 131 |  | rpxr 13044 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ*) | 
| 132 |  | blval 24396 | . . . . . . . . . . . 12
⊢
((((dist‘𝑆)
↾ ((Base‘𝑆)
× (Base‘𝑆)))
∈ (∞Met‘(Base‘𝑆)) ∧ (0g‘𝑆) ∈ (Base‘𝑆) ∧ 𝑥 ∈ ℝ*) →
((0g‘𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) = {𝑦 ∈ (Base‘𝑆) ∣ ((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥}) | 
| 133 | 19, 52, 131, 132 | syl2an3an 1424 | . . . . . . . . . . 11
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) →
((0g‘𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) = {𝑦 ∈ (Base‘𝑆) ∣ ((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥}) | 
| 134 | 133 | sseq1d 4015 | . . . . . . . . . 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 4072 | . . . . . . . . . 10
⊢ ({𝑦 ∈ (Base‘𝑆) ∣
((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥} ⊆ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) ↔ ∀𝑦 ∈ (Base‘𝑆)(((0g‘𝑆)((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑥 → 𝑦 ∈ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)))) | 
| 136 | 134, 135 | bitrdi 287 | . . . . . . . . 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 2737 | . . . . . . . . . 10
⊢ (𝑆 normOp 𝑇) = (𝑆 normOp 𝑇) | 
| 138 |  | nmhmcn.g | . . . . . . . . . 10
⊢ 𝐺 = (Scalar‘𝑆) | 
| 139 |  | nmhmcn.b | . . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐺) | 
| 140 | 10 | adantr 480 | . . . . . . . . . 10
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → 𝑆 ∈ (NrmMod ∩
ℂMod)) | 
| 141 | 21 | adantr 480 | . . . . . . . . . 10
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → 𝑇 ∈ (NrmMod ∩
ℂMod)) | 
| 142 |  | rpreccl 13061 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (1 / 𝑥) ∈
ℝ+) | 
| 143 | 142 | adantl 481 | . . . . . . . . . . 11
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℝ+) | 
| 144 | 143 | rpxrd 13078 | . . . . . . . . . 10
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℝ*) | 
| 145 |  | simpr 484 | . . . . . . . . . 10
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) | 
| 146 |  | simpl3 1194 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → ℚ ⊆ 𝐵) | 
| 147 | 146 | ad2antrr 726 | . . . . . . . . . 10
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → ℚ
⊆ 𝐵) | 
| 148 | 137, 16, 78, 106, 138, 139, 140, 141, 103, 144, 145, 147 | nmoleub2b 25151 | . . . . . . . . 9
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → (((𝑆 normOp 𝑇)‘𝐹) ≤ (1 / 𝑥) ↔ ∀𝑦 ∈ (Base‘𝑆)(((norm‘𝑆)‘𝑦) < 𝑥 → (((norm‘𝑇)‘(𝐹‘𝑦)) / 𝑥) ≤ (1 / 𝑥)))) | 
| 149 | 130, 136,
148 | 3imtr4d 294 | . . . . . . . 8
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) →
(((0g‘𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) ⊆ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) → ((𝑆 normOp 𝑇)‘𝐹) ≤ (1 / 𝑥))) | 
| 150 | 73, 100, 54 | 3jca 1129 | . . . . . . . . 9
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇))) | 
| 151 | 142 | rpred 13077 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (1 / 𝑥) ∈
ℝ) | 
| 152 | 137 | bddnghm 24747 | . . . . . . . . . 10
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ ((1 / 𝑥) ∈ ℝ ∧ ((𝑆 normOp 𝑇)‘𝐹) ≤ (1 / 𝑥))) → 𝐹 ∈ (𝑆 NGHom 𝑇)) | 
| 153 | 152 | expr 456 | . . . . . . . . 9
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ (1 / 𝑥) ∈ ℝ) → (((𝑆 normOp 𝑇)‘𝐹) ≤ (1 / 𝑥) → 𝐹 ∈ (𝑆 NGHom 𝑇))) | 
| 154 | 150, 151,
153 | syl2an 596 | . . . . . . . 8
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) → (((𝑆 normOp 𝑇)‘𝐹) ≤ (1 / 𝑥) → 𝐹 ∈ (𝑆 NGHom 𝑇))) | 
| 155 | 149, 154 | syld 47 | . . . . . . 7
⊢
(((((𝑆 ∈
(NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧
ℚ ⊆ 𝐵) ∧
𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ ℝ+) →
(((0g‘𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) ⊆ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) → 𝐹 ∈ (𝑆 NGHom 𝑇))) | 
| 156 | 155 | rexlimdva 3155 | . . . . . 6
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (∃𝑥 ∈ ℝ+
((0g‘𝑆)(ball‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))𝑥) ⊆ (◡𝐹 “ ((0g‘𝑇)(ball‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))1)) → 𝐹 ∈ (𝑆 NGHom 𝑇))) | 
| 157 | 69, 156 | mpd 15 | . . . . 5
⊢ ((((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝑆 NGHom 𝑇)) | 
| 158 | 157 | ex 412 | . . . 4
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹 ∈ (𝑆 NGHom 𝑇))) | 
| 159 | 9, 158 | impbid2 226 | . . 3
⊢ (((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → (𝐹 ∈ (𝑆 NGHom 𝑇) ↔ 𝐹 ∈ (𝐽 Cn 𝐾))) | 
| 160 | 159 | pm5.32da 579 | . 2
⊢ ((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) → ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇)) ↔ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)))) | 
| 161 | 6, 160 | bitrd 279 | 1
⊢ ((𝑆 ∈ (NrmMod ∩
ℂMod) ∧ 𝑇 ∈
(NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)))) |