Theorem nlelch 9950

Description: The null space of a continuous linear functional is a closed subspace. Remark 3.8 of [Beran] p. 103.

Hypotheses

Ref	Expression
nlelch.1	|- T e. LinFn
nlelch.2	|- T e. ConFn

Assertion

Ref	Expression
nlelch	|- (null` T) e. CH

Proof of Theorem nlelch

Step	Hyp	Ref	Expression
1		closedsub 9048	. 2 |- ((null` T) e. CH <-> ((null` T) e. SH /\ A.gA.h((g:NN-->(null` T) /\ g ~~>v h) -> h e. (null` T))))
2		nlelch.1	. . 3 |- T e. LinFn
3	2	nlelsh 9949	. 2 |- (null` T) e. SH
4		squeeze0 5882	. . . . . 6 |- (((abs` (T` h)) e. RR /\ 0 <_ (abs` (T` h)) /\ A.y e. RR (0 < y -> (abs` (T` h)) < y)) -> (abs` (T` h)) = 0)
5		visset 1810	. . . . . . . . . 10 |- g e. V
6		visset 1810	. . . . . . . . . 10 |- h e. V
7	5, 6	hlimvec 9013	. . . . . . . . 9 |- (g ~~>v h -> h e. H~)
8	2	lnfnf 9926	. . . . . . . . . 10 |- T:H~-->CC
9	8	ffvelrni 3810	. . . . . . . . 9 |- (h e. H~ -> (T` h) e. CC)
10	7, 9	syl 10	. . . . . . . 8 |- (g ~~>v h -> (T` h) e. CC)
11		absclt 6783	. . . . . . . 8 |- ((T` h) e. CC -> (abs` (T` h)) e. RR)
12	10, 11	syl 10	. . . . . . 7 |- (g ~~>v h -> (abs` (T` h)) e. RR)
13	12	adantl 388	. . . . . 6 |- ((g:NN-->(null` T) /\ g ~~>v h) -> (abs` (T` h)) e. RR)
14		absge0t 6804	. . . . . . . 8 |- ((T` h) e. CC -> 0 <_ (abs` (T` h)))
15	10, 14	syl 10	. . . . . . 7 |- (g ~~>v h -> 0 <_ (abs` (T` h)))
16	15	adantl 388	. . . . . 6 |- ((g:NN-->(null` T) /\ g ~~>v h) -> 0 <_ (abs` (T` h)))
17		nlelch.2	. . . . . . . . . . . . 13 |- T e. ConFn
18		cnfnct 9811	. . . . . . . . . . . . 13 |- (((T e. ConFn /\ h e. H~) /\ (y e. RR /\ 0 < y)) -> E.x e. RR (0 < x /\ A.v e. H~ ((normh` (v -h h)) < x -> (abs` ((T` v) - (T` h))) < y)))
19	17, 18	mpanl1 705	. . . . . . . . . . . 12 |- ((h e. H~ /\ (y e. RR /\ 0 < y)) -> E.x e. RR (0 < x /\ A.v e. H~ ((normh` (v -h h)) < x -> (abs` ((T` v) - (T` h))) < y)))
20	19, 7	sylan 448	. . . . . . . . . . 11 |- ((g ~~>v h /\ (y e. RR /\ 0 < y)) -> E.x e. RR (0 < x /\ A.v e. H~ ((normh` (v -h h)) < x -> (abs` ((T` v) - (T` h))) < y)))
21	20	adantll 392	. . . . . . . . . 10 |- (((g:NN-->(null` T) /\ g ~~>v h) /\ (y e. RR /\ 0 < y)) -> E.x e. RR (0 < x /\ A.v e. H~ ((normh` (v -h h)) < x -> (abs` ((T` v) - (T` h))) < y)))
22	5, 6	hlimconv 9014	. . . . . . . . . . . . . . . . . 18 |- (g ~~>v h -> A.x e. RR (0 < x -> E.m e. NN A.n e. NN (m <_ n -> (normh` ((g` n) -h h)) < x)))
23		ra4 1692	. . . . . . . . . . . . . . . . . 18 |- (A.x e. RR (0 < x -> E.m e. NN A.n e. NN (m <_ n -> (normh` ((g` n) -h h)) < x)) -> (x e. RR -> (0 < x -> E.m e. NN A.n e. NN (m <_ n -> (normh` ((g` n) -h h)) < x))))
24	22, 23	syl 10	. . . . . . . . . . . . . . . . 17 |- (g ~~>v h -> (x e. RR -> (0 < x -> E.m e. NN A.n e. NN (m <_ n -> (normh` ((g` n) -h h)) < x))))
25	24	imp32 363	. . . . . . . . . . . . . . . 16 |- ((g ~~>v h /\ (x e. RR /\ 0 < x)) -> E.m e. NN A.n e. NN (m <_ n -> (normh` ((g` n) -h h)) < x))
26	25	adantlr 393	. . . . . . . . . . . . . . 15 |- (((g ~~>v h /\ (y e. RR /\ 0 < y)) /\ (x e. RR /\ 0 < x)) -> E.m e. NN A.n e. NN (m <_ n -> (normh` ((g` n) -h h)) < x))
27	26	adantlll 396	. . . . . . . . . . . . . 14 |- ((((g:NN-->(null` T) /\ g ~~>v h) /\ (y e. RR /\ 0 < y)) /\ (x e. RR /\ 0 < x)) -> E.m e. NN A.n e. NN (m <_ n -> (normh` ((g` n) -h h)) < x))
28	27	adantrrr 403	. . . . . . . . . . . . 13 |- ((((g:NN-->(null` T) /\ g ~~>v h) /\ (y e. RR /\ 0 < y)) /\ (x e. RR /\ (0 < x /\ A.v e. H~ ((normh` (v -h h)) < x -> (abs` ((T` v) - (T` h))) < y)))) -> E.m e. NN A.n e. NN (m <_ n -> (normh` ((g` n) -h h)) < x))
29		breq2 2619	. . . . . . . . . . . . . . . . . . . . 21 |- (n = m -> (m <_ n <-> m <_ m))
30	29	imbi1d 612	. . . . . . . . . . . . . . . . . . . 20 |- (n = m -> ((m <_ n -> (abs` (T` h)) < y) <-> (m <_ m -> (abs` (T` h)) < y)))
31	30	rcla4v 1870	. . . . . . . . . . . . . . . . . . 19 |- (m e. NN -> (A.n e. NN (m <_ n -> (abs` (T` h)) < y) -> (m <_ m -> (abs` (T` h)) < y)))
32		absnegt 6782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((T` h) e. CC -> (abs` -u(T` h)) = (abs` (T` h)))
33	10, 32	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (g ~~>v h -> (abs` -u(T` h)) = (abs` (T` h)))
34	33	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((g:NN-->(null` T) /\ g ~~>v h) /\ n e. NN) -> (abs` -u(T` h)) = (abs` (T` h)))
35		ffvelrn 3809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((g:NN-->(null` T) /\ n e. NN) -> (g` n) e. (null` T))
36		elnlfn2t 9810	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((T:H~-->CC /\ (g` n) e. (null` T)) -> (T` (g` n)) = 0)
37	8, 36	mpan 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((g` n) e. (null` T) -> (T` (g` n)) = 0)
38	35, 37	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((g:NN-->(null` T) /\ n e. NN) -> (T` (g` n)) = 0)
39	38	opreq1d 3970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((g:NN-->(null` T) /\ n e. NN) -> ((T` (g` n)) - (T` h)) = (0 - (T` h)))
40		df-neg 5341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- -u(T` h) = (0 - (T` h))
41	39, 40	syl6reqr 1524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((g:NN-->(null` T) /\ n e. NN) -> -u(T` h) = ((T` (g` n)) - (T` h)))
42	41	fveq2d 3723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((g:NN-->(null` T) /\ n e. NN) -> (abs` -u(T` h)) = (abs` ((T` (g` n)) - (T` h))))
43	42	adantlr 393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((g:NN-->(null` T) /\ g ~~>v h) /\ n e. NN) -> (abs` -u(T` h)) = (abs` ((T` (g` n)) - (T` h))))
44	34, 43	eqtr3d 1507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((g:NN-->(null` T) /\ g ~~>v h) /\ n e. NN) -> (abs` (T` h)) = (abs` ((T` (g` n)) - (T` h))))
45	44	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((g:NN-->(null` T) /\ g ~~>v h) /\ n e. NN) /\ A.v e. H~ ((normh` (v -h h)) < x -> (abs` ((T` v) - (T` h))) < y)) /\ (normh` ((g` n) -h h)) < x) -> (abs` (T` h)) = (abs` ((T` (g` n)) - (T` h))))
46		opreq1 3963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (v = (g` n) -> (v -h h) = ((g` n) -h h))
47	46	fveq2d 3723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (v = (g` n) -> (normh` (v -h h)) = (normh` ((g` n) -h h)))
48	47	breq1d 2625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (v = (g` n) -> ((normh` (v -h h)) < x <-> (normh` ((g` n) -h h)) < x))
49		fveq2 3719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (v = (g` n) -> (T` v) = (T` (g` n)))
50	49	opreq1d 3970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (v = (g` n) -> ((T` v) - (T` h)) = ((T` (g` n)) - (T` h)))
51	50	fveq2d 3723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (v = (g` n) -> (abs` ((T` v) - (T` h))) = (abs` ((T` (g` n)) - (T` h))))
52	51	breq1d 2625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (v = (g` n) -> ((abs` ((T` v) - (T`