# 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 ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≤ ( ( norm𝐴 ) · ( norm𝐵 ) ) )

### Proof

Step Hyp Ref Expression
1 fvoveq1 ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) = ( abs ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ·ih 𝐵 ) ) )
2 fveq2 ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( norm𝐴 ) = ( norm ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) )
3 2 oveq1d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( norm𝐴 ) · ( norm𝐵 ) ) = ( ( norm ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) · ( norm𝐵 ) ) )
4 1 3 breq12d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≤ ( ( norm𝐴 ) · ( norm𝐵 ) ) ↔ ( abs ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ·ih 𝐵 ) ) ≤ ( ( norm ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) · ( norm𝐵 ) ) ) )
5 oveq2 ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ·ih 𝐵 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) )
6 5 fveq2d ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( abs ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ·ih 𝐵 ) ) = ( abs ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) )
7 fveq2 ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( norm𝐵 ) = ( norm ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) )
8 7 oveq2d ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( ( norm ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) · ( norm𝐵 ) ) = ( ( norm ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) · ( norm ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) )
9 6 8 breq12d ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( ( abs ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ·ih 𝐵 ) ) ≤ ( ( norm ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) · ( norm𝐵 ) ) ↔ ( abs ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) ≤ ( ( norm ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) · ( norm ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) ) )
10 ifhvhv0 if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ∈ ℋ
11 ifhvhv0 if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ∈ ℋ
12 10 11 bcsiHIL ( abs ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ·ih if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) ≤ ( ( norm ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) · ( norm ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) )
13 4 9 12 dedth2h ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≤ ( ( norm𝐴 ) · ( norm𝐵 ) ) )