Metamath Proof Explorer

Theorem bcs3

Description: Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL . (Contributed by NM, 26-May-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 abshicom ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = B ⋅ ih A
2 1 3adant3 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ norm ℎ ⁡ B ≤ 1 → A ⋅ ih B = B ⋅ ih A
3 bcs2 ⊢ B ∈ ℋ ∧ A ∈ ℋ ∧ norm ℎ ⁡ B ≤ 1 → B ⋅ ih A ≤ norm ℎ ⁡ A
4 3 3com12 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ norm ℎ ⁡ B ≤ 1 → B ⋅ ih A ≤ norm ℎ ⁡ A
5 2 4 eqbrtrd ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ norm ℎ ⁡ B ≤ 1 → A ⋅ ih B ≤ norm ℎ ⁡ A