Theorem bcseq 5073

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

Hypotheses

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

Assertion

Ref	Expression
bcseq	|- (((A .i B) x. (B .i A)) = ((A .i A) x. (B .i B)) <-> ((B .i B) .s A) = ((A .i B) .s B))

Proof of Theorem bcseq

Step	Hyp	Ref	Expression
1		opreq1 3006	. . . . . . . . . 10 |- (((A .i B) x. (B .i A)) = ((A .i A) x. (B .i B)) -> (((A .i B) x. (B .i A)) x. (B .i B)) = (((A .i A) x. (B .i B)) x. (B .i B)))
2	1	cleqcomd 1106	. . . . . . . . 9 |- (((A .i B) x. (B .i A)) = ((A .i A) x. (B .i B)) -> (((A .i A) x. (B .i B)) x. (B .i B)) = (((A .i B) x. (B .i A)) x. (B .i B)))
3		normlem8.2	. . . . . . . . . . . 12 |- B e. H~
4	3, 3	hicl 5044	. . . . . . . . . . 11 |- (B .i B) e. CC
5		normlem8.1	. . . . . . . . . . . 12 |- A e. H~
6	4, 5	hvmulcl 4990	. . . . . . . . . . 11 |- ((B .i B) .s A) e. H~
7		his5 5050	. . . . . . . . . . 11 |- (((B .i B) e. CC /\ ((B .i B) .s A) e. H~ /\ A e. H~) -> (((B .i B) .s A) .i ((B .i B) .s A)) = ((*` (B .i B)) x. (((B .i B) .s A) .i A)))
8	4, 6, 5, 7	mp3an 642	. . . . . . . . . 10 |- (((B .i B) .s A) .i ((B .i B) .s A)) = ((*` (B .i B)) x. (((B .i B) .s A) .i A))
9		hiidrclt 5053	. . . . . . . . . . . . 13 |- (B e. H~ -> (B .i B) e. RR)
10	3, 9	ax-mp 6	. . . . . . . . . . . 12 |- (B .i B) e. RR
11		cjret 4829	. . . . . . . . . . . 12 |- ((B .i B) e. RR -> (*` (B .i B)) = (B .i B))
12	10, 11	ax-mp 6	. . . . . . . . . . 11 |- (*` (B .i B)) = (B .i B)
13		ax-his3 5047	. . . . . . . . . . . 12 |- (((B .i B) e. CC /\ A e. H~ /\ A e. H~) -> (((B .i B) .s A) .i A) = ((B .i B) x. (A .i A)))
14	4, 5, 5, 13	mp3an 642	. . . . . . . . . . 11 |- (((B .i B) .s A) .i A) = ((B .i B) x. (A .i A))
15	12, 14	opreq12i 3011	. . . . . . . . . 10 |- ((*` (B .i B)) x. (((B .i B) .s A) .i A)) = ((B .i B) x. ((B .i B) x. (A .i A)))
16	5, 5	hicl 5044	. . . . . . . . . . . . 13 |- (A .i A) e. CC
17	4, 16	mulcl 4105	. . . . . . . . . . . 12 |- ((B .i B) x. (A .i A)) e. CC
18	4, 17	mulcom 4107	. . . . . . . . . . 11 |- ((B .i B) x. ((B .i B) x. (A .i A))) = (((B .i B) x. (A .i A)) x. (B .i B))
19	16, 4	mulcom 4107	. . . . . . . . . . . 12 |- ((A .i A) x. (B .i B)) = ((B .i B) x. (A .i A))
20	19	opreq1i 3009	. . . . . . . . . . 11 |- (((A .i A) x. (B .i B)) x. (B .i B)) = (((B .i B) x. (A .i A)) x. (B .i B))
21	18, 20	eqtr4 1122	. . . . . . . . . 10 |- ((B .i B) x. ((B .i B) x. (A .i A))) = (((A .i A) x. (B .i B)) x. (B .i B))
22	8, 15, 21	3eqtr 1123	. . . . . . . . 9 |- (((B .i B) .s A) .i ((B .i B) .s A)) = (((A .i A) x. (B .i B)) x. (B .i B))
23	5, 3	hicl 5044	. . . . . . . . . . 11 |- (A .i B) e. CC
24		his5 5050	. . . . . . . . . . 11 |- (((A .i B) e. CC /\ ((B .i B) .s A) e. H~ /\ B e. H~) -> (((B .i B) .s A) .i ((A .i B) .s B)) = ((*` (A .i B)) x. (((B .i B) .s A) .i B)))
25	23, 6, 3, 24	mp3an 642	. . . . . . . . . 10 |- (((B .i B) .s A) .i ((A .i B) .s B)) = ((*` (A .i B)) x. (((B .i B) .s A) .i B))
26		ax-his1 5045	. . . . . . . . . . . . 13 |- ((B e. H~ /\ A e. H~) -> (B .i A) = (*` (A .i B)))
27	3, 5, 26	mp2an 520	. . . . . . . . . . . 12 |- (B .i A) = (*` (A .i B))
28	27	cleqcomi 1105	. . . . . . . . . . 11 |- (*` (A .i B)) = (B .i A)
29		ax-his3 5047	. . . . . . . . . . . 12 |- (((B .i B) e. CC /\ A e. H~ /\ B e. H~) -> (((B .i B) .s A) .i B) = ((B .i B) x. (A .i B)))
30	4, 5, 3, 29	mp3an 642	. . . . . . . . . . 11 |- (((B .i B) .s A) .i B) = ((B .i B) x. (A .i B))
31	28, 30	opreq12i 3011	. . . . . . . . . 10 |- ((*` (A .i B)) x. (((B .i B) .s A) .i B)) = ((B .i A) x. ((B .i B) x. (A .i B)))
32	3, 5	hicl 5044	. . . . . . . . . . . 12 |- (B .i A) e. CC
33	4, 23	mulcl 4105	. . . . . . . . . . . 12 |- ((B .i B) x. (A .i B)) e. CC
34	32, 33	mulcom 4107	. . . . . . . . . . 11 |- ((B .i A) x. ((B .i B) x. (A .i B))) = (((B .i B) x. (A .i B)) x. (B .i A))
35	4, 23, 32	mulass 4109	. . . . . . . . . . 11 |- (((B .i B) x. (A .i B)) x. (B .i A)) = ((B .i B) x. ((A .i B) x. (B .i A)))
36	23, 32	mulcl 4105	. . . . . . . . . . . 12 |- ((A .i B) x. (B .i A)) e. CC
37	4, 36	mulcom 4107	. . . . . . . . . . 11 |- ((B .i B) x. ((A .i B) x. (B .i A))) = (((A .i B) x. (B .i A)) x. (B .i B))
38	34, 35, 37	3eqtr 1123	. . . . . . . . . 10 |- ((B .i A) x. ((B .i B) x. (A .i B))) = (((A .i B) x. (B .i A)) x. (B .i B))
39	25, 31, 38	3eqtr 1123	. . . . . . . . 9 |- (((B .i B) .s A) .i ((A .i B) .s B)) = (((A .i B) x. (B .i A)) x. (B .i B))
40	2, 22, 39	3eqtr4g 1147	. . . . . . . 8 |- (((A .i B) x. (B .i A)) = ((A .i A) x. (B .i B)) -> (((B .i B) .s A) .i ((B .i B) .s A)) = (((B .i B) .s A) .i ((A .i B) .s B)))
41		ax-his3 5047	. . . . . . . . . . . 12 |- (((A .i B) e. CC /\ B e. H~ /\ A e. H~) -> (((A .i B) .s B) .i A) = ((A .i B) x. (B .i A)))
42	23, 3, 5, 41	mp3an 642	. . . . . . . . . . 11 |- (((A .i B) .s B) .i A) = ((A .i B) x. (B .i A))
43	12, 42	opreq12i 3011	. . . . . . . . . 10 |- ((*` (B .i B)) x. (((A .i B) .s B) .i A)) = ((B .i B) x. ((A .i B) x. (B .i A)))
44	23, 3	hvmulcl 4990	. . . . . . . . . . 11 |- ((A .i B) .s B) e. H~
45		his5 5050	. . . . . . . . . . 11 |- (((B .i B) e. CC /\ ((A .i B) .s B) e. H~ /\ A e. H~) -> (((A .i B) .s B) .i ((B .i B) .s A)) = ((*` (B .i B)) x. (((A .i B) .s B) .i A)))
46	4, 44, 5, 45	mp3an 642	. . . . . . . . . 10 |- (((A .i B) .s B) .i ((B .i B) .s A)) = ((*` (B .i B)) x. (((A .i B) .s B) .i A))
47		his5 5050	. . . . . . . . . . . 12 |- (((A .i B) e. CC /\ ((A .i B) .s B) e. H~ /\ B e. H~) -> (((A .i B) .s B) .i ((A .i B) .s B)) = ((*` (A .i B)) x. (((A .i B) .s B) .i B)))
48	23, 44, 3, 47	mp3an 642	. . . . . . . . . . 11 |- (((A .i B) .s B) .i ((A .i B) .s B)) = ((*` (A .i B)) x. (((A .i B) .s B) .i B))
49		ax-his3 5047	. . . . . . . . . . . . 13 |- (((A .i B) e. CC /\ B e. H~ /\ B e. H~) -> (((A .i B) .s B) .i B) = ((A .i B) x. (B .i B)))
50	23, 3, 3, 49	mp3an 642	. . . . . . . . . . . 12 |- (((A .i B) .s B) .i B) = ((A .i B) x. (B .i B))
51	28, 50	opreq12i 3011	. . . . . . . . . . 11 |- ((*` (A .i B)) x. (((A .i B) .s B) .i B)) = ((B .i A) x. ((A .i B) x. (B .i B)))
52	23, 4	mulcl 4105	. . . . . . . . . . . . 13 |- ((A .i B) x. (B .i B)) e. CC
53	32, 52	mulcom 4107	. . . . . . . . . . . 12 |- ((B .i A) x. ((A .i B) x. (B .i B))) = (((A .i B) x. (B .i B)) x. (B .i A))
54	23, 4, 32	mul23 4179	. . . . . . . . . . . 12 |- (((A .i B) x. (B .i B)) x. (B .i A)) = (((A .i B) x. (B .i A)) x. (B .i B))
55	36, 4	mulcom 4107	. . . . . . . . . . . 12 |- (((A .i B) x. (B .i A)) x. (B .i B)) = ((B .i B) x. ((A .i B) x. (B .i A)))
56	53, 54, 55	3eqtr 1123	. . . . . . . . . . 11 |- ((B .i A) x. ((A .i B) x.