Theorem bcsALT 8967

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 3709	. . 3 |- ((A .ih B) = 0 -> (abs` (A .ih B)) = (abs` 0))
2		abs0 6814	. . . 4 |- (abs` 0) = 0
3		bcs.1	. . . . . 6 |- A e. H~
4		normge0t 8913	. . . . . 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 8913	. . . . . 6 |- (B e. H~ -> 0 <_ (normh` B))
8	6, 7	ax-mp 7	. . . . 5 |- 0 <_ (normh` B)
9	3	normcl 8919	. . . . . 6 |- (normh` A) e. RR
10	6	normcl 8919	. . . . . 6 |- (normh` B) e. RR
11	9, 10	mulge0 5581	. . . . 5 |- ((0 <_ (normh` A) /\ 0 <_ (normh` B)) -> 0 <_ ((normh` A) x. (normh` B)))
12	5, 8, 11	mp2an 695	. . . 4 |- 0 <_ ((normh` A) x. (normh` B))
13	2, 12	eqbrtr 2624	. . 3 |- (abs` 0) <_ ((normh` A) x. (normh` B))
14	1, 13	syl6eqbr 2642	. 2 |- ((A .ih B) = 0 -> (abs` (A .ih B)) <_ ((normh` A) x. (normh` B)))
15		df-ne 1579	. . . 4 |- ((A .ih B) =/= 0 <-> -. (A .ih B) = 0)
16	3, 6	hicl 8869	. . . . . . 7 |- (A .ih B) e. CC
17	16	abslem2 6846	. . . . . 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 8887	. . . . . . . 8 |- (B .ih A) = (*` (A .ih B))
19	18	opreq2i 3957	. . . . . . 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 3957	. . . . . 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 1512	. . . . 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 6777	. . . . . . . 8 |- ((abs` (A .ih B)) = 0 <-> (A .ih B) = 0)
23	22	necon3bii 1590	. . . . . . 7 |- ((abs` (A .ih B)) =/= 0 <-> (A .ih B) =/= 0)
24	16	abscl 6774	. . . . . . . . . 10 |- (abs` (A .ih B)) e. RR
25	24	recn 5286	. . . . . . . . 9 |- (abs` (A .ih B)) e. CC
26	16, 25	divclz 5680	. . . . . . . 8 |- ((abs` (A .ih B)) =/= 0 -> ((A .ih B) / (abs` (A .ih B))) e. CC)
27	16, 25	divrecz 5701	. . . . . . . . . 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 3713	. . . . . . . . 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 5683	. . . . . . . . . . . 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 6793	. . . . . . . . . . 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 6797	. . . . . . . . . . . 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 5758	. . . . . . . . . . . 12 |- ((abs` (A .ih B)) =/= 0 -> (1 / (abs` (A .ih B))) e. RR)
35		ltlet 5493	. . . . . . . . . . . . 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 5412	. . . . . . . . . . . . . 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 6778	. . . . . . . . . . . . . . 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 5816	. . . . . . . . . . . . . 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 3961	. . . . . . . . . 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 1499	. . . . . . . . 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 5697	. . . . . . . . 9 |- ((abs` (A .ih B)) =/= 0 -> ((abs` (A .ih B)) x. (1 / (abs` (A .ih B)))) = 1)
47	28, 45, 46	3eqtrd 1503	. . . . . . . 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 8906	. . . . . 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 2625	. . . 4 |- ((A .ih B) =/= 0 -> (2 x. (abs` (A .ih B))) <_ (2 x. ((sqr` (B .ih B))