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 e. ~H
normlem7t.2 
|- B e. ~H
Assertion bcseqi 
|- ( ( ( 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

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