Metamath Proof Explorer

Theorem bcs3

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

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

Proof

Step Hyp Ref Expression
1 abshicom 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( abs ` ( A .ih B ) ) = ( abs ` ( B .ih A ) ) )
2 1 3adant3 
 |-  ( ( A e. ~H /\ B e. ~H /\ ( normh ` B ) <_ 1 ) -> ( abs ` ( A .ih B ) ) = ( abs ` ( B .ih A ) ) )
3 bcs2 
 |-  ( ( B e. ~H /\ A e. ~H /\ ( normh ` B ) <_ 1 ) -> ( abs ` ( B .ih A ) ) <_ ( normh ` A ) )
4 3 3com12 
 |-  ( ( A e. ~H /\ B e. ~H /\ ( normh ` B ) <_ 1 ) -> ( abs ` ( B .ih A ) ) <_ ( normh ` A ) )
5 2 4 eqbrtrd 
 |-  ( ( A e. ~H /\ B e. ~H /\ ( normh ` B ) <_ 1 ) -> ( abs ` ( A .ih B ) ) <_ ( normh ` A ) )