Metamath Proof Explorer

Theorem bcs2

Description: Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL . (Contributed by NM, 24-May-2006) (New usage is discouraged.)

Ref Expression
Assertion bcs2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → A ⋅ ih B ≤ norm ℎ ⁡ B

Proof

Step Hyp Ref Expression
1 hicl ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B ∈ ℂ
2 1 abscld ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B ∈ ℝ
3 2 3adant3 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → A ⋅ ih B ∈ ℝ
4 normcl ⊢ A ∈ ℋ → norm ℎ ⁡ A ∈ ℝ
5 normcl ⊢ B ∈ ℋ → norm ℎ ⁡ B ∈ ℝ
6 remulcl ⊢ norm ℎ ⁡ A ∈ ℝ ∧ norm ℎ ⁡ B ∈ ℝ → norm ℎ ⁡ A ⁢ norm ℎ ⁡ B ∈ ℝ
7 4 5 6 syl2an ⊢ A ∈ ℋ ∧ B ∈ ℋ → norm ℎ ⁡ A ⁢ norm ℎ ⁡ B ∈ ℝ
8 7 3adant3 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → norm ℎ ⁡ A ⁢ norm ℎ ⁡ B ∈ ℝ
9 5 3ad2ant2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → norm ℎ ⁡ B ∈ ℝ
10 bcs ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B ≤ norm ℎ ⁡ A ⁢ norm ℎ ⁡ B
11 10 3adant3 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → A ⋅ ih B ≤ norm ℎ ⁡ A ⁢ norm ℎ ⁡ B
12 4 3ad2ant1 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → norm ℎ ⁡ A ∈ ℝ
13 normge0 ⊢ B ∈ ℋ → 0 ≤ norm ℎ ⁡ B
14 13 3ad2ant2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → 0 ≤ norm ℎ ⁡ B
15 9 14 jca ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → norm ℎ ⁡ B ∈ ℝ ∧ 0 ≤ norm ℎ ⁡ B
16 simp3 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → norm ℎ ⁡ A ≤ 1
17 1re ⊢ 1 ∈ ℝ
18 lemul1a ⊢ norm ℎ ⁡ A ∈ ℝ ∧ 1 ∈ ℝ ∧ norm ℎ ⁡ B ∈ ℝ ∧ 0 ≤ norm ℎ ⁡ B ∧ norm ℎ ⁡ A ≤ 1 → norm ℎ ⁡ A ⁢ norm ℎ ⁡ B ≤ 1 ⁢ norm ℎ ⁡ B
19 17 18 mp3anl2 ⊢ norm ℎ ⁡ A ∈ ℝ ∧ norm ℎ ⁡ B ∈ ℝ ∧ 0 ≤ norm ℎ ⁡ B ∧ norm ℎ ⁡ A ≤ 1 → norm ℎ ⁡ A ⁢ norm ℎ ⁡ B ≤ 1 ⁢ norm ℎ ⁡ B
20 12 15 16 19 syl21anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → norm ℎ ⁡ A ⁢ norm ℎ ⁡ B ≤ 1 ⁢ norm ℎ ⁡ B
21 5 recnd ⊢ B ∈ ℋ → norm ℎ ⁡ B ∈ ℂ
22 21 mulid2d ⊢ B ∈ ℋ → 1 ⁢ norm ℎ ⁡ B = norm ℎ ⁡ B
23 22 3ad2ant2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → 1 ⁢ norm ℎ ⁡ B = norm ℎ ⁡ B
24 20 23 breqtrd ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → norm ℎ ⁡ A ⁢ norm ℎ ⁡ B ≤ norm ℎ ⁡ B
25 3 8 9 11 24 letrd ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ norm ℎ ⁡ A ≤ 1 → A ⋅ ih B ≤ norm ℎ ⁡ B