Theorem ipblnfi

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 . (Contributed by NM, 12-Jan-2008) (Revised by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ipblnfi.1	|- X = ( BaseSet ` U )
	ipblnfi.7	|- P = ( .iOLD ` U )
	ipblnfi.9	|- U e. CPreHilOLD
	ipblnfi.c	|- C = <. <. + , x. >. , abs >.
	ipblnfi.l	|- B = ( U BLnOp C )
	ipblnfi.f	|- F = ( x e. X |-> ( x P A ) )
Assertion	ipblnfi	|- ( A e. X -> F e. B )

Proof

Step	Hyp	Ref	Expression
1		ipblnfi.1	|- X = ( BaseSet ` U )
2		ipblnfi.7	|- P = ( .iOLD ` U )
3		ipblnfi.9	|- U e. CPreHilOLD
4		ipblnfi.c	|- C = <. <. + , x. >. , abs >.
5		ipblnfi.l	|- B = ( U BLnOp C )
6		ipblnfi.f	|- F = ( x e. X |-> ( x P A ) )
7	3	phnvi	|- U e. NrmCVec
8	1 2	dipcl	|- ( ( U e. NrmCVec /\ x e. X /\ A e. X ) -> ( x P A ) e. CC )
9	7 8	mp3an1	|- ( ( x e. X /\ A e. X ) -> ( x P A ) e. CC )
10	9	ancoms	|- ( ( A e. X /\ x e. X ) -> ( x P A ) e. CC )
11	10 6	fmptd	|- ( A e. X -> F : X --> CC )
12		eqid	|- ( .sOLD ` U ) = ( .sOLD ` U )
13	1 12	nvscl	|- ( ( U e. NrmCVec /\ y e. CC /\ z e. X ) -> ( y ( .sOLD ` U ) z ) e. X )
14	7 13	mp3an1	|- ( ( y e. CC /\ z e. X ) -> ( y ( .sOLD ` U ) z ) e. X )
15	14	ad2ant2lr	|- ( ( ( A e. X /\ y e. CC ) /\ ( z e. X /\ w e. X ) ) -> ( y ( .sOLD ` U ) z ) e. X )
16		simprr	|- ( ( ( A e. X /\ y e. CC ) /\ ( z e. X /\ w e. X ) ) -> w e. X )
17		simpll	|- ( ( ( A e. X /\ y e. CC ) /\ ( z e. X /\ w e. X ) ) -> A e. X )
18		eqid	|- ( +v ` U ) = ( +v ` U )
19	1 18 2	dipdir	|- ( ( U e. CPreHilOLD /\ ( ( y ( .sOLD ` U ) z ) e. X /\ w e. X /\ A e. X ) ) -> ( ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) P A ) = ( ( ( y ( .sOLD ` U ) z ) P A ) + ( w P A ) ) )
20	3 19	mpan	|- ( ( ( y ( .sOLD ` U ) z ) e. X /\ w e. X /\ A e. X ) -> ( ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) P A ) = ( ( ( y ( .sOLD ` U ) z ) P A ) + ( w P A ) ) )
21	15 16 17 20	syl3anc	|- ( ( ( A e. X /\ y e. CC ) /\ ( z e. X /\ w e. X ) ) -> ( ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) P A ) = ( ( ( y ( .sOLD ` U ) z ) P A ) + ( w P A ) ) )
22		simplr	|- ( ( ( A e. X /\ y e. CC ) /\ ( z e. X /\ w e. X ) ) -> y e. CC )
23		simprl	|- ( ( ( A e. X /\ y e. CC ) /\ ( z e. X /\ w e. X ) ) -> z e. X )
24	1 18 12 2 3	ipassi	|- ( ( y e. CC /\ z e. X /\ A e. X ) -> ( ( y ( .sOLD ` U ) z ) P A ) = ( y x. ( z P A ) ) )
25	22 23 17 24	syl3anc	|- ( ( ( A e. X /\ y e. CC ) /\ ( z e. X /\ w e. X ) ) -> ( ( y ( .sOLD ` U ) z ) P A ) = ( y x. ( z P A ) ) )
26	25	oveq1d	|- ( ( ( A e. X /\ y e. CC ) /\ ( z e. X /\ w e. X ) ) -> ( ( ( y ( .sOLD ` U ) z ) P A ) + ( w P A ) ) = ( ( y x. ( z P A ) ) + ( w P A ) ) )
27	21 26	eqtrd	|- ( ( ( A e. X /\ y e. CC ) /\ ( z e. X /\ w e. X ) ) -> ( ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) P A ) = ( ( y x. ( z P A ) ) + ( w P A ) ) )
28	14	adantll	|- ( ( ( A e. X /\ y e. CC ) /\ z e. X ) -> ( y ( .sOLD ` U ) z ) e. X )
29	1 18	nvgcl	|- ( ( U e. NrmCVec /\ ( y ( .sOLD ` U ) z ) e. X /\ w e. X ) -> ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) e. X )
30	7 29	mp3an1	|- ( ( ( y ( .sOLD ` U ) z ) e. X /\ w e. X ) -> ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) e. X )
31	28 30	sylan	|- ( ( ( ( A e. X /\ y e. CC ) /\ z e. X ) /\ w e. X ) -> ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) e. X )
32	31	anasss	|- ( ( ( A e. X /\ y e. CC ) /\ ( z e. X /\ w e. X ) ) -> ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) e. X )
33		oveq1	|- ( x = ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) -> ( x P A ) = ( ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) P A ) )
34		ovex	|- ( ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) P A ) e. _V
35	33 6 34	fvmpt	|- ( ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) e. X -> ( F ` ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) ) = ( ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) P A ) )
36	32 35	syl	|- ( ( ( A e. X /\ y e. CC ) /\ ( z e. X /\ w e. X ) ) -> ( F ` ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) ) = ( ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) P A ) )
37		oveq1	|- ( x = z -> ( x P A ) = ( z P A ) )
38		ovex	|- ( z P A ) e. _V
39	37 6 38	fvmpt	|- ( z e. X -> ( F ` z ) = ( z P A ) )
40	39	ad2antrl	|- ( ( ( A e. X /\ y e. CC ) /\ ( z e. X /\ w e. X ) ) -> ( F ` z ) = ( z P A ) )
41	40	oveq2d	|- ( ( ( A e. X /\ y e. CC ) /\ ( z e. X /\ w e. X ) ) -> ( y x. ( F ` z ) ) = ( y x. ( z P A ) ) )
42		oveq1	|- ( x = w -> ( x P A ) = ( w P A ) )
43		ovex	|- ( w P A ) e. _V
44	42 6 43	fvmpt	|- ( w e. X -> ( F ` w ) = ( w P A ) )
45	44	ad2antll	|- ( ( ( A e. X /\ y e. CC ) /\ ( z e. X /\ w e. X ) ) -> ( F ` w ) = ( w P A ) )
46	41 45	oveq12d	|- ( ( ( A e. X /\ y e. CC ) /\ ( z e. X /\ w e. X ) ) -> ( ( y x. ( F ` z ) ) + ( F ` w ) ) = ( ( y x. ( z P A ) ) + ( w P A ) ) )
47	27 36 46	3eqtr4d	|- ( ( ( A e. X /\ y e. CC ) /\ ( z e. X /\ w e. X ) ) -> ( F ` ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) ) = ( ( y x. ( F ` z ) ) + ( F ` w ) ) )
48	47	ralrimivva	|- ( ( A e. X /\ y e. CC ) -> A. z e. X A. w e. X ( F ` ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) ) = ( ( y x. ( F ` z ) ) + ( F ` w ) ) )
49	48	ralrimiva	|- ( A e. X -> A. y e. CC A. z e. X A. w e. X ( F ` ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) ) = ( ( y x. ( F ` z ) ) + ( F ` w ) ) )
50	4	cnnv	|- C e. NrmCVec
51	4	cnnvba	|- CC = ( BaseSet ` C )
52	4	cnnvg	|- + = ( +v ` C )
53	4	cnnvs	|- x. = ( .sOLD ` C )
54		eqid	|- ( U LnOp C ) = ( U LnOp C )
55	1 51 18 52 12 53 54	islno	|- ( ( U e. NrmCVec /\ C e. NrmCVec ) -> ( F e. ( U LnOp C ) <-> ( F : X --> CC /\ A. y e. CC A. z e. X A. w e. X ( F ` ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) ) = ( ( y x. ( F ` z ) ) + ( F ` w ) ) ) ) )
56	7 50 55	mp2an	|- ( F e. ( U LnOp C ) <-> ( F : X --> CC /\ A. y e. CC A. z e. X A. w e. X ( F ` ( ( y ( .sOLD ` U ) z ) ( +v ` U ) w ) ) = ( ( y x. ( F ` z ) ) + ( F ` w ) ) ) )
57	11 49 56	sylanbrc	|- ( A e. X -> F e. ( U LnOp C ) )
58		eqid	|- ( normCV ` U ) = ( normCV ` U )
59	1 58	nvcl	|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( normCV ` U ) ` A ) e. RR )
60	7 59	mpan	|- ( A e. X -> ( ( normCV ` U ) ` A ) e. RR )
61	1 58 2 3	sii	|- ( ( z e. X /\ A e. X ) -> ( abs ` ( z P A ) ) <_ ( ( ( normCV ` U ) ` z ) x. ( ( normCV ` U ) ` A ) ) )
62	61	ancoms	|- ( ( A e. X /\ z e. X ) -> ( abs ` ( z P A ) ) <_ ( ( ( normCV ` U ) ` z ) x. ( ( normCV ` U ) ` A ) ) )
63	39	adantl	|- ( ( A e. X /\ z e. X ) -> ( F ` z ) = ( z P A ) )
64	63	fveq2d	|- ( ( A e. X /\ z e. X ) -> ( abs ` ( F ` z ) ) = ( abs ` ( z P A ) ) )
65	60	recnd	|- ( A e. X -> ( ( normCV ` U ) ` A ) e. CC )
66	1 58	nvcl	|- ( ( U e. NrmCVec /\ z e. X ) -> ( ( normCV ` U ) ` z ) e. RR )
67	7 66	mpan	|- ( z e. X -> ( ( normCV ` U ) ` z ) e. RR )
68	67	recnd	|- ( z e. X -> ( ( normCV ` U ) ` z ) e. CC )
69		mulcom	|- ( ( ( ( normCV ` U ) ` A ) e. CC /\ ( ( normCV ` U ) ` z ) e. CC ) -> ( ( ( normCV ` U ) ` A ) x. ( ( normCV ` U ) ` z ) ) = ( ( ( normCV ` U ) ` z ) x. ( ( normCV ` U ) ` A ) ) )
70	65 68 69	syl2an	|- ( ( A e. X /\ z e. X ) -> ( ( ( normCV ` U ) ` A ) x. ( ( normCV ` U ) ` z ) ) = ( ( ( normCV ` U ) ` z ) x. ( ( normCV ` U ) ` A ) ) )
71	62 64 70	3brtr4d	|- ( ( A e. X /\ z e. X ) -> ( abs ` ( F ` z ) ) <_ ( ( ( normCV ` U ) ` A ) x. ( ( normCV ` U ) ` z ) ) )
72	71	ralrimiva	|- ( A e. X -> A. z e. X ( abs ` ( F ` z ) ) <_ ( ( ( normCV ` U ) ` A ) x. ( ( normCV ` U ) ` z ) ) )
73	4	cnnvnm	|- abs = ( normCV ` C )
74	1 58 73 54 5 7 50	blo3i	|- ( ( F e. ( U LnOp C ) /\ ( ( normCV ` U ) ` A ) e. RR /\ A. z e. X ( abs ` ( F ` z ) ) <_ ( ( ( normCV ` U ) ` A ) x. ( ( normCV ` U ) ` z ) ) ) -> F e. B )
75	57 60 72 74	syl3anc	|- ( A e. X -> F e. B )