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 ABAihBnormAnormB

Proof

Step Hyp Ref Expression
1 fvoveq1 A=ifAA0AihB=ifAA0ihB
2 fveq2 A=ifAA0normA=normifAA0
3 2 oveq1d A=ifAA0normAnormB=normifAA0normB
4 1 3 breq12d A=ifAA0AihBnormAnormBifAA0ihBnormifAA0normB
5 oveq2 B=ifBB0ifAA0ihB=ifAA0ihifBB0
6 5 fveq2d B=ifBB0ifAA0ihB=ifAA0ihifBB0
7 fveq2 B=ifBB0normB=normifBB0
8 7 oveq2d B=ifBB0normifAA0normB=normifAA0normifBB0
9 6 8 breq12d B=ifBB0ifAA0ihBnormifAA0normBifAA0ihifBB0normifAA0normifBB0
10 ifhvhv0 ifAA0
11 ifhvhv0 ifBB0
12 10 11 bcsiHIL ifAA0ihifBB0normifAA0normifBB0
13 4 9 12 dedth2h ABAihBnormAnormB