Theorem bcsiALT

Description: Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of Beran p. 98. (Contributed by NM, 11-Oct-1999) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bcs.1	$$⊢A\in \mathscr{H}$$
	bcs.2	$$⊢B\in \mathscr{H}$$
Assertion	bcsiALT	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\le {norm}_{ℎ}\left(A\right){norm}_{ℎ}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		bcs.1	$$⊢A\in \mathscr{H}$$
2		bcs.2	$$⊢B\in \mathscr{H}$$
3		fveq2	$$⊢A{\cdot }_{\mathrm{ih}}B=0\to \left|A{\cdot }_{\mathrm{ih}}B\right|=\left|0\right|$$
4		abs0	$$⊢\left|0\right|=0$$
5		normge0	$$⊢A\in \mathscr{H}\to 0\le {norm}_{ℎ}\left(A\right)$$
6	1 5	ax-mp	$$⊢0\le {norm}_{ℎ}\left(A\right)$$
7		normge0	$$⊢B\in \mathscr{H}\to 0\le {norm}_{ℎ}\left(B\right)$$
8	2 7	ax-mp	$$⊢0\le {norm}_{ℎ}\left(B\right)$$
9	1	normcli	$$⊢{norm}_{ℎ}\left(A\right)\in ℝ$$
10	2	normcli	$$⊢{norm}_{ℎ}\left(B\right)\in ℝ$$
11	9 10	mulge0i	$$⊢\left(0\le {norm}_{ℎ}\left(A\right)\wedge 0\le {norm}_{ℎ}\left(B\right)\right)\to 0\le {norm}_{ℎ}\left(A\right){norm}_{ℎ}\left(B\right)$$
12	6 8 11	mp2an	$$⊢0\le {norm}_{ℎ}\left(A\right){norm}_{ℎ}\left(B\right)$$
13	4 12	eqbrtri	$$⊢\left|0\right|\le {norm}_{ℎ}\left(A\right){norm}_{ℎ}\left(B\right)$$
14	3 13	eqbrtrdi	$$⊢A{\cdot }_{\mathrm{ih}}B=0\to \left|A{\cdot }_{\mathrm{ih}}B\right|\le {norm}_{ℎ}\left(A\right){norm}_{ℎ}\left(B\right)$$
15		df-ne	$$⊢A{\cdot }_{\mathrm{ih}}B\ne 0\leftrightarrow \neg A{\cdot }_{\mathrm{ih}}B=0$$
16	2 1	his1i	$$⊢B{\cdot }_{\mathrm{ih}}A=\overline{A{\cdot }_{\mathrm{ih}}B}$$
17	16	oveq2i	$$⊢\left(\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)\left(B{\cdot }_{\mathrm{ih}}A\right)=\left(\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)\overline{A{\cdot }_{\mathrm{ih}}B}$$
18	17	oveq2i	$$⊢\stackrel{‾}{\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}}\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)\left(B{\cdot }_{\mathrm{ih}}A\right)=\stackrel{‾}{\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}}\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)\overline{A{\cdot }_{\mathrm{ih}}B}$$
19	1 2	hicli	$$⊢A{\cdot }_{\mathrm{ih}}B\in ℂ$$
20		abslem2	$$⊢\left(A{\cdot }_{\mathrm{ih}}B\in ℂ\wedge A{\cdot }_{\mathrm{ih}}B\ne 0\right)\to \stackrel{‾}{\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}}\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)\overline{A{\cdot }_{\mathrm{ih}}B}=2\left|A{\cdot }_{\mathrm{ih}}B\right|$$
21	19 20	mpan	$$⊢A{\cdot }_{\mathrm{ih}}B\ne 0\to \stackrel{‾}{\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}}\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)\overline{A{\cdot }_{\mathrm{ih}}B}=2\left|A{\cdot }_{\mathrm{ih}}B\right|$$
22	18 21	syl5req	$$⊢A{\cdot }_{\mathrm{ih}}B\ne 0\to 2\left|A{\cdot }_{\mathrm{ih}}B\right|=\stackrel{‾}{\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}}\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)\left(B{\cdot }_{\mathrm{ih}}A\right)$$
23	19	abs00i	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|=0\leftrightarrow A{\cdot }_{\mathrm{ih}}B=0$$
24	23	necon3bii	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\ne 0\leftrightarrow A{\cdot }_{\mathrm{ih}}B\ne 0$$
25	19	abscli	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\in ℝ$$
26	25	recni	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\in ℂ$$
27	19 26	divclzi	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\ne 0\to \frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\in ℂ$$
28	19 26	divreczi	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\ne 0\to \frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}=\left(A{\cdot }_{\mathrm{ih}}B\right)\left(\frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)$$
29	28	fveq2d	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\ne 0\to \left|\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right|=\left|\left(A{\cdot }_{\mathrm{ih}}B\right)\left(\frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)\right|$$
30	26	recclzi	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\ne 0\to \frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\in ℂ$$
31		absmul	$$⊢\left(A{\cdot }_{\mathrm{ih}}B\in ℂ\wedge \frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\in ℂ\right)\to \left|\left(A{\cdot }_{\mathrm{ih}}B\right)\left(\frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)\right|=\left|A{\cdot }_{\mathrm{ih}}B\right|\left|\frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right|$$
32	19 30 31	sylancr	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\ne 0\to \left|\left(A{\cdot }_{\mathrm{ih}}B\right)\left(\frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)\right|=\left|A{\cdot }_{\mathrm{ih}}B\right|\left|\frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right|$$
33	25	rerecclzi	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\ne 0\to \frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\in ℝ$$
34		0re	$$⊢0\in ℝ$$
35	33 34	jctil	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\ne 0\to \left(0\in ℝ\wedge \frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\in ℝ\right)$$
36	19	absgt0i	$$⊢A{\cdot }_{\mathrm{ih}}B\ne 0\leftrightarrow 0<\left|A{\cdot }_{\mathrm{ih}}B\right|$$
37	24 36	bitri	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\ne 0\leftrightarrow 0<\left|A{\cdot }_{\mathrm{ih}}B\right|$$
38	25	recgt0i	$$⊢0<\left|A{\cdot }_{\mathrm{ih}}B\right|\to 0<\frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}$$
39	37 38	sylbi	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\ne 0\to 0<\frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}$$
40		ltle	$$⊢\left(0\in ℝ\wedge \frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\in ℝ\right)\to \left(0<\frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\to 0\le \frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)$$
41	35 39 40	sylc	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\ne 0\to 0\le \frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}$$
42	33 41	absidd	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\ne 0\to \left|\frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right|=\frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}$$
43	42	oveq2d	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\ne 0\to \left|A{\cdot }_{\mathrm{ih}}B\right|\left|\frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right|=\left|A{\cdot }_{\mathrm{ih}}B\right|\left(\frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)$$
44	32 43	eqtrd	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\ne 0\to \left|\left(A{\cdot }_{\mathrm{ih}}B\right)\left(\frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)\right|=\left|A{\cdot }_{\mathrm{ih}}B\right|\left(\frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)$$
45	26	recidzi	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\ne 0\to \left|A{\cdot }_{\mathrm{ih}}B\right|\left(\frac{1}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)=1$$
46	29 44 45	3eqtrd	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\ne 0\to \left|\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right|=1$$
47	27 46	jca	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\ne 0\to \left(\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\in ℂ\wedge \left|\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right|=1\right)$$
48	24 47	sylbir	$$⊢A{\cdot }_{\mathrm{ih}}B\ne 0\to \left(\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\in ℂ\wedge \left|\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right|=1\right)$$
49	1 2	normlem7tALT	$$⊢\left(\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\in ℂ\wedge \left|\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right|=1\right)\to \stackrel{‾}{\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}}\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)\left(B{\cdot }_{\mathrm{ih}}A\right)\le 2\sqrt{B{\cdot }_{\mathrm{ih}}B}\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
50	48 49	syl	$$⊢A{\cdot }_{\mathrm{ih}}B\ne 0\to \stackrel{‾}{\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}}\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(\frac{A{\cdot }_{\mathrm{ih}}B}{\left|A{\cdot }_{\mathrm{ih}}B\right|}\right)\left(B{\cdot }_{\mathrm{ih}}A\right)\le 2\sqrt{B{\cdot }_{\mathrm{ih}}B}\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
51	22 50	eqbrtrd	$$⊢A{\cdot }_{\mathrm{ih}}B\ne 0\to 2\left|A{\cdot }_{\mathrm{ih}}B\right|\le 2\sqrt{B{\cdot }_{\mathrm{ih}}B}\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
52	15 51	sylbir	$$⊢\neg A{\cdot }_{\mathrm{ih}}B=0\to 2\left|A{\cdot }_{\mathrm{ih}}B\right|\le 2\sqrt{B{\cdot }_{\mathrm{ih}}B}\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
53	10	recni	$$⊢{norm}_{ℎ}\left(B\right)\in ℂ$$
54	9	recni	$$⊢{norm}_{ℎ}\left(A\right)\in ℂ$$
55		normval	$$⊢B\in \mathscr{H}\to {norm}_{ℎ}\left(B\right)=\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
56	2 55	ax-mp	$$⊢{norm}_{ℎ}\left(B\right)=\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
57		normval	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(A\right)=\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
58	1 57	ax-mp	$$⊢{norm}_{ℎ}\left(A\right)=\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
59	56 58	oveq12i	$$⊢{norm}_{ℎ}\left(B\right){norm}_{ℎ}\left(A\right)=\sqrt{B{\cdot }_{\mathrm{ih}}B}\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
60	53 54 59	mulcomli	$$⊢{norm}_{ℎ}\left(A\right){norm}_{ℎ}\left(B\right)=\sqrt{B{\cdot }_{\mathrm{ih}}B}\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
61	60	breq2i	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\le {norm}_{ℎ}\left(A\right){norm}_{ℎ}\left(B\right)\leftrightarrow \left|A{\cdot }_{\mathrm{ih}}B\right|\le \sqrt{B{\cdot }_{\mathrm{ih}}B}\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
62		2pos	$$⊢0<2$$
63		hiidge0	$$⊢B\in \mathscr{H}\to 0\le B{\cdot }_{\mathrm{ih}}B$$
64		hiidrcl	$$⊢B\in \mathscr{H}\to B{\cdot }_{\mathrm{ih}}B\in ℝ$$
65	2 64	ax-mp	$$⊢B{\cdot }_{\mathrm{ih}}B\in ℝ$$
66	65	sqrtcli	$$⊢0\le B{\cdot }_{\mathrm{ih}}B\to \sqrt{B{\cdot }_{\mathrm{ih}}B}\in ℝ$$
67	2 63 66	mp2b	$$⊢\sqrt{B{\cdot }_{\mathrm{ih}}B}\in ℝ$$
68		hiidge0	$$⊢A\in \mathscr{H}\to 0\le A{\cdot }_{\mathrm{ih}}A$$
69		hiidrcl	$$⊢A\in \mathscr{H}\to A{\cdot }_{\mathrm{ih}}A\in ℝ$$
70	1 69	ax-mp	$$⊢A{\cdot }_{\mathrm{ih}}A\in ℝ$$
71	70	sqrtcli	$$⊢0\le A{\cdot }_{\mathrm{ih}}A\to \sqrt{A{\cdot }_{\mathrm{ih}}A}\in ℝ$$
72	1 68 71	mp2b	$$⊢\sqrt{A{\cdot }_{\mathrm{ih}}A}\in ℝ$$
73	67 72	remulcli	$$⊢\sqrt{B{\cdot }_{\mathrm{ih}}B}\sqrt{A{\cdot }_{\mathrm{ih}}A}\in ℝ$$
74		2re	$$⊢2\in ℝ$$
75	25 73 74	lemul2i	$$⊢0<2\to \left(\left|A{\cdot }_{\mathrm{ih}}B\right|\le \sqrt{B{\cdot }_{\mathrm{ih}}B}\sqrt{A{\cdot }_{\mathrm{ih}}A}\leftrightarrow 2\left|A{\cdot }_{\mathrm{ih}}B\right|\le 2\sqrt{B{\cdot }_{\mathrm{ih}}B}\sqrt{A{\cdot }_{\mathrm{ih}}A}\right)$$
76	62 75	ax-mp	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\le \sqrt{B{\cdot }_{\mathrm{ih}}B}\sqrt{A{\cdot }_{\mathrm{ih}}A}\leftrightarrow 2\left|A{\cdot }_{\mathrm{ih}}B\right|\le 2\sqrt{B{\cdot }_{\mathrm{ih}}B}\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
77	61 76	bitri	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\le {norm}_{ℎ}\left(A\right){norm}_{ℎ}\left(B\right)\leftrightarrow 2\left|A{\cdot }_{\mathrm{ih}}B\right|\le 2\sqrt{B{\cdot }_{\mathrm{ih}}B}\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
78	52 77	sylibr	$$⊢\neg A{\cdot }_{\mathrm{ih}}B=0\to \left|A{\cdot }_{\mathrm{ih}}B\right|\le {norm}_{ℎ}\left(A\right){norm}_{ℎ}\left(B\right)$$
79	14 78	pm2.61i	$$⊢\left|A{\cdot }_{\mathrm{ih}}B\right|\le {norm}_{ℎ}\left(A\right){norm}_{ℎ}\left(B\right)$$