| 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 𝐾)))) |