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 𝑉 = ( Base ‘ 𝑊 )
ipcau.h , = ( ·𝑖𝑊 )
ipcau.n 𝑁 = ( norm ‘ 𝑊 )
Assertion ipcau ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋𝑉𝑌𝑉 ) → ( abs ‘ ( 𝑋 , 𝑌 ) ) ≤ ( ( 𝑁𝑋 ) · ( 𝑁𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 ipcau.v 𝑉 = ( Base ‘ 𝑊 )
2 ipcau.h , = ( ·𝑖𝑊 )
3 ipcau.n 𝑁 = ( norm ‘ 𝑊 )
4 eqid ( toℂPreHil ‘ 𝑊 ) = ( toℂPreHil ‘ 𝑊 )
5 eqid ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
6 simp1 ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋𝑉𝑌𝑉 ) → 𝑊 ∈ ℂPreHil )
7 cphphl ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil )
8 6 7 syl ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋𝑉𝑌𝑉 ) → 𝑊 ∈ PreHil )
9 eqid ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
10 5 9 cphsca ( 𝑊 ∈ ℂPreHil → ( Scalar ‘ 𝑊 ) = ( ℂflds ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
11 6 10 syl ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋𝑉𝑌𝑉 ) → ( Scalar ‘ 𝑊 ) = ( ℂflds ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
12 5 9 cphsqrtcl ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( √ ‘ 𝑥 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
13 6 12 sylan ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋𝑉𝑌𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( √ ‘ 𝑥 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
14 1 2 ipge0 ( ( 𝑊 ∈ ℂPreHil ∧ 𝑥𝑉 ) → 0 ≤ ( 𝑥 , 𝑥 ) )
15 6 14 sylan ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋𝑉𝑌𝑉 ) ∧ 𝑥𝑉 ) → 0 ≤ ( 𝑥 , 𝑥 ) )
16 eqid ( norm ‘ ( toℂPreHil ‘ 𝑊 ) ) = ( norm ‘ ( toℂPreHil ‘ 𝑊 ) )
17 eqid ( ( 𝑌 , 𝑋 ) / ( 𝑌 , 𝑌 ) ) = ( ( 𝑌 , 𝑋 ) / ( 𝑌 , 𝑌 ) )
18 simp2 ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋𝑉𝑌𝑉 ) → 𝑋𝑉 )
19 simp3 ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋𝑉𝑌𝑉 ) → 𝑌𝑉 )
20 4 1 5 8 11 2 13 15 9 16 17 18 19 ipcau2 ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋𝑉𝑌𝑉 ) → ( abs ‘ ( 𝑋 , 𝑌 ) ) ≤ ( ( ( norm ‘ ( toℂPreHil ‘ 𝑊 ) ) ‘ 𝑋 ) · ( ( norm ‘ ( toℂPreHil ‘ 𝑊 ) ) ‘ 𝑌 ) ) )
21 4 3 cphtcphnm ( 𝑊 ∈ ℂPreHil → 𝑁 = ( norm ‘ ( toℂPreHil ‘ 𝑊 ) ) )
22 6 21 syl ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋𝑉𝑌𝑉 ) → 𝑁 = ( norm ‘ ( toℂPreHil ‘ 𝑊 ) ) )
23 22 fveq1d ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋𝑉𝑌𝑉 ) → ( 𝑁𝑋 ) = ( ( norm ‘ ( toℂPreHil ‘ 𝑊 ) ) ‘ 𝑋 ) )
24 22 fveq1d ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋𝑉𝑌𝑉 ) → ( 𝑁𝑌 ) = ( ( norm ‘ ( toℂPreHil ‘ 𝑊 ) ) ‘ 𝑌 ) )
25 23 24 oveq12d ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋𝑉𝑌𝑉 ) → ( ( 𝑁𝑋 ) · ( 𝑁𝑌 ) ) = ( ( ( norm ‘ ( toℂPreHil ‘ 𝑊 ) ) ‘ 𝑋 ) · ( ( norm ‘ ( toℂPreHil ‘ 𝑊 ) ) ‘ 𝑌 ) ) )
26 20 25 breqtrrd ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋𝑉𝑌𝑉 ) → ( abs ‘ ( 𝑋 , 𝑌 ) ) ≤ ( ( 𝑁𝑋 ) · ( 𝑁𝑌 ) ) )