Theorem sm1cnilem 8347

Description: Lemma for sm1cni 8348.

Hypotheses

Ref	Expression
sm1cni.1	|- X = (Base` U)
sm1cni.4	|- S = (.s` U)
sm1cni.7	|- C = (abs o. - )
sm1cni.8	|- D = (IndMet` U)
sm1cni.j	|- J = (Open` C)
sm1cni.k	|- K = (Open` D)
sm1cni.f	|- F = {<.w, v>. | (w e. CC /\ v = (wSA))}
sm1cni.9	|- U e. NrmCVec
sm1cni.a	|- A e. X
sm1cni.2	|- G = (+v` U)
sm1cnilem.6	|- N = (norm` U)

Assertion

Ref	Expression
sm1cnilem	|- F e. (J Cn K)

Distinct variable groups:   w,v,A   v,S,w   v,X,w

Proof of Theorem sm1cnilem

Step	Hyp	Ref	Expression
1		sm1cni.7	. . . 4 |- C = (abs o. - )
2	1	cnmet 7904	. . 3 |- C e. Met
3		sm1cni.9	. . . 4 |- U e. NrmCVec
4		sm1cni.8	. . . . 5 |- D = (IndMet` U)
5	4	imsmet 8324	. . . 4 |- (U e. NrmCVec -> D e. Met)
6	3, 5	ax-mp 7	. . 3 |- D e. Met
7	1	cnmetba 7903	. . . 4 |- CC = dom dom C
8		sm1cni.j	. . . 4 |- J = (Open` C)
9		sm1cni.1	. . . . 5 |- X = (Base` U)
10	9, 4, 3	imsbai 8322	. . . 4 |- X = dom dom D
11		sm1cni.k	. . . 4 |- K = (Open` D)
12	7, 8, 10, 11	metcn 7889	. . 3 |- ((C e. Met /\ D e. Met) -> (F e. (J Cn K) <-> (F:CC-->X /\ A.r e. CC A.s e. RR (0 < s -> E.t e. RR (0 < t /\ A.u e. CC ((rCu) < t -> ((F` r)D(F` u)) < s))))))
13	2, 6, 12	mp2an 697	. 2 |- (F e. (J Cn K) <-> (F:CC-->X /\ A.r e. CC A.s e. RR (0 < s -> E.t e. RR (0 < t /\ A.u e. CC ((rCu) < t -> ((F` r)D(F` u)) < s)))))
14		sm1cni.f	. . 3 |- F = {<.w, v>. | (w e. CC /\ v = (wSA))}
15		sm1cni.a	. . . 4 |- A e. X
16		sm1cni.4	. . . . 5 |- S = (.s` U)
17	9, 16	nvscl 8247	. . . 4 |- ((U e. NrmCVec /\ w e. CC /\ A e. X) -> (wSA) e. X)
18	3, 15, 17	mp3an13 907	. . 3 |- (w e. CC -> (wSA) e. X)
19	14, 18	fopab 3827	. 2 |- F:CC-->X
20		opreq2 3969	. . . . . . . . . . 11 |- ((N` A) = 0 -> ((abs` (r - u)) x. (N` A)) = ((abs` (r - u)) x. 0))
21	20	breq1d 2629	. . . . . . . . . 10 |- ((N` A) = 0 -> (((abs` (r - u)) x. (N` A)) < s <-> ((abs` (r - u)) x. 0) < s))
22	21	imbi2d 612	. . . . . . . . 9 |- ((N` A) = 0 -> (((abs` (r - u)) < t -> ((abs` (r - u)) x. (N` A)) < s) <-> ((abs` (r - u)) < t -> ((abs` (r - u)) x. 0) < s)))
23	22	ralbidv 1663	. . . . . . . 8 |- ((N` A) = 0 -> (A.u e. CC ((abs` (r - u)) < t -> ((abs` (r - u)) x. (N` A)) < s) <-> A.u e. CC ((abs` (r - u)) < t -> ((abs` (r - u)) x. 0) < s)))
24	23	anbi2d 616	. . . . . . 7 |- ((N` A) = 0 -> ((0 < t /\ A.u e. CC ((abs` (r - u)) < t -> ((abs` (r - u)) x. (N` A)) < s)) <-> (0 < t /\ A.u e. CC ((abs` (r - u)) < t -> ((abs` (r - u)) x. 0) < s))))
25	24	rexbidv 1664	. . . . . 6 |- ((N` A) = 0 -> (E.t e. RR (0 < t /\ A.u e. CC ((abs` (r - u)) < t -> ((abs` (r - u)) x. (N` A)) < s)) <-> E.t e. RR (0 < t /\ A.u e. CC ((abs` (r - u)) < t -> ((abs` (r - u)) x. 0) < s))))
26		breq2 2623	. . . . . . . . 9 |- (t = (s / (N` A)) -> (0 < t <-> 0 < (s / (N` A))))
27		breq2 2623	. . . . . . . . . . 11 |- (t = (s / (N` A)) -> ((abs` (r - u)) < t <-> (abs` (r - u)) < (s / (N` A))))
28	27	imbi1d 613	. . . . . . . . . 10 |- (t = (s / (N` A)) -> (((abs` (r - u)) < t -> ((abs` (r - u)) x. (N` A)) < s) <-> ((abs` (r - u)) < (s / (N` A)) -> ((abs` (r - u)) x. (N` A)) < s)))
29	28	ralbidv 1663	. . . . . . . . 9 |- (t = (s / (N` A)) -> (A.u e. CC ((abs` (r - u)) < t -> ((abs` (r - u)) x. (N` A)) < s) <-> A.u e. CC ((abs` (r - u)) < (s / (N` A)) -> ((abs` (r - u)) x. (N` A)) < s)))
30	26, 29	anbi12d 628	. . . . . . . 8 |- (t = (s / (N` A)) -> ((0 < t /\ A.u e. CC ((abs` (r - u)) < t -> ((abs` (r - u)) x. (N` A)) < s)) <-> (0 < (s / (N` A)) /\ A.u e. CC ((abs` (r - u)) < (s / (N` A)) -> ((abs` (r - u)) x. (N` A)) < s))))
31	30	rcla4ev 1877	. . . . . . 7 |- (((s / (N` A)) e. RR /\ (0 < (s / (N` A)) /\ A.u e. CC ((abs` (r - u)) < (s / (N` A)) -> ((abs` (r - u)) x. (N` A)) < s))) -> E.t e. RR (0 < t /\ A.u e. CC ((abs` (r - u)) < t -> ((abs` (r - u)) x. (N` A)) < s)))
32		sm1cnilem.6	. . . . . . . . . . 11 |- N = (norm` U)
33	9, 32, 3, 15	nvcli 8288	. . . . . . . . . 10 |- (N` A) e. RR
34		redivclt 5800	. . . . . . . . . 10 |- ((s e. RR /\ (N` A) e. RR /\ (N` A) =/= 0) -> (s / (N` A)) e. RR)
35	33, 34	mp3an2 904	. . . . . . . . 9 |- ((s e. RR /\ (N` A) =/= 0) -> (s / (N` A)) e. RR)
36	35	adantll 392	. . . . . . . 8 |- (((r e. CC /\ s e. RR) /\ (N` A) =/= 0) -> (s / (N` A)) e. RR)
37	36	adantlr 393	. . . . . . 7 |- ((((r e. CC /\ s e. RR) /\ 0 < s) /\ (N` A) =/= 0) -> (s / (N` A)) e. RR)
38		divgt0t 5855	. . . . . . . . . . 11 |- (((s e. RR /\ 0 < s) /\ ((N` A) e. RR /\ 0 < (N` A))) -> 0 < (s / (N` A)))
39	33, 38	mpanr1 709	. . . . . . . . . 10 |- (((s e. RR /\ 0 < s) /\ 0 < (N` A)) -> 0 < (s / (N` A)))
40	9, 32	nvge0 8302	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ A e. X) -> 0 <_ (N` A))
41	3, 15, 40	mp2an 697	. . . . . . . . . . 11 |- 0 <_ (N` A)
42		0re 5440	. . . . . . . . . . . . 13 |- 0 e. RR
43	42, 33	ltlen 5576	. . . . . . . . . . . 12 |- (0 < (N` A) <-> (0 <_ (N` A) /\ (N` A) =/= 0))
44	43	biimpr 152	. . . . . . . . . . 11 |- ((0 <_ (N` A) /\ (N` A) =/= 0) -> 0 < (N` A))
45	41, 44	mpan 695	. . . . . . . . . 10 |- ((N` A) =/= 0 -> 0 < (N` A))
46	39, 45	sylan2 451	. . . . . . . . 9 |- (((s e. RR /\ 0 < s) /\ (N` A) =/= 0) -> 0 < (s / (N` A)))
47	46	adantlll 396	. . . . . . . 8 |- ((((r e. CC /\ s e. RR) /\ 0 < s) /\ (N` A) =/= 0) -> 0 < (s / (N` A)))
48		ltmuldivtOLD 5864	. . . . . . . . . . 11 |- ((((abs` (r - u)) e. RR /\ (N` A) e. RR /\ s e. RR) /\ 0 < (N` A)) -> (((abs` (r - u)) x. (N` A)) < s <-> (abs` (r - u)) < (s / (N` A))))
49		subclt 5367	. . . . . . . . . . . . . . . 16 |- ((r e. CC /\ u e. CC) -> (r - u) e. CC)
50		absclt 6833	. . . . . . . . . . . . . . . 16 |- ((r - u) e. CC -> (abs` (r - u)) e. RR)
51	49, 50	syl 10	. . . . . . . . . . . . . . 15 |- ((r e. CC /\ u e. CC) -> (abs` (r - u)) e. RR)
52	51	adantlr 393	. . . . . . . . . . . . . 14 |- (((r e. CC /\ s e. RR) /\ u e. CC) -> (abs` (r - u)) e. RR)
53	52	adantlr 393	. . . . . . . . . . . . 13 |- ((((r e. CC /\ s e. RR) /\ 0 < s) /\ u e. CC) -> (abs` (r - u)) e. RR)
54	53	adantlr 393	. . . . . . . . . . . 12 |- (((((r e. CC /\ s e. RR) /\ 0 < s) /\ (N` A) =/= 0) /\ u e. CC) -> (abs` (r - u)) e. RR)
55	33	a1i 8	. . . . . . . . . . . 12