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 β€˜ ( 𝑋 , π‘Œ ) ) ≀ ( ( 𝑁 β€˜ 𝑋 ) Β· ( 𝑁 β€˜ π‘Œ ) ) )