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 , ˙ = 𝑖 W
ipcau.n N = norm W
Assertion ipcau W CPreHil X V Y V X , ˙ Y N X N Y

Proof

Step Hyp Ref Expression
1 ipcau.v V = Base W
2 ipcau.h , ˙ = 𝑖 W
3 ipcau.n N = norm W
4 eqid toCPreHil W = toCPreHil W
5 eqid Scalar W = Scalar W
6 simp1 W CPreHil X V Y V W CPreHil
7 cphphl W CPreHil W PreHil
8 6 7 syl W CPreHil X V Y V W PreHil
9 eqid Base Scalar W = Base Scalar W
10 5 9 cphsca W CPreHil Scalar W = fld 𝑠 Base Scalar W
11 6 10 syl W CPreHil X V Y V Scalar W = fld 𝑠 Base Scalar W
12 5 9 cphsqrtcl W CPreHil x Base Scalar W x 0 x x Base Scalar W
13 6 12 sylan W CPreHil X V Y V x Base Scalar W x 0 x x Base Scalar W
14 1 2 ipge0 W CPreHil x V 0 x , ˙ x
15 6 14 sylan W CPreHil X V Y V x 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 CPreHil X V Y V X V
19 simp3 W CPreHil X V Y V Y V
20 4 1 5 8 11 2 13 15 9 16 17 18 19 ipcau2 W CPreHil X V Y V X , ˙ Y norm toCPreHil W X norm toCPreHil W Y
21 4 3 cphtcphnm W CPreHil N = norm toCPreHil W
22 6 21 syl W CPreHil X V Y V N = norm toCPreHil W
23 22 fveq1d W CPreHil X V Y V N X = norm toCPreHil W X
24 22 fveq1d W CPreHil X V Y V N Y = norm toCPreHil W Y
25 23 24 oveq12d W CPreHil X V Y V N X N Y = norm toCPreHil W X norm toCPreHil W Y
26 20 25 breqtrrd W CPreHil X V Y V X , ˙ Y N X N Y