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 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
ipblnfi.7 โŠข ๐‘ƒ = ( ยท๐‘–OLD โ€˜ ๐‘ˆ )
ipblnfi.9 โŠข ๐‘ˆ โˆˆ CPreHilOLD
ipblnfi.c โŠข ๐ถ = โŸจ โŸจ + , ยท โŸฉ , abs โŸฉ
ipblnfi.l โŠข ๐ต = ( ๐‘ˆ BLnOp ๐ถ )
ipblnfi.f โŠข ๐น = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ๐‘ฅ ๐‘ƒ ๐ด ) )
Assertion ipblnfi ( ๐ด โˆˆ ๐‘‹ โ†’ ๐น โˆˆ ๐ต )

Proof

Step Hyp Ref Expression
1 ipblnfi.1 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
2 ipblnfi.7 โŠข ๐‘ƒ = ( ยท๐‘–OLD โ€˜ ๐‘ˆ )
3 ipblnfi.9 โŠข ๐‘ˆ โˆˆ CPreHilOLD
4 ipblnfi.c โŠข ๐ถ = โŸจ โŸจ + , ยท โŸฉ , abs โŸฉ
5 ipblnfi.l โŠข ๐ต = ( ๐‘ˆ BLnOp ๐ถ )
6 ipblnfi.f โŠข ๐น = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ๐‘ฅ ๐‘ƒ ๐ด ) )
7 3 phnvi โŠข ๐‘ˆ โˆˆ NrmCVec
8 1 2 dipcl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘ฅ โˆˆ ๐‘‹ โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( ๐‘ฅ ๐‘ƒ ๐ด ) โˆˆ โ„‚ )
9 7 8 mp3an1 โŠข ( ( ๐‘ฅ โˆˆ ๐‘‹ โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( ๐‘ฅ ๐‘ƒ ๐ด ) โˆˆ โ„‚ )
10 9 ancoms โŠข ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ( ๐‘ฅ ๐‘ƒ ๐ด ) โˆˆ โ„‚ )
11 10 6 fmptd โŠข ( ๐ด โˆˆ ๐‘‹ โ†’ ๐น : ๐‘‹ โŸถ โ„‚ )
12 eqid โŠข ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
13 1 12 nvscl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ ๐‘‹ ) โ†’ ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) โˆˆ ๐‘‹ )
14 7 13 mp3an1 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ ๐‘‹ ) โ†’ ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) โˆˆ ๐‘‹ )
15 14 ad2ant2lr โŠข ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ( ๐‘ง โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) ) โ†’ ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) โˆˆ ๐‘‹ )
16 simprr โŠข ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ( ๐‘ง โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) ) โ†’ ๐‘ค โˆˆ ๐‘‹ )
17 simpll โŠข ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ( ๐‘ง โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) ) โ†’ ๐ด โˆˆ ๐‘‹ )
18 eqid โŠข ( +๐‘ฃ โ€˜ ๐‘ˆ ) = ( +๐‘ฃ โ€˜ ๐‘ˆ )
19 1 18 2 dipdir โŠข ( ( ๐‘ˆ โˆˆ CPreHilOLD โˆง ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ โˆง ๐ด โˆˆ ๐‘‹ ) ) โ†’ ( ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) ๐‘ƒ ๐ด ) = ( ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ๐‘ƒ ๐ด ) + ( ๐‘ค ๐‘ƒ ๐ด ) ) )
20 3 19 mpan โŠข ( ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) ๐‘ƒ ๐ด ) = ( ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ๐‘ƒ ๐ด ) + ( ๐‘ค ๐‘ƒ ๐ด ) ) )
21 15 16 17 20 syl3anc โŠข ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ( ๐‘ง โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) ) โ†’ ( ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) ๐‘ƒ ๐ด ) = ( ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ๐‘ƒ ๐ด ) + ( ๐‘ค ๐‘ƒ ๐ด ) ) )
22 simplr โŠข ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ( ๐‘ง โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) ) โ†’ ๐‘ฆ โˆˆ โ„‚ )
23 simprl โŠข ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ( ๐‘ง โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) ) โ†’ ๐‘ง โˆˆ ๐‘‹ )
24 1 18 12 2 3 ipassi โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ ๐‘‹ โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ๐‘ƒ ๐ด ) = ( ๐‘ฆ ยท ( ๐‘ง ๐‘ƒ ๐ด ) ) )
25 22 23 17 24 syl3anc โŠข ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ( ๐‘ง โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) ) โ†’ ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ๐‘ƒ ๐ด ) = ( ๐‘ฆ ยท ( ๐‘ง ๐‘ƒ ๐ด ) ) )
26 25 oveq1d โŠข ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ( ๐‘ง โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) ) โ†’ ( ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ๐‘ƒ ๐ด ) + ( ๐‘ค ๐‘ƒ ๐ด ) ) = ( ( ๐‘ฆ ยท ( ๐‘ง ๐‘ƒ ๐ด ) ) + ( ๐‘ค ๐‘ƒ ๐ด ) ) )
27 21 26 eqtrd โŠข ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ( ๐‘ง โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) ) โ†’ ( ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) ๐‘ƒ ๐ด ) = ( ( ๐‘ฆ ยท ( ๐‘ง ๐‘ƒ ๐ด ) ) + ( ๐‘ค ๐‘ƒ ๐ด ) ) )
28 14 adantll โŠข ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ๐‘ง โˆˆ ๐‘‹ ) โ†’ ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) โˆˆ ๐‘‹ )
29 1 18 nvgcl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) โ†’ ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) โˆˆ ๐‘‹ )
30 7 29 mp3an1 โŠข ( ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) โ†’ ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) โˆˆ ๐‘‹ )
31 28 30 sylan โŠข ( ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ๐‘ง โˆˆ ๐‘‹ ) โˆง ๐‘ค โˆˆ ๐‘‹ ) โ†’ ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) โˆˆ ๐‘‹ )
32 31 anasss โŠข ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ( ๐‘ง โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) ) โ†’ ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) โˆˆ ๐‘‹ )
33 oveq1 โŠข ( ๐‘ฅ = ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) โ†’ ( ๐‘ฅ ๐‘ƒ ๐ด ) = ( ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) ๐‘ƒ ๐ด ) )
34 ovex โŠข ( ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) ๐‘ƒ ๐ด ) โˆˆ V
35 33 6 34 fvmpt โŠข ( ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) โˆˆ ๐‘‹ โ†’ ( ๐น โ€˜ ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) ) = ( ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) ๐‘ƒ ๐ด ) )
36 32 35 syl โŠข ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ( ๐‘ง โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) ) โ†’ ( ๐น โ€˜ ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) ) = ( ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) ๐‘ƒ ๐ด ) )
37 oveq1 โŠข ( ๐‘ฅ = ๐‘ง โ†’ ( ๐‘ฅ ๐‘ƒ ๐ด ) = ( ๐‘ง ๐‘ƒ ๐ด ) )
38 ovex โŠข ( ๐‘ง ๐‘ƒ ๐ด ) โˆˆ V
39 37 6 38 fvmpt โŠข ( ๐‘ง โˆˆ ๐‘‹ โ†’ ( ๐น โ€˜ ๐‘ง ) = ( ๐‘ง ๐‘ƒ ๐ด ) )
40 39 ad2antrl โŠข ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ( ๐‘ง โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) ) โ†’ ( ๐น โ€˜ ๐‘ง ) = ( ๐‘ง ๐‘ƒ ๐ด ) )
41 40 oveq2d โŠข ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ( ๐‘ง โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) ) โ†’ ( ๐‘ฆ ยท ( ๐น โ€˜ ๐‘ง ) ) = ( ๐‘ฆ ยท ( ๐‘ง ๐‘ƒ ๐ด ) ) )
42 oveq1 โŠข ( ๐‘ฅ = ๐‘ค โ†’ ( ๐‘ฅ ๐‘ƒ ๐ด ) = ( ๐‘ค ๐‘ƒ ๐ด ) )
43 ovex โŠข ( ๐‘ค ๐‘ƒ ๐ด ) โˆˆ V
44 42 6 43 fvmpt โŠข ( ๐‘ค โˆˆ ๐‘‹ โ†’ ( ๐น โ€˜ ๐‘ค ) = ( ๐‘ค ๐‘ƒ ๐ด ) )
45 44 ad2antll โŠข ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ( ๐‘ง โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) ) โ†’ ( ๐น โ€˜ ๐‘ค ) = ( ๐‘ค ๐‘ƒ ๐ด ) )
46 41 45 oveq12d โŠข ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ( ๐‘ง โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) ) โ†’ ( ( ๐‘ฆ ยท ( ๐น โ€˜ ๐‘ง ) ) + ( ๐น โ€˜ ๐‘ค ) ) = ( ( ๐‘ฆ ยท ( ๐‘ง ๐‘ƒ ๐ด ) ) + ( ๐‘ค ๐‘ƒ ๐ด ) ) )
47 27 36 46 3eqtr4d โŠข ( ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ( ๐‘ง โˆˆ ๐‘‹ โˆง ๐‘ค โˆˆ ๐‘‹ ) ) โ†’ ( ๐น โ€˜ ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) ) = ( ( ๐‘ฆ ยท ( ๐น โ€˜ ๐‘ง ) ) + ( ๐น โ€˜ ๐‘ค ) ) )
48 47 ralrimivva โŠข ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ โ„‚ ) โ†’ โˆ€ ๐‘ง โˆˆ ๐‘‹ โˆ€ ๐‘ค โˆˆ ๐‘‹ ( ๐น โ€˜ ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) ) = ( ( ๐‘ฆ ยท ( ๐น โ€˜ ๐‘ง ) ) + ( ๐น โ€˜ ๐‘ค ) ) )
49 48 ralrimiva โŠข ( ๐ด โˆˆ ๐‘‹ โ†’ โˆ€ ๐‘ฆ โˆˆ โ„‚ โˆ€ ๐‘ง โˆˆ ๐‘‹ โˆ€ ๐‘ค โˆˆ ๐‘‹ ( ๐น โ€˜ ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) ) = ( ( ๐‘ฆ ยท ( ๐น โ€˜ ๐‘ง ) ) + ( ๐น โ€˜ ๐‘ค ) ) )
50 4 cnnv โŠข ๐ถ โˆˆ NrmCVec
51 4 cnnvba โŠข โ„‚ = ( BaseSet โ€˜ ๐ถ )
52 4 cnnvg โŠข + = ( +๐‘ฃ โ€˜ ๐ถ )
53 4 cnnvs โŠข ยท = ( ยท๐‘ OLD โ€˜ ๐ถ )
54 eqid โŠข ( ๐‘ˆ LnOp ๐ถ ) = ( ๐‘ˆ LnOp ๐ถ )
55 1 51 18 52 12 53 54 islno โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ถ โˆˆ NrmCVec ) โ†’ ( ๐น โˆˆ ( ๐‘ˆ LnOp ๐ถ ) โ†” ( ๐น : ๐‘‹ โŸถ โ„‚ โˆง โˆ€ ๐‘ฆ โˆˆ โ„‚ โˆ€ ๐‘ง โˆˆ ๐‘‹ โˆ€ ๐‘ค โˆˆ ๐‘‹ ( ๐น โ€˜ ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) ) = ( ( ๐‘ฆ ยท ( ๐น โ€˜ ๐‘ง ) ) + ( ๐น โ€˜ ๐‘ค ) ) ) ) )
56 7 50 55 mp2an โŠข ( ๐น โˆˆ ( ๐‘ˆ LnOp ๐ถ ) โ†” ( ๐น : ๐‘‹ โŸถ โ„‚ โˆง โˆ€ ๐‘ฆ โˆˆ โ„‚ โˆ€ ๐‘ง โˆˆ ๐‘‹ โˆ€ ๐‘ค โˆˆ ๐‘‹ ( ๐น โ€˜ ( ( ๐‘ฆ ( ยท๐‘ OLD โ€˜ ๐‘ˆ ) ๐‘ง ) ( +๐‘ฃ โ€˜ ๐‘ˆ ) ๐‘ค ) ) = ( ( ๐‘ฆ ยท ( ๐น โ€˜ ๐‘ง ) ) + ( ๐น โ€˜ ๐‘ค ) ) ) )
57 11 49 56 sylanbrc โŠข ( ๐ด โˆˆ ๐‘‹ โ†’ ๐น โˆˆ ( ๐‘ˆ LnOp ๐ถ ) )
58 eqid โŠข ( normCV โ€˜ ๐‘ˆ ) = ( normCV โ€˜ ๐‘ˆ )
59 1 58 nvcl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐ด ) โˆˆ โ„ )
60 7 59 mpan โŠข ( ๐ด โˆˆ ๐‘‹ โ†’ ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐ด ) โˆˆ โ„ )
61 1 58 2 3 sii โŠข ( ( ๐‘ง โˆˆ ๐‘‹ โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( abs โ€˜ ( ๐‘ง ๐‘ƒ ๐ด ) ) โ‰ค ( ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐‘ง ) ยท ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐ด ) ) )
62 61 ancoms โŠข ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ง โˆˆ ๐‘‹ ) โ†’ ( abs โ€˜ ( ๐‘ง ๐‘ƒ ๐ด ) ) โ‰ค ( ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐‘ง ) ยท ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐ด ) ) )
63 39 adantl โŠข ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ง โˆˆ ๐‘‹ ) โ†’ ( ๐น โ€˜ ๐‘ง ) = ( ๐‘ง ๐‘ƒ ๐ด ) )
64 63 fveq2d โŠข ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ง โˆˆ ๐‘‹ ) โ†’ ( abs โ€˜ ( ๐น โ€˜ ๐‘ง ) ) = ( abs โ€˜ ( ๐‘ง ๐‘ƒ ๐ด ) ) )
65 60 recnd โŠข ( ๐ด โˆˆ ๐‘‹ โ†’ ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐ด ) โˆˆ โ„‚ )
66 1 58 nvcl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘ง โˆˆ ๐‘‹ ) โ†’ ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐‘ง ) โˆˆ โ„ )
67 7 66 mpan โŠข ( ๐‘ง โˆˆ ๐‘‹ โ†’ ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐‘ง ) โˆˆ โ„ )
68 67 recnd โŠข ( ๐‘ง โˆˆ ๐‘‹ โ†’ ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐‘ง ) โˆˆ โ„‚ )
69 mulcom โŠข ( ( ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐ด ) โˆˆ โ„‚ โˆง ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐‘ง ) โˆˆ โ„‚ ) โ†’ ( ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐ด ) ยท ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐‘ง ) ) = ( ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐‘ง ) ยท ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐ด ) ) )
70 65 68 69 syl2an โŠข ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ง โˆˆ ๐‘‹ ) โ†’ ( ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐ด ) ยท ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐‘ง ) ) = ( ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐‘ง ) ยท ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐ด ) ) )
71 62 64 70 3brtr4d โŠข ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐‘ง โˆˆ ๐‘‹ ) โ†’ ( abs โ€˜ ( ๐น โ€˜ ๐‘ง ) ) โ‰ค ( ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐ด ) ยท ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐‘ง ) ) )
72 71 ralrimiva โŠข ( ๐ด โˆˆ ๐‘‹ โ†’ โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ( ๐น โ€˜ ๐‘ง ) ) โ‰ค ( ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐ด ) ยท ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐‘ง ) ) )
73 4 cnnvnm โŠข abs = ( normCV โ€˜ ๐ถ )
74 1 58 73 54 5 7 50 blo3i โŠข ( ( ๐น โˆˆ ( ๐‘ˆ LnOp ๐ถ ) โˆง ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐ด ) โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ( ๐น โ€˜ ๐‘ง ) ) โ‰ค ( ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐ด ) ยท ( ( normCV โ€˜ ๐‘ˆ ) โ€˜ ๐‘ง ) ) ) โ†’ ๐น โˆˆ ๐ต )
75 57 60 72 74 syl3anc โŠข ( ๐ด โˆˆ ๐‘‹ โ†’ ๐น โˆˆ ๐ต )