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