# 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 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to \left|{A}{\cdot }_{\mathrm{ih}}{B}\right|\le {norm}_{ℎ}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 hicl ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{B}\in ℂ$
2 1 abscld ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left|{A}{\cdot }_{\mathrm{ih}}{B}\right|\in ℝ$
3 2 3adant3 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to \left|{A}{\cdot }_{\mathrm{ih}}{B}\right|\in ℝ$
4 normcl ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({A}\right)\in ℝ$
5 normcl ${⊢}{B}\in ℋ\to {norm}_{ℎ}\left({B}\right)\in ℝ$
6 remulcl ${⊢}\left({norm}_{ℎ}\left({A}\right)\in ℝ\wedge {norm}_{ℎ}\left({B}\right)\in ℝ\right)\to {norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({B}\right)\in ℝ$
7 4 5 6 syl2an ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({B}\right)\in ℝ$
8 7 3adant3 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to {norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({B}\right)\in ℝ$
9 5 3ad2ant2 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to {norm}_{ℎ}\left({B}\right)\in ℝ$
10 bcs ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left|{A}{\cdot }_{\mathrm{ih}}{B}\right|\le {norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({B}\right)$
11 10 3adant3 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to \left|{A}{\cdot }_{\mathrm{ih}}{B}\right|\le {norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({B}\right)$
12 4 3ad2ant1 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to {norm}_{ℎ}\left({A}\right)\in ℝ$
13 normge0 ${⊢}{B}\in ℋ\to 0\le {norm}_{ℎ}\left({B}\right)$
14 13 3ad2ant2 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to 0\le {norm}_{ℎ}\left({B}\right)$
15 9 14 jca ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to \left({norm}_{ℎ}\left({B}\right)\in ℝ\wedge 0\le {norm}_{ℎ}\left({B}\right)\right)$
16 simp3 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to {norm}_{ℎ}\left({A}\right)\le 1$
17 1re ${⊢}1\in ℝ$
18 lemul1a ${⊢}\left(\left({norm}_{ℎ}\left({A}\right)\in ℝ\wedge 1\in ℝ\wedge \left({norm}_{ℎ}\left({B}\right)\in ℝ\wedge 0\le {norm}_{ℎ}\left({B}\right)\right)\right)\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to {norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({B}\right)\le 1{norm}_{ℎ}\left({B}\right)$
19 17 18 mp3anl2 ${⊢}\left(\left({norm}_{ℎ}\left({A}\right)\in ℝ\wedge \left({norm}_{ℎ}\left({B}\right)\in ℝ\wedge 0\le {norm}_{ℎ}\left({B}\right)\right)\right)\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to {norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({B}\right)\le 1{norm}_{ℎ}\left({B}\right)$
20 12 15 16 19 syl21anc ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to {norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({B}\right)\le 1{norm}_{ℎ}\left({B}\right)$
21 5 recnd ${⊢}{B}\in ℋ\to {norm}_{ℎ}\left({B}\right)\in ℂ$
22 21 mulid2d ${⊢}{B}\in ℋ\to 1{norm}_{ℎ}\left({B}\right)={norm}_{ℎ}\left({B}\right)$
23 22 3ad2ant2 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to 1{norm}_{ℎ}\left({B}\right)={norm}_{ℎ}\left({B}\right)$
24 20 23 breqtrd ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to {norm}_{ℎ}\left({A}\right){norm}_{ℎ}\left({B}\right)\le {norm}_{ℎ}\left({B}\right)$
25 3 8 9 11 24 letrd ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to \left|{A}{\cdot }_{\mathrm{ih}}{B}\right|\le {norm}_{ℎ}\left({B}\right)$