nlmvscnlem2

Description: Lemma for nlmvscn . Compare this proof with the similar elementary proof mulcn2 for continuity of multiplication on CC . (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	nlmvscn.f	$⊢ F = Scalar (W)$
	nlmvscn.v	$⊢ V = {Base}_{W}$
	nlmvscn.k	$⊢ K = {Base}_{F}$
	nlmvscn.d	$⊢ D = dist (W)$
	nlmvscn.e	$⊢ E = dist (F)$
	nlmvscn.n	$⊢ N = norm (W)$
	nlmvscn.a	$⊢ A = norm (F)$
	nlmvscn.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	nlmvscn.t	$⊢ T = \frac{\frac{R}{2}}{A (B) + 1}$
	nlmvscn.u	$⊢ U = \frac{\frac{R}{2}}{N (X) + T}$
	nlmvscn.w	$⊢ φ \to W \in NrmMod$
	nlmvscn.r	$⊢ φ \to R \in ℝ^{+}$
	nlmvscn.b	$⊢ φ \to B \in K$
	nlmvscn.x	$⊢ φ \to X \in V$
	nlmvscn.c	$⊢ φ \to C \in K$
	nlmvscn.y	$⊢ φ \to Y \in V$
	nlmvscn.1	$⊢ φ \to B E C < U$
	nlmvscn.2	$⊢ φ \to X D Y < T$
Assertion	nlmvscnlem2	$⊢ φ \to (B \underset{˙}{\cdot} X) D (C \underset{˙}{\cdot} Y) < R$

Proof

Step	Hyp	Ref	Expression
1		nlmvscn.f	$⊢ F = Scalar (W)$
2		nlmvscn.v	$⊢ V = {Base}_{W}$
3		nlmvscn.k	$⊢ K = {Base}_{F}$
4		nlmvscn.d	$⊢ D = dist (W)$
5		nlmvscn.e	$⊢ E = dist (F)$
6		nlmvscn.n	$⊢ N = norm (W)$
7		nlmvscn.a	$⊢ A = norm (F)$
8		nlmvscn.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
9		nlmvscn.t	$⊢ T = \frac{\frac{R}{2}}{A (B) + 1}$
10		nlmvscn.u	$⊢ U = \frac{\frac{R}{2}}{N (X) + T}$
11		nlmvscn.w	$⊢ φ \to W \in NrmMod$
12		nlmvscn.r	$⊢ φ \to R \in ℝ^{+}$
13		nlmvscn.b	$⊢ φ \to B \in K$
14		nlmvscn.x	$⊢ φ \to X \in V$
15		nlmvscn.c	$⊢ φ \to C \in K$
16		nlmvscn.y	$⊢ φ \to Y \in V$
17		nlmvscn.1	$⊢ φ \to B E C < U$
18		nlmvscn.2	$⊢ φ \to X D Y < T$
19		nlmngp	$⊢ W \in NrmMod \to W \in NrmGrp$
20	11 19	syl	$⊢ φ \to W \in NrmGrp$
21		ngpms	$⊢ W \in NrmGrp \to W \in MetSp$
22	20 21	syl	$⊢ φ \to W \in MetSp$
23		nlmlmod	$⊢ W \in NrmMod \to W \in LMod$
24	11 23	syl	$⊢ φ \to W \in LMod$
25	2 1 8 3	lmodvscl	$⊢ (W \in LMod \land B \in K \land X \in V) \to B \underset{˙}{\cdot} X \in V$
26	24 13 14 25	syl3anc	$⊢ φ \to B \underset{˙}{\cdot} X \in V$
27	2 1 8 3	lmodvscl	$⊢ (W \in LMod \land C \in K \land Y \in V) \to C \underset{˙}{\cdot} Y \in V$
28	24 15 16 27	syl3anc	$⊢ φ \to C \underset{˙}{\cdot} Y \in V$
29	2 4	mscl	$⊢ (W \in MetSp \land B \underset{˙}{\cdot} X \in V \land C \underset{˙}{\cdot} Y \in V) \to (B \underset{˙}{\cdot} X) D (C \underset{˙}{\cdot} Y) \in ℝ$
30	22 26 28 29	syl3anc	$⊢ φ \to (B \underset{˙}{\cdot} X) D (C \underset{˙}{\cdot} Y) \in ℝ$
31	2 1 8 3	lmodvscl	$⊢ (W \in LMod \land B \in K \land Y \in V) \to B \underset{˙}{\cdot} Y \in V$
32	24 13 16 31	syl3anc	$⊢ φ \to B \underset{˙}{\cdot} Y \in V$
33	2 4	mscl	$⊢ (W \in MetSp \land B \underset{˙}{\cdot} X \in V \land B \underset{˙}{\cdot} Y \in V) \to (B \underset{˙}{\cdot} X) D (B \underset{˙}{\cdot} Y) \in ℝ$
34	22 26 32 33	syl3anc	$⊢ φ \to (B \underset{˙}{\cdot} X) D (B \underset{˙}{\cdot} Y) \in ℝ$
35	2 4	mscl	$⊢ (W \in MetSp \land B \underset{˙}{\cdot} Y \in V \land C \underset{˙}{\cdot} Y \in V) \to (B \underset{˙}{\cdot} Y) D (C \underset{˙}{\cdot} Y) \in ℝ$
36	22 32 28 35	syl3anc	$⊢ φ \to (B \underset{˙}{\cdot} Y) D (C \underset{˙}{\cdot} Y) \in ℝ$
37	34 36	readdcld	$⊢ φ \to ((B \underset{˙}{\cdot} X) D (B \underset{˙}{\cdot} Y)) + ((B \underset{˙}{\cdot} Y) D (C \underset{˙}{\cdot} Y)) \in ℝ$
38	12	rpred	$⊢ φ \to R \in ℝ$
39	2 4	mstri	$⊢ (W \in MetSp \land (B \underset{˙}{\cdot} X \in V \land C \underset{˙}{\cdot} Y \in V \land B \underset{˙}{\cdot} Y \in V)) \to (B \underset{˙}{\cdot} X) D (C \underset{˙}{\cdot} Y) \leq ((B \underset{˙}{\cdot} X) D (B \underset{˙}{\cdot} Y)) + ((B \underset{˙}{\cdot} Y) D (C \underset{˙}{\cdot} Y))$
40	22 26 28 32 39	syl13anc	$⊢ φ \to (B \underset{˙}{\cdot} X) D (C \underset{˙}{\cdot} Y) \leq ((B \underset{˙}{\cdot} X) D (B \underset{˙}{\cdot} Y)) + ((B \underset{˙}{\cdot} Y) D (C \underset{˙}{\cdot} Y))$
41	1	nlmngp2	$⊢ W \in NrmMod \to F \in NrmGrp$
42	11 41	syl	$⊢ φ \to F \in NrmGrp$
43	3 7	nmcl	$⊢ (F \in NrmGrp \land B \in K) \to A (B) \in ℝ$
44	42 13 43	syl2anc	$⊢ φ \to A (B) \in ℝ$
45	3 7	nmge0	$⊢ (F \in NrmGrp \land B \in K) \to 0 \leq A (B)$
46	42 13 45	syl2anc	$⊢ φ \to 0 \leq A (B)$
47	44 46	ge0p1rpd	$⊢ φ \to A (B) + 1 \in ℝ^{+}$
48	47	rpred	$⊢ φ \to A (B) + 1 \in ℝ$
49	2 4	mscl	$⊢ (W \in MetSp \land X \in V \land Y \in V) \to X D Y \in ℝ$
50	22 14 16 49	syl3anc	$⊢ φ \to X D Y \in ℝ$
51	48 50	remulcld	$⊢ φ \to (A (B) + 1) (X D Y) \in ℝ$
52	38	rehalfcld	$⊢ φ \to \frac{R}{2} \in ℝ$
53	2 8 1 3 4 7	nlmdsdi	$⊢ (W \in NrmMod \land (B \in K \land X \in V \land Y \in V)) \to A (B) (X D Y) = (B \underset{˙}{\cdot} X) D (B \underset{˙}{\cdot} Y)$
54	11 13 14 16 53	syl13anc	$⊢ φ \to A (B) (X D Y) = (B \underset{˙}{\cdot} X) D (B \underset{˙}{\cdot} Y)$
55		msxms	$⊢ W \in MetSp \to W \in ∞MetSp$
56	22 55	syl	$⊢ φ \to W \in ∞MetSp$
57	2 4	xmsge0	$⊢ (W \in ∞MetSp \land X \in V \land Y \in V) \to 0 \leq X D Y$
58	56 14 16 57	syl3anc	$⊢ φ \to 0 \leq X D Y$
59	44	lep1d	$⊢ φ \to A (B) \leq A (B) + 1$
60	44 48 50 58 59	lemul1ad	$⊢ φ \to A (B) (X D Y) \leq (A (B) + 1) (X D Y)$
61	54 60	eqbrtrrd	$⊢ φ \to (B \underset{˙}{\cdot} X) D (B \underset{˙}{\cdot} Y) \leq (A (B) + 1) (X D Y)$
62	18 9	breqtrdi	$⊢ φ \to X D Y < \frac{\frac{R}{2}}{A (B) + 1}$
63	50 52 47	ltmuldiv2d	$⊢ φ \to ((A (B) + 1) (X D Y) < \frac{R}{2} \leftrightarrow X D Y < \frac{\frac{R}{2}}{A (B) + 1})$
64	62 63	mpbird	$⊢ φ \to (A (B) + 1) (X D Y) < \frac{R}{2}$
65	34 51 52 61 64	lelttrd	$⊢ φ \to (B \underset{˙}{\cdot} X) D (B \underset{˙}{\cdot} Y) < \frac{R}{2}$
66		ngpms	$⊢ F \in NrmGrp \to F \in MetSp$
67	42 66	syl	$⊢ φ \to F \in MetSp$
68	3 5	mscl	$⊢ (F \in MetSp \land B \in K \land C \in K) \to B E C \in ℝ$
69	67 13 15 68	syl3anc	$⊢ φ \to B E C \in ℝ$
70	2 6	nmcl	$⊢ (W \in NrmGrp \land X \in V) \to N (X) \in ℝ$
71	20 14 70	syl2anc	$⊢ φ \to N (X) \in ℝ$
72	12	rphalfcld	$⊢ φ \to \frac{R}{2} \in ℝ^{+}$
73	72 47	rpdivcld	$⊢ φ \to \frac{\frac{R}{2}}{A (B) + 1} \in ℝ^{+}$
74	9 73	eqeltrid	$⊢ φ \to T \in ℝ^{+}$
75	74	rpred	$⊢ φ \to T \in ℝ$
76	71 75	readdcld	$⊢ φ \to N (X) + T \in ℝ$
77	69 76	remulcld	$⊢ φ \to (B E C) (N (X) + T) \in ℝ$
78	2 8 1 3 4 6 5	nlmdsdir	$⊢ (W \in NrmMod \land (B \in K \land C \in K \land Y \in V)) \to (B E C) N (Y) = (B \underset{˙}{\cdot} Y) D (C \underset{˙}{\cdot} Y)$
79	11 13 15 16 78	syl13anc	$⊢ φ \to (B E C) N (Y) = (B \underset{˙}{\cdot} Y) D (C \underset{˙}{\cdot} Y)$
80	2 6	nmcl	$⊢ (W \in NrmGrp \land Y \in V) \to N (Y) \in ℝ$
81	20 16 80	syl2anc	$⊢ φ \to N (Y) \in ℝ$
82		msxms	$⊢ F \in MetSp \to F \in ∞MetSp$
83	67 82	syl	$⊢ φ \to F \in ∞MetSp$
84	3 5	xmsge0	$⊢ (F \in ∞MetSp \land B \in K \land C \in K) \to 0 \leq B E C$
85	83 13 15 84	syl3anc	$⊢ φ \to 0 \leq B E C$
86	81 71	resubcld	$⊢ φ \to N (Y) - N (X) \in ℝ$
87		eqid	$⊢ -_{W} = -_{W}$
88	2 6 87	nm2dif	$⊢ (W \in NrmGrp \land Y \in V \land X \in V) \to N (Y) - N (X) \leq N (Y -_{W} X)$
89	20 16 14 88	syl3anc	$⊢ φ \to N (Y) - N (X) \leq N (Y -_{W} X)$
90	6 2 87 4	ngpdsr	$⊢ (W \in NrmGrp \land X \in V \land Y \in V) \to X D Y = N (Y -_{W} X)$
91	20 14 16 90	syl3anc	$⊢ φ \to X D Y = N (Y -_{W} X)$
92	89 91	breqtrrd	$⊢ φ \to N (Y) - N (X) \leq X D Y$
93	50 75 18	ltled	$⊢ φ \to X D Y \leq T$
94	86 50 75 92 93	letrd	$⊢ φ \to N (Y) - N (X) \leq T$
95	81 71 75	lesubadd2d	$⊢ φ \to (N (Y) - N (X) \leq T \leftrightarrow N (Y) \leq N (X) + T)$
96	94 95	mpbid	$⊢ φ \to N (Y) \leq N (X) + T$
97	81 76 69 85 96	lemul2ad	$⊢ φ \to (B E C) N (Y) \leq (B E C) (N (X) + T)$
98	79 97	eqbrtrrd	$⊢ φ \to (B \underset{˙}{\cdot} Y) D (C \underset{˙}{\cdot} Y) \leq (B E C) (N (X) + T)$
99	17 10	breqtrdi	$⊢ φ \to B E C < \frac{\frac{R}{2}}{N (X) + T}$
100		0red	$⊢ φ \to 0 \in ℝ$
101	2 6	nmge0	$⊢ (W \in NrmGrp \land X \in V) \to 0 \leq N (X)$
102	20 14 101	syl2anc	$⊢ φ \to 0 \leq N (X)$
103	71 74	ltaddrpd	$⊢ φ \to N (X) < N (X) + T$
104	100 71 76 102 103	lelttrd	$⊢ φ \to 0 < N (X) + T$
105		ltmuldiv	$⊢ (B E C \in ℝ \land \frac{R}{2} \in ℝ \land (N (X) + T \in ℝ \land 0 < N (X) + T)) \to ((B E C) (N (X) + T) < \frac{R}{2} \leftrightarrow B E C < \frac{\frac{R}{2}}{N (X) + T})$
106	69 52 76 104 105	syl112anc	$⊢ φ \to ((B E C) (N (X) + T) < \frac{R}{2} \leftrightarrow B E C < \frac{\frac{R}{2}}{N (X) + T})$
107	99 106	mpbird	$⊢ φ \to (B E C) (N (X) + T) < \frac{R}{2}$
108	36 77 52 98 107	lelttrd	$⊢ φ \to (B \underset{˙}{\cdot} Y) D (C \underset{˙}{\cdot} Y) < \frac{R}{2}$
109	34 36 38 65 108	lt2halvesd	$⊢ φ \to ((B \underset{˙}{\cdot} X) D (B \underset{˙}{\cdot} Y)) + ((B \underset{˙}{\cdot} Y) D (C \underset{˙}{\cdot} Y)) < R$
110	30 37 38 40 109	lelttrd	$⊢ φ \to (B \underset{˙}{\cdot} X) D (C \underset{˙}{\cdot} Y) < R$

Metamath Proof Explorer

Theorem nlmvscnlem2

Proof