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

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 ‘ 𝑊 ) = ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
11 6 10 syl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( Scalar ‘ 𝑊 ) = ( ℂfld ↾s ( 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 ‘ ( 𝑋 , 𝑌 ) ) ≤ ( ( 𝑁 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) )