Metamath Proof Explorer

Theorem sii

Description: Schwarz inequality. Part of Lemma 3-2.1(a) of Kreyszig p. 137. This is also called the Cauchy-Schwarz inequality by some authors and Bunjakovaskij-Cauchy-Schwarz inequality by others. See also theorems bcseqi , bcsiALT , bcsiHIL , csbren . This is Metamath 100 proof #78. (Contributed by NM, 12-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses sii.1 ⊢ X = BaseSet ⁡ U
sii.6 ⊢ N = norm CV ⁡ U
sii.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
sii.9 ⊢ U ∈ CPreHil OLD
Assertion sii ⊢ A ∈ X ∧ B ∈ X → A P B ≤ N ⁡ A ⁢ N ⁡ B

Proof

Step Hyp Ref Expression
1 sii.1 ⊢ X = BaseSet ⁡ U
2 sii.6 ⊢ N = norm CV ⁡ U
3 sii.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
4 sii.9 ⊢ U ∈ CPreHil OLD
5 fvoveq1 ⊢ A = if A ∈ X A 0 vec ⁡ U → A P B = if A ∈ X A 0 vec ⁡ U P B
6 fveq2 ⊢ A = if A ∈ X A 0 vec ⁡ U → N ⁡ A = N ⁡ if A ∈ X A 0 vec ⁡ U
7 6 oveq1d ⊢ A = if A ∈ X A 0 vec ⁡ U → N ⁡ A ⁢ N ⁡ B = N ⁡ if A ∈ X A 0 vec ⁡ U ⁢ N ⁡ B
8 5 7 breq12d ⊢ A = if A ∈ X A 0 vec ⁡ U → A P B ≤ N ⁡ A ⁢ N ⁡ B ↔ if A ∈ X A 0 vec ⁡ U P B ≤ N ⁡ if A ∈ X A 0 vec ⁡ U ⁢ N ⁡ B
9 oveq2 ⊢ B = if B ∈ X B 0 vec ⁡ U → if A ∈ X A 0 vec ⁡ U P B = if A ∈ X A 0 vec ⁡ U P if B ∈ X B 0 vec ⁡ U
10 9 fveq2d ⊢ B = if B ∈ X B 0 vec ⁡ U → if A ∈ X A 0 vec ⁡ U P B = if A ∈ X A 0 vec ⁡ U P if B ∈ X B 0 vec ⁡ U
11 fveq2 ⊢ B = if B ∈ X B 0 vec ⁡ U → N ⁡ B = N ⁡ if B ∈ X B 0 vec ⁡ U
12 11 oveq2d ⊢ B = if B ∈ X B 0 vec ⁡ U → N ⁡ if A ∈ X A 0 vec ⁡ U ⁢ N ⁡ B = N ⁡ if A ∈ X A 0 vec ⁡ U ⁢ N ⁡ if B ∈ X B 0 vec ⁡ U
13 10 12 breq12d ⊢ B = if B ∈ X B 0 vec ⁡ U → if A ∈ X A 0 vec ⁡ U P B ≤ N ⁡ if A ∈ X A 0 vec ⁡ U ⁢ N ⁡ B ↔ if A ∈ X A 0 vec ⁡ U P if B ∈ X B 0 vec ⁡ U ≤ N ⁡ if A ∈ X A 0 vec ⁡ U ⁢ N ⁡ if B ∈ X B 0 vec ⁡ U
14 eqid ⊢ 0 vec ⁡ U = 0 vec ⁡ U
15 1 14 4 elimph ⊢ if A ∈ X A 0 vec ⁡ U ∈ X
16 1 14 4 elimph ⊢ if B ∈ X B 0 vec ⁡ U ∈ X
17 1 2 3 4 15 16 siii ⊢ if A ∈ X A 0 vec ⁡ U P if B ∈ X B 0 vec ⁡ U ≤ N ⁡ if A ∈ X A 0 vec ⁡ U ⁢ N ⁡ if B ∈ X B 0 vec ⁡ U
18 8 13 17 dedth2h ⊢ A ∈ X ∧ B ∈ X → A P B ≤ N ⁡ A ⁢ N ⁡ B