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⋅ihB⁢B⋅ihA=A⋅ihA⁢B⋅ihB↔B⋅ihB⋅ℎA=A⋅ihB⋅ℎB

Proof

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