Theorem bcs 5101

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
bcs	|- (abs` (A .i B)) <_ ((norm` A) x. (norm` B))

Proof of Theorem bcs

Step	Hyp	Ref	Expression
1		fveq2 2832	. . 3 |- ((A .i B) = 0 -> (abs` (A .i B)) = (abs` 0))
2		cleqid 1102	. . . . 5 |- 0 = 0
3		0cn 4100	. . . . . 6 |- 0 e. CC
4	3	abs00 4839	. . . . 5 |- ((abs` 0) = 0 <-> 0 = 0)
5	2, 4	mpbir 165	. . . 4 |- (abs` 0) = 0
6		bcs.1	. . . . . 6 |- A e. H~
7		normge0t 5077	. . . . . 6 |- (A e. H~ -> 0 <_ (norm` A))
8	6, 7	ax-mp 6	. . . . 5 |- 0 <_ (norm` A)
9		bcs.2	. . . . . 6 |- B e. H~
10		normge0t 5077	. . . . . 6 |- (B e. H~ -> 0 <_ (norm` B))
11	9, 10	ax-mp 6	. . . . 5 |- 0 <_ (norm` B)
12	6	normcl 5081	. . . . . 6 |- (norm` A) e. RR
13	9	normcl 5081	. . . . . 6 |- (norm` B) e. RR
14	12, 13	mulge0 4335	. . . . 5 |- ((0 <_ (norm` A) /\ 0 <_ (norm` B)) -> 0 <_ ((norm` A) x. (norm` B)))
15	8, 11, 14	mp2an 520	. . . 4 |- 0 <_ ((norm` A) x. (norm` B))
16	5, 15	eqbrtr 2076	. . 3 |- (abs` 0) <_ ((norm` A) x. (norm` B))
17	1, 16	syl6eqbr 2092	. 2 |- ((A .i B) = 0 -> (abs` (A .i B)) <_ ((norm` A) x. (norm` B)))
18		df-ne 1192	. . . 4 |- ((A .i B) =/= 0 <-> -. (A .i B) = 0)
19	6, 9	hicl 5044	. . . . . . 7 |- (A .i B) e. CC
20	19	abslem2 4867	. . . . . 6 |- ((A .i B) =/= 0 -> (((*` ((A .i B) / (abs` (A .i B)))) x. (A .i B)) + (((A .i B) / (abs` (A .i B))) x. (*` (A .i B)))) = (2 x. (abs` (A .i B))))
21		ax-his1 5045	. . . . . . . . 9 |- ((B e. H~ /\ A e. H~) -> (B .i A) = (*` (A .i B)))
22	9, 6, 21	mp2an 520	. . . . . . . 8 |- (B .i A) = (*` (A .i B))
23	22	opreq2i 3010	. . . . . . 7 |- (((A .i B) / (abs` (A .i B))) x. (B .i A)) = (((A .i B) / (abs` (A .i B))) x. (*` (A .i B)))
24	23	opreq2i 3010	. . . . . 6 |- (((*` ((A .i B) / (abs` (A .i B)))) x. (A .i B)) + (((A .i B) / (abs` (A .i B))) x. (B .i A))) = (((*` ((A .i B) / (abs` (A .i B)))) x. (A .i B)) + (((A .i B) / (abs` (A .i B))) x. (*` (A .i B))))
25	20, 24	syl5req 1137	. . . . 5 |- ((A .i B) =/= 0 -> (2 x. (abs` (A .i B))) = (((*` ((A .i B) / (abs` (A .i B)))) x. (A .i B)) + (((A .i B) / (abs` (A .i B))) x. (B .i A))))
26	19	abs00 4839	. . . . . . . . 9 |- ((abs` (A .i B)) = 0 <-> (A .i B) = 0)
27	26	negbii 162	. . . . . . . 8 |- (-. (abs` (A .i B)) = 0 <-> -. (A .i B) = 0)
28		df-ne 1192	. . . . . . . 8 |- ((abs` (A .i B)) =/= 0 <-> -. (abs` (A .i B)) = 0)
29	27, 28, 18	3bitr4 158	. . . . . . 7 |- ((abs` (A .i B)) =/= 0 <-> (A .i B) =/= 0)
30	19	abscl 4840	. . . . . . . . . 10 |- (abs` (A .i B)) e. RR
31	30	recn 4098	. . . . . . . . 9 |- (abs` (A .i B)) e. CC
32	19, 31	divclz 4222	. . . . . . . 8 |- ((abs` (A .i B)) =/= 0 -> ((A .i B) / (abs` (A .i B))) e. CC)
33	19, 31	divrecz 4237	. . . . . . . . . 10 |- ((abs` (A .i B)) =/= 0 -> ((A .i B) / (abs` (A .i B))) = ((A .i B) x. (1 / (abs` (A .i B)))))
34	33	fveq2d 2836	. . . . . . . . 9 |- ((abs` (A .i B)) =/= 0 -> (abs` ((A .i B) / (abs` (A .i B)))) = (abs` ((A .i B) x. (1 / (abs` (A .i B))))))
35		1cn 4101	. . . . . . . . . . . . 13 |- 1 e. CC
36	35, 31	divclz 4222	. . . . . . . . . . . 12 |- ((abs` (A .i B)) =/= 0 -> (1 / (abs` (A .i B))) e. CC)
37	36, 19	jctil 240	. . . . . . . . . . 11 |- ((abs` (A .i B)) =/= 0 -> ((A .i B) e. CC /\ (1 / (abs` (A .i B))) e. CC))
38		absmult 4849	. . . . . . . . . . 11 |- (((A .i B) e. CC /\ (1 / (abs` (A .i B))) e. CC) -> (abs` ((A .i B) x. (1 / (abs` (A .i B))))) = ((abs` (A .i B)) x. (abs` (1 / (abs` (A .i B))))))
39	37, 38	syl 12	. . . . . . . . . 10 |- ((abs` (A .i B)) =/= 0 -> (abs` ((A .i B) x. (1 / (abs` (A .i B))))) = ((abs` (A .i B)) x. (abs` (1 / (abs` (A .i B))))))
40		absidt 4862	. . . . . . . . . . . 12 |- ((1 / (abs` (A .i B))) e. RR -> (0 <_ (1 / (abs` (A .i B))) -> (abs` (1 / (abs` (A .i B)))) = (1 / (abs` (A .i B)))))
41		ax1re 4064	. . . . . . . . . . . . 13 |- 1 e. RR
42	41, 30	redivclz 4275	. . . . . . . . . . . 12 |- ((abs` (A .i B)) =/= 0 -> (1 / (abs` (A .i B))) e. RR)
43		ltlet 4286	. . . . . . . . . . . . 13 |- ((0 e. RR /\ (1 / (abs` (A .i B))) e. RR) -> (0 < (1 / (abs` (A .i B))) -> 0 <_ (1 / (abs` (A .i B)))))
44		ax0re 4063	. . . . . . . . . . . . . 14 |- 0 e. RR
45	42, 44	jctil 240	. . . . . . . . . . . . 13 |- ((abs` (A .i B)) =/= 0 -> (0 e. RR /\ (1 / (abs` (A .i B))) e. RR))
46	19	absgt0 4842	. . . . . . . . . . . . . . 15 |- (-. (A .i B) = 0 <-> 0 < (abs` (A .i B)))
47	28, 27, 46	3bitr 155	. . . . . . . . . . . . . 14 |- ((abs` (A .i B)) =/= 0 <-> 0 < (abs` (A .i B)))
48	30	recgt0 4386	. . . . . . . . . . . . . 14 |- (0 < (abs` (A .i B)) -> 0 < (1 / (abs` (A .i B))))
49	47, 48	sylbi 174	. . . . . . . . . . . . 13 |- ((abs` (A .i B)) =/= 0 -> 0 < (1 / (abs` (A .i B))))
50	43, 45, 49	sylc 62	. . . . . . . . . . . 12 |- ((abs` (A .i B)) =/= 0 -> 0 <_ (1 / (abs` (A .i B))))
51	40, 42, 50	sylc 62	. . . . . . . . . . 11 |- ((abs` (A .i B)) =/= 0 -> (abs` (1 / (abs` (A .i B)))) = (1 / (abs` (A .i B))))
52	51	opreq2d 3013	. . . . . . . . . 10 |- ((abs` (A .i B)) =/= 0 -> ((abs` (A .i B)) x. (abs` (1 / (abs` (A .i B))))) = ((abs` (A .i B)) x. (1 / (abs` (A .i B)))))
53	39, 52	eqtrd 1128	. . . . . . . . 9 |- ((abs` (A .i B)) =/= 0 -> (abs` ((A .i B) x. (1 / (abs` (A .i B))))) = ((abs` (A .i B)) x. (1 / (abs` (A .i B)))))
54	31	recidz 4234	. . . . . . . . 9 |- ((abs` (A .i B)) =/= 0 -> ((abs` (A .i B)) x. (1 / (abs` (A .i B)))) = 1)
55	34, 53, 54	3eqtrd 1132	. . . . . . . 8 |- ((abs` (A .i B)) =/= 0 -> (abs` ((A .i B) / (abs` (A .i B)))) = 1)
56	32, 55	jca 236	. . . . . . 7 |- ((abs` (A .i B)) =/= 0 -> (((A .i B) / (abs` (A .i B))) e. CC /\ (abs` ((A .i B) / (abs` (A .i B)))) = 1))
57	29, 56	sylbir 176	. . . . . 6 |- ((A .i B) =/= 0 -> (((A .i B) / (abs` (A .i B))) e. CC /\ (abs` ((A .i B) / (abs` (A .i B)))) = 1))
58	6, 9	normlem7t 5072	. . . . . 6 |- ((((A .i B) / (abs` (A .i B))) e. CC /\ (abs` ((A .i B) / (abs` (A .i B)))) = 1) -> (((*` ((A .i B) / (abs` (A .i B)))) x. (A .i B)) + (((A .i B) / (abs` (A .i B))) x. (B .i A))) <_ (2 x. ((sqr` (B .i B)) x. (sqr` (A .i A)))))
59	57, 58	syl 12	. . . . 5 |- ((A .i B) =/= 0 -> (((*` ((A .i B) / (abs` (A .i B)))) x. (A .i B)) + (((A .i B) / (abs` (A .i B))) x.