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 eqtrdi ⊢ 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