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	mullidd	⊢ ( 𝐵 ∈ ℋ → ( 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ℎ ‘ 𝐵 ) )