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 ) )