Theorem occllem6 9178

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) .ih S))}
occllem6.2	|- A e. H~
occllem6.3	|- S e. H~
occllem6.4	|- F e. V

Assertion

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

Distinct variable groups:   x,y,F   x,S,y

Proof of Theorem occllem6

Step	Hyp	Ref	Expression
1		ffvelrn 3814	. . . . . . . . . 10 |- ((G:NN-->CC /\ v e. NN) -> (G` v) e. CC)
2		occllem6.1	. . . . . . . . . . 11 |- G = {<.x, y>. | (x e. NN /\ y = ((F` x) .ih S))}
3		occllem6.3	. . . . . . . . . . 11 |- S e. H~
4	2, 3	occllem4 9176	. . . . . . . . . 10 |- (F:NN-->H~ -> G:NN-->CC)
5	1, 4	sylan 448	. . . . . . . . 9 |- ((F:NN-->H~ /\ v e. NN) -> (G` v) e. CC)
6	5	r19.21aiva 1714	. . . . . . . 8 |- (F:NN-->H~ -> A.v e. NN (G` v) e. CC)
7		occllem6.2	. . . . . . . . 9 |- A e. H~
8	7, 3	hicl 8948	. . . . . . . 8 |- (A .ih S) e. CC
9	6, 8	jctil 292	. . . . . . 7 |- (F:NN-->H~ -> ((A .ih S) e. CC /\ A.v e. NN (G` v) e. CC))
10	9	adantr 389	. . . . . 6 |- ((F:NN-->H~ /\ A e. H~) -> ((A .ih S) e. CC /\ A.v e. NN (G` v) e. CC))
11	10	a1i 8	. . . . 5 |- (S =/= 0h -> ((F:NN-->H~ /\ A e. H~) -> ((A .ih S) e. CC /\ A.v e. NN (G` v) e. CC)))
12	11	adantrd 391	. . . 4 |- (S =/= 0h -> (((F:NN-->H~ /\ A e. H~) /\ A.z e. RR (0 < z -> E.w e. NN A.v e. NN (w <_ v -> (normh` ((F` v) -h A)) < z))) -> ((A .ih S) e. CC /\ A.v e. NN (G` v) e. CC)))
13	3	normcl 8998	. . . . . . . . . . . . . . . . . . 19 |- (normh` S) e. RR
14		redivclt 5800	. . . . . . . . . . . . . . . . . . 19 |- ((u e. RR /\ (normh` S) e. RR /\ (normh` S) =/= 0) -> (u / (normh` S)) e. RR)
15	13, 14	mp3an2 904	. . . . . . . . . . . . . . . . . 18 |- ((u e. RR /\ (normh` S) =/= 0) -> (u / (normh` S)) e. RR)
16	13	gt0ne0 5611	. . . . . . . . . . . . . . . . . 18 |- (0 < (normh` S) -> (normh` S) =/= 0)
17	15, 16	sylan2 451	. . . . . . . . . . . . . . . . 17 |- ((u e. RR /\ 0 < (normh` S)) -> (u / (normh` S)) e. RR)
18	17	adantlr 393	. . . . . . . . . . . . . . . 16 |- (((u e. RR /\ 0 < u) /\ 0 < (normh` S)) -> (u / (normh` S)) e. RR)
19		divgt0t 5855	. . . . . . . . . . . . . . . . 17 |- (((u e. RR /\ 0 < u) /\ ((normh` S) e. RR /\ 0 < (normh` S))) -> 0 < (u / (normh` S)))
20	13, 19	mpanr1 709	. . . . . . . . . . . . . . . 16 |- (((u e. RR /\ 0 < u) /\ 0 < (normh` S)) -> 0 < (u / (normh` S)))
21	18, 20	jca 288	. . . . . . . . . . . . . . 15 |- (((u e. RR /\ 0 < u) /\ 0 < (normh` S)) -> ((u / (normh` S)) e. RR /\ 0 < (u / (normh` S))))
22	21	expcom 374	. . . . . . . . . . . . . 14 |- (0 < (normh` S) -> ((u e. RR /\ 0 < u) -> ((u / (normh` S)) e. RR /\ 0 < (u / (normh` S)))))
23	22	adantr 389	. . . . . . . . . . . . 13 |- ((0 < (normh` S) /\ F:NN-->H~) -> ((u e. RR /\ 0 < u) -> ((u / (normh` S)) e. RR /\ 0 < (u / (normh` S)))))
24	23	imim1d 28	. . . . . . . . . . . 12 |- ((0 < (normh` S) /\ F:NN-->H~) -> ((((u / (normh` S)) e. RR /\ 0 < (u / (normh` S))) -> E.w e. NN A.v e. NN (w <_ v -> (normh` ((F` v) -h A)) < (u / (normh` S)))) -> ((u e. RR /\ 0 < u) -> E.w e. NN A.v e. NN (w <_ v -> (normh` ((F` v) -h A)) < (u / (normh` S))))))
25		ltmuldivtOLD 5864	. . . . . . . . . . . . . . . . . . . 20 |- ((((normh` ((F` v) -h A)) e. RR /\ (normh` S) e. RR /\ u e. RR) /\ 0 < (normh` S)) -> (((normh` ((F` v) -h A)) x. (normh` S)) < u <-> (normh` ((F` v) -h A)) < (u / (normh` S))))
26	13, 25	mp3anl2 911	. . . . . . . . . . . . . . . . . . 19 |- ((((normh` ((F` v) -h A)) e. RR /\ u e. RR) /\ 0 < (normh` S)) -> (((normh` ((F` v) -h A)) x. (normh` S)) < u <-> (normh` ((F` v) -h A)) < (u / (normh` S))))
27		ffvelrn 3814	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F:NN-->H~ /\ v e. NN) -> (F` v) e. H~)
28	27, 7	jctir 293	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F:NN-->H~ /\ v e. NN) -> ((F` v) e. H~ /\ A e. H~))
29		hvsubclt 8887	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F` v) e. H~ /\ A e. H~) -> ((F` v) -h A) e. H~)
30		normclt 8991	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F` v) -h A) e. H~ -> (normh` ((F` v) -h A)) e. RR)
31	28, 29, 30	3syl 20	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F:NN-->H~ /\ v e. NN) -> (normh` ((F` v) -h A)) e. RR)
32	31	adantll 392	. . . . . . . . . . . . . . . . . . . . 21 |- (((0 < (normh` S) /\ F:NN-->H~) /\ v e. NN) -> (normh` ((F` v) -h A)) e. RR)
33	32	adantlr 393	. . . . . . . . . . . . . . . . . . . 20 |- ((((0 < (normh` S) /\ F:NN-->H~) /\ (u e. RR /\ 0 < u)) /\ v e. NN) -> (normh` ((F` v) -h A)) e. RR)
34		pm3.26 319	. . . . . . . . . . . . . . . . . . . . 21 |- ((u e. RR /\ 0 < u) -> u e. RR)
35	34	ad2antlr 405	. . . . . . . . . . . . . . . . . . . 20 |- ((((0 < (normh` S) /\ F:NN-->H~) /\ (u e. RR /\ 0 < u)) /\ v e. NN) -> u e. RR)
36	33, 35	jca 288	. . . . . . . . . . . . . . . . . . 19 |- ((((0 < (normh` S) /\ F:NN-->H~) /\ (u e. RR /\ 0 < u)) /\ v e. NN) -> ((normh` ((F` v) -h A)) e. RR /\ u e. RR))
37		pm3.26 319	. . . . . . . . . . . . . . . . . . . 20 |- ((0 < (normh` S) /\ F:NN-->H~) -> 0 < (normh` S))
38	37	ad2antrr 404	. . . . . . . . . . . . . . . . . . 19 |- ((((0 < (normh` S) /\ F:NN-->H~) /\ (u e. RR /\ 0 < u)) /\ v e. NN) -> 0 < (normh` S))
39	26, 36, 38	sylanc 471	. . . . . . . . . . . . . . . . . 18 |- ((((0 < (normh` S) /\ F:NN-->H~) /\ (u e. RR /\ 0 < u)) /\ v e. NN) -> (((normh` ((F` v) -h A)) x. (normh` S)) < u <-> (normh` ((F` v) -h A)) < (u / (normh` S))))
40	27, 7	jctil 292	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((F:NN-->H~ /\ v e. NN) -> (A e. H~ /\ (F` v) e. H~))
41	3	occllem2 9174	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A e. H~ /\ (F` v) e. H~) -> (abs` (((F` v) .ih S) - (A .ih S))) <_ ((normh` ((F` v) -h A)) x. (normh` S)))
42	40, 41	syl 10	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F:NN-->H~ /\ v e. NN) -> (abs` (((F` v) .ih S) - (A .ih S))) <_ ((normh` ((F` v) -h A)) x. (normh` S)))
43	2	occllem3 9175	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (v e. NN -> (G` v) = ((F` v) .ih S))
44	43	opreq1d 3975	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (v e. NN -> ((G` v) - (A .ih S)) = (((F` v) .ih S) - (A .ih S)))
45	44	fveq2d 3728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (v e. NN -> (abs` ((G` v) - (A .ih S))) = (abs` (((F` v) .ih S) - (A .ih S))))
46	45	breq1d 2629	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (v e. NN -> ((abs` ((G` v) - (A .ih S))) <_ ((normh` ((F` v) -h A)) x. (normh` S)) <-> (abs` (((F` v) .ih S) - (A .ih S))) <_ ((normh` ((F` v) -h A)) x. (normh` S))))
47	46	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F:NN-->H~ /\ v e. NN) -> ((abs` ((G` v) - (A .ih S))) <_ ((normh` ((F` v) -h A)) x. (normh` S)) <-> (abs` (((F` v) .ih S) - (A .ih S))) <_ ((normh` ((F` v) -h A)) x. (normh` S))))
48	42, 47	mpbird 196	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F:NN-->H~ /\ v