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⋅ihB≤normℎ⁡B

Proof

Step Hyp Ref Expression
1 hicl ⊢A∈ℋ∧B∈ℋ→A⋅ihB∈ℂ
2 1 abscld ⊢A∈ℋ∧B∈ℋ→A⋅ihB∈ℝ
3 2 3adant3 ⊢A∈ℋ∧B∈ℋ∧normℎ⁡A≤1→A⋅ihB∈ℝ
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⋅ihB≤normℎ⁡A⁢normℎ⁡B
11 10 3adant3 ⊢A∈ℋ∧B∈ℋ∧normℎ⁡A≤1→A⋅ihB≤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⋅ihB≤normℎ⁡B