# 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 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left|{A}{\cdot }_{\mathrm{ih}}{B}\right|\le {norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 fvoveq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left|{A}{\cdot }_{\mathrm{ih}}{B}\right|=\left|if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{B}\right|$
2 fveq2 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {norm}_{ℎ}\left({A}\right)={norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
3 2 oveq1d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({B}\right)={norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){norm}_{ℎ}\left({B}\right)$
4 1 3 breq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left(\left|{A}{\cdot }_{\mathrm{ih}}{B}\right|\le {norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({B}\right)↔\left|if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{B}\right|\le {norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){norm}_{ℎ}\left({B}\right)\right)$
5 oveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{B}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)$
6 5 fveq2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left|if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{B}\right|=\left|if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right|$
7 fveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {norm}_{ℎ}\left({B}\right)={norm}_{ℎ}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
8 7 oveq2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){norm}_{ℎ}\left({B}\right)={norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){norm}_{ℎ}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
9 6 8 breq12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left(\left|if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{B}\right|\le {norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){norm}_{ℎ}\left({B}\right)↔\left|if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right|\le {norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){norm}_{ℎ}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)$
10 ifhvhv0 ${⊢}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in ℋ$
11 ifhvhv0 ${⊢}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\in ℋ$
12 10 11 bcsiHIL ${⊢}\left|if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right|\le {norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){norm}_{ℎ}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
13 4 9 12 dedth2h ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left|{A}{\cdot }_{\mathrm{ih}}{B}\right|\le {norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({B}\right)$