Metamath Proof Explorer

Theorem bcs2

Description: Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL . (Contributed by NM, 24-May-2006) (New usage is discouraged.)

Ref Expression
Assertion bcs2 
|- ( ( A e. ~H /\ B e. ~H /\ ( normh ` A ) <_ 1 ) -> ( abs ` ( A .ih B ) ) <_ ( normh ` B ) )

Proof

Step Hyp Ref Expression
1 hicl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A .ih B ) e. CC )
2 1 abscld 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( abs ` ( A .ih B ) ) e. RR )
3 2 3adant3 
 |-  ( ( A e. ~H /\ B e. ~H /\ ( normh ` A ) <_ 1 ) -> ( abs ` ( A .ih B ) ) e. RR )
4 normcl 
 |-  ( A e. ~H -> ( normh ` A ) e. RR )
5 normcl 
 |-  ( B e. ~H -> ( normh ` B ) e. RR )
6 remulcl 
 |-  ( ( ( normh ` A ) e. RR /\ ( normh ` B ) e. RR ) -> ( ( normh ` A ) x. ( normh ` B ) ) e. RR )
7 4 5 6 syl2an 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( normh ` A ) x. ( normh ` B ) ) e. RR )
8 7 3adant3 
 |-  ( ( A e. ~H /\ B e. ~H /\ ( normh ` A ) <_ 1 ) -> ( ( normh ` A ) x. ( normh ` B ) ) e. RR )
9 5 3ad2ant2 
 |-  ( ( A e. ~H /\ B e. ~H /\ ( normh ` A ) <_ 1 ) -> ( normh ` B ) e. RR )
10 bcs 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( abs ` ( A .ih B ) ) <_ ( ( normh ` A ) x. ( normh ` B ) ) )
11 10 3adant3 
 |-  ( ( A e. ~H /\ B e. ~H /\ ( normh ` A ) <_ 1 ) -> ( abs ` ( A .ih B ) ) <_ ( ( normh ` A ) x. ( normh ` B ) ) )
12 4 3ad2ant1 
 |-  ( ( A e. ~H /\ B e. ~H /\ ( normh ` A ) <_ 1 ) -> ( normh ` A ) e. RR )
13 normge0 
 |-  ( B e. ~H -> 0 <_ ( normh ` B ) )
14 13 3ad2ant2 
 |-  ( ( A e. ~H /\ B e. ~H /\ ( normh ` A ) <_ 1 ) -> 0 <_ ( normh ` B ) )
15 9 14 jca 
 |-  ( ( A e. ~H /\ B e. ~H /\ ( normh ` A ) <_ 1 ) -> ( ( normh ` B ) e. RR /\ 0 <_ ( normh ` B ) ) )
16 simp3 
 |-  ( ( A e. ~H /\ B e. ~H /\ ( normh ` A ) <_ 1 ) -> ( normh ` A ) <_ 1 )
17 1re 
 |-  1 e. RR
18 lemul1a 
 |-  ( ( ( ( normh ` A ) e. RR /\ 1 e. RR /\ ( ( normh ` B ) e. RR /\ 0 <_ ( normh ` B ) ) ) /\ ( normh ` A ) <_ 1 ) -> ( ( normh ` A ) x. ( normh ` B ) ) <_ ( 1 x. ( normh ` B ) ) )
19 17 18 mp3anl2 
 |-  ( ( ( ( normh ` A ) e. RR /\ ( ( normh ` B ) e. RR /\ 0 <_ ( normh ` B ) ) ) /\ ( normh ` A ) <_ 1 ) -> ( ( normh ` A ) x. ( normh ` B ) ) <_ ( 1 x. ( normh ` B ) ) )
20 12 15 16 19 syl21anc 
 |-  ( ( A e. ~H /\ B e. ~H /\ ( normh ` A ) <_ 1 ) -> ( ( normh ` A ) x. ( normh ` B ) ) <_ ( 1 x. ( normh ` B ) ) )
21 5 recnd 
 |-  ( B e. ~H -> ( normh ` B ) e. CC )
22 21 mullidd 
 |-  ( B e. ~H -> ( 1 x. ( normh ` B ) ) = ( normh ` B ) )
23 22 3ad2ant2 
 |-  ( ( A e. ~H /\ B e. ~H /\ ( normh ` A ) <_ 1 ) -> ( 1 x. ( normh ` B ) ) = ( normh ` B ) )
24 20 23 breqtrd 
 |-  ( ( A e. ~H /\ B e. ~H /\ ( normh ` A ) <_ 1 ) -> ( ( normh ` A ) x. ( normh ` B ) ) <_ ( normh ` B ) )
25 3 8 9 11 24 letrd 
 |-  ( ( A e. ~H /\ B e. ~H /\ ( normh ` A ) <_ 1 ) -> ( abs ` ( A .ih B ) ) <_ ( normh ` B ) )