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	$⊢ F = Scalar (W)$
	nlmvscn.sf	$⊢ \underset{˙}{\cdot} = \cdot_{𝑠𝑓} (W)$
	nlmvscn.j	$⊢ J = TopOpen (W)$
	nlmvscn.kf	$⊢ K = TopOpen (F)$
Assertion	nlmvscn	$⊢ W \in NrmMod \to \underset{˙}{\cdot} \in ((K \times_{t} J) Cn J)$

Proof

Step	Hyp	Ref	Expression
1		nlmvscn.f	$⊢ F = Scalar (W)$
2		nlmvscn.sf	$⊢ \underset{˙}{\cdot} = \cdot_{𝑠𝑓} (W)$
3		nlmvscn.j	$⊢ J = TopOpen (W)$
4		nlmvscn.kf	$⊢ K = TopOpen (F)$
5		nlmlmod	$⊢ W \in NrmMod \to W \in LMod$
6		eqid	$⊢ {Base}_{W} = {Base}_{W}$
7		eqid	$⊢ {Base}_{F} = {Base}_{F}$
8	6 1 7 2	lmodscaf	$⊢ W \in LMod \to \underset{˙}{\cdot} : {Base}_{F} \times {Base}_{W} ⟶ {Base}_{W}$
9	5 8	syl	$⊢ W \in NrmMod \to \underset{˙}{\cdot} : {Base}_{F} \times {Base}_{W} ⟶ {Base}_{W}$
10		eqid	$⊢ dist (W) = dist (W)$
11		eqid	$⊢ dist (F) = dist (F)$
12		eqid	$⊢ norm (W) = norm (W)$
13		eqid	$⊢ norm (F) = norm (F)$
14		eqid	$⊢ \cdot_{W} = \cdot_{W}$
15		eqid	$⊢ \frac{\frac{r}{2}}{norm (F) (x) + 1} = \frac{\frac{r}{2}}{norm (F) (x) + 1}$
16		eqid	$⊢ \frac{\frac{r}{2}}{norm (W) (y) + (\frac{\frac{r}{2}}{norm (F) (x) + 1})} = \frac{\frac{r}{2}}{norm (W) (y) + (\frac{\frac{r}{2}}{norm (F) (x) + 1})}$
17		simpll	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land r \in ℝ^{+}) \to W \in NrmMod$
18		simpr	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land r \in ℝ^{+}) \to r \in ℝ^{+}$
19		simplrl	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land r \in ℝ^{+}) \to x \in {Base}_{F}$
20		simplrr	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land r \in ℝ^{+}) \to y \in {Base}_{W}$
21	1 6 7 10 11 12 13 14 15 16 17 18 19 20	nlmvscnlem1	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land r \in ℝ^{+}) \to \exists s \in ℝ^{+} \forall z \in {Base}_{F} \forall w \in {Base}_{W} ((x dist (F) z < s \land y dist (W) w < s) \to (x \cdot_{W} y) dist (W) (z \cdot_{W} w) < r)$
22	21	ralrimiva	$⊢ (W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \to \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in {Base}_{F} \forall w \in {Base}_{W} ((x dist (F) z < s \land y dist (W) w < s) \to (x \cdot_{W} y) dist (W) (z \cdot_{W} w) < r)$
23		simplrl	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to x \in {Base}_{F}$
24		simprl	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to z \in {Base}_{F}$
25	23 24	ovresd	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to x ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}) z = x dist (F) z$
26	25	breq1d	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to (x ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}) z < s \leftrightarrow x dist (F) z < s)$
27		simplrr	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to y \in {Base}_{W}$
28		simprr	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to w \in {Base}_{W}$
29	27 28	ovresd	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w = y dist (W) w$
30	29	breq1d	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to (y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s \leftrightarrow y dist (W) w < s)$
31	26 30	anbi12d	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to ((x ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \leftrightarrow (x dist (F) z < s \land y dist (W) w < s))$
32	6 1 7 2 14	scafval	$⊢ (x \in {Base}_{F} \land y \in {Base}_{W}) \to x \underset{˙}{\cdot} y = x \cdot_{W} y$
33	32	ad2antlr	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to x \underset{˙}{\cdot} y = x \cdot_{W} y$
34	6 1 7 2 14	scafval	$⊢ (z \in {Base}_{F} \land w \in {Base}_{W}) \to z \underset{˙}{\cdot} w = z \cdot_{W} w$
35	34	adantl	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to z \underset{˙}{\cdot} w = z \cdot_{W} w$
36	33 35	oveq12d	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to (x \underset{˙}{\cdot} y) ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) (z \underset{˙}{\cdot} w) = (x \cdot_{W} y) ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) (z \cdot_{W} w)$
37	5	ad2antrr	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to W \in LMod$
38	6 1 14 7	lmodvscl	$⊢ (W \in LMod \land x \in {Base}_{F} \land y \in {Base}_{W}) \to x \cdot_{W} y \in {Base}_{W}$
39	37 23 27 38	syl3anc	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to x \cdot_{W} y \in {Base}_{W}$
40	6 1 14 7	lmodvscl	$⊢ (W \in LMod \land z \in {Base}_{F} \land w \in {Base}_{W}) \to z \cdot_{W} w \in {Base}_{W}$
41	37 24 28 40	syl3anc	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to z \cdot_{W} w \in {Base}_{W}$
42	39 41	ovresd	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to (x \cdot_{W} y) ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) (z \cdot_{W} w) = (x \cdot_{W} y) dist (W) (z \cdot_{W} w)$
43	36 42	eqtrd	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to (x \underset{˙}{\cdot} y) ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) (z \underset{˙}{\cdot} w) = (x \cdot_{W} y) dist (W) (z \cdot_{W} w)$
44	43	breq1d	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to ((x \underset{˙}{\cdot} y) ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) (z \underset{˙}{\cdot} w) < r \leftrightarrow (x \cdot_{W} y) dist (W) (z \cdot_{W} w) < r)$
45	31 44	imbi12d	$⊢ ((W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \land (z \in {Base}_{F} \land w \in {Base}_{W})) \to (((x ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \to (x \underset{˙}{\cdot} y) ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) (z \underset{˙}{\cdot} w) < r) \leftrightarrow ((x dist (F) z < s \land y dist (W) w < s) \to (x \cdot_{W} y) dist (W) (z \cdot_{W} w) < r))$
46	45	2ralbidva	$⊢ (W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \to (\forall z \in {Base}_{F} \forall w \in {Base}_{W} ((x ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \to (x \underset{˙}{\cdot} y) ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) (z \underset{˙}{\cdot} w) < r) \leftrightarrow \forall z \in {Base}_{F} \forall w \in {Base}_{W} ((x dist (F) z < s \land y dist (W) w < s) \to (x \cdot_{W} y) dist (W) (z \cdot_{W} w) < r))$
47	46	rexbidv	$⊢ (W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \to (\exists s \in ℝ^{+} \forall z \in {Base}_{F} \forall w \in {Base}_{W} ((x ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \to (x \underset{˙}{\cdot} y) ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) (z \underset{˙}{\cdot} w) < r) \leftrightarrow \exists s \in ℝ^{+} \forall z \in {Base}_{F} \forall w \in {Base}_{W} ((x dist (F) z < s \land y dist (W) w < s) \to (x \cdot_{W} y) dist (W) (z \cdot_{W} w) < r))$
48	47	ralbidv	$⊢ (W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \to (\forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in {Base}_{F} \forall w \in {Base}_{W} ((x ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \to (x \underset{˙}{\cdot} y) ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) (z \underset{˙}{\cdot} w) < r) \leftrightarrow \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in {Base}_{F} \forall w \in {Base}_{W} ((x dist (F) z < s \land y dist (W) w < s) \to (x \cdot_{W} y) dist (W) (z \cdot_{W} w) < r))$
49	22 48	mpbird	$⊢ (W \in NrmMod \land (x \in {Base}_{F} \land y \in {Base}_{W})) \to \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in {Base}_{F} \forall w \in {Base}_{W} ((x ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \to (x \underset{˙}{\cdot} y) ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) (z \underset{˙}{\cdot} w) < r)$
50	49	ralrimivva	$⊢ W \in NrmMod \to \forall x \in {Base}_{F} \forall y \in {Base}_{W} \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in {Base}_{F} \forall w \in {Base}_{W} ((x ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \to (x \underset{˙}{\cdot} y) ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) (z \underset{˙}{\cdot} w) < r)$
51	1	nlmngp2	$⊢ W \in NrmMod \to F \in NrmGrp$
52		ngpms	$⊢ F \in NrmGrp \to F \in MetSp$
53	51 52	syl	$⊢ W \in NrmMod \to F \in MetSp$
54		msxms	$⊢ F \in MetSp \to F \in ∞MetSp$
55		eqid	$⊢ {dist (F) ↾}_{({Base}_{F} \times {Base}_{F})} = {dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}$
56	7 55	xmsxmet	$⊢ F \in ∞MetSp \to {dist (F) ↾}_{({Base}_{F} \times {Base}_{F})} \in ∞Met ({Base}_{F})$
57	53 54 56	3syl	$⊢ W \in NrmMod \to {dist (F) ↾}_{({Base}_{F} \times {Base}_{F})} \in ∞Met ({Base}_{F})$
58		nlmngp	$⊢ W \in NrmMod \to W \in NrmGrp$
59		ngpms	$⊢ W \in NrmGrp \to W \in MetSp$
60	58 59	syl	$⊢ W \in NrmMod \to W \in MetSp$
61		msxms	$⊢ W \in MetSp \to W \in ∞MetSp$
62		eqid	$⊢ {dist (W) ↾}_{({Base}_{W} \times {Base}_{W})} = {dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}$
63	6 62	xmsxmet	$⊢ W \in ∞MetSp \to {dist (W) ↾}_{({Base}_{W} \times {Base}_{W})} \in ∞Met ({Base}_{W})$
64	60 61 63	3syl	$⊢ W \in NrmMod \to {dist (W) ↾}_{({Base}_{W} \times {Base}_{W})} \in ∞Met ({Base}_{W})$
65		eqid	$⊢ MetOpen ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}) = MetOpen ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})})$
66		eqid	$⊢ MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) = MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})$
67	65 66 66	txmetcn	$⊢ ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})} \in ∞Met ({Base}_{F}) \land {dist (W) ↾}_{({Base}_{W} \times {Base}_{W})} \in ∞Met ({Base}_{W}) \land {dist (W) ↾}_{({Base}_{W} \times {Base}_{W})} \in ∞Met ({Base}_{W})) \to (\underset{˙}{\cdot} \in ((MetOpen ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}) \times_{t} MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})) Cn MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})) \leftrightarrow (\underset{˙}{\cdot} : {Base}_{F} \times {Base}_{W} ⟶ {Base}_{W} \land \forall x \in {Base}_{F} \forall y \in {Base}_{W} \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in {Base}_{F} \forall w \in {Base}_{W} ((x ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \to (x \underset{˙}{\cdot} y) ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) (z \underset{˙}{\cdot} w) < r)))$
68	57 64 64 67	syl3anc	$⊢ W \in NrmMod \to (\underset{˙}{\cdot} \in ((MetOpen ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}) \times_{t} MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})) Cn MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})) \leftrightarrow (\underset{˙}{\cdot} : {Base}_{F} \times {Base}_{W} ⟶ {Base}_{W} \land \forall x \in {Base}_{F} \forall y \in {Base}_{W} \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in {Base}_{F} \forall w \in {Base}_{W} ((x ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \to (x \underset{˙}{\cdot} y) ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) (z \underset{˙}{\cdot} w) < r)))$
69	9 50 68	mpbir2and	$⊢ W \in NrmMod \to \underset{˙}{\cdot} \in ((MetOpen ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}) \times_{t} MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})) Cn MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}))$
70	4 7 55	mstopn	$⊢ F \in MetSp \to K = MetOpen ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})})$
71	53 70	syl	$⊢ W \in NrmMod \to K = MetOpen ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})})$
72	3 6 62	mstopn	$⊢ W \in MetSp \to J = MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})$
73	60 72	syl	$⊢ W \in NrmMod \to J = MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})$
74	71 73	oveq12d	$⊢ W \in NrmMod \to K \times_{t} J = MetOpen ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}) \times_{t} MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})$
75	74 73	oveq12d	$⊢ W \in NrmMod \to (K \times_{t} J) Cn J = (MetOpen ({dist (F) ↾}_{({Base}_{F} \times {Base}_{F})}) \times_{t} MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})) Cn MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})$
76	69 75	eleqtrrd	$⊢ W \in NrmMod \to \underset{˙}{\cdot} \in ((K \times_{t} J) Cn J)$

Metamath Proof Explorer

Theorem nlmvscn

Proof