nlmvscnlem1

	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$
Assertion	nlmvscnlem1	$⊢ φ \to \exists r \in ℝ^{+} \forall x \in K \forall y \in V ((B E x < r \land X D y < r) \to (B \underset{˙}{\cdot} X) D (x \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	12	rphalfcld	$⊢ φ \to \frac{R}{2} \in ℝ^{+}$
16	1	nlmngp2	$⊢ W \in NrmMod \to F \in NrmGrp$
17	11 16	syl	$⊢ φ \to F \in NrmGrp$
18	3 7	nmcl	$⊢ (F \in NrmGrp \land B \in K) \to A (B) \in ℝ$
19	17 13 18	syl2anc	$⊢ φ \to A (B) \in ℝ$
20	3 7	nmge0	$⊢ (F \in NrmGrp \land B \in K) \to 0 \leq A (B)$
21	17 13 20	syl2anc	$⊢ φ \to 0 \leq A (B)$
22	19 21	ge0p1rpd	$⊢ φ \to A (B) + 1 \in ℝ^{+}$
23	15 22	rpdivcld	$⊢ φ \to \frac{\frac{R}{2}}{A (B) + 1} \in ℝ^{+}$
24	9 23	eqeltrid	$⊢ φ \to T \in ℝ^{+}$
25		nlmngp	$⊢ W \in NrmMod \to W \in NrmGrp$
26	11 25	syl	$⊢ φ \to W \in NrmGrp$
27	2 6	nmcl	$⊢ (W \in NrmGrp \land X \in V) \to N (X) \in ℝ$
28	26 14 27	syl2anc	$⊢ φ \to N (X) \in ℝ$
29	24	rpred	$⊢ φ \to T \in ℝ$
30	28 29	readdcld	$⊢ φ \to N (X) + T \in ℝ$
31		0red	$⊢ φ \to 0 \in ℝ$
32	2 6	nmge0	$⊢ (W \in NrmGrp \land X \in V) \to 0 \leq N (X)$
33	26 14 32	syl2anc	$⊢ φ \to 0 \leq N (X)$
34	28 24	ltaddrpd	$⊢ φ \to N (X) < N (X) + T$
35	31 28 30 33 34	lelttrd	$⊢ φ \to 0 < N (X) + T$
36	30 35	elrpd	$⊢ φ \to N (X) + T \in ℝ^{+}$
37	15 36	rpdivcld	$⊢ φ \to \frac{\frac{R}{2}}{N (X) + T} \in ℝ^{+}$
38	10 37	eqeltrid	$⊢ φ \to U \in ℝ^{+}$
39	24 38	ifcld	$⊢ φ \to if (T \leq U, T, U) \in ℝ^{+}$
40	11	adantr	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to W \in NrmMod$
41	12	adantr	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to R \in ℝ^{+}$
42	13	adantr	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to B \in K$
43	14	adantr	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to X \in V$
44		simprll	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to x \in K$
45		simprlr	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to y \in V$
46	17	adantr	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to F \in NrmGrp$
47		ngpms	$⊢ F \in NrmGrp \to F \in MetSp$
48	46 47	syl	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to F \in MetSp$
49	3 5	mscl	$⊢ (F \in MetSp \land B \in K \land x \in K) \to B E x \in ℝ$
50	48 42 44 49	syl3anc	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to B E x \in ℝ$
51	39	adantr	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to if (T \leq U, T, U) \in ℝ^{+}$
52	51	rpred	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to if (T \leq U, T, U) \in ℝ$
53	38	rpred	$⊢ φ \to U \in ℝ$
54	53	adantr	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to U \in ℝ$
55		simprrl	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to B E x < if (T \leq U, T, U)$
56	29	adantr	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to T \in ℝ$
57		min2	$⊢ (T \in ℝ \land U \in ℝ) \to if (T \leq U, T, U) \leq U$
58	56 54 57	syl2anc	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to if (T \leq U, T, U) \leq U$
59	50 52 54 55 58	ltletrd	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to B E x < U$
60		ngpms	$⊢ W \in NrmGrp \to W \in MetSp$
61	26 60	syl	$⊢ φ \to W \in MetSp$
62	61	adantr	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to W \in MetSp$
63	2 4	mscl	$⊢ (W \in MetSp \land X \in V \land y \in V) \to X D y \in ℝ$
64	62 43 45 63	syl3anc	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to X D y \in ℝ$
65		simprrr	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to X D y < if (T \leq U, T, U)$
66		min1	$⊢ (T \in ℝ \land U \in ℝ) \to if (T \leq U, T, U) \leq T$
67	56 54 66	syl2anc	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to if (T \leq U, T, U) \leq T$
68	64 52 56 65 67	ltletrd	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to X D y < T$
69	1 2 3 4 5 6 7 8 9 10 40 41 42 43 44 45 59 68	nlmvscnlem2	$⊢ (φ \land ((x \in K \land y \in V) \land (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))) \to (B \underset{˙}{\cdot} X) D (x \underset{˙}{\cdot} y) < R$
70	69	expr	$⊢ (φ \land (x \in K \land y \in V)) \to ((B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)) \to (B \underset{˙}{\cdot} X) D (x \underset{˙}{\cdot} y) < R)$
71	70	ralrimivva	$⊢ φ \to \forall x \in K \forall y \in V ((B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)) \to (B \underset{˙}{\cdot} X) D (x \underset{˙}{\cdot} y) < R)$
72		breq2	$⊢ r = if (T \leq U, T, U) \to (B E x < r \leftrightarrow B E x < if (T \leq U, T, U))$
73		breq2	$⊢ r = if (T \leq U, T, U) \to (X D y < r \leftrightarrow X D y < if (T \leq U, T, U))$
74	72 73	anbi12d	$⊢ r = if (T \leq U, T, U) \to ((B E x < r \land X D y < r) \leftrightarrow (B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)))$
75	74	imbi1d	$⊢ r = if (T \leq U, T, U) \to (((B E x < r \land X D y < r) \to (B \underset{˙}{\cdot} X) D (x \underset{˙}{\cdot} y) < R) \leftrightarrow ((B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)) \to (B \underset{˙}{\cdot} X) D (x \underset{˙}{\cdot} y) < R))$
76	75	2ralbidv	$⊢ r = if (T \leq U, T, U) \to (\forall x \in K \forall y \in V ((B E x < r \land X D y < r) \to (B \underset{˙}{\cdot} X) D (x \underset{˙}{\cdot} y) < R) \leftrightarrow \forall x \in K \forall y \in V ((B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)) \to (B \underset{˙}{\cdot} X) D (x \underset{˙}{\cdot} y) < R))$
77	76	rspcev	$⊢ (if (T \leq U, T, U) \in ℝ^{+} \land \forall x \in K \forall y \in V ((B E x < if (T \leq U, T, U) \land X D y < if (T \leq U, T, U)) \to (B \underset{˙}{\cdot} X) D (x \underset{˙}{\cdot} y) < R)) \to \exists r \in ℝ^{+} \forall x \in K \forall y \in V ((B E x < r \land X D y < r) \to (B \underset{˙}{\cdot} X) D (x \underset{˙}{\cdot} y) < R)$
78	39 71 77	syl2anc	$⊢ φ \to \exists r \in ℝ^{+} \forall x \in K \forall y \in V ((B E x < r \land X D y < r) \to (B \underset{˙}{\cdot} X) D (x \underset{˙}{\cdot} y) < R)$

Metamath Proof Explorer

Theorem nlmvscnlem1

Proof