Metamath Proof Explorer

Theorem siii

Description: Inference from sii . (Contributed by NM, 20-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses siii.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
siii.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
siii.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
siii.9 ⊢ 𝑈 ∈ CPreHilOLD
siii.a ⊢ 𝐴 ∈ 𝑋
siii.b ⊢ 𝐵 ∈ 𝑋
Assertion siii ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 siii.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 siii.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
3 siii.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
4 siii.9 ⊢ 𝑈 ∈ CPreHilOLD
5 siii.a ⊢ 𝐴 ∈ 𝑋
6 siii.b ⊢ 𝐵 ∈ 𝑋
7 oveq2 ⊢ ( 𝐵 = ( 0vec ‘ 𝑈 ) → ( 𝐴 𝑃 𝐵 ) = ( 𝐴 𝑃 ( 0vec ‘ 𝑈 ) ) )
8 4 phnvi ⊢ 𝑈 ∈ NrmCVec
9 eqid ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
10 1 9 3 dip0r ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝑃 ( 0vec ‘ 𝑈 ) ) = 0 )
11 8 5 10 mp2an ⊢ ( 𝐴 𝑃 ( 0vec ‘ 𝑈 ) ) = 0
12 7 11 eqtrdi ⊢ ( 𝐵 = ( 0vec ‘ 𝑈 ) → ( 𝐴 𝑃 𝐵 ) = 0 )
13 12 abs00bd ⊢ ( 𝐵 = ( 0vec ‘ 𝑈 ) → ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) = 0 )
14 1 2 nvge0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ 𝐴 ) )
15 8 5 14 mp2an ⊢ 0 ≤ ( 𝑁 ‘ 𝐴 )
16 1 2 nvge0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ 𝐵 ) )
17 8 6 16 mp2an ⊢ 0 ≤ ( 𝑁 ‘ 𝐵 )
18 1 2 8 5 nvcli ⊢ ( 𝑁 ‘ 𝐴 ) ∈ ℝ
19 1 2 8 6 nvcli ⊢ ( 𝑁 ‘ 𝐵 ) ∈ ℝ
20 18 19 mulge0i ⊢ ( ( 0 ≤ ( 𝑁 ‘ 𝐴 ) ∧ 0 ≤ ( 𝑁 ‘ 𝐵 ) ) → 0 ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )
21 15 17 20 mp2an ⊢ 0 ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) )
22 13 21 eqbrtrdi ⊢ ( 𝐵 = ( 0vec ‘ 𝑈 ) → ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )
23 1 3 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
24 8 5 6 23 mp3an ⊢ ( 𝐴 𝑃 𝐵 ) ∈ ℂ
25 absval ⊢ ( ( 𝐴 𝑃 𝐵 ) ∈ ℂ → ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) = ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) ) ) )
26 24 25 ax-mp ⊢ ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) = ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) ) )
27 19 recni ⊢ ( 𝑁 ‘ 𝐵 ) ∈ ℂ
28 27 sqeq0i ⊢ ( ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) = 0 ↔ ( 𝑁 ‘ 𝐵 ) = 0 )
29 1 9 2 nvz ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐵 ) = 0 ↔ 𝐵 = ( 0vec ‘ 𝑈 ) ) )
30 8 6 29 mp2an ⊢ ( ( 𝑁 ‘ 𝐵 ) = 0 ↔ 𝐵 = ( 0vec ‘ 𝑈 ) )
31 28 30 bitri ⊢ ( ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) = 0 ↔ 𝐵 = ( 0vec ‘ 𝑈 ) )
32 31 necon3bii ⊢ ( ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ≠ 0 ↔ 𝐵 ≠ ( 0vec ‘ 𝑈 ) )
33 1 3 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 𝑃 𝐴 ) ∈ ℂ )
34 8 6 5 33 mp3an ⊢ ( 𝐵 𝑃 𝐴 ) ∈ ℂ
35 19 resqcli ⊢ ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ∈ ℝ
36 35 recni ⊢ ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ∈ ℂ
37 34 36 divcan1zi ⊢ ( ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ≠ 0 → ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) = ( 𝐵 𝑃 𝐴 ) )
38 32 37 sylbir ⊢ ( 𝐵 ≠ ( 0vec ‘ 𝑈 ) → ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) = ( 𝐵 𝑃 𝐴 ) )
39 1 3 dipcj ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) = ( 𝐵 𝑃 𝐴 ) )
40 8 5 6 39 mp3an ⊢ ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) = ( 𝐵 𝑃 𝐴 )
41 38 40 eqtr4di ⊢ ( 𝐵 ≠ ( 0vec ‘ 𝑈 ) → ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) = ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) )
42 41 oveq2d ⊢ ( 𝐵 ≠ ( 0vec ‘ 𝑈 ) → ( ( 𝐴 𝑃 𝐵 ) · ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) = ( ( 𝐴 𝑃 𝐵 ) · ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) ) )
43 42 fveq2d ⊢ ( 𝐵 ≠ ( 0vec ‘ 𝑈 ) → ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) = ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) ) ) )
44 26 43 eqtr4id ⊢ ( 𝐵 ≠ ( 0vec ‘ 𝑈 ) → ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) = ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) )
45 38 eqcomd ⊢ ( 𝐵 ≠ ( 0vec ‘ 𝑈 ) → ( 𝐵 𝑃 𝐴 ) = ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
46 34 36 divclzi ⊢ ( ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ≠ 0 → ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ∈ ℂ )
47 32 46 sylbir ⊢ ( 𝐵 ≠ ( 0vec ‘ 𝑈 ) → ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ∈ ℂ )
48 1 3 ipipcj ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝑃 𝐵 ) · ( 𝐵 𝑃 𝐴 ) ) = ( ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ↑ 2 ) )
49 8 5 6 48 mp3an ⊢ ( ( 𝐴 𝑃 𝐵 ) · ( 𝐵 𝑃 𝐴 ) ) = ( ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ↑ 2 )
50 24 34 49 mulcomli ⊢ ( ( 𝐵 𝑃 𝐴 ) · ( 𝐴 𝑃 𝐵 ) ) = ( ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ↑ 2 )
51 50 oveq1i ⊢ ( ( ( 𝐵 𝑃 𝐴 ) · ( 𝐴 𝑃 𝐵 ) ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) = ( ( ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ↑ 2 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) )
52 div23 ⊢ ( ( ( 𝐵 𝑃 𝐴 ) ∈ ℂ ∧ ( 𝐴 𝑃 𝐵 ) ∈ ℂ ∧ ( ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ∈ ℂ ∧ ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ≠ 0 ) ) → ( ( ( 𝐵 𝑃 𝐴 ) · ( 𝐴 𝑃 𝐵 ) ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) = ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( 𝐴 𝑃 𝐵 ) ) )
53 34 24 52 mp3an12 ⊢ ( ( ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ∈ ℂ ∧ ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ≠ 0 ) → ( ( ( 𝐵 𝑃 𝐴 ) · ( 𝐴 𝑃 𝐵 ) ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) = ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( 𝐴 𝑃 𝐵 ) ) )
54 36 53 mpan ⊢ ( ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ≠ 0 → ( ( ( 𝐵 𝑃 𝐴 ) · ( 𝐴 𝑃 𝐵 ) ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) = ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( 𝐴 𝑃 𝐵 ) ) )
55 32 54 sylbir ⊢ ( 𝐵 ≠ ( 0vec ‘ 𝑈 ) → ( ( ( 𝐵 𝑃 𝐴 ) · ( 𝐴 𝑃 𝐵 ) ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) = ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( 𝐴 𝑃 𝐵 ) ) )
56 51 55 syl5reqr ⊢ ( 𝐵 ≠ ( 0vec ‘ 𝑈 ) → ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( 𝐴 𝑃 𝐵 ) ) = ( ( ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ↑ 2 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
57 24 abscli ⊢ ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ
58 57 resqcli ⊢ ( ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ↑ 2 ) ∈ ℝ
59 58 35 redivclzi ⊢ ( ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ≠ 0 → ( ( ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ↑ 2 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ∈ ℝ )
60 32 59 sylbir ⊢ ( 𝐵 ≠ ( 0vec ‘ 𝑈 ) → ( ( ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ↑ 2 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ∈ ℝ )
61 56 60 eqeltrd ⊢ ( 𝐵 ≠ ( 0vec ‘ 𝑈 ) → ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ )
62 30 necon3bii ⊢ ( ( 𝑁 ‘ 𝐵 ) ≠ 0 ↔ 𝐵 ≠ ( 0vec ‘ 𝑈 ) )
63 19 sqgt0i ⊢ ( ( 𝑁 ‘ 𝐵 ) ≠ 0 → 0 < ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) )
64 62 63 sylbir ⊢ ( 𝐵 ≠ ( 0vec ‘ 𝑈 ) → 0 < ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) )
65 57 sqge0i ⊢ 0 ≤ ( ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ↑ 2 )
66 divge0 ⊢ ( ( ( ( ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ↑ 2 ) ) ∧ ( ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ∈ ℝ ∧ 0 < ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) → 0 ≤ ( ( ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ↑ 2 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
67 58 65 66 mpanl12 ⊢ ( ( ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ∈ ℝ ∧ 0 < ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) → 0 ≤ ( ( ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ↑ 2 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
68 35 64 67 sylancr ⊢ ( 𝐵 ≠ ( 0vec ‘ 𝑈 ) → 0 ≤ ( ( ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ↑ 2 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
69 68 56 breqtrrd ⊢ ( 𝐵 ≠ ( 0vec ‘ 𝑈 ) → 0 ≤ ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( 𝐴 𝑃 𝐵 ) ) )
70 eqid ⊢ ( −𝑣 ‘ 𝑈 ) = ( −𝑣 ‘ 𝑈 )
71 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
72 1 2 3 4 5 6 70 71 siilem2 ⊢ ( ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ∈ ℂ ∧ ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( 𝐴 𝑃 𝐵 ) ) ) → ( ( 𝐵 𝑃 𝐴 ) = ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) → ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) ) )
73 47 61 69 72 syl3anc ⊢ ( 𝐵 ≠ ( 0vec ‘ 𝑈 ) → ( ( 𝐵 𝑃 𝐴 ) = ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) → ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) ) )
74 45 73 mpd ⊢ ( 𝐵 ≠ ( 0vec ‘ 𝑈 ) → ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( ( ( 𝐵 𝑃 𝐴 ) / ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )
75 44 74 eqbrtrd ⊢ ( 𝐵 ≠ ( 0vec ‘ 𝑈 ) → ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )
76 22 75 pm2.61ine ⊢ ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) )