Theorem ipblnfi 8512

Description: A function F generated by varying the first argument of an inner product (with its second argument a fixed vector A) is a bounded linear functional, i.e. a bounded linear operator from the vector space to CC.

Hypotheses

Ref	Expression
ipblnfi.1	|- X = (Base` U)
ipblnfi.7	|- P = (.i` U)
ipblnfi.9	|- U e. CPreHil
ipblnfi.c	|- C = <.<. + , x. >., abs>.
ipblnfi.l	|- B = (U BLnOp C)
ipblnfi.f	|- F = {<.x, y>. | (x e. X /\ y = (xPA))}

Assertion

Ref	Expression
ipblnfi	|- (A e. X -> F e. B)

Distinct variable groups:   x,y,A   x,P,y   x,U,y   x,X,y

Proof of Theorem ipblnfi

Step	Hyp	Ref	Expression
1		ipblnfi.1	. . 3 |- X = (Base` U)
2		eqid 1478	. . 3 |- (norm` U) = (norm` U)
3		ipblnfi.c	. . . 4 |- C = <.<. + , x. >., abs>.
4	3	cnnvnm 8308	. . 3 |- abs = (norm` C)
5		eqid 1478	. . 3 |- (U LnOp C) = (U LnOp C)
6		ipblnfi.l	. . 3 |- B = (U BLnOp C)
7		ipblnfi.9	. . . 4 |- U e. CPreHil
8	7	phnvi 8471	. . 3 |- U e. NrmCVec
9	3	cnnv 8303	. . 3 |- C e. NrmCVec
10	1, 2, 4, 5, 6, 8, 9	blo3i 8458	. 2 |- ((F e. (U LnOp C) /\ ((norm` U)` A) e. RR /\ A.z e. X (abs` (F` z)) <_ (((norm` U)` A) x. ((norm` U)` z))) -> F e. B)
11		ipblnfi.7	. . . . . . . . 9 |- P = (.i` U)
12	1, 11	ipcl 8361	. . . . . . . 8 |- ((U e. NrmCVec /\ x e. X /\ A e. X) -> (xPA) e. CC)
13	8, 12	mp3an1 905	. . . . . . 7 |- ((x e. X /\ A e. X) -> (xPA) e. CC)
14	13	ancoms 438	. . . . . 6 |- ((A e. X /\ x e. X) -> (xPA) e. CC)
15	14	r19.21aiva 1717	. . . . 5 |- (A e. X -> A.x e. X (xPA) e. CC)
16		ipblnfi.f	. . . . . 6 |- F = {<.x, y>. | (x e. X /\ y = (xPA))}
17	16	fopab2 3829	. . . . 5 |- (A.x e. X (xPA) e. CC <-> F:X-->CC)
18	15, 17	sylib 198	. . . 4 |- (A e. X -> F:X-->CC)
19		eqid 1478	. . . . . . . . . . . . . 14 |- (+v` U) = (+v` U)
20	1, 19, 11	ipdir 8498	. . . . . . . . . . . . 13 |- ((U e. CPreHil /\ (z e. X /\ (w(.s` U)v) e. X /\ A e. X)) -> ((z(+v` U)(w(.s` U)v))PA) = ((zPA) + ((w(.s` U)v)PA)))
21	7, 20	mpan 697	. . . . . . . . . . . 12 |- ((z e. X /\ (w(.s` U)v) e. X /\ A e. X) -> ((z(+v` U)(w(.s` U)v))PA) = ((zPA) + ((w(.s` U)v)PA)))
22		eqid 1478	. . . . . . . . . . . . . 14 |- (.s` U) = (.s` U)
23	1, 22	nvscl 8243	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ w e. CC /\ v e. X) -> (w(.s` U)v) e. X)
24	8, 23	mp3an1 905	. . . . . . . . . . . 12 |- ((w e. CC /\ v e. X) -> (w(.s` U)v) e. X)
25	21, 24	syl3an2 862	. . . . . . . . . . 11 |- ((z e. X /\ (w e. CC /\ v e. X) /\ A e. X) -> ((z(+v` U)(w(.s` U)v))PA) = ((zPA) + ((w(.s` U)v)PA)))
26	25	3expa 835	. . . . . . . . . 10 |- (((z e. X /\ (w e. CC /\ v e. X)) /\ A e. X) -> ((z(+v` U)(w(.s` U)v))PA) = ((zPA) + ((w(.s` U)v)PA)))
27	1, 19	nvgcl 8235	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ z e. X /\ (w(.s` U)v) e. X) -> (z(+v` U)(w(.s` U)v)) e. X)
28	8, 27	mp3an1 905	. . . . . . . . . . . . 13 |- ((z e. X /\ (w(.s` U)v) e. X) -> (z(+v` U)(w(.s` U)v)) e. X)
29	28, 24	sylan2 453	. . . . . . . . . . . 12 |- ((z e. X /\ (w e. CC /\ v e. X)) -> (z(+v` U)(w(.s` U)v)) e. X)
30		opreq1 3974	. . . . . . . . . . . . 13 |- (x = (z(+v` U)(w(.s` U)v)) -> (xPA) = ((z(+v` U)(w(.s` U)v))PA))
31		oprex 3989	. . . . . . . . . . . . 13 |- ((z(+v` U)(w(.s` U)v))PA) e. V
32	30, 16, 31	fvopab4 3786	. . . . . . . . . . . 12 |- ((z(+v` U)(w(.s` U)v)) e. X -> (F` (z(+v` U)(w(.s` U)v))) = ((z(+v` U)(w(.s` U)v))PA))
33	29, 32	syl 10	. . . . . . . . . . 11 |- ((z e. X /\ (w e. CC /\ v e. X)) -> (F` (z(+v` U)(w(.s` U)v))) = ((z(+v` U)(w(.s` U)v))PA))
34	33	adantr 391	. . . . . . . . . 10 |- (((z e. X /\ (w e. CC /\ v e. X)) /\ A e. X) -> (F` (z(+v` U)(w(.s` U)v))) = ((z(+v` U)(w(.s` U)v))PA))
35		opreq1 3974	. . . . . . . . . . . . 13 |- (x = z -> (xPA) = (zPA))
36		oprex 3989	. . . . . . . . . . . . 13 |- (zPA) e. V
37	35, 16, 36	fvopab4 3786	. . . . . . . . . . . 12 |- (z e. X -> (F` z) = (zPA))
38	37	ad2antrr 406	. . . . . . . . . . 11 |- (((z e. X /\ (w e. CC /\ v e. X)) /\ A e. X) -> (F` z) = (zPA))
39		opreq1 3974	. . . . . . . . . . . . . . . 16 |- (x = v -> (xPA) = (vPA))
40		oprex 3989	. . . . . . . . . . . . . . . 16 |- (vPA) e. V
41	39, 16, 40	fvopab4 3786	. . . . . . . . . . . . . . 15 |- (v e. X -> (F` v) = (vPA))
42	41	opreq2d 3982	. . . . . . . . . . . . . 14 |- (v e. X -> (w x. (F` v)) = (w x. (vPA)))
43	42	adantl 390	. . . . . . . . . . . . 13 |- ((w e. CC /\ v e. X) -> (w x. (F` v)) = (w x. (vPA)))
44	43	ad2antlr 407	. . . . . . . . . . . 12 |- (((z e. X /\ (w e. CC /\ v e. X)) /\ A e. X) -> (w x. (F` v)) = (w x. (vPA)))
45	1, 19, 22, 11, 7	ipassi 8497	. . . . . . . . . . . . . 14 |- ((w e. CC /\ v e. X /\ A e. X) -> ((w(.s` U)v)PA) = (w x. (vPA)))
46	45	3expa 835	. . . . . . . . . . . . 13 |- (((w e. CC /\ v e. X) /\ A e. X) -> ((w(.s` U)v)PA) = (w x. (vPA)))
47	46	adantll 394	. . . . . . . . . . . 12 |- (((z e. X /\ (w e. CC /\ v e. X)) /\ A e. X) -> ((w(.s` U)v)PA) = (w x. (vPA)))
48	44, 47	eqtr4d 1513	. . . . . . . . . . 11 |- (((z e. X /\ (w e. CC /\ v e. X)) /\ A e. X) -> (w x. (F` v)) = ((w(.s` U)v)PA))
49	38, 48	opreq12d 3984	. . . . . . . . . 10 |- (((z e. X /\ (w e. CC /\ v e. X)) /\ A e. X) -> ((F` z) + (w x. (F` v))) = ((zPA) + ((w(.s` U)v)PA)))
50	26, 34, 49	3eqtr4d 1520	. . . . . . . . 9 |- (((z e. X /\ (w e. CC /\ v e. X)) /\ A e. X) -> (F` (z(+v` U)(w(.s` U)v))) = ((F` z) + (w x. (F` v))))
51	50	exp42 385	. . . . . . . 8 |- (z e. X -> (w e. CC -> (v e. X -> (A e. X -> (F` (z(+v` U)(w(.s` U)v))) = ((F` z) + (w x. (F` v)))))))
52	51	com4r 41	. . . . . . 7 |- (A e. X -> (z e. X -> (w e. CC -> (v e. X -> (F` (z(+v` U)(w(.s` U)v))) = ((F` z) + (w x. (F` v)))))))
53	52	imp3a 361	. . . . . 6 |- (A e. X -> ((z e. X /\ w e. CC) -> (v e. X -> (F` (z(+v` U)(w(.s` U)v))) = ((F` z) + (w x. (F` v))))))
54	53	r19.21adv 1721	. . . . 5 |- (A e. X -> ((z e. X /\ w e. CC) -> A.v e. X (F` (z(+v` U)(w(.s` U)v))) = ((F` z) + (w x. (F` v)))))
55	54	r19.21aivv 1723	. . . 4 |- (A e. X -> A.z e. X A.w e. CC A.v e. X (F` (z(+v` U)(w(.s` U)v))) = ((F` z) + (w x. (F` v))))
56	18, 55	jca 288	. . 3 |- (A e. X -> (F:X-->CC /\ A.z e. X A.w e. CC A.v e. X (F` (z(+v` U)(w(.s` U)v))) = ((F` z) + (w x. (F` v)))))
57	3	cnnvba 8305	. . . . 5 |- CC = (Base` C)
58	3	cnnvg 8304	. . . . 5 |- + = (+v` C)
59	3	cnnvs 83