Metamath Proof Explorer

Theorem ipcau

Description: The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space. Part of Lemma 3.2-1(a) of Kreyszig p. 137. This is Metamath 100 proof #78. (Contributed by NM, 12-Jan-2008) (Revised by Mario Carneiro, 11-Oct-2015)

Ref Expression
Hypotheses ipcau.v 
|- V = ( Base ` W )
ipcau.h 
|- ., = ( .i ` W )
ipcau.n 
|- N = ( norm ` W )
Assertion ipcau 
|- ( ( W e. CPreHil /\ X e. V /\ Y e. V ) -> ( abs ` ( X ., Y ) ) <_ ( ( N ` X ) x. ( N ` Y ) ) )

Proof

Step Hyp Ref Expression
1 ipcau.v 
 |-  V = ( Base ` W )
2 ipcau.h 
 |-  ., = ( .i ` W )
3 ipcau.n 
 |-  N = ( norm ` W )
4 eqid 
 |-  ( toCPreHil ` W ) = ( toCPreHil ` W )
5 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
6 simp1 
 |-  ( ( W e. CPreHil /\ X e. V /\ Y e. V ) -> W e. CPreHil )
7 cphphl 
 |-  ( W e. CPreHil -> W e. PreHil )
8 6 7 syl 
 |-  ( ( W e. CPreHil /\ X e. V /\ Y e. V ) -> W e. PreHil )
9 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
10 5 9 cphsca 
 |-  ( W e. CPreHil -> ( Scalar ` W ) = ( CCfld |`s ( Base ` ( Scalar ` W ) ) ) )
11 6 10 syl 
 |-  ( ( W e. CPreHil /\ X e. V /\ Y e. V ) -> ( Scalar ` W ) = ( CCfld |`s ( Base ` ( Scalar ` W ) ) ) )
12 5 9 cphsqrtcl 
 |-  ( ( W e. CPreHil /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ x e. RR /\ 0 <_ x ) ) -> ( sqrt ` x ) e. ( Base ` ( Scalar ` W ) ) )
13 6 12 sylan 
 |-  ( ( ( W e. CPreHil /\ X e. V /\ Y e. V ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ x e. RR /\ 0 <_ x ) ) -> ( sqrt ` x ) e. ( Base ` ( Scalar ` W ) ) )
14 1 2 ipge0 
 |-  ( ( W e. CPreHil /\ x e. V ) -> 0 <_ ( x ., x ) )
15 6 14 sylan 
 |-  ( ( ( W e. CPreHil /\ X e. V /\ Y e. V ) /\ x e. V ) -> 0 <_ ( x ., x ) )
16 eqid 
 |-  ( norm ` ( toCPreHil ` W ) ) = ( norm ` ( toCPreHil ` W ) )
17 eqid 
 |-  ( ( Y ., X ) / ( Y ., Y ) ) = ( ( Y ., X ) / ( Y ., Y ) )
18 simp2 
 |-  ( ( W e. CPreHil /\ X e. V /\ Y e. V ) -> X e. V )
19 simp3 
 |-  ( ( W e. CPreHil /\ X e. V /\ Y e. V ) -> Y e. V )
20 4 1 5 8 11 2 13 15 9 16 17 18 19 ipcau2 
 |-  ( ( W e. CPreHil /\ X e. V /\ Y e. V ) -> ( abs ` ( X ., Y ) ) <_ ( ( ( norm ` ( toCPreHil ` W ) ) ` X ) x. ( ( norm ` ( toCPreHil ` W ) ) ` Y ) ) )
21 4 3 cphtcphnm 
 |-  ( W e. CPreHil -> N = ( norm ` ( toCPreHil ` W ) ) )
22 6 21 syl 
 |-  ( ( W e. CPreHil /\ X e. V /\ Y e. V ) -> N = ( norm ` ( toCPreHil ` W ) ) )
23 22 fveq1d 
 |-  ( ( W e. CPreHil /\ X e. V /\ Y e. V ) -> ( N ` X ) = ( ( norm ` ( toCPreHil ` W ) ) ` X ) )
24 22 fveq1d 
 |-  ( ( W e. CPreHil /\ X e. V /\ Y e. V ) -> ( N ` Y ) = ( ( norm ` ( toCPreHil ` W ) ) ` Y ) )
25 23 24 oveq12d 
 |-  ( ( W e. CPreHil /\ X e. V /\ Y e. V ) -> ( ( N ` X ) x. ( N ` Y ) ) = ( ( ( norm ` ( toCPreHil ` W ) ) ` X ) x. ( ( norm ` ( toCPreHil ` W ) ) ` Y ) ) )
26 20 25 breqtrrd 
 |-  ( ( W e. CPreHil /\ X e. V /\ Y e. V ) -> ( abs ` ( X ., Y ) ) <_ ( ( N ` X ) x. ( N ` Y ) ) )