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

Proof

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