Metamath Proof Explorer

Theorem bcsiALT

Description: Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of Beran p. 98. (Contributed by NM, 11-Oct-1999) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses bcs.1 ⊢ 𝐴 ∈ ℋ
bcs.2 ⊢ 𝐵 ∈ ℋ
Assertion bcsiALT ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≤ ( ( normℎ ‘ 𝐴 ) · ( normℎ ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 bcs.1 ⊢ 𝐴 ∈ ℋ
2 bcs.2 ⊢ 𝐵 ∈ ℋ
3 fveq2 ⊢ ( ( 𝐴 ·ih 𝐵 ) = 0 → ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) = ( abs ‘ 0 ) )
4 abs0 ⊢ ( abs ‘ 0 ) = 0
5 normge0 ⊢ ( 𝐴 ∈ ℋ → 0 ≤ ( normℎ ‘ 𝐴 ) )
6 1 5 ax-mp ⊢ 0 ≤ ( normℎ ‘ 𝐴 )
7 normge0 ⊢ ( 𝐵 ∈ ℋ → 0 ≤ ( normℎ ‘ 𝐵 ) )
8 2 7 ax-mp ⊢ 0 ≤ ( normℎ ‘ 𝐵 )
9 1 normcli ⊢ ( normℎ ‘ 𝐴 ) ∈ ℝ
10 2 normcli ⊢ ( normℎ ‘ 𝐵 ) ∈ ℝ
11 9 10 mulge0i ⊢ ( ( 0 ≤ ( normℎ ‘ 𝐴 ) ∧ 0 ≤ ( normℎ ‘ 𝐵 ) ) → 0 ≤ ( ( normℎ ‘ 𝐴 ) · ( normℎ ‘ 𝐵 ) ) )
12 6 8 11 mp2an ⊢ 0 ≤ ( ( normℎ ‘ 𝐴 ) · ( normℎ ‘ 𝐵 ) )
13 4 12 eqbrtri ⊢ ( abs ‘ 0 ) ≤ ( ( normℎ ‘ 𝐴 ) · ( normℎ ‘ 𝐵 ) )
14 3 13 eqbrtrdi ⊢ ( ( 𝐴 ·ih 𝐵 ) = 0 → ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≤ ( ( normℎ ‘ 𝐴 ) · ( normℎ ‘ 𝐵 ) ) )
15 df-ne ⊢ ( ( 𝐴 ·ih 𝐵 ) ≠ 0 ↔ ¬ ( 𝐴 ·ih 𝐵 ) = 0 )
16 2 1 his1i ⊢ ( 𝐵 ·ih 𝐴 ) = ( ∗ ‘ ( 𝐴 ·ih 𝐵 ) )
17 16 oveq2i ⊢ ( ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) · ( 𝐵 ·ih 𝐴 ) ) = ( ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) · ( ∗ ‘ ( 𝐴 ·ih 𝐵 ) ) )
18 17 oveq2i ⊢ ( ( ( ∗ ‘ ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) · ( 𝐴 ·ih 𝐵 ) ) + ( ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) · ( 𝐵 ·ih 𝐴 ) ) ) = ( ( ( ∗ ‘ ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) · ( 𝐴 ·ih 𝐵 ) ) + ( ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) · ( ∗ ‘ ( 𝐴 ·ih 𝐵 ) ) ) )
19 1 2 hicli ⊢ ( 𝐴 ·ih 𝐵 ) ∈ ℂ
20 abslem2 ⊢ ( ( ( 𝐴 ·ih 𝐵 ) ∈ ℂ ∧ ( 𝐴 ·ih 𝐵 ) ≠ 0 ) → ( ( ( ∗ ‘ ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) · ( 𝐴 ·ih 𝐵 ) ) + ( ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) · ( ∗ ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) = ( 2 · ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) )
21 19 20 mpan ⊢ ( ( 𝐴 ·ih 𝐵 ) ≠ 0 → ( ( ( ∗ ‘ ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) · ( 𝐴 ·ih 𝐵 ) ) + ( ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) · ( ∗ ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) = ( 2 · ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) )
22 18 21 syl5req ⊢ ( ( 𝐴 ·ih 𝐵 ) ≠ 0 → ( 2 · ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) = ( ( ( ∗ ‘ ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) · ( 𝐴 ·ih 𝐵 ) ) + ( ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) · ( 𝐵 ·ih 𝐴 ) ) ) )
23 19 abs00i ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) = 0 ↔ ( 𝐴 ·ih 𝐵 ) = 0 )
24 23 necon3bii ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≠ 0 ↔ ( 𝐴 ·ih 𝐵 ) ≠ 0 )
25 19 abscli ⊢ ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ∈ ℝ
26 25 recni ⊢ ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ∈ ℂ
27 19 26 divclzi ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≠ 0 → ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ∈ ℂ )
28 19 26 divreczi ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≠ 0 → ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) = ( ( 𝐴 ·ih 𝐵 ) · ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) )
29 28 fveq2d ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≠ 0 → ( abs ‘ ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) = ( abs ‘ ( ( 𝐴 ·ih 𝐵 ) · ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) ) )
30 26 recclzi ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≠ 0 → ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ∈ ℂ )
31 absmul ⊢ ( ( ( 𝐴 ·ih 𝐵 ) ∈ ℂ ∧ ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ∈ ℂ ) → ( abs ‘ ( ( 𝐴 ·ih 𝐵 ) · ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) ) = ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) · ( abs ‘ ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) ) )
32 19 30 31 sylancr ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≠ 0 → ( abs ‘ ( ( 𝐴 ·ih 𝐵 ) · ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) ) = ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) · ( abs ‘ ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) ) )
33 25 rerecclzi ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≠ 0 → ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ∈ ℝ )
34 0re ⊢ 0 ∈ ℝ
35 33 34 jctil ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≠ 0 → ( 0 ∈ ℝ ∧ ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ∈ ℝ ) )
36 19 absgt0i ⊢ ( ( 𝐴 ·ih 𝐵 ) ≠ 0 ↔ 0 < ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) )
37 24 36 bitri ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≠ 0 ↔ 0 < ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) )
38 25 recgt0i ⊢ ( 0 < ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) → 0 < ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) )
39 37 38 sylbi ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≠ 0 → 0 < ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) )
40 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ∈ ℝ ) → ( 0 < ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) → 0 ≤ ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) )
41 35 39 40 sylc ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≠ 0 → 0 ≤ ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) )
42 33 41 absidd ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≠ 0 → ( abs ‘ ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) = ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) )
43 42 oveq2d ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≠ 0 → ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) · ( abs ‘ ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) ) = ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) · ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) )
44 32 43 eqtrd ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≠ 0 → ( abs ‘ ( ( 𝐴 ·ih 𝐵 ) · ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) ) = ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) · ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) )
45 26 recidzi ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≠ 0 → ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) · ( 1 / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) = 1 )
46 29 44 45 3eqtrd ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≠ 0 → ( abs ‘ ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) = 1 )
47 27 46 jca ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≠ 0 → ( ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) = 1 ) )
48 24 47 sylbir ⊢ ( ( 𝐴 ·ih 𝐵 ) ≠ 0 → ( ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) = 1 ) )
49 1 2 normlem7tALT ⊢ ( ( ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) = 1 ) → ( ( ( ∗ ‘ ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) · ( 𝐴 ·ih 𝐵 ) ) + ( ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) · ( 𝐵 ·ih 𝐴 ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) ) )
50 48 49 syl ⊢ ( ( 𝐴 ·ih 𝐵 ) ≠ 0 → ( ( ( ∗ ‘ ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ) · ( 𝐴 ·ih 𝐵 ) ) + ( ( ( 𝐴 ·ih 𝐵 ) / ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) · ( 𝐵 ·ih 𝐴 ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) ) )
51 22 50 eqbrtrd ⊢ ( ( 𝐴 ·ih 𝐵 ) ≠ 0 → ( 2 · ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) ) )
52 15 51 sylbir ⊢ ( ¬ ( 𝐴 ·ih 𝐵 ) = 0 → ( 2 · ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) ) )
53 10 recni ⊢ ( normℎ ‘ 𝐵 ) ∈ ℂ
54 9 recni ⊢ ( normℎ ‘ 𝐴 ) ∈ ℂ
55 normval ⊢ ( 𝐵 ∈ ℋ → ( normℎ ‘ 𝐵 ) = ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) )
56 2 55 ax-mp ⊢ ( normℎ ‘ 𝐵 ) = ( √ ‘ ( 𝐵 ·ih 𝐵 ) )
57 normval ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ 𝐴 ) = ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) )
58 1 57 ax-mp ⊢ ( normℎ ‘ 𝐴 ) = ( √ ‘ ( 𝐴 ·ih 𝐴 ) )
59 56 58 oveq12i ⊢ ( ( normℎ ‘ 𝐵 ) · ( normℎ ‘ 𝐴 ) ) = ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) )
60 53 54 59 mulcomli ⊢ ( ( normℎ ‘ 𝐴 ) · ( normℎ ‘ 𝐵 ) ) = ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) )
61 60 breq2i ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≤ ( ( normℎ ‘ 𝐴 ) · ( normℎ ‘ 𝐵 ) ) ↔ ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≤ ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) )
62 2pos ⊢ 0 < 2
63 hiidge0 ⊢ ( 𝐵 ∈ ℋ → 0 ≤ ( 𝐵 ·ih 𝐵 ) )
64 hiidrcl ⊢ ( 𝐵 ∈ ℋ → ( 𝐵 ·ih 𝐵 ) ∈ ℝ )
65 2 64 ax-mp ⊢ ( 𝐵 ·ih 𝐵 ) ∈ ℝ
66 65 sqrtcli ⊢ ( 0 ≤ ( 𝐵 ·ih 𝐵 ) → ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ∈ ℝ )
67 2 63 66 mp2b ⊢ ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ∈ ℝ
68 hiidge0 ⊢ ( 𝐴 ∈ ℋ → 0 ≤ ( 𝐴 ·ih 𝐴 ) )
69 hiidrcl ⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ·ih 𝐴 ) ∈ ℝ )
70 1 69 ax-mp ⊢ ( 𝐴 ·ih 𝐴 ) ∈ ℝ
71 70 sqrtcli ⊢ ( 0 ≤ ( 𝐴 ·ih 𝐴 ) → ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ∈ ℝ )
72 1 68 71 mp2b ⊢ ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ∈ ℝ
73 67 72 remulcli ⊢ ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) ∈ ℝ
74 2re ⊢ 2 ∈ ℝ
75 25 73 74 lemul2i ⊢ ( 0 < 2 → ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≤ ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) ↔ ( 2 · ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) ) ) )
76 62 75 ax-mp ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≤ ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) ↔ ( 2 · ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) ) )
77 61 76 bitri ⊢ ( ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≤ ( ( normℎ ‘ 𝐴 ) · ( normℎ ‘ 𝐵 ) ) ↔ ( 2 · ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) ) )
78 52 77 sylibr ⊢ ( ¬ ( 𝐴 ·ih 𝐵 ) = 0 → ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≤ ( ( normℎ ‘ 𝐴 ) · ( normℎ ‘ 𝐵 ) ) )
79 14 78 pm2.61i ⊢ ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≤ ( ( normℎ ‘ 𝐴 ) · ( normℎ ‘ 𝐵 ) )