Metamath Proof Explorer


Theorem bcsiALT

Description: Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of Beran p. 98. (Contributed by NM, 11-Oct-1999) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses bcs.1
|- A e. ~H
bcs.2
|- B e. ~H
Assertion bcsiALT
|- ( abs ` ( A .ih B ) ) <_ ( ( normh ` A ) x. ( normh ` B ) )

Proof

Step Hyp Ref Expression
1 bcs.1
 |-  A e. ~H
2 bcs.2
 |-  B e. ~H
3 fveq2
 |-  ( ( A .ih B ) = 0 -> ( abs ` ( A .ih B ) ) = ( abs ` 0 ) )
4 abs0
 |-  ( abs ` 0 ) = 0
5 normge0
 |-  ( A e. ~H -> 0 <_ ( normh ` A ) )
6 1 5 ax-mp
 |-  0 <_ ( normh ` A )
7 normge0
 |-  ( B e. ~H -> 0 <_ ( normh ` B ) )
8 2 7 ax-mp
 |-  0 <_ ( normh ` B )
9 1 normcli
 |-  ( normh ` A ) e. RR
10 2 normcli
 |-  ( normh ` B ) e. RR
11 9 10 mulge0i
 |-  ( ( 0 <_ ( normh ` A ) /\ 0 <_ ( normh ` B ) ) -> 0 <_ ( ( normh ` A ) x. ( normh ` B ) ) )
12 6 8 11 mp2an
 |-  0 <_ ( ( normh ` A ) x. ( normh ` B ) )
13 4 12 eqbrtri
 |-  ( abs ` 0 ) <_ ( ( normh ` A ) x. ( normh ` B ) )
14 3 13 eqbrtrdi
 |-  ( ( A .ih B ) = 0 -> ( abs ` ( A .ih B ) ) <_ ( ( normh ` A ) x. ( normh ` B ) ) )
15 df-ne
 |-  ( ( A .ih B ) =/= 0 <-> -. ( A .ih B ) = 0 )
16 2 1 his1i
 |-  ( B .ih A ) = ( * ` ( A .ih B ) )
17 16 oveq2i
 |-  ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( B .ih A ) ) = ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( * ` ( A .ih B ) ) )
18 17 oveq2i
 |-  ( ( ( * ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) x. ( A .ih B ) ) + ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( B .ih A ) ) ) = ( ( ( * ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) x. ( A .ih B ) ) + ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( * ` ( A .ih B ) ) ) )
19 1 2 hicli
 |-  ( A .ih B ) e. CC
20 abslem2
 |-  ( ( ( A .ih B ) e. CC /\ ( A .ih B ) =/= 0 ) -> ( ( ( * ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) x. ( A .ih B ) ) + ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( * ` ( A .ih B ) ) ) ) = ( 2 x. ( abs ` ( A .ih B ) ) ) )
21 19 20 mpan
 |-  ( ( A .ih B ) =/= 0 -> ( ( ( * ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) x. ( A .ih B ) ) + ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( * ` ( A .ih B ) ) ) ) = ( 2 x. ( abs ` ( A .ih B ) ) ) )
22 18 21 eqtr2id
 |-  ( ( A .ih B ) =/= 0 -> ( 2 x. ( abs ` ( A .ih B ) ) ) = ( ( ( * ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) x. ( A .ih B ) ) + ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( B .ih A ) ) ) )
23 19 abs00i
 |-  ( ( abs ` ( A .ih B ) ) = 0 <-> ( A .ih B ) = 0 )
24 23 necon3bii
 |-  ( ( abs ` ( A .ih B ) ) =/= 0 <-> ( A .ih B ) =/= 0 )
25 19 abscli
 |-  ( abs ` ( A .ih B ) ) e. RR
26 25 recni
 |-  ( abs ` ( A .ih B ) ) e. CC
27 19 26 divclzi
 |-  ( ( abs ` ( A .ih B ) ) =/= 0 -> ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) e. CC )
28 19 26 divreczi
 |-  ( ( abs ` ( A .ih B ) ) =/= 0 -> ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) = ( ( A .ih B ) x. ( 1 / ( abs ` ( A .ih B ) ) ) ) )
29 28 fveq2d
 |-  ( ( abs ` ( A .ih B ) ) =/= 0 -> ( abs ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) = ( abs ` ( ( A .ih B ) x. ( 1 / ( abs ` ( A .ih B ) ) ) ) ) )
30 26 recclzi
 |-  ( ( abs ` ( A .ih B ) ) =/= 0 -> ( 1 / ( abs ` ( A .ih B ) ) ) e. CC )
31 absmul
 |-  ( ( ( A .ih B ) e. CC /\ ( 1 / ( abs ` ( A .ih B ) ) ) e. CC ) -> ( abs ` ( ( A .ih B ) x. ( 1 / ( abs ` ( A .ih B ) ) ) ) ) = ( ( abs ` ( A .ih B ) ) x. ( abs ` ( 1 / ( abs ` ( A .ih B ) ) ) ) ) )
32 19 30 31 sylancr
 |-  ( ( abs ` ( A .ih B ) ) =/= 0 -> ( abs ` ( ( A .ih B ) x. ( 1 / ( abs ` ( A .ih B ) ) ) ) ) = ( ( abs ` ( A .ih B ) ) x. ( abs ` ( 1 / ( abs ` ( A .ih B ) ) ) ) ) )
33 25 rerecclzi
 |-  ( ( abs ` ( A .ih B ) ) =/= 0 -> ( 1 / ( abs ` ( A .ih B ) ) ) e. RR )
34 0re
 |-  0 e. RR
35 33 34 jctil
 |-  ( ( abs ` ( A .ih B ) ) =/= 0 -> ( 0 e. RR /\ ( 1 / ( abs ` ( A .ih B ) ) ) e. RR ) )
36 19 absgt0i
 |-  ( ( A .ih B ) =/= 0 <-> 0 < ( abs ` ( A .ih B ) ) )
37 24 36 bitri
 |-  ( ( abs ` ( A .ih B ) ) =/= 0 <-> 0 < ( abs ` ( A .ih B ) ) )
38 25 recgt0i
 |-  ( 0 < ( abs ` ( A .ih B ) ) -> 0 < ( 1 / ( abs ` ( A .ih B ) ) ) )
39 37 38 sylbi
 |-  ( ( abs ` ( A .ih B ) ) =/= 0 -> 0 < ( 1 / ( abs ` ( A .ih B ) ) ) )
40 ltle
 |-  ( ( 0 e. RR /\ ( 1 / ( abs ` ( A .ih B ) ) ) e. RR ) -> ( 0 < ( 1 / ( abs ` ( A .ih B ) ) ) -> 0 <_ ( 1 / ( abs ` ( A .ih B ) ) ) ) )
41 35 39 40 sylc
 |-  ( ( abs ` ( A .ih B ) ) =/= 0 -> 0 <_ ( 1 / ( abs ` ( A .ih B ) ) ) )
42 33 41 absidd
 |-  ( ( abs ` ( A .ih B ) ) =/= 0 -> ( abs ` ( 1 / ( abs ` ( A .ih B ) ) ) ) = ( 1 / ( abs ` ( A .ih B ) ) ) )
43 42 oveq2d
 |-  ( ( abs ` ( A .ih B ) ) =/= 0 -> ( ( abs ` ( A .ih B ) ) x. ( abs ` ( 1 / ( abs ` ( A .ih B ) ) ) ) ) = ( ( abs ` ( A .ih B ) ) x. ( 1 / ( abs ` ( A .ih B ) ) ) ) )
44 32 43 eqtrd
 |-  ( ( abs ` ( A .ih B ) ) =/= 0 -> ( abs ` ( ( A .ih B ) x. ( 1 / ( abs ` ( A .ih B ) ) ) ) ) = ( ( abs ` ( A .ih B ) ) x. ( 1 / ( abs ` ( A .ih B ) ) ) ) )
45 26 recidzi
 |-  ( ( abs ` ( A .ih B ) ) =/= 0 -> ( ( abs ` ( A .ih B ) ) x. ( 1 / ( abs ` ( A .ih B ) ) ) ) = 1 )
46 29 44 45 3eqtrd
 |-  ( ( abs ` ( A .ih B ) ) =/= 0 -> ( abs ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) = 1 )
47 27 46 jca
 |-  ( ( abs ` ( A .ih B ) ) =/= 0 -> ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) e. CC /\ ( abs ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) = 1 ) )
48 24 47 sylbir
 |-  ( ( A .ih B ) =/= 0 -> ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) e. CC /\ ( abs ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) = 1 ) )
49 1 2 normlem7tALT
 |-  ( ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) e. CC /\ ( abs ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) = 1 ) -> ( ( ( * ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) x. ( A .ih B ) ) + ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( B .ih A ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) )
50 48 49 syl
 |-  ( ( A .ih B ) =/= 0 -> ( ( ( * ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) x. ( A .ih B ) ) + ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( B .ih A ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) )
51 22 50 eqbrtrd
 |-  ( ( A .ih B ) =/= 0 -> ( 2 x. ( abs ` ( A .ih B ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) )
52 15 51 sylbir
 |-  ( -. ( A .ih B ) = 0 -> ( 2 x. ( abs ` ( A .ih B ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) )
53 10 recni
 |-  ( normh ` B ) e. CC
54 9 recni
 |-  ( normh ` A ) e. CC
55 normval
 |-  ( B e. ~H -> ( normh ` B ) = ( sqrt ` ( B .ih B ) ) )
56 2 55 ax-mp
 |-  ( normh ` B ) = ( sqrt ` ( B .ih B ) )
57 normval
 |-  ( A e. ~H -> ( normh ` A ) = ( sqrt ` ( A .ih A ) ) )
58 1 57 ax-mp
 |-  ( normh ` A ) = ( sqrt ` ( A .ih A ) )
59 56 58 oveq12i
 |-  ( ( normh ` B ) x. ( normh ` A ) ) = ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) )
60 53 54 59 mulcomli
 |-  ( ( normh ` A ) x. ( normh ` B ) ) = ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) )
61 60 breq2i
 |-  ( ( abs ` ( A .ih B ) ) <_ ( ( normh ` A ) x. ( normh ` B ) ) <-> ( abs ` ( A .ih B ) ) <_ ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) )
62 2pos
 |-  0 < 2
63 hiidge0
 |-  ( B e. ~H -> 0 <_ ( B .ih B ) )
64 hiidrcl
 |-  ( B e. ~H -> ( B .ih B ) e. RR )
65 2 64 ax-mp
 |-  ( B .ih B ) e. RR
66 65 sqrtcli
 |-  ( 0 <_ ( B .ih B ) -> ( sqrt ` ( B .ih B ) ) e. RR )
67 2 63 66 mp2b
 |-  ( sqrt ` ( B .ih B ) ) e. RR
68 hiidge0
 |-  ( A e. ~H -> 0 <_ ( A .ih A ) )
69 hiidrcl
 |-  ( A e. ~H -> ( A .ih A ) e. RR )
70 1 69 ax-mp
 |-  ( A .ih A ) e. RR
71 70 sqrtcli
 |-  ( 0 <_ ( A .ih A ) -> ( sqrt ` ( A .ih A ) ) e. RR )
72 1 68 71 mp2b
 |-  ( sqrt ` ( A .ih A ) ) e. RR
73 67 72 remulcli
 |-  ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) e. RR
74 2re
 |-  2 e. RR
75 25 73 74 lemul2i
 |-  ( 0 < 2 -> ( ( abs ` ( A .ih B ) ) <_ ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) <-> ( 2 x. ( abs ` ( A .ih B ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) ) )
76 62 75 ax-mp
 |-  ( ( abs ` ( A .ih B ) ) <_ ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) <-> ( 2 x. ( abs ` ( A .ih B ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) )
77 61 76 bitri
 |-  ( ( abs ` ( A .ih B ) ) <_ ( ( normh ` A ) x. ( normh ` B ) ) <-> ( 2 x. ( abs ` ( A .ih B ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) )
78 52 77 sylibr
 |-  ( -. ( A .ih B ) = 0 -> ( abs ` ( A .ih B ) ) <_ ( ( normh ` A ) x. ( normh ` B ) ) )
79 14 78 pm2.61i
 |-  ( abs ` ( A .ih B ) ) <_ ( ( normh ` A ) x. ( normh ` B ) )