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 e. ~H
	bcs.2	|- B e. ~H
Assertion	bcsiHIL	|- ( abs ` ( A .ih B ) ) <_ ( ( normh ` A ) x. ( normh ` B ) )

Proof

Step	Hyp	Ref	Expression
1		bcs.1	|- A e. ~H
2		bcs.2	|- B e. ~H
3		df-hba	|- ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )
4		eqid	|- <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
5	4	hhnm	|- normh = ( normCV ` <. <. +h , .h >. , normh >. )
6	4	hhip	|- .ih = ( .iOLD ` <. <. +h , .h >. , normh >. )
7	4	hhph	|- <. <. +h , .h >. , normh >. e. CPreHilOLD
8	3 5 6 7 1 2	siii	|- ( abs ` ( A .ih B ) ) <_ ( ( normh ` A ) x. ( normh ` B ) )