# Metamath Proof Explorer

## Theorem bcsiHIL

Description: Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of Beran p. 98. (Proved from ZFC version.) (Contributed by NM, 24-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses bcs.1 ${⊢}{A}\in ℋ$
bcs.2 ${⊢}{B}\in ℋ$
Assertion bcsiHIL ${⊢}\left|{A}{\cdot }_{\mathrm{ih}}{B}\right|\le {norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 bcs.1 ${⊢}{A}\in ℋ$
2 bcs.2 ${⊢}{B}\in ℋ$
3 df-hba ${⊢}ℋ=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$
4 eqid ${⊢}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$
5 4 hhnm ${⊢}{norm}_{ℎ}={norm}_{CV}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$
6 4 hhip ${⊢}{\cdot }_{\mathrm{ih}}={\cdot }_{\mathrm{𝑖OLD}}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$
7 4 hhph ${⊢}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in {CPreHil}_{\mathrm{OLD}}$
8 3 5 6 7 1 2 siii ${⊢}\left|{A}{\cdot }_{\mathrm{ih}}{B}\right|\le {norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({B}\right)$