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 ⊢A∈ℋ
bcs.2 ⊢B∈ℋ
Assertion bcsiALT ⊢A⋅ihB≤normℎ⁡A⁢normℎ⁡B

Proof

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