Metamath Proof Explorer

Theorem ipcau

Description: The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space. (Contributed 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