Metamath Proof Explorer

Theorem bcs

Description: Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of Beran p. 98. (Contributed by NM, 16-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion bcs ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B ≤ norm ℎ ⁡ A ⁢ norm ℎ ⁡ B

Proof

Step Hyp Ref Expression
1 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih B = if A ∈ ℋ A 0 ℎ ⋅ ih B
2 fveq2 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ
3 2 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A ⁢ norm ℎ ⁡ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ ⁢ norm ℎ ⁡ B
4 1 3 breq12d ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih B ≤ norm ℎ ⁡ A ⁢ norm ℎ ⁡ B ↔ if A ∈ ℋ A 0 ℎ ⋅ ih B ≤ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ ⁢ norm ℎ ⁡ B
5 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih B = if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ
6 5 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih B = if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ
7 fveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ B = norm ℎ ⁡ if B ∈ ℋ B 0 ℎ
8 7 oveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ ⁢ norm ℎ ⁡ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ ⁢ norm ℎ ⁡ if B ∈ ℋ B 0 ℎ
9 6 8 breq12d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih B ≤ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ ⁢ norm ℎ ⁡ B ↔ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ ≤ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ ⁢ norm ℎ ⁡ if B ∈ ℋ B 0 ℎ
10 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
11 ifhvhv0 ⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ
12 10 11 bcsiHIL ⊢ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ ≤ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ ⁢ norm ℎ ⁡ if B ∈ ℋ B 0 ℎ
13 4 9 12 dedth2h ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B ≤ norm ℎ ⁡ A ⁢ norm ℎ ⁡ B