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 \mathscr{H}$$
	bcs.2	$$⊢B\in \mathscr{H}$$
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 \mathscr{H}$$
2		bcs.2	$$⊢B\in \mathscr{H}$$
3		df-hba	$$⊢\mathscr{H}=\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)$$