This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sii

Description: Obsolete version of ipcau as of 22-Sep-2024. Schwarz inequality. Part of Lemma 3-2.1(a) of Kreyszig p. 137. This is also called the Cauchy-Schwarz inequality by some authors and Bunjakovaskij-Cauchy-Schwarz inequality by others. See also Theorems bcseqi , bcsiALT , bcsiHIL , csbren . (Contributed by NM, 12-Jan-2008) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses sii.1 
|- X = ( BaseSet ` U )
sii.6 
|- N = ( normCV ` U )
sii.7 
|- P = ( .iOLD ` U )
sii.9 
|- U e. CPreHilOLD
Assertion sii 
|- ( ( A e. X /\ B e. X ) -> ( abs ` ( A P B ) ) <_ ( ( N ` A ) x. ( N ` B ) ) )

Proof

Step Hyp Ref Expression
1 sii.1 
 |-  X = ( BaseSet ` U )
2 sii.6 
 |-  N = ( normCV ` U )
3 sii.7 
 |-  P = ( .iOLD ` U )
4 sii.9 
 |-  U e. CPreHilOLD
5 fvoveq1 
 |-  ( A = if ( A e. X , A , ( 0vec ` U ) ) -> ( abs ` ( A P B ) ) = ( abs ` ( if ( A e. X , A , ( 0vec ` U ) ) P B ) ) )
6 fveq2 
 |-  ( A = if ( A e. X , A , ( 0vec ` U ) ) -> ( N ` A ) = ( N ` if ( A e. X , A , ( 0vec ` U ) ) ) )
7 6 oveq1d 
 |-  ( A = if ( A e. X , A , ( 0vec ` U ) ) -> ( ( N ` A ) x. ( N ` B ) ) = ( ( N ` if ( A e. X , A , ( 0vec ` U ) ) ) x. ( N ` B ) ) )
8 5 7 breq12d 
 |-  ( A = if ( A e. X , A , ( 0vec ` U ) ) -> ( ( abs ` ( A P B ) ) <_ ( ( N ` A ) x. ( N ` B ) ) <-> ( abs ` ( if ( A e. X , A , ( 0vec ` U ) ) P B ) ) <_ ( ( N ` if ( A e. X , A , ( 0vec ` U ) ) ) x. ( N ` B ) ) ) )
9 oveq2 
 |-  ( B = if ( B e. X , B , ( 0vec ` U ) ) -> ( if ( A e. X , A , ( 0vec ` U ) ) P B ) = ( if ( A e. X , A , ( 0vec ` U ) ) P if ( B e. X , B , ( 0vec ` U ) ) ) )
10 9 fveq2d 
 |-  ( B = if ( B e. X , B , ( 0vec ` U ) ) -> ( abs ` ( if ( A e. X , A , ( 0vec ` U ) ) P B ) ) = ( abs ` ( if ( A e. X , A , ( 0vec ` U ) ) P if ( B e. X , B , ( 0vec ` U ) ) ) ) )
11 fveq2 
 |-  ( B = if ( B e. X , B , ( 0vec ` U ) ) -> ( N ` B ) = ( N ` if ( B e. X , B , ( 0vec ` U ) ) ) )
12 11 oveq2d 
 |-  ( B = if ( B e. X , B , ( 0vec ` U ) ) -> ( ( N ` if ( A e. X , A , ( 0vec ` U ) ) ) x. ( N ` B ) ) = ( ( N ` if ( A e. X , A , ( 0vec ` U ) ) ) x. ( N ` if ( B e. X , B , ( 0vec ` U ) ) ) ) )
13 10 12 breq12d 
 |-  ( B = if ( B e. X , B , ( 0vec ` U ) ) -> ( ( abs ` ( if ( A e. X , A , ( 0vec ` U ) ) P B ) ) <_ ( ( N ` if ( A e. X , A , ( 0vec ` U ) ) ) x. ( N ` B ) ) <-> ( abs ` ( if ( A e. X , A , ( 0vec ` U ) ) P if ( B e. X , B , ( 0vec ` U ) ) ) ) <_ ( ( N ` if ( A e. X , A , ( 0vec ` U ) ) ) x. ( N ` if ( B e. X , B , ( 0vec ` U ) ) ) ) ) )
14 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
15 1 14 4 elimph 
 |-  if ( A e. X , A , ( 0vec ` U ) ) e. X
16 1 14 4 elimph 
 |-  if ( B e. X , B , ( 0vec ` U ) ) e. X
17 1 2 3 4 15 16 siii 
 |-  ( abs ` ( if ( A e. X , A , ( 0vec ` U ) ) P if ( B e. X , B , ( 0vec ` U ) ) ) ) <_ ( ( N ` if ( A e. X , A , ( 0vec ` U ) ) ) x. ( N ` if ( B e. X , B , ( 0vec ` U ) ) ) )
18 8 13 17 dedth2h 
 |-  ( ( A e. X /\ B e. X ) -> ( abs ` ( A P B ) ) <_ ( ( N ` A ) x. ( N ` B ) ) )