Theorem occllem6 5185

Description: Lemma for closure of complement of Hilbert subspace. Part of Remark 3.12 of [Beran] p. 107.

Hypotheses

Ref	Expression
occllem6.1	|- G = {<.x, y>. | (x e. NN /\ y = ((F` x) .i S))}
occllem6.2	|- A e. H~
occllem6.3	|- S e. H~
occllem6.4	|- F e. V

Assertion

Ref	Expression
occllem6	|- (-. S = 0v -> (F ~~>v A -> G ~~> (A .i S)))

Distinct variable group(s):   x,y,F   x,S,y

Proof of Theorem occllem6

Step	Hyp	Ref	Expression
1		occllem6.1	. . . . . . . 8 |- G = {<.x, y>. | (x e. NN /\ y = ((F` x) .i S))}
2		occllem6.3	. . . . . . . 8 |- S e. H~
3	1, 2	occllem4 5183	. . . . . . 7 |- (F:NN-->H~ -> G:NN-->CC)
4		occllem6.2	. . . . . . . 8 |- A e. H~
5	4, 2	hicl 5044	. . . . . . 7 |- (A .i S) e. CC
6	3, 5	jctir 241	. . . . . 6 |- (F:NN-->H~ -> (G:NN-->CC /\ (A .i S) e. CC))
7	6	adantr 306	. . . . 5 |- ((F:NN-->H~ /\ A e. H~) -> (G:NN-->CC /\ (A .i S) e. CC))
8	7	a1i 7	. . . 4 |- (-. S = 0v -> ((F:NN-->H~ /\ A e. H~) -> (G:NN-->CC /\ (A .i S) e. CC)))
9	8	adantrd 308	. . 3 |- (-. S = 0v -> (((F:NN-->H~ /\ A e. H~) /\ A.z e. RR (0 < z -> E.w e. NN A.v e. NN (w <_ v -> (norm` ((F` v) -v A)) < z))) -> (G:NN-->CC /\ (A .i S) e. CC)))
10	2	normcl 5081	. . . . . . . . . . . . . . . . . 18 |- (norm` S) e. RR
11		redivclt 4276	. . . . . . . . . . . . . . . . . . 19 |- (((u e. RR /\ (norm` S) e. RR) /\ (norm` S) =/= 0) -> (u / (norm` S)) e. RR)
12	11	exp 291	. . . . . . . . . . . . . . . . . 18 |- ((u e. RR /\ (norm` S) e. RR) -> ((norm` S) =/= 0 -> (u / (norm` S)) e. RR))
13	10, 12	mpan2 519	. . . . . . . . . . . . . . . . 17 |- (u e. RR -> ((norm` S) =/= 0 -> (u / (norm` S)) e. RR))
14	10	gt0ne0 4340	. . . . . . . . . . . . . . . . 17 |- (0 < (norm` S) -> (norm` S) =/= 0)
15	13, 14	syl5 22	. . . . . . . . . . . . . . . 16 |- (u e. RR -> (0 < (norm` S) -> (u / (norm` S)) e. RR))
16	15	adantr 306	. . . . . . . . . . . . . . 15 |- ((u e. RR /\ 0 < u) -> (0 < (norm` S) -> (u / (norm` S)) e. RR))
17		divgt0t 4402	. . . . . . . . . . . . . . . . . 18 |- ((u e. RR /\ (norm` S) e. RR) -> ((0 < u /\ 0 < (norm` S)) -> 0 < (u / (norm` S))))
18	10, 17	mpan2 519	. . . . . . . . . . . . . . . . 17 |- (u e. RR -> ((0 < u /\ 0 < (norm` S)) -> 0 < (u / (norm` S))))
19	18	exp3a 292	. . . . . . . . . . . . . . . 16 |- (u e. RR -> (0 < u -> (0 < (norm` S) -> 0 < (u / (norm` S)))))
20	19	imp 277	. . . . . . . . . . . . . . 15 |- ((u e. RR /\ 0 < u) -> (0 < (norm` S) -> 0 < (u / (norm` S))))
21	16, 20	jcad 455	. . . . . . . . . . . . . 14 |- ((u e. RR /\ 0 < u) -> (0 < (norm` S) -> ((u / (norm` S)) e. RR /\ 0 < (u / (norm` S)))))
22	21	com12 13	. . . . . . . . . . . . 13 |- (0 < (norm` S) -> ((u e. RR /\ 0 < u) -> ((u / (norm` S)) e. RR /\ 0 < (u / (norm` S)))))
23	22	adantr 306	. . . . . . . . . . . 12 |- ((0 < (norm` S) /\ F:NN-->H~) -> ((u e. RR /\ 0 < u) -> ((u / (norm` S)) e. RR /\ 0 < (u / (norm` S)))))
24	23	syl4d 28	. . . . . . . . . . 11 |- ((0 < (norm` S) /\ F:NN-->H~) -> ((((u / (norm` S)) e. RR /\ 0 < (u / (norm` S))) -> E.w e. NN A.v e. NN (w <_ v -> (norm` ((F` v) -v A)) < (u / (norm` S)))) -> ((u e. RR /\ 0 < u) -> E.w e. NN A.v e. NN (w <_ v -> (norm` ((F` v) -v A)) < (u / (norm` S))))))
25		ltmuldivt 4406	. . . . . . . . . . . . . . . . . . 19 |- (((norm` ((F` v) -v A)) e. RR /\ (norm` S) e. RR /\ u e. RR) -> (0 < (norm` S) -> (((norm` ((F` v) -v A)) x. (norm` S)) < u <-> (norm` ((F` v) -v A)) < (u / (norm` S)))))
26	10, 25	mp3an2 640	. . . . . . . . . . . . . . . . . 18 |- (((norm` ((F` v) -v A)) e. RR /\ u e. RR) -> (0 < (norm` S) -> (((norm` ((F` v) -v A)) x. (norm` S)) < u <-> (norm` ((F` v) -v A)) < (u / (norm` S)))))
27		ffvrn 2890	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F:NN-->H~ /\ v e. NN) -> (F` v) e. H~)
28	27, 4	jctir 241	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F:NN-->H~ /\ v e. NN) -> ((F` v) e. H~ /\ A e. H~))
29		hvsubclt 4998	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F` v) e. H~ /\ A e. H~) -> ((F` v) -v A) e. H~)
30		normclt 5076	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F` v) -v A) e. H~ -> (norm` ((F` v) -v A)) e. RR)
31	28, 29, 30	3syl 21	. . . . . . . . . . . . . . . . . . . . 21 |- ((F:NN-->H~ /\ v e. NN) -> (norm` ((F` v) -v A)) e. RR)
32	31	adantll 309	. . . . . . . . . . . . . . . . . . . 20 |- (((0 < (norm` S) /\ F:NN-->H~) /\ v e. NN) -> (norm` ((F` v) -v A)) e. RR)
33	32	adantlr 310	. . . . . . . . . . . . . . . . . . 19 |- ((((0 < (norm` S) /\ F:NN-->H~) /\ (u e. RR /\ 0 < u)) /\ v e. NN) -> (norm` ((F` v) -v A)) e. RR)
34		pm3.26 256	. . . . . . . . . . . . . . . . . . . 20 |- ((u e. RR /\ 0 < u) -> u e. RR)
35	34	ad2antlr 321	. . . . . . . . . . . . . . . . . . 19 |- ((((0 < (norm` S) /\ F:NN-->H~) /\ (u e. RR /\ 0 < u)) /\ v e. NN) -> u e. RR)
36	33, 35	jca 236	. . . . . . . . . . . . . . . . . 18 |- ((((0 < (norm` S) /\ F:NN-->H~) /\ (u e. RR /\ 0 < u)) /\ v e. NN) -> ((norm` ((F` v) -v A)) e. RR /\ u e. RR))
37		pm3.26 256	. . . . . . . . . . . . . . . . . . 19 |- ((0 < (norm` S) /\ F:NN-->H~) -> 0 < (norm` S))
38	37	ad2antll 320	. . . . . . . . . . . . . . . . . 18 |- ((((0 < (norm` S) /\ F:NN-->H~) /\ (u e. RR /\ 0 < u)) /\ v e. NN) -> 0 < (norm` S))
39	26, 36, 38	sylc 62	. . . . . . . . . . . . . . . . 17 |- ((((0 < (norm` S) /\ F:NN-->H~) /\ (u e. RR /\ 0 < u)) /\ v e. NN) -> (((norm` ((F` v) -v A)) x. (norm` S)) < u <-> (norm` ((F` v) -v A)) < (u / (norm` S))))
40	27, 4	jctil 240	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F:NN-->H~ /\ v e. NN) -> (A e. H~ /\ (F` v) e. H~))
41	2	occllem2 5181	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. H~ /\ (F` v) e. H~) -> (abs` (((F` v) .i S) - (A .i S))) <_ ((norm` ((F` v) -v A)) x. (norm` S)))
42	40, 41	syl 12	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F:NN-->H~ /\ v e. NN) -> (abs` (((F` v) .i S) - (A .i S))) <_ ((norm` ((F` v) -v A)) x. (norm` S)))
43	1	occllem3 5182	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (v e. NN -> (G` v) = ((F` v) .i S))
44	43	opreq1d 3012	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (v e. NN -> ((G` v) - (A .i S)) = (((F` v) .i S) - (A .i S)))
45	44	fveq2d 2836	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (v e. NN -> (abs` ((G` v) - (A .i S))) = (abs` (((F` v) .i S) - (A .i S))))
46	45	breq1d 2071	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (v e. NN -> ((abs` ((G` v) - (A .i S))) <_ ((norm` ((F` v) -v A)) x. (norm` S)) <-> (abs` (((F` v) .i S) - (A .i S))) <_ ((norm` ((F` v) -v A)) x. (norm` S))))
47	46	adantl 305	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F:NN-->H~ /\ v e. NN) -> ((abs` ((G` v) - (A .i S))) <_ ((norm` ((F` v) -v A)) x. (norm` S)) <-> (abs` (((F` v) .i S) - (A .i S))) <_ ((norm` ((F` v) -v A)) x. (norm` S))))
48	42, 47	mpbird 171	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F:NN-->H~ /\ v e. NN) -> (abs` ((G` v) - (A .i S))) <_ ((norm` ((F` v) -v A