Metamath Proof Explorer

Theorem nlmvscn

Description: The scalar multiplication of a normed module is continuous. Lemma for nrgtrg and nlmtlm . (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses nlmvscn.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
nlmvscn.sf ⊢ · = ( ·sf ‘ 𝑊 )
nlmvscn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
nlmvscn.kf ⊢ 𝐾 = ( TopOpen ‘ 𝐹 )
Assertion nlmvscn ( 𝑊 ∈ NrmMod → · ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 nlmvscn.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 nlmvscn.sf ⊢ · = ( ·sf ‘ 𝑊 )
3 nlmvscn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
4 nlmvscn.kf ⊢ 𝐾 = ( TopOpen ‘ 𝐹 )
5 nlmlmod ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ LMod )
6 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
7 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
8 6 1 7 2 lmodscaf ⊢ ( 𝑊 ∈ LMod → · : ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝑊 ) ) ⟶ ( Base ‘ 𝑊 ) )
9 5 8 syl ⊢ ( 𝑊 ∈ NrmMod → · : ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝑊 ) ) ⟶ ( Base ‘ 𝑊 ) )
10 eqid ⊢ ( dist ‘ 𝑊 ) = ( dist ‘ 𝑊 )
11 eqid ⊢ ( dist ‘ 𝐹 ) = ( dist ‘ 𝐹 )
12 eqid ⊢ ( norm ‘ 𝑊 ) = ( norm ‘ 𝑊 )
13 eqid ⊢ ( norm ‘ 𝐹 ) = ( norm ‘ 𝐹 )
14 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
15 eqid ⊢ ( ( 𝑟 / 2 ) / ( ( ( norm ‘ 𝐹 ) ‘ 𝑥 ) + 1 ) ) = ( ( 𝑟 / 2 ) / ( ( ( norm ‘ 𝐹 ) ‘ 𝑥 ) + 1 ) )
16 eqid ⊢ ( ( 𝑟 / 2 ) / ( ( ( norm ‘ 𝑊 ) ‘ 𝑦 ) + ( ( 𝑟 / 2 ) / ( ( ( norm ‘ 𝐹 ) ‘ 𝑥 ) + 1 ) ) ) ) = ( ( 𝑟 / 2 ) / ( ( ( norm ‘ 𝑊 ) ‘ 𝑦 ) + ( ( 𝑟 / 2 ) / ( ( ( norm ‘ 𝐹 ) ‘ 𝑥 ) + 1 ) ) ) )
17 simpll ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑊 ∈ NrmMod )
18 simpr ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ+ )
19 simplrl ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑥 ∈ ( Base ‘ 𝐹 ) )
20 simplrr ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
21 1 6 7 10 11 12 13 14 15 16 17 18 19 20 nlmvscnlem1 ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( dist ‘ 𝐹 ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( dist ‘ 𝑊 ) ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) < 𝑟 ) )
22 21 ralrimiva ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( dist ‘ 𝐹 ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( dist ‘ 𝑊 ) ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) < 𝑟 ) )
23 simplrl ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐹 ) )
24 simprl ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐹 ) )
25 23 24 ovresd ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) 𝑧 ) = ( 𝑥 ( dist ‘ 𝐹 ) 𝑧 ) )
26 25 breq1d ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) 𝑧 ) < 𝑠 ↔ ( 𝑥 ( dist ‘ 𝐹 ) 𝑧 ) < 𝑠 ) )
27 simplrr ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
28 simprr ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑤 ∈ ( Base ‘ 𝑊 ) )
29 27 28 ovresd ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) = ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) )
30 29 breq1d ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ↔ ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) < 𝑠 ) )
31 26 30 anbi12d ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( ( 𝑥 ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) ↔ ( ( 𝑥 ( dist ‘ 𝐹 ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) < 𝑠 ) ) )
32 6 1 7 2 14 scafval ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 · 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) )
33 32 ad2antlr ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 · 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) )
34 6 1 7 2 14 scafval ⊢ ( ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑧 · 𝑤 ) = ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) )
35 34 adantl ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑧 · 𝑤 ) = ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) )
36 33 35 oveq12d ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 · 𝑦 ) ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ( 𝑧 · 𝑤 ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) )
37 5 ad2antrr ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑊 ∈ LMod )
38 6 1 14 7 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ ( Base ‘ 𝑊 ) )
39 37 23 27 38 syl3anc ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ ( Base ‘ 𝑊 ) )
40 6 1 14 7 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ∈ ( Base ‘ 𝑊 ) )
41 37 24 28 40 syl3anc ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ∈ ( Base ‘ 𝑊 ) )
42 39 41 ovresd ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( dist ‘ 𝑊 ) ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) )
43 36 42 eqtrd ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 · 𝑦 ) ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ( 𝑧 · 𝑤 ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( dist ‘ 𝑊 ) ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) )
44 43 breq1d ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( ( 𝑥 · 𝑦 ) ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ( 𝑧 · 𝑤 ) ) < 𝑟 ↔ ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( dist ‘ 𝑊 ) ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) < 𝑟 ) )
45 31 44 imbi12d ⊢ ( ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐹 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( ( ( 𝑥 ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 · 𝑦 ) ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ( 𝑧 · 𝑤 ) ) < 𝑟 ) ↔ ( ( ( 𝑥 ( dist ‘ 𝐹 ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( dist ‘ 𝑊 ) ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) < 𝑟 ) ) )
46 45 2ralbidva ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 · 𝑦 ) ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ( 𝑧 · 𝑤 ) ) < 𝑟 ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( dist ‘ 𝐹 ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( dist ‘ 𝑊 ) ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) < 𝑟 ) ) )
47 46 rexbidv ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 · 𝑦 ) ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ( 𝑧 · 𝑤 ) ) < 𝑟 ) ↔ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( dist ‘ 𝐹 ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( dist ‘ 𝑊 ) ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) < 𝑟 ) ) )
48 47 ralbidv ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 · 𝑦 ) ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ( 𝑧 · 𝑤 ) ) < 𝑟 ) ↔ ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( dist ‘ 𝐹 ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( dist ‘ 𝑊 ) ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) < 𝑟 ) ) )
49 22 48 mpbird ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 · 𝑦 ) ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ( 𝑧 · 𝑤 ) ) < 𝑟 ) )
50 49 ralrimivva ⊢ ( 𝑊 ∈ NrmMod → ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 · 𝑦 ) ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ( 𝑧 · 𝑤 ) ) < 𝑟 ) )
51 1 nlmngp2 ⊢ ( 𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp )
52 ngpms ⊢ ( 𝐹 ∈ NrmGrp → 𝐹 ∈ MetSp )
53 51 52 syl ⊢ ( 𝑊 ∈ NrmMod → 𝐹 ∈ MetSp )
54 msxms ⊢ ( 𝐹 ∈ MetSp → 𝐹 ∈ ∞MetSp )
55 eqid ⊢ ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) = ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) )
56 7 55 xmsxmet ⊢ ( 𝐹 ∈ ∞MetSp → ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝐹 ) ) )
57 53 54 56 3syl ⊢ ( 𝑊 ∈ NrmMod → ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝐹 ) ) )
58 nlmngp ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp )
59 ngpms ⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ MetSp )
60 58 59 syl ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ MetSp )
61 msxms ⊢ ( 𝑊 ∈ MetSp → 𝑊 ∈ ∞MetSp )
62 eqid ⊢ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) = ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) )
63 6 62 xmsxmet ⊢ ( 𝑊 ∈ ∞MetSp → ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑊 ) ) )
64 60 61 63 3syl ⊢ ( 𝑊 ∈ NrmMod → ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑊 ) ) )
65 eqid ⊢ ( MetOpen ‘ ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) ) = ( MetOpen ‘ ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) )
66 eqid ⊢ ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) = ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) )
67 65 66 66 txmetcn ⊢ ( ( ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝐹 ) ) ∧ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑊 ) ) ∧ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑊 ) ) ) → ( · ∈ ( ( ( MetOpen ‘ ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) ) ×t ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ) Cn ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ) ↔ ( · : ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝑊 ) ) ⟶ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 · 𝑦 ) ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ( 𝑧 · 𝑤 ) ) < 𝑟 ) ) ) )
68 57 64 64 67 syl3anc ⊢ ( 𝑊 ∈ NrmMod → ( · ∈ ( ( ( MetOpen ‘ ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) ) ×t ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ) Cn ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ) ↔ ( · : ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝑊 ) ) ⟶ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 · 𝑦 ) ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ( 𝑧 · 𝑤 ) ) < 𝑟 ) ) ) )
69 9 50 68 mpbir2and ⊢ ( 𝑊 ∈ NrmMod → · ∈ ( ( ( MetOpen ‘ ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) ) ×t ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ) Cn ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ) )
70 4 7 55 mstopn ⊢ ( 𝐹 ∈ MetSp → 𝐾 = ( MetOpen ‘ ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) ) )
71 53 70 syl ⊢ ( 𝑊 ∈ NrmMod → 𝐾 = ( MetOpen ‘ ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) ) )
72 3 6 62 mstopn ⊢ ( 𝑊 ∈ MetSp → 𝐽 = ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) )
73 60 72 syl ⊢ ( 𝑊 ∈ NrmMod → 𝐽 = ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) )
74 71 73 oveq12d ⊢ ( 𝑊 ∈ NrmMod → ( 𝐾 ×t 𝐽 ) = ( ( MetOpen ‘ ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) ) ×t ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ) )
75 74 73 oveq12d ⊢ ( 𝑊 ∈ NrmMod → ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) = ( ( ( MetOpen ‘ ( ( dist ‘ 𝐹 ) ↾ ( ( Base ‘ 𝐹 ) × ( Base ‘ 𝐹 ) ) ) ) ×t ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ) Cn ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ) )
76 69 75 eleqtrrd ⊢ ( 𝑊 ∈ NrmMod → · ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )