Theorem bcseq 8925

Description: Equality case of Bunjakovaskij-Cauchy-Schwarz inequality. Specifically, in the equality case the two vectors are collinear. Compare bcsHIL 8986.

Hypotheses

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

Assertion

Ref	Expression
bcseq	|- (((A .ih B) x. (B .ih A)) = ((A .ih A) x. (B .ih B)) <-> ((B .ih B) .h A) = ((A .ih B) .h B))

Proof of Theorem bcseq

Step	Hyp	Ref	Expression
1		opreq1 3959	. . . . . . . . . 10 |- (((A .ih B) x. (B .ih A)) = ((A .ih A) x. (B .ih B)) -> (((A .ih B) x. (B .ih A)) x. (B .ih B)) = (((A .ih A) x. (B .ih B)) x. (B .ih B)))
2	1	eqcomd 1477	. . . . . . . . 9 |- (((A .ih B) x. (B .ih A)) = ((A .ih A) x. (B .ih B)) -> (((A .ih A) x. (B .ih B)) x. (B .ih B)) = (((A .ih B) x. (B .ih A)) x. (B .ih B)))
3		normlem7t.2	. . . . . . . . . . . 12 |- B e. H~
4	3, 3	hicl 8887	. . . . . . . . . . 11 |- (B .ih B) e. CC
5		normlem7t.1	. . . . . . . . . . . 12 |- A e. H~
6	4, 5	hvmulcl 8823	. . . . . . . . . . 11 |- ((B .ih B) .h A) e. H~
7		his5t 8892	. . . . . . . . . . 11 |- (((B .ih B) e. CC /\ ((B .ih B) .h A) e. H~ /\ A e. H~) -> (((B .ih B) .h A) .ih ((B .ih B) .h A)) = ((*` (B .ih B)) x. (((B .ih B) .h A) .ih A)))
8	4, 6, 5, 7	mp3an 914	. . . . . . . . . 10 |- (((B .ih B) .h A) .ih ((B .ih B) .h A)) = ((*` (B .ih B)) x. (((B .ih B) .h A) .ih A))
9		hiidrclt 8900	. . . . . . . . . . . . 13 |- (B e. H~ -> (B .ih B) e. RR)
10	3, 9	ax-mp 7	. . . . . . . . . . . 12 |- (B .ih B) e. RR
11		cjret 6753	. . . . . . . . . . . 12 |- ((B .ih B) e. RR -> (*` (B .ih B)) = (B .ih B))
12	10, 11	ax-mp 7	. . . . . . . . . . 11 |- (*` (B .ih B)) = (B .ih B)
13		ax-his3 8890	. . . . . . . . . . . 12 |- (((B .ih B) e. CC /\ A e. H~ /\ A e. H~) -> (((B .ih B) .h A) .ih A) = ((B .ih B) x. (A .ih A)))
14	4, 5, 5, 13	mp3an 914	. . . . . . . . . . 11 |- (((B .ih B) .h A) .ih A) = ((B .ih B) x. (A .ih A))
15	12, 14	opreq12i 3964	. . . . . . . . . 10 |- ((*` (B .ih B)) x. (((B .ih B) .h A) .ih A)) = ((B .ih B) x. ((B .ih B) x. (A .ih A)))
16	5, 5	hicl 8887	. . . . . . . . . . . . 13 |- (A .ih A) e. CC
17	4, 16	mulcl 5301	. . . . . . . . . . . 12 |- ((B .ih B) x. (A .ih A)) e. CC
18	4, 17	mulcom 5303	. . . . . . . . . . 11 |- ((B .ih B) x. ((B .ih B) x. (A .ih A))) = (((B .ih B) x. (A .ih A)) x. (B .ih B))
19	16, 4	mulcom 5303	. . . . . . . . . . . 12 |- ((A .ih A) x. (B .ih B)) = ((B .ih B) x. (A .ih A))
20	19	opreq1i 3962	. . . . . . . . . . 11 |- (((A .ih A) x. (B .ih B)) x. (B .ih B)) = (((B .ih B) x. (A .ih A)) x. (B .ih B))
21	18, 20	eqtr4 1495	. . . . . . . . . 10 |- ((B .ih B) x. ((B .ih B) x. (A .ih A))) = (((A .ih A) x. (B .ih B)) x. (B .ih B))
22	8, 15, 21	3eqtr 1496	. . . . . . . . 9 |- (((B .ih B) .h A) .ih ((B .ih B) .h A)) = (((A .ih A) x. (B .ih B)) x. (B .ih B))
23	5, 3	hicl 8887	. . . . . . . . . . 11 |- (A .ih B) e. CC
24		his5t 8892	. . . . . . . . . . 11 |- (((A .ih B) e. CC /\ ((B .ih B) .h A) e. H~ /\ B e. H~) -> (((B .ih B) .h A) .ih ((A .ih B) .h B)) = ((*` (A .ih B)) x. (((B .ih B) .h A) .ih B)))
25	23, 6, 3, 24	mp3an 914	. . . . . . . . . 10 |- (((B .ih B) .h A) .ih ((A .ih B) .h B)) = ((*` (A .ih B)) x. (((B .ih B) .h A) .ih B))
26	3, 5	his1 8905	. . . . . . . . . . . 12 |- (B .ih A) = (*` (A .ih B))
27	26	eqcomi 1476	. . . . . . . . . . 11 |- (*` (A .ih B)) = (B .ih A)
28		ax-his3 8890	. . . . . . . . . . . 12 |- (((B .ih B) e. CC /\ A e. H~ /\ B e. H~) -> (((B .ih B) .h A) .ih B) = ((B .ih B) x. (A .ih B)))
29	4, 5, 3, 28	mp3an 914	. . . . . . . . . . 11 |- (((B .ih B) .h A) .ih B) = ((B .ih B) x. (A .ih B))
30	27, 29	opreq12i 3964	. . . . . . . . . 10 |- ((*` (A .ih B)) x. (((B .ih B) .h A) .ih B)) = ((B .ih A) x. ((B .ih B) x. (A .ih B)))
31	3, 5	hicl 8887	. . . . . . . . . . . 12 |- (B .ih A) e. CC
32	4, 23	mulcl 5301	. . . . . . . . . . . 12 |- ((B .ih B) x. (A .ih B)) e. CC
33	31, 32	mulcom 5303	. . . . . . . . . . 11 |- ((B .ih A) x. ((B .ih B) x. (A .ih B))) = (((B .ih B) x. (A .ih B)) x. (B .ih A))
34	4, 23, 31	mulass 5305	. . . . . . . . . . 11 |- (((B .ih B) x. (A .ih B)) x. (B .ih A)) = ((B .ih B) x. ((A .ih B) x. (B .ih A)))
35	23, 31	mulcl 5301	. . . . . . . . . . . 12 |- ((A .ih B) x. (B .ih A)) e. CC
36	4, 35	mulcom 5303	. . . . . . . . . . 11 |- ((B .ih B) x. ((A .ih B) x. (B .ih A))) = (((A .ih B) x. (B .ih A)) x. (B .ih B))
37	33, 34, 36	3eqtr 1496	. . . . . . . . . 10 |- ((B .ih A) x. ((B .ih B) x. (A .ih B))) = (((A .ih B) x. (B .ih A)) x. (B .ih B))
38	25, 30, 37	3eqtr 1496	. . . . . . . . 9 |- (((B .ih B) .h A) .ih ((A .ih B) .h B)) = (((A .ih B) x. (B .ih A)) x. (B .ih B))
39	2, 22, 38	3eqtr4g 1528	. . . . . . . 8 |- (((A .ih B) x. (B .ih A)) = ((A .ih A) x. (B .ih B)) -> (((B .ih B) .h A) .ih ((B .ih B) .h A)) = (((B .ih B) .h A) .ih ((A .ih B) .h B)))
40		ax-his3 8890	. . . . . . . . . . . 12 |- (((A .ih B) e. CC /\ B e. H~ /\ A e. H~) -> (((A .ih B) .h B) .ih A) = ((A .ih B) x. (B .ih A)))
41	23, 3, 5, 40	mp3an 914	. . . . . . . . . . 11 |- (((A .ih B) .h B) .ih A) = ((A .ih B) x. (B .ih A))
42	12, 41	opreq12i 3964	. . . . . . . . . 10 |- ((*` (B .ih B)) x. (((A .ih B) .h B) .ih A)) = ((B .ih B) x. ((A .ih B) x. (B .ih A)))
43	23, 3	hvmulcl 8823	. . . . . . . . . . 11 |- ((A .ih B) .h B) e. H~
44		his5t 8892	. . . . . . . . . . 11 |- (((B .ih B) e. CC /\ ((A .ih B) .h B) e. H~ /\ A e. H~) -> (((A .ih B) .h B) .ih ((B .ih B) .h A)) = ((*` (B .ih B)) x. (((A .ih B) .h B) .ih A)))
45	4, 43, 5, 44	mp3an 914	. . . . . . . . . 10 |- (((A .ih B) .h B) .ih ((B .ih B) .h A)) = ((*` (B .ih B)) x. (((A .ih B) .h B) .ih A))
46		his5t 8892	. . . . . . . . . . . 12 |- (((A .ih B) e. CC /\ ((A .ih B) .h B) e. H~ /\ B e. H~) -> (((A .ih B) .h B) .ih ((A .ih B) .h B)) = ((*` (A .ih B)) x. (((A .ih B) .h B) .ih B)))
47	23, 43, 3, 46	mp3an 914	. . . . . . . . . . 11 |- (((A .ih B) .h B) .ih ((A .ih B) .h B)) = ((*` (A .ih B)) x. (((A .ih B) .h B) .ih B))
48		ax-his3 8890	. . . . . . . . . . . . 13 |- (((A .ih B) e. CC /\ B e. H~ /\ B e. H~) -> (((A .ih B) .h B) .ih B) = ((A .ih B) x. (B .ih B)))
49	23, 3, 3, 48	mp3an 914	. . . . . . . . . . . 12 |- (((A .ih B) .h B) .ih B) = ((A .ih B) x. (B .ih B))
50	27, 49	opreq12i 3964	. . . . . . . . . . 11 |- ((*` (A .ih B)) x. (((A .ih B) .h B) .ih B)) = ((B .ih A) x. ((A .ih B) x. (B .ih B)))
51	23, 4	mulcl 5301	. . . . . . . . . . . . 13 |- ((A .ih B) x. (B .ih B)) e. CC
52	31, 51	mulcom 5303	. . . . . . . . . . . 12 |- ((B .ih A) x. ((A .ih B) x. (B .ih B))) = (((A .ih B) x. (B .ih B)) x. (B .ih A))
53	23, 4, 31	mul23 5404	. . . . . . . . . . . 12 |- (((A .ih B) x. (B .ih B)) x. (B .ih A)) = (((A .ih B) x. (B .ih A)) x. (B .ih B))
54	35, 4	mulcom 5303	. . . . . . . . . . . 12 |- (((A .ih B) x. (B .ih A)) x. (B .ih B)) = ((B .ih B)