Theorem lnopcon 9878

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

Hypothesis

Ref	Expression
lnopcon.1	|- T e. LinOp

Assertion

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

Distinct variable group:   x,y,T

Proof of Theorem lnopcon

Step	Hyp	Ref	Expression
1		opreq1 3953	. . . . . 6 |- (x = (normop` T) -> (x x. (normh` y)) = ((normop` T) x. (normh` y)))
2	1	breq2d 2620	. . . . 5 |- (x = (normop` T) -> ((normh` (T` y)) <_ (x x. (normh` y)) <-> (normh` (T` y)) <_ ((normop` T) x. (normh` y))))
3	2	ralbidv 1655	. . . 4 |- (x = (normop` T) -> (A.y e. H~ (normh` (T` y)) <_ (x x. (normh` y)) <-> A.y e. H~ (normh` (T` y)) <_ ((normop` T) x. (normh` y))))
4	3	rcla4ev 1868	. . 3 |- (((normop` T) e. RR /\ A.y e. H~ (normh` (T` y)) <_ ((normop` T) x. (normh` y))) -> E.x e. RR A.y e. H~ (normh` (T` y)) <_ (x x. (normh` y)))
5		lnopcon.1	. . . 4 |- T e. LinOp
6		nmcopext 9874	. . . 4 |- ((T e. LinOp /\ T e. ConOp) -> (normop` T) e. RR)
7	5, 6	mpan 693	. . 3 |- (T e. ConOp -> (normop` T) e. RR)
8		nmcoplbt 9875	. . . . 5 |- ((T e. LinOp /\ T e. ConOp /\ y e. H~) -> (normh` (T` y)) <_ ((normop` T) x. (normh` y)))
9	5, 8	mp3an1 900	. . . 4 |- ((T e. ConOp /\ y e. H~) -> (normh` (T` y)) <_ ((normop` T) x. (normh` y)))
10	9	r19.21aiva 1706	. . 3 |- (T e. ConOp -> A.y e. H~ (normh` (T` y)) <_ ((normop` T) x. (normh` y)))
11	4, 7, 10	sylanc 471	. 2 |- (T e. ConOp -> E.x e. RR A.y e. H~ (normh` (T` y)) <_ (x x. (normh` y)))
12		prodge02t 5785	. . . . . . . . 9 |- (((x e. RR /\ (normh` z) e. RR) /\ (0 < (normh` z) /\ 0 <_ (x x. (normh` z)))) -> 0 <_ x)
13		normclt 8912	. . . . . . . . . . . . 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~ (normh` (T` y)) <_ (x x. (normh` y))) -> (x e. RR /\ (normh` z) e. RR))
18		normgt0tOLD 8914	. . . . . . . . . . . 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~ (normh` (T` y)) <_ (x x. (normh` y))) -> 0 < (normh` z))
21		0re 5412	. . . . . . . . . . . 12 |- 0 e. RR
22	21	a1i 8	. . . . . . . . . . 11 |- ((((z e. H~ /\ -. z = 0h) /\ x e. RR) /\ A.y e. H~ (normh` (T` y)) <_ (x x. (normh` y))) -> 0 e. RR)
23	5	lnopf 9809	. . . . . . . . . . . . . . 15 |- T:H~-->H~
24	23	ffvelrni 3800	. . . . . . . . . . . . . 14 |- (z e. H~ -> (T` z) e. H~)
25		normclt 8912	. . . . . . . . . . . . . 14 |- ((T` z) e. H~ -> (normh` (T` z)) e. RR)
26	24, 25	syl 10	. . . . . . . . . . . . 13 |- (z e. H~ -> (normh` (T` z)) e. RR)
27	26	adantr 389	. . . . . . . . . . . 12 |- ((z e. H~ /\ -. z = 0h) -> (normh` (T` z)) e. RR)
28	27	ad2antrr 404	. . . . . . . . . . 11 |- ((((z e. H~ /\ -. z = 0h) /\ x e. RR) /\ A.y e. H~ (normh` (T` y)) <_ (x x. (normh` y))) -> (normh` (T` z)) e. RR)
29		axmulrcl 5246	. . . . . . . . . . . . . . 15 |- ((x e. RR /\ (normh` z) e. RR) -> (x x. (normh` z)) e. RR)
30	29, 13	sylan2 451	. . . . . . . . . . . . . 14 |- ((x e. RR /\ z e. H~) -> (x x. (normh` z)) e. RR)
31	30	ancoms 436	. . . . . . . . . . . . 13 |- ((z e. H~ /\ x e. RR) -> (x x. (normh` z)) e. RR)
32	31	adantlr 393	. . . . . . . . . . . 12 |- (((z e. H~ /\ -. z = 0h) /\ x e. RR) -> (x x. (normh` z)) e. RR)
33	32	adantr 389	. . . . . . . . . . 11 |- ((((z e. H~ /\ -. z = 0h) /\ x e. RR) /\ A.y e. H~ (normh` (T` y)) <_ (x x. (normh` y))) -> (x x. (normh` z)) e. RR)
34		normge0t 8913	. . . . . . . . . . . . . 14 |- ((T` z) e. H~ -> 0 <_ (normh` (T` z)))
35	24, 34	syl 10	. . . . . . . . . . . . 13 |- (z e. H~ -> 0 <_ (normh` (T` z)))
36	35	adantr 389	. . . . . . . . . . . 12 |- ((z e. H~ /\ -. z = 0h) -> 0 <_ (normh` (T` z)))
37	36	ad2antrr 404	. . . . . . . . . . 11 |- ((((z e. H~ /\ -. z = 0h) /\ x e. RR) /\ A.y e. H~ (normh` (T` y)) <_ (x x. (normh` y))) -> 0 <_ (normh` (T` z)))
38		fveq2 3709	. . . . . . . . . . . . . . . 16 |- (y = z -> (T` y) = (T` z))
39	38	fveq2d 3713	. . . . . . . . . . . . . . 15 |- (y = z -> (normh` (T` y)) = (normh` (T` z)))
40		fveq2 3709	. . . . . . . . . . . . . . . 16 |- (y = z -> (normh` y) = (normh` z))
41	40	opreq2d 3961	. . . . . . . . . . . . . . 15 |- (y = z -> (x x. (normh` y)) = (x x. (normh` z)))
42	39, 41	breq12d 2621	. . . . . . . . . . . . . 14 |- (y = z -> ((normh` (T` y)) <_ (x x. (normh` y)) <-> (normh` (T` z)) <_ (x x. (normh` z))))
43	42	rcla4va 1866	. . . . . . . . . . . . 13 |- ((z e. H~ /\ A.y e. H~ (normh` (T` y)) <_ (x x. (normh` y))) -> (normh` (T` z)) <_ (x x. (normh` z)))
44	43	adantlr 393	. . . . . . . . . . . 12 |- (((z e. H~ /\ -. z = 0h) /\ A.y e. H~ (normh` (T` y)) <_ (x x. (normh` y))) -> (normh` (T` z)) <_ (x x. (normh` z)))
45	44	adantlr 393	. . . . . . . . . . 11 |- ((((z e. H~ /\ -. z = 0h) /\ x e. RR) /\ A.y e. H~ (normh` (T` y)) <_ (x x. (normh` y))) -> (normh` (T` z)) <_ (x x. (normh` z)))
46	22, 28, 33, 37, 45	letrd 5499	. . . . . . . . . 10 |- ((((z e. H~ /\ -. z = 0h) /\ x e. RR) /\ A.y e. H~ (normh` (T` y)) <_ (x x. (normh` y))) -> 0 <_ (x x. (normh` z)))
47	20, 46	jca 288	. . . . . . . . 9 |- ((((z e. H~ /\ -. z = 0h) /\ x e. RR) /\ A.y e. H~ (normh` (T` y)) <_ (x x. (normh` y))) -> (0 < (normh` z) /\ 0 <_ (x x. (normh` z))))
48	12, 17, 47	sylanc 471	. . . . . . . 8 |- ((((z e. H~ /\ -. z = 0h) /\ x e. RR) /\ A.y e. H~ (normh` (T` y)) <_ (x x. (normh` y))) -> 0 <_ x)
49		leloet 5491	. . . . . . . . . 10 |- ((0 e. RR /\ x e. RR) -> (0 <_ x <-> (0 < x \/ 0 = x)))
50	21, 49	mpan 693	. . . . . . . . 9 |- (x e. RR -> (0 <_ x <-> (0 < x \/ 0 = x)))
51	50	ad2antlr 405	. . . . . . . 8 |- ((((z e. H~ /\ -. z = 0h) /\ x e. RR) /\ A.y e. H~ (normh` (T` y)) <_ (x x. (normh` y))) -> (0 <_ x <-> (0 < x \/ 0 = x)))
52	48, 51	mpbid 195	. . . . . . 7 |- ((((z e. H~ /\ -. z = 0h) /\ x e. RR) /\ A.y e. H~ (normh` (T` y)) <_ (x x. (normh` y))) -> (0 < x \/ 0 = x))
53		breq2 2613	. . . . . . . . . . . . . . . 16 |- (v = (w / x) -> (0 < v <-> 0 < (w / x)))
54		breq2 2613	. . . . . . . . . . . . . . . . . 18 |- (v = (w / x) -> ((normh` (u -h z)) < v <-> (normh` (u -h z)) < (w / x)))
55	54	imbi1d 611	. . . . . . . . . . . . . . . . 17 |- (v = (w / x) -> (((normh` (u -h z)) < v -> (normh` ((T` u) -h (T` z))) < w) <-> ((normh` (u -h z)) < (w / x) -> (normh` ((T` u) -h (T` z))) < w)))
56	55	ralbidv 1655	. . . . .