Theorem nmcopexlem1 9889

Description: Lemma for nmcopex 9895 (Theorem 3.5(i) of [Beran] p. 99). A sufficient condition for the norm of an operator to be real, based on its definition and the properties of supremum. Compared to Beran, we use a direct proof instead of a proof by contradiction.

Hypotheses

Ref	Expression
nmcopex.1	|- T e. LinOp
nmcopex.2	|- T e. ConOp

Assertion

Ref	Expression
nmcopexlem1	|- ((n e. NN /\ A.x e. H~ ((normh` x) <_ 1 -> -. n < (normh` (T` x)))) -> (normop` T) e. RR)

Distinct variable group:   x,T,n

Proof of Theorem nmcopexlem1

Step	Hyp	Ref	Expression
1		ra4 1691	. . . . . . . . 9 |- (A.n e. RR E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))}n < y -> (n e. RR -> E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))}n < y))
2	1	impcom 351	. . . . . . . 8 |- ((n e. RR /\ A.n e. RR E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))}n < y) -> E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))}n < y)
3		nnret 5885	. . . . . . . 8 |- (n e. NN -> n e. RR)
4		nmcopex.1	. . . . . . . . . . . . 13 |- T e. LinOp
5	4	lnopf 9832	. . . . . . . . . . . 12 |- T:H~-->H~
6		nmopsetretHIL 9731	. . . . . . . . . . . 12 |- (T:H~-->H~ -> {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))} (_ RR)
7	5, 6	ax-mp 7	. . . . . . . . . . 11 |- {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))} (_ RR
8		ressxr 5478	. . . . . . . . . . 11 |- RR (_ RR*
9	7, 8	sstri 2069	. . . . . . . . . 10 |- {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))} (_ RR*
10		supxrunb2 6045	. . . . . . . . . . 11 |- ({z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))} (_ RR* -> (A.n e. RR E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))}n < y <-> sup({z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))}, RR*, < ) = +oo))
11		nmopvalt 9722	. . . . . . . . . . . . 13 |- (T:H~-->H~ -> (normop` T) = sup({z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))}, RR*, < ))
12	5, 11	ax-mp 7	. . . . . . . . . . . 12 |- (normop` T) = sup({z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))}, RR*, < )
13	12	eqeq1i 1479	. . . . . . . . . . 11 |- ((normop` T) = +oo <-> sup({z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))}, RR*, < ) = +oo)
14	10, 13	syl6rbbr 538	. . . . . . . . . 10 |- ({z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))} (_ RR* -> ((normop` T) = +oo <-> A.n e. RR E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))}n < y))
15	9, 14	ax-mp 7	. . . . . . . . 9 |- ((normop` T) = +oo <-> A.n e. RR E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))}n < y)
16	15	biimp 151	. . . . . . . 8 |- ((normop` T) = +oo -> A.n e. RR E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))}n < y)
17	2, 3, 16	syl2an 454	. . . . . . 7 |- ((n e. NN /\ (normop` T) = +oo) -> E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))}n < y)
18		rexcom4 1820	. . . . . . . . 9 |- (E.x e. H~ E.y(((normh` x) <_ 1 /\ y = (normh` (T` x))) /\ n < y) <-> E.yE.x e. H~ (((normh` x) <_ 1 /\ y = (normh` (T` x))) /\ n < y))
19		19.42v 1306	. . . . . . . . . . 11 |- (E.y((normh` x) <_ 1 /\ (y = (normh` (T` x)) /\ n < y)) <-> ((normh` x) <_ 1 /\ E.y(y = (normh` (T` x)) /\ n < y)))
20		anass 439	. . . . . . . . . . . . 13 |- ((((normh` x) <_ 1 /\ y = (normh` (T` x))) /\ n < y) <-> ((normh` x) <_ 1 /\ (y = (normh` (T` x)) /\ n < y)))
21	20	bicomi 172	. . . . . . . . . . . 12 |- (((normh` x) <_ 1 /\ (y = (normh` (T` x)) /\ n < y)) <-> (((normh` x) <_ 1 /\ y = (normh` (T` x))) /\ n < y))
22	21	exbii 1049	. . . . . . . . . . 11 |- (E.y((normh` x) <_ 1 /\ (y = (normh` (T` x)) /\ n < y)) <-> E.y(((normh` x) <_ 1 /\ y = (normh` (T` x))) /\ n < y))
23		fvex 3723	. . . . . . . . . . . . 13 |- (normh` (T` x)) e. V
24		breq2 2618	. . . . . . . . . . . . 13 |- (y = (normh` (T` x)) -> (n < y <-> n < (normh` (T` x))))
25	23, 24	ceqsexv 1831	. . . . . . . . . . . 12 |- (E.y(y = (normh` (T` x)) /\ n < y) <-> n < (normh` (T` x)))
26	25	anbi2i 480	. . . . . . . . . . 11 |- (((normh` x) <_ 1 /\ E.y(y = (normh` (T` x)) /\ n < y)) <-> ((normh` x) <_ 1 /\ n < (normh` (T` x))))
27	19, 22, 26	3bitr3r 182	. . . . . . . . . 10 |- (((normh` x) <_ 1 /\ n < (normh` (T` x))) <-> E.y(((normh` x) <_ 1 /\ y = (normh` (T` x))) /\ n < y))
28	27	rexbii 1665	. . . . . . . . 9 |- (E.x e. H~ ((normh` x) <_ 1 /\ n < (normh` (T` x))) <-> E.x e. H~ E.y(((normh` x) <_ 1 /\ y = (normh` (T` x))) /\ n < y))
29		visset 1809	. . . . . . . . . . . . 13 |- y e. V
30		eqeq1 1478	. . . . . . . . . . . . . . 15 |- (z = y -> (z = (normh` (T` x)) <-> y = (normh` (T` x))))
31	30	anbi2d 615	. . . . . . . . . . . . . 14 |- (z = y -> (((normh` x) <_ 1 /\ z = (normh` (T` x))) <-> ((normh` x) <_ 1 /\ y = (normh` (T` x)))))
32	31	rexbidv 1661	. . . . . . . . . . . . 13 |- (z = y -> (E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x))) <-> E.x e. H~ ((normh` x) <_ 1 /\ y = (normh` (T` x)))))
33	29, 32	elab 1893	. . . . . . . . . . . 12 |- (y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))} <-> E.x e. H~ ((normh` x) <_ 1 /\ y = (normh` (T` x))))
34	33	anbi1i 481	. . . . . . . . . . 11 |- ((y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))} /\ n < y) <-> (E.x e. H~ ((normh` x) <_ 1 /\ y = (normh` (T` x))) /\ n < y))
35		r19.41v 1760	. . . . . . . . . . 11 |- (E.x e. H~ (((normh` x) <_ 1 /\ y = (normh` (T` x))) /\ n < y) <-> (E.x e. H~ ((normh` x) <_ 1 /\ y = (normh` (T` x))) /\ n < y))
36	34, 35	bitr4 176	. . . . . . . . . 10 |- ((y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))} /\ n < y) <-> E.x e. H~ (((normh` x) <_ 1 /\ y = (normh` (T` x))) /\ n < y))
37	36	exbii 1049	. . . . . . . . 9 |- (E.y(y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))} /\ n < y) <-> E.yE.x e. H~ (((normh` x) <_ 1 /\ y = (normh` (T` x))) /\ n < y))
38	18, 28, 37	3bitr4 183	. . . . . . . 8 |- (E.x e. H~ ((normh` x) <_ 1 /\ n < (normh` (T` x))) <-> E.y(y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))} /\ n < y))
39		df-rex 1647	. . . . . . . 8 |- (E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))}n < y <-> E.y(y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (normh` (T` x)))} /\ n < y))
40	38, 39	bitr4 176	. . . . . . 7 |- (E.x e. H~ ((normh` x) <_ 1 /\ n < (normh` (T`