Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  bcs Structured version   Visualization version   GIF version

Theorem bcs 28952
 Description: Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression
bcs ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (abs‘(𝐴 ·ih 𝐵)) ≤ ((norm𝐴) · (norm𝐵)))

Proof of Theorem bcs
StepHypRef Expression
1 fvoveq1 7173 . . 3 (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0) → (abs‘(𝐴 ·ih 𝐵)) = (abs‘(if(𝐴 ∈ ℋ, 𝐴, 0) ·ih 𝐵)))
2 fveq2 6665 . . . 4 (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0) → (norm𝐴) = (norm‘if(𝐴 ∈ ℋ, 𝐴, 0)))
32oveq1d 7165 . . 3 (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0) → ((norm𝐴) · (norm𝐵)) = ((norm‘if(𝐴 ∈ ℋ, 𝐴, 0)) · (norm𝐵)))
41, 3breq12d 5072 . 2 (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0) → ((abs‘(𝐴 ·ih 𝐵)) ≤ ((norm𝐴) · (norm𝐵)) ↔ (abs‘(if(𝐴 ∈ ℋ, 𝐴, 0) ·ih 𝐵)) ≤ ((norm‘if(𝐴 ∈ ℋ, 𝐴, 0)) · (norm𝐵))))
5 oveq2 7158 . . . 4 (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0) → (if(𝐴 ∈ ℋ, 𝐴, 0) ·ih 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0) ·ih if(𝐵 ∈ ℋ, 𝐵, 0)))
65fveq2d 6669 . . 3 (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0) → (abs‘(if(𝐴 ∈ ℋ, 𝐴, 0) ·ih 𝐵)) = (abs‘(if(𝐴 ∈ ℋ, 𝐴, 0) ·ih if(𝐵 ∈ ℋ, 𝐵, 0))))
7 fveq2 6665 . . . 4 (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0) → (norm𝐵) = (norm‘if(𝐵 ∈ ℋ, 𝐵, 0)))
87oveq2d 7166 . . 3 (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0) → ((norm‘if(𝐴 ∈ ℋ, 𝐴, 0)) · (norm𝐵)) = ((norm‘if(𝐴 ∈ ℋ, 𝐴, 0)) · (norm‘if(𝐵 ∈ ℋ, 𝐵, 0))))
96, 8breq12d 5072 . 2 (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0) → ((abs‘(if(𝐴 ∈ ℋ, 𝐴, 0) ·ih 𝐵)) ≤ ((norm‘if(𝐴 ∈ ℋ, 𝐴, 0)) · (norm𝐵)) ↔ (abs‘(if(𝐴 ∈ ℋ, 𝐴, 0) ·ih if(𝐵 ∈ ℋ, 𝐵, 0))) ≤ ((norm‘if(𝐴 ∈ ℋ, 𝐴, 0)) · (norm‘if(𝐵 ∈ ℋ, 𝐵, 0)))))
10 ifhvhv0 28793 . . 3 if(𝐴 ∈ ℋ, 𝐴, 0) ∈ ℋ
11 ifhvhv0 28793 . . 3 if(𝐵 ∈ ℋ, 𝐵, 0) ∈ ℋ
1210, 11bcsiHIL 28951 . 2 (abs‘(if(𝐴 ∈ ℋ, 𝐴, 0) ·ih if(𝐵 ∈ ℋ, 𝐵, 0))) ≤ ((norm‘if(𝐴 ∈ ℋ, 𝐴, 0)) · (norm‘if(𝐵 ∈ ℋ, 𝐵, 0)))
134, 9, 12dedth2h 4524 1 ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (abs‘(𝐴 ·ih 𝐵)) ≤ ((norm𝐴) · (norm𝐵)))