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

Theorem bcs 27422
 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 oveq1 6556 . . . 4 (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0) → (𝐴 ·ih 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0) ·ih 𝐵))
21fveq2d 6107 . . 3 (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0) → (abs‘(𝐴 ·ih 𝐵)) = (abs‘(if(𝐴 ∈ ℋ, 𝐴, 0) ·ih 𝐵)))
3 fveq2 6103 . . . 4 (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0) → (norm𝐴) = (norm‘if(𝐴 ∈ ℋ, 𝐴, 0)))
43oveq1d 6564 . . 3 (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0) → ((norm𝐴) · (norm𝐵)) = ((norm‘if(𝐴 ∈ ℋ, 𝐴, 0)) · (norm𝐵)))
52, 4breq12d 4596 . 2 (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0) → ((abs‘(𝐴 ·ih 𝐵)) ≤ ((norm𝐴) · (norm𝐵)) ↔ (abs‘(if(𝐴 ∈ ℋ, 𝐴, 0) ·ih 𝐵)) ≤ ((norm‘if(𝐴 ∈ ℋ, 𝐴, 0)) · (norm𝐵))))
6 oveq2 6557 . . . 4 (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0) → (if(𝐴 ∈ ℋ, 𝐴, 0) ·ih 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0) ·ih if(𝐵 ∈ ℋ, 𝐵, 0)))
76fveq2d 6107 . . 3 (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0) → (abs‘(if(𝐴 ∈ ℋ, 𝐴, 0) ·ih 𝐵)) = (abs‘(if(𝐴 ∈ ℋ, 𝐴, 0) ·ih if(𝐵 ∈ ℋ, 𝐵, 0))))
8 fveq2 6103 . . . 4 (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0) → (norm𝐵) = (norm‘if(𝐵 ∈ ℋ, 𝐵, 0)))
98oveq2d 6565 . . 3 (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0) → ((norm‘if(𝐴 ∈ ℋ, 𝐴, 0)) · (norm𝐵)) = ((norm‘if(𝐴 ∈ ℋ, 𝐴, 0)) · (norm‘if(𝐵 ∈ ℋ, 𝐵, 0))))
107, 9breq12d 4596 . 2 (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0) → ((abs‘(if(𝐴 ∈ ℋ, 𝐴, 0) ·ih 𝐵)) ≤ ((norm‘if(𝐴 ∈ ℋ, 𝐴, 0)) · (norm𝐵)) ↔ (abs‘(if(𝐴 ∈ ℋ, 𝐴, 0) ·ih if(𝐵 ∈ ℋ, 𝐵, 0))) ≤ ((norm‘if(𝐴 ∈ ℋ, 𝐴, 0)) · (norm‘if(𝐵 ∈ ℋ, 𝐵, 0)))))
11 ifhvhv0 27263 . . 3 if(𝐴 ∈ ℋ, 𝐴, 0) ∈ ℋ
12 ifhvhv0 27263 . . 3 if(𝐵 ∈ ℋ, 𝐵, 0) ∈ ℋ
1311, 12bcsiHIL 27421 . 2 (abs‘(if(𝐴 ∈ ℋ, 𝐴, 0) ·ih if(𝐵 ∈ ℋ, 𝐵, 0))) ≤ ((norm‘if(𝐴 ∈ ℋ, 𝐴, 0)) · (norm‘if(𝐵 ∈ ℋ, 𝐵, 0)))
145, 10, 13dedth2h 4090 1 ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (abs‘(𝐴 ·ih 𝐵)) ≤ ((norm𝐴) · (norm𝐵)))