Theorem bcsALT 9046

Description: Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98.

Hypotheses

Ref	Expression
bcs.1	|- A e. H~
bcs.2	|- B e. H~

Assertion

Ref	Expression
bcsALT	|- (abs` (A .ih B)) <_ ((normh` A) x. (normh` B))

Proof of Theorem bcsALT

Step	Hyp	Ref	Expression
1		fveq2 3724	. . 3 |- ((A .ih B) = 0 -> (abs` (A .ih B)) = (abs` 0))
2		abs0 6877	. . . 4 |- (abs` 0) = 0
3		bcs.1	. . . . . 6 |- A e. H~
4		normge0t 8992	. . . . . 6 |- (A e. H~ -> 0 <_ (normh` A))
5	3, 4	ax-mp 7	. . . . 5 |- 0 <_ (normh` A)
6		bcs.2	. . . . . 6 |- B e. H~
7		normge0t 8992	. . . . . 6 |- (B e. H~ -> 0 <_ (normh` B))
8	6, 7	ax-mp 7	. . . . 5 |- 0 <_ (normh` B)
9	3	normcl 8998	. . . . . 6 |- (normh` A) e. RR
10	6	normcl 8998	. . . . . 6 |- (normh` B) e. RR
11	9, 10	mulge0 5607	. . . . 5 |- ((0 <_ (normh` A) /\ 0 <_ (normh` B)) -> 0 <_ ((normh` A) x. (normh` B)))
12	5, 8, 11	mp2an 697	. . . 4 |- 0 <_ ((normh` A) x. (normh` B))
13	2, 12	eqbrtr 2634	. . 3 |- (abs` 0) <_ ((normh` A) x. (normh` B))
14	1, 13	syl6eqbr 2652	. 2 |- ((A .ih B) = 0 -> (abs` (A .ih B)) <_ ((normh` A) x. (normh` B)))
15		df-ne 1587	. . . 4 |- ((A .ih B) =/= 0 <-> -. (A .ih B) = 0)
16	3, 6	hicl 8948	. . . . . . 7 |- (A .ih B) e. CC
17	16	abslem2 6909	. . . . . 6 |- ((A .ih B) =/= 0 -> (((*` ((A .ih B) / (abs` (A .ih B)))) x. (A .ih B)) + (((A .ih B) / (abs` (A .ih B))) x. (*` (A .ih B)))) = (2 x. (abs` (A .ih B))))
18	6, 3	his1 8966	. . . . . . . 8 |- (B .ih A) = (*` (A .ih B))
19	18	opreq2i 3972	. . . . . . 7 |- (((A .ih B) / (abs` (A .ih B))) x. (B .ih A)) = (((A .ih B) / (abs` (A .ih B))) x. (*` (A .ih B)))
20	19	opreq2i 3972	. . . . . 6 |- (((*` ((A .ih B) / (abs` (A .ih B)))) x. (A .ih B)) + (((A .ih B) / (abs` (A .ih B))) x. (B .ih A))) = (((*` ((A .ih B) / (abs` (A .ih B)))) x. (A .ih B)) + (((A .ih B) / (abs` (A .ih B))) x. (*` (A .ih B))))
21	17, 20	syl5req 1520	. . . . 5 |- ((A .ih B) =/= 0 -> (2 x. (abs` (A .ih B))) = (((*` ((A .ih B) / (abs` (A .ih B)))) x. (A .ih B)) + (((A .ih B) / (abs` (A .ih B))) x. (B .ih A))))
22	16	abs00 6842	. . . . . . . 8 |- ((abs` (A .ih B)) = 0 <-> (A .ih B) = 0)
23	22	necon3bii 1598	. . . . . . 7 |- ((abs` (A .ih B)) =/= 0 <-> (A .ih B) =/= 0)
24	16	abscl 6839	. . . . . . . . . 10 |- (abs` (A .ih B)) e. RR
25	24	recn 5314	. . . . . . . . 9 |- (abs` (A .ih B)) e. CC
26	16, 25	divclz 5711	. . . . . . . 8 |- ((abs` (A .ih B)) =/= 0 -> ((A .ih B) / (abs` (A .ih B))) e. CC)
27	16, 25	divrecz 5738	. . . . . . . . . 10 |- ((abs` (A .ih B)) =/= 0 -> ((A .ih B) / (abs` (A .ih B))) = ((A .ih B) x. (1 / (abs` (A .ih B)))))
28	27	fveq2d 3728	. . . . . . . . 9 |- ((abs` (A .ih B)) =/= 0 -> (abs` ((A .ih B) / (abs` (A .ih B)))) = (abs` ((A .ih B) x. (1 / (abs` (A .ih B))))))
29	25	recclz 5714	. . . . . . . . . . . 12 |- ((abs` (A .ih B)) =/= 0 -> (1 / (abs` (A .ih B))) e. CC)
30	29, 16	jctil 292	. . . . . . . . . . 11 |- ((abs` (A .ih B)) =/= 0 -> ((A .ih B) e. CC /\ (1 / (abs` (A .ih B))) e. CC))
31		absmult 6858	. . . . . . . . . . 11 |- (((A .ih B) e. CC /\ (1 / (abs` (A .ih B))) e. CC) -> (abs` ((A .ih B) x. (1 / (abs` (A .ih B))))) = ((abs` (A .ih B)) x. (abs` (1 / (abs` (A .ih B))))))
32	30, 31	syl 10	. . . . . . . . . 10 |- ((abs` (A .ih B)) =/= 0 -> (abs` ((A .ih B) x. (1 / (abs` (A .ih B))))) = ((abs` (A .ih B)) x. (abs` (1 / (abs` (A .ih B))))))
33		absidt 6862	. . . . . . . . . . . 12 |- (((1 / (abs` (A .ih B))) e. RR /\ 0 <_ (1 / (abs` (A .ih B)))) -> (abs` (1 / (abs` (A .ih B)))) = (1 / (abs` (A .ih B))))
34	24	rerecclz 5802	. . . . . . . . . . . 12 |- ((abs` (A .ih B)) =/= 0 -> (1 / (abs` (A .ih B))) e. RR)
35		ltlet 5520	. . . . . . . . . . . . 13 |- ((0 e. RR /\ (1 / (abs` (A .ih B))) e. RR) -> (0 < (1 / (abs` (A .ih B))) -> 0 <_ (1 / (abs` (A .ih B)))))
36		0re 5440	. . . . . . . . . . . . . 14 |- 0 e. RR
37	34, 36	jctil 292	. . . . . . . . . . . . 13 |- ((abs` (A .ih B)) =/= 0 -> (0 e. RR /\ (1 / (abs` (A .ih B))) e. RR))
38	16	absgt0 6843	. . . . . . . . . . . . . . 15 |- ((A .ih B) =/= 0 <-> 0 < (abs` (A .ih B)))
39	23, 38	bitr 173	. . . . . . . . . . . . . 14 |- ((abs` (A .ih B)) =/= 0 <-> 0 < (abs` (A .ih B)))
40	24	recgt0 5862	. . . . . . . . . . . . . 14 |- (0 < (abs` (A .ih B)) -> 0 < (1 / (abs` (A .ih B))))
41	39, 40	sylbi 199	. . . . . . . . . . . . 13 |- ((abs` (A .ih B)) =/= 0 -> 0 < (1 / (abs` (A .ih B))))
42	35, 37, 41	sylc 68	. . . . . . . . . . . 12 |- ((abs` (A .ih B)) =/= 0 -> 0 <_ (1 / (abs` (A .ih B))))
43	33, 34, 42	sylanc 471	. . . . . . . . . . 11 |- ((abs` (A .ih B)) =/= 0 -> (abs` (1 / (abs` (A .ih B)))) = (1 / (abs` (A .ih B))))
44	43	opreq2d 3976	. . . . . . . . . 10 |- ((abs` (A .ih B)) =/= 0 -> ((abs` (A .ih B)) x. (abs` (1 / (abs` (A .ih B))))) = ((abs` (A .ih B)) x. (1 / (abs` (A .ih B)))))
45	32, 44	eqtrd 1507	. . . . . . . . 9 |- ((abs` (A .ih B)) =/= 0 -> (abs` ((A .ih B) x. (1 / (abs` (A .ih B))))) = ((abs` (A .ih B)) x. (1 / (abs` (A .ih B)))))
46	25	recidz 5734	. . . . . . . . 9 |- ((abs` (A .ih B)) =/= 0 -> ((abs` (A .ih B)) x. (1 / (abs` (A .ih B)))) = 1)
47	28, 45, 46	3eqtrd 1511	. . . . . . . 8 |- ((abs` (A .ih B)) =/= 0 -> (abs` ((A .ih B) / (abs` (A .ih B)))) = 1)
48	26, 47	jca 288	. . . . . . 7 |- ((abs` (A .ih B)) =/= 0 -> (((A .ih B) / (abs` (A .ih B))) e. CC /\ (abs` ((A .ih B) / (abs` (A .ih B)))) = 1))
49	23, 48	sylbir 201	. . . . . 6 |- ((A .ih B) =/= 0 -> (((A .ih B) / (abs` (A .ih B))) e. CC /\ (abs` ((A .ih B) / (abs` (A .ih B)))) = 1))
50	3, 6	normlem7tALT 8985	. . . . . 6 |- ((((A .ih B) / (abs` (A .ih B))) e. CC /\ (abs` ((A .ih B) / (abs` (A .ih B)))) = 1) -> (((*` ((A .ih B) / (abs` (A .ih B)))) x. (A .ih B)) + (((A .ih B) / (abs` (A .ih B))) x. (B .ih A))) <_ (2 x. ((sqr` (B .ih B)) x. (sqr` (A .ih A)))))
51	49, 50	syl 10	. . . . 5 |- ((A .ih B) =/= 0 -> (((*` ((A .ih B) / (abs` (A .ih B)))) x. (A .ih B)) + (((A .ih B) / (abs` (A .ih B))) x. (B .ih A))) <_ (2 x. ((sqr` (B .ih B)) x. (sqr` (A .ih A)))))
52	21, 51	eqbrtrd 2635	. . . 4 |- ((A .ih B) =/= 0 -> (2 x. (abs` (A .ih B))) <_ (2 x. ((sqr` (B .ih B)