Theorem lnfncon 9990

Description: A condition equivalent to "T is continuous" when T is linear. Theorem 3.5(iii) of [Beran] p. 99.

Hypothesis

Ref	Expression
lnfncon.1	|- T e. LinFn

Assertion

Ref	Expression
lnfncon	|- (T e. ConFn <-> E.x e. RR A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y)))

Distinct variable group:   x,y,T

Proof of Theorem lnfncon

Step	Hyp	Ref	Expression
1		opreq1 3968	. . . . . 6 |- (x = (normfn` T) -> (x x. (normh` y)) = ((normfn` T) x. (normh` y)))
2	1	breq2d 2630	. . . . 5 |- (x = (normfn` T) -> ((abs` (T` y)) <_ (x x. (normh` y)) <-> (abs` (T` y)) <_ ((normfn` T) x. (normh` y))))
3	2	ralbidv 1663	. . . 4 |- (x = (normfn` T) -> (A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y)) <-> A.y e. H~ (abs` (T` y)) <_ ((normfn` T) x. (normh` y))))
4	3	rcla4ev 1877	. . 3 |- (((normfn` T) e. RR /\ A.y e. H~ (abs` (T` y)) <_ ((normfn` T) x. (normh` y))) -> E.x e. RR A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y)))
5		lnfncon.1	. . . 4 |- T e. LinFn
6		nmcfnext 9988	. . . 4 |- ((T e. LinFn /\ T e. ConFn) -> (normfn` T) e. RR)
7	5, 6	mpan 695	. . 3 |- (T e. ConFn -> (normfn` T) e. RR)
8		nmcfnlbt 9989	. . . . 5 |- ((T e. LinFn /\ T e. ConFn /\ y e. H~) -> (abs` (T` y)) <_ ((normfn` T) x. (normh` y)))
9	5, 8	mp3an1 903	. . . 4 |- ((T e. ConFn /\ y e. H~) -> (abs` (T` y)) <_ ((normfn` T) x. (normh` y)))
10	9	r19.21aiva 1714	. . 3 |- (T e. ConFn -> A.y e. H~ (abs` (T` y)) <_ ((normfn` T) x. (normh` y)))
11	4, 7, 10	sylanc 471	. 2 |- (T e. ConFn -> E.x e. RR A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y)))
12		prodge02t 5829	. . . . . . . . 9 |- (((x e. RR /\ (normh` z) e. RR) /\ (0 < (normh` z) /\ 0 <_ (x x. (normh` z)))) -> 0 <_ x)
13		normclt 8991	. . . . . . . . . . . . 13 |- (z e. H~ -> (normh` z) e. RR)
14	13	adantr 389	. . . . . . . . . . . 12 |- ((z e. H~ /\ z =/= 0h) -> (normh` z) e. RR)
15	14	anim2i 335	. . . . . . . . . . 11 |- ((x e. RR /\ (z e. H~ /\ z =/= 0h)) -> (x e. RR /\ (normh` z) e. RR))
16	15	ancoms 436	. . . . . . . . . 10 |- (((z e. H~ /\ z =/= 0h) /\ x e. RR) -> (x e. RR /\ (normh` z) e. RR))
17	16	adantr 389	. . . . . . . . 9 |- ((((z e. H~ /\ z =/= 0h) /\ x e. RR) /\ A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y))) -> (x e. RR /\ (normh` z) e. RR))
18		normgt0t 8994	. . . . . . . . . . . 12 |- (z e. H~ -> (z =/= 0h <-> 0 < (normh` z)))
19	18	biimpa 416	. . . . . . . . . . 11 |- ((z e. H~ /\ z =/= 0h) -> 0 < (normh` z))
20	19	ad2antrr 404	. . . . . . . . . 10 |- ((((z e. H~ /\ z =/= 0h) /\ x e. RR) /\ A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y))) -> 0 < (normh` z))
21		0re 5440	. . . . . . . . . . . . 13 |- 0 e. RR
22	21	a1i 8	. . . . . . . . . . . 12 |- (((z e. H~ /\ x e. RR) /\ A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y))) -> 0 e. RR)
23	5	lnfnf 9970	. . . . . . . . . . . . . . 15 |- T:H~-->CC
24	23	ffvelrni 3815	. . . . . . . . . . . . . 14 |- (z e. H~ -> (T` z) e. CC)
25		absclt 6833	. . . . . . . . . . . . . 14 |- ((T` z) e. CC -> (abs` (T` z)) e. RR)
26	24, 25	syl 10	. . . . . . . . . . . . 13 |- (z e. H~ -> (abs` (T` z)) e. RR)
27	26	ad2antrr 404	. . . . . . . . . . . 12 |- (((z e. H~ /\ x e. RR) /\ A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y))) -> (abs` (T` z)) e. RR)
28		axmulrcl 5274	. . . . . . . . . . . . . . 15 |- ((x e. RR /\ (normh` z) e. RR) -> (x x. (normh` z)) e. RR)
29	28, 13	sylan2 451	. . . . . . . . . . . . . 14 |- ((x e. RR /\ z e. H~) -> (x x. (normh` z)) e. RR)
30	29	ancoms 436	. . . . . . . . . . . . 13 |- ((z e. H~ /\ x e. RR) -> (x x. (normh` z)) e. RR)
31	30	adantr 389	. . . . . . . . . . . 12 |- (((z e. H~ /\ x e. RR) /\ A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y))) -> (x x. (normh` z)) e. RR)
32		absge0t 6854	. . . . . . . . . . . . . 14 |- ((T` z) e. CC -> 0 <_ (abs` (T` z)))
33	24, 32	syl 10	. . . . . . . . . . . . 13 |- (z e. H~ -> 0 <_ (abs` (T` z)))
34	33	ad2antrr 404	. . . . . . . . . . . 12 |- (((z e. H~ /\ x e. RR) /\ A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y))) -> 0 <_ (abs` (T` z)))
35		fveq2 3724	. . . . . . . . . . . . . . . 16 |- (y = z -> (T` y) = (T` z))
36	35	fveq2d 3728	. . . . . . . . . . . . . . 15 |- (y = z -> (abs` (T` y)) = (abs` (T` z)))
37		fveq2 3724	. . . . . . . . . . . . . . . 16 |- (y = z -> (normh` y) = (normh` z))
38	37	opreq2d 3976	. . . . . . . . . . . . . . 15 |- (y = z -> (x x. (normh` y)) = (x x. (normh` z)))
39	36, 38	breq12d 2631	. . . . . . . . . . . . . 14 |- (y = z -> ((abs` (T` y)) <_ (x x. (normh` y)) <-> (abs` (T` z)) <_ (x x. (normh` z))))
40	39	rcla4va 1875	. . . . . . . . . . . . 13 |- ((z e. H~ /\ A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y))) -> (abs` (T` z)) <_ (x x. (normh` z)))
41	40	adantlr 393	. . . . . . . . . . . 12 |- (((z e. H~ /\ x e. RR) /\ A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y))) -> (abs` (T` z)) <_ (x x. (normh` z)))
42	22, 27, 31, 34, 41	letrd 5526	. . . . . . . . . . 11 |- (((z e. H~ /\ x e. RR) /\ A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y))) -> 0 <_ (x x. (normh` z)))
43	42	adantllr 397	. . . . . . . . . 10 |- ((((z e. H~ /\ z =/= 0h) /\ x e. RR) /\ A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y))) -> 0 <_ (x x. (normh` z)))
44	20, 43	jca 288	. . . . . . . . 9 |- ((((z e. H~ /\ z =/= 0h) /\ x e. RR) /\ A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y))) -> (0 < (normh` z) /\ 0 <_ (x x. (normh` z))))
45	12, 17, 44	sylanc 471	. . . . . . . 8 |- ((((z e. H~ /\ z =/= 0h) /\ x e. RR) /\ A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y))) -> 0 <_ x)
46		leloet 5518	. . . . . . . . . 10 |- ((0 e. RR /\ x e. RR) -> (0 <_ x <-> (0 < x \/ 0 = x)))
47	21, 46	mpan 695	. . . . . . . . 9 |- (x e. RR -> (0 <_ x <-> (0 < x \/ 0 = x)))
48	47	ad2antlr 405	. . . . . . . 8 |- ((((z e. H~ /\ z =/= 0h) /\ x e. RR) /\ A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y))) -> (0 <_ x <-> (0 < x \/ 0 = x)))
49	45, 48	mpbid 195	. . . . . . 7 |- ((((z e. H~ /\ z =/= 0h) /\ x e. RR) /\ A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y))) -> (0 < x \/ 0 = x))
50		breq2 2623	. . . . . . . . . . . . . . . 16 |- (v = (w / x) -> (0 < v <-> 0 < (w / x)))
51		breq2 2623	. . . . . . . . . . . . . . . . . 18 |- (v = (w / x) -> ((normh` (u -h z)) < v <-> (normh` (u -h z)) < (w / x)))
52	51	imbi1d 613	. . . . . . . . . . . . . . . . 17 |- (v = (w / x) -> (((normh` (u -h z)) < v -> (abs` ((T` u) - (T` z))) < w) <-> ((normh` (u -h z)) < (w / x) -> (abs` ((T` u) - (T` z))) < w)))
53	52	ralbidv 1663	. . . . . . . . . . . . . . . 16 |- (v = (w / x) -> (A.u e. H~ ((normh` (u -h z)) < v -> (abs` ((T` u) - (T` z))) < w) <-> A.u e. H~ ((normh` (u -h z)) < (w / x) -> (abs` ((T` u) - (T` z))) < w)))
54	50, 53	anbi12d 628	. . . . . . . . . . . . . . 15 |- (v = (w / x) -> ((0 < v /\ A.u e. H~ ((normh` (u -h z)) < v -> (abs` ((T` u) - (T` z))) < w)) <->