Metamath Proof Explorer


Theorem bcseqi

Description: Equality case of Bunjakovaskij-Cauchy-Schwarz inequality. Specifically, in the equality case the two vectors are collinear. Compare bcsiHIL . (Contributed by NM, 16-Jul-2001) (New usage is discouraged.)

Ref Expression
Hypotheses normlem7t.1 A
normlem7t.2 B
Assertion bcseqi A ih B B ih A = A ih A B ih B B ih B A = A ih B B

Proof

Step Hyp Ref Expression
1 normlem7t.1 A
2 normlem7t.2 B
3 2 2 hicli B ih B
4 3 1 hvmulcli B ih B A
5 1 2 hicli A ih B
6 5 2 hvmulcli A ih B B
7 4 6 4 6 normlem9 B ih B A - A ih B B ih B ih B A - A ih B B = B ih B A ih B ih B A + A ih B B ih A ih B B - B ih B A ih A ih B B + A ih B B ih B ih B A
8 oveq1 A ih B B ih A = A ih A B ih B A ih B B ih A B ih B = A ih A B ih B B ih B
9 8 eqcomd A ih B B ih A = A ih A B ih B A ih A B ih B B ih B = A ih B B ih A B ih B
10 his5 B ih B B ih B A A B ih B A ih B ih B A = B ih B B ih B A ih A
11 3 4 1 10 mp3an B ih B A ih B ih B A = B ih B B ih B A ih A
12 hiidrcl B B ih B
13 cjre B ih B B ih B = B ih B
14 2 12 13 mp2b B ih B = B ih B
15 ax-his3 B ih B A A B ih B A ih A = B ih B A ih A
16 3 1 1 15 mp3an B ih B A ih A = B ih B A ih A
17 14 16 oveq12i B ih B B ih B A ih A = B ih B B ih B A ih A
18 1 1 hicli A ih A
19 3 18 mulcli B ih B A ih A
20 3 19 mulcomi B ih B B ih B A ih A = B ih B A ih A B ih B
21 18 3 mulcomi A ih A B ih B = B ih B A ih A
22 21 oveq1i A ih A B ih B B ih B = B ih B A ih A B ih B
23 20 22 eqtr4i B ih B B ih B A ih A = A ih A B ih B B ih B
24 11 17 23 3eqtri B ih B A ih B ih B A = A ih A B ih B B ih B
25 his5 A ih B B ih B A B B ih B A ih A ih B B = A ih B B ih B A ih B
26 5 4 2 25 mp3an B ih B A ih A ih B B = A ih B B ih B A ih B
27 2 1 his1i B ih A = A ih B
28 27 eqcomi A ih B = B ih A
29 ax-his3 B ih B A B B ih B A ih B = B ih B A ih B
30 3 1 2 29 mp3an B ih B A ih B = B ih B A ih B
31 28 30 oveq12i A ih B B ih B A ih B = B ih A B ih B A ih B
32 2 1 hicli B ih A
33 3 5 mulcli B ih B A ih B
34 32 33 mulcomi B ih A B ih B A ih B = B ih B A ih B B ih A
35 3 5 32 mulassi B ih B A ih B B ih A = B ih B A ih B B ih A
36 5 32 mulcli A ih B B ih A
37 3 36 mulcomi B ih B A ih B B ih A = A ih B B ih A B ih B
38 34 35 37 3eqtri B ih A B ih B A ih B = A ih B B ih A B ih B
39 26 31 38 3eqtri B ih B A ih A ih B B = A ih B B ih A B ih B
40 9 24 39 3eqtr4g A ih B B ih A = A ih A B ih B B ih B A ih B ih B A = B ih B A ih A ih B B
41 ax-his3 A ih B B A A ih B B ih A = A ih B B ih A
42 5 2 1 41 mp3an A ih B B ih A = A ih B B ih A
43 14 42 oveq12i B ih B A ih B B ih A = B ih B A ih B B ih A
44 his5 B ih B A ih B B A A ih B B ih B ih B A = B ih B A ih B B ih A
45 3 6 1 44 mp3an A ih B B ih B ih B A = B ih B A ih B B ih A
46 his5 A ih B A ih B B B A ih B B ih A ih B B = A ih B A ih B B ih B
47 5 6 2 46 mp3an A ih B B ih A ih B B = A ih B A ih B B ih B
48 ax-his3 A ih B B B A ih B B ih B = A ih B B ih B
49 5 2 2 48 mp3an A ih B B ih B = A ih B B ih B
50 28 49 oveq12i A ih B A ih B B ih B = B ih A A ih B B ih B
51 5 3 mulcli A ih B B ih B
52 32 51 mulcomi B ih A A ih B B ih B = A ih B B ih B B ih A
53 5 3 32 mul32i A ih B B ih B B ih A = A ih B B ih A B ih B
54 36 3 mulcomi A ih B B ih A B ih B = B ih B A ih B B ih A
55 52 53 54 3eqtri B ih A A ih B B ih B = B ih B A ih B B ih A
56 47 50 55 3eqtri A ih B B ih A ih B B = B ih B A ih B B ih A
57 43 45 56 3eqtr4ri A ih B B ih A ih B B = A ih B B ih B ih B A
58 57 a1i A ih B B ih A = A ih A B ih B A ih B B ih A ih B B = A ih B B ih B ih B A
59 40 58 oveq12d A ih B B ih A = A ih A B ih B B ih B A ih B ih B A + A ih B B ih A ih B B = B ih B A ih A ih B B + A ih B B ih B ih B A
60 59 oveq1d A ih B B ih A = A ih A B ih B B ih B A ih B ih B A + A ih B B ih A ih B B - B ih B A ih A ih B B + A ih B B ih B ih B A = B ih B A ih A ih B B + A ih B B ih B ih B A - B ih B A ih A ih B B + A ih B B ih B ih B A
61 4 6 hicli B ih B A ih A ih B B
62 6 4 hicli A ih B B ih B ih B A
63 61 62 addcli B ih B A ih A ih B B + A ih B B ih B ih B A
64 63 subidi B ih B A ih A ih B B + A ih B B ih B ih B A - B ih B A ih A ih B B + A ih B B ih B ih B A = 0
65 60 64 syl6eq A ih B B ih A = A ih A B ih B B ih B A ih B ih B A + A ih B B ih A ih B B - B ih B A ih A ih B B + A ih B B ih B ih B A = 0
66 7 65 syl5eq A ih B B ih A = A ih A B ih B B ih B A - A ih B B ih B ih B A - A ih B B = 0
67 4 6 hvsubcli B ih B A - A ih B B
68 his6 B ih B A - A ih B B B ih B A - A ih B B ih B ih B A - A ih B B = 0 B ih B A - A ih B B = 0
69 67 68 ax-mp B ih B A - A ih B B ih B ih B A - A ih B B = 0 B ih B A - A ih B B = 0
70 66 69 sylib A ih B B ih A = A ih A B ih B B ih B A - A ih B B = 0
71 4 6 hvsubeq0i B ih B A - A ih B B = 0 B ih B A = A ih B B
72 70 71 sylib A ih B B ih A = A ih A B ih B B ih B A = A ih B B
73 oveq1 B ih B A = A ih B B B ih B A ih A = A ih B B ih A
74 21 16 eqtr4i A ih A B ih B = B ih B A ih A
75 42 eqcomi A ih B B ih A = A ih B B ih A
76 73 74 75 3eqtr4g B ih B A = A ih B B A ih A B ih B = A ih B B ih A
77 76 eqcomd B ih B A = A ih B B A ih B B ih A = A ih A B ih B
78 72 77 impbii A ih B B ih A = A ih A B ih B B ih B A = A ih B B