Theorem nmcfnexlem1 9980

Description: Lemma for nmcfnex 9986. Show a condition for the norm of a functional to exist, 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
nmcfnex.1	|- T e. LinFn
nmcfnex.2	|- T e. ConFn

Assertion

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

Distinct variable group:   x,T,n

Proof of Theorem nmcfnexlem1

Step	Hyp	Ref	Expression
1		ra4 1694	. . . . . . . . 9 |- (A.n e. RR E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))}n < y -> (n e. RR -> E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (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 = (abs` (T` x)))}n < y) -> E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))}n < y)
3		nnret 5929	. . . . . . . 8 |- (n e. NN -> n e. RR)
4		nmcfnex.1	. . . . . . . . . . . . 13 |- T e. LinFn
5	4	lnfnf 9970	. . . . . . . . . . . 12 |- T:H~-->CC
6		nmfnsetret 9804	. . . . . . . . . . . 12 |- (T:H~-->CC -> {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))} (_ RR)
7	5, 6	ax-mp 7	. . . . . . . . . . 11 |- {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))} (_ RR
8		ressxr 5498	. . . . . . . . . . 11 |- RR (_ RR*
9	7, 8	sstri 2073	. . . . . . . . . 10 |- {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))} (_ RR*
10		supxrunb2 6090	. . . . . . . . . . 11 |- ({z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))} (_ RR* -> (A.n e. RR E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))}n < y <-> sup({z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))}, RR*, < ) = +oo))
11		nmfnvalt 9803	. . . . . . . . . . . . 13 |- (T:H~-->CC -> (normfn` T) = sup({z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))}, RR*, < ))
12	5, 11	ax-mp 7	. . . . . . . . . . . 12 |- (normfn` T) = sup({z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))}, RR*, < )
13	12	eqeq1i 1482	. . . . . . . . . . 11 |- ((normfn` T) = +oo <-> sup({z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))}, RR*, < ) = +oo)
14	10, 13	syl6rbbr 539	. . . . . . . . . 10 |- ({z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))} (_ RR* -> ((normfn` T) = +oo <-> A.n e. RR E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))}n < y))
15	9, 14	ax-mp 7	. . . . . . . . 9 |- ((normfn` T) = +oo <-> A.n e. RR E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))}n < y)
16	15	biimp 151	. . . . . . . 8 |- ((normfn` T) = +oo -> A.n e. RR E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))}n < y)
17	2, 3, 16	syl2an 454	. . . . . . 7 |- ((n e. NN /\ (normfn` T) = +oo) -> E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))}n < y)
18		rexcom4 1824	. . . . . . . . 9 |- (E.x e. H~ E.y(((normh` x) <_ 1 /\ y = (abs` (T` x))) /\ n < y) <-> E.yE.x e. H~ (((normh` x) <_ 1 /\ y = (abs` (T` x))) /\ n < y))
19		19.42v 1308	. . . . . . . . . . 11 |- (E.y((normh` x) <_ 1 /\ (y = (abs` (T` x)) /\ n < y)) <-> ((normh` x) <_ 1 /\ E.y(y = (abs` (T` x)) /\ n < y)))
20		anass 439	. . . . . . . . . . . . 13 |- ((((normh` x) <_ 1 /\ y = (abs` (T` x))) /\ n < y) <-> ((normh` x) <_ 1 /\ (y = (abs` (T` x)) /\ n < y)))
21	20	bicomi 172	. . . . . . . . . . . 12 |- (((normh` x) <_ 1 /\ (y = (abs` (T` x)) /\ n < y)) <-> (((normh` x) <_ 1 /\ y = (abs` (T` x))) /\ n < y))
22	21	exbii 1051	. . . . . . . . . . 11 |- (E.y((normh` x) <_ 1 /\ (y = (abs` (T` x)) /\ n < y)) <-> E.y(((normh` x) <_ 1 /\ y = (abs` (T` x))) /\ n < y))
23		fvex 3732	. . . . . . . . . . . . 13 |- (abs` (T` x)) e. V
24		breq2 2623	. . . . . . . . . . . . 13 |- (y = (abs` (T` x)) -> (n < y <-> n < (abs` (T` x))))
25	23, 24	ceqsexv 1835	. . . . . . . . . . . 12 |- (E.y(y = (abs` (T` x)) /\ n < y) <-> n < (abs` (T` x)))
26	25	anbi2i 480	. . . . . . . . . . 11 |- (((normh` x) <_ 1 /\ E.y(y = (abs` (T` x)) /\ n < y)) <-> ((normh` x) <_ 1 /\ n < (abs` (T` x))))
27	19, 22, 26	3bitr3r 182	. . . . . . . . . 10 |- (((normh` x) <_ 1 /\ n < (abs` (T` x))) <-> E.y(((normh` x) <_ 1 /\ y = (abs` (T` x))) /\ n < y))
28	27	rexbii 1668	. . . . . . . . 9 |- (E.x e. H~ ((normh` x) <_ 1 /\ n < (abs` (T` x))) <-> E.x e. H~ E.y(((normh` x) <_ 1 /\ y = (abs` (T` x))) /\ n < y))
29		visset 1813	. . . . . . . . . . . . 13 |- y e. V
30		eqeq1 1481	. . . . . . . . . . . . . . 15 |- (z = y -> (z = (abs` (T` x)) <-> y = (abs` (T` x))))
31	30	anbi2d 616	. . . . . . . . . . . . . 14 |- (z = y -> (((normh` x) <_ 1 /\ z = (abs` (T` x))) <-> ((normh` x) <_ 1 /\ y = (abs` (T` x)))))
32	31	rexbidv 1664	. . . . . . . . . . . . 13 |- (z = y -> (E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x))) <-> E.x e. H~ ((normh` x) <_ 1 /\ y = (abs` (T` x)))))
33	29, 32	elab 1897	. . . . . . . . . . . 12 |- (y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))} <-> E.x e. H~ ((normh` x) <_ 1 /\ y = (abs` (T` x))))
34	33	anbi1i 481	. . . . . . . . . . 11 |- ((y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))} /\ n < y) <-> (E.x e. H~ ((normh` x) <_ 1 /\ y = (abs` (T` x))) /\ n < y))
35		r19.41v 1763	. . . . . . . . . . 11 |- (E.x e. H~ (((normh` x) <_ 1 /\ y = (abs` (T` x))) /\ n < y) <-> (E.x e. H~ ((normh` x) <_ 1 /\ y = (abs` (T` x))) /\ n < y))
36	34, 35	bitr4 176	. . . . . . . . . 10 |- ((y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))} /\ n < y) <-> E.x e. H~ (((normh` x) <_ 1 /\ y = (abs` (T` x))) /\ n < y))
37	36	exbii 1051	. . . . . . . . 9 |- (E.y(y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))} /\ n < y) <-> E.yE.x e. H~ (((normh` x) <_ 1 /\ y = (abs` (T` x))) /\ n < y))
38	18, 28, 37	3bitr4 183	. . . . . . . 8 |- (E.x e. H~ ((normh` x) <_ 1 /\ n < (abs` (T` x))) <-> E.y(y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))} /\ n < y))
39		df-rex 1650	. . . . . . . 8 |- (E.y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))}n < y <-> E.y(y e. {z | E.x e. H~ ((normh` x) <_ 1 /\ z = (abs` (T` x)))} /\ n < y))
40	38, 39	bitr4 176	. . . . . . 7 |- (E.x e. H~ ((normh` x) <_ 1 /\ n < (abs` (T` x))) <->