This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )