Metamath Proof Explorer


Theorem siilem1

Description: Lemma for sii . (Contributed by NM, 23-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 𝐵𝑋
sii1.3 𝑀 = ( −𝑣𝑈 )
sii1.4 𝑆 = ( ·𝑠OLD𝑈 )
sii1.c 𝐶 ∈ ℂ
sii1.r ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ
sii1.z 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) )
Assertion siilem1 ( ( 𝐵 𝑃 𝐴 ) = ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) → ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) ≤ ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) )

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 sii1.3 𝑀 = ( −𝑣𝑈 )
8 sii1.4 𝑆 = ( ·𝑠OLD𝑈 )
9 sii1.c 𝐶 ∈ ℂ
10 sii1.r ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ
11 sii1.z 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) )
12 4 phnvi 𝑈 ∈ NrmCVec
13 9 cjcli ( ∗ ‘ 𝐶 ) ∈ ℂ
14 1 8 nvscl ( ( 𝑈 ∈ NrmCVec ∧ ( ∗ ‘ 𝐶 ) ∈ ℂ ∧ 𝐵𝑋 ) → ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ∈ 𝑋 )
15 12 13 6 14 mp3an ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ∈ 𝑋
16 1 7 nvmcl ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ∧ ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ∈ 𝑋 ) → ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ∈ 𝑋 )
17 12 5 15 16 mp3an ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ∈ 𝑋
18 1 2 12 17 nvcli ( 𝑁 ‘ ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) ∈ ℝ
19 18 sqge0i 0 ≤ ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) ↑ 2 )
20 17 5 15 3pm3.2i ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ∈ 𝑋𝐴𝑋 ∧ ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ∈ 𝑋 )
21 1 7 3 dipsubdi ( ( 𝑈 ∈ CPreHilOLD ∧ ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ∈ 𝑋𝐴𝑋 ∧ ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) = ( ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 𝐴 ) − ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) )
22 4 20 21 mp2an ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) = ( ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 𝐴 ) − ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) )
23 1 2 3 ipidsq ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ∈ 𝑋 ) → ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) = ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) ↑ 2 ) )
24 12 17 23 mp2an ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) = ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) ↑ 2 )
25 13 6 15 3pm3.2i ( ( ∗ ‘ 𝐶 ) ∈ ℂ ∧ 𝐵𝑋 ∧ ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ∈ 𝑋 )
26 1 8 3 dipass ( ( 𝑈 ∈ CPreHilOLD ∧ ( ( ∗ ‘ 𝐶 ) ∈ ℂ ∧ 𝐵𝑋 ∧ ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ∈ 𝑋 ) ) → ( ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) = ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) )
27 4 25 26 mp2an ( ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) = ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) )
28 6 9 6 3pm3.2i ( 𝐵𝑋𝐶 ∈ ℂ ∧ 𝐵𝑋 )
29 1 8 3 dipassr2 ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐵𝑋𝐶 ∈ ℂ ∧ 𝐵𝑋 ) ) → ( 𝐵 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) = ( 𝐶 · ( 𝐵 𝑃 𝐵 ) ) )
30 4 28 29 mp2an ( 𝐵 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) = ( 𝐶 · ( 𝐵 𝑃 𝐵 ) )
31 1 2 3 ipidsq ( ( 𝑈 ∈ NrmCVec ∧ 𝐵𝑋 ) → ( 𝐵 𝑃 𝐵 ) = ( ( 𝑁𝐵 ) ↑ 2 ) )
32 12 6 31 mp2an ( 𝐵 𝑃 𝐵 ) = ( ( 𝑁𝐵 ) ↑ 2 )
33 32 oveq2i ( 𝐶 · ( 𝐵 𝑃 𝐵 ) ) = ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) )
34 30 33 eqtri ( 𝐵 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) = ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) )
35 34 oveq2i ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) = ( ( ∗ ‘ 𝐶 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) )
36 27 35 eqtri ( ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) = ( ( ∗ ‘ 𝐶 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) )
37 36 oveq2i ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) − ( ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) = ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) − ( ( ∗ ‘ 𝐶 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) )
38 37 oveq2i ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 𝐴 ) ) ) − ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) − ( ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) ) = ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 𝐴 ) ) ) − ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) − ( ( ∗ ‘ 𝐶 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) )
39 1 2 12 5 nvcli ( 𝑁𝐴 ) ∈ ℝ
40 39 recni ( 𝑁𝐴 ) ∈ ℂ
41 40 sqcli ( ( 𝑁𝐴 ) ↑ 2 ) ∈ ℂ
42 1 3 dipcl ( ( 𝑈 ∈ NrmCVec ∧ 𝐵𝑋𝐴𝑋 ) → ( 𝐵 𝑃 𝐴 ) ∈ ℂ )
43 12 6 5 42 mp3an ( 𝐵 𝑃 𝐴 ) ∈ ℂ
44 13 43 mulcli ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 𝐴 ) ) ∈ ℂ
45 10 recni ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℂ
46 1 2 12 6 nvcli ( 𝑁𝐵 ) ∈ ℝ
47 46 recni ( 𝑁𝐵 ) ∈ ℂ
48 47 sqcli ( ( 𝑁𝐵 ) ↑ 2 ) ∈ ℂ
49 9 48 mulcli ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ∈ ℂ
50 13 49 mulcli ( ( ∗ ‘ 𝐶 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ∈ ℂ
51 sub4 ( ( ( ( ( 𝑁𝐴 ) ↑ 2 ) ∈ ℂ ∧ ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 𝐴 ) ) ∈ ℂ ) ∧ ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℂ ∧ ( ( ∗ ‘ 𝐶 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ∈ ℂ ) ) → ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 𝐴 ) ) ) − ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) − ( ( ∗ ‘ 𝐶 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) ) = ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) − ( ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 𝐴 ) ) − ( ( ∗ ‘ 𝐶 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) ) )
52 41 44 45 50 51 mp4an ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 𝐴 ) ) ) − ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) − ( ( ∗ ‘ 𝐶 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) ) = ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) − ( ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 𝐴 ) ) − ( ( ∗ ‘ 𝐶 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) )
53 38 52 eqtri ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 𝐴 ) ) ) − ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) − ( ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) ) = ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) − ( ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 𝐴 ) ) − ( ( ∗ ‘ 𝐶 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) )
54 5 15 5 3pm3.2i ( 𝐴𝑋 ∧ ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ∈ 𝑋𝐴𝑋 )
55 1 7 3 dipsubdir ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴𝑋 ∧ ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ∈ 𝑋𝐴𝑋 ) ) → ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 𝐴 ) = ( ( 𝐴 𝑃 𝐴 ) − ( ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) 𝑃 𝐴 ) ) )
56 4 54 55 mp2an ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 𝐴 ) = ( ( 𝐴 𝑃 𝐴 ) − ( ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) 𝑃 𝐴 ) )
57 1 2 3 ipidsq ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( 𝐴 𝑃 𝐴 ) = ( ( 𝑁𝐴 ) ↑ 2 ) )
58 12 5 57 mp2an ( 𝐴 𝑃 𝐴 ) = ( ( 𝑁𝐴 ) ↑ 2 )
59 13 6 5 3pm3.2i ( ( ∗ ‘ 𝐶 ) ∈ ℂ ∧ 𝐵𝑋𝐴𝑋 )
60 1 8 3 dipass ( ( 𝑈 ∈ CPreHilOLD ∧ ( ( ∗ ‘ 𝐶 ) ∈ ℂ ∧ 𝐵𝑋𝐴𝑋 ) ) → ( ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) 𝑃 𝐴 ) = ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 𝐴 ) ) )
61 4 59 60 mp2an ( ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) 𝑃 𝐴 ) = ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 𝐴 ) )
62 58 61 oveq12i ( ( 𝐴 𝑃 𝐴 ) − ( ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) 𝑃 𝐴 ) ) = ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 𝐴 ) ) )
63 56 62 eqtri ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 𝐴 ) = ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 𝐴 ) ) )
64 5 15 15 3pm3.2i ( 𝐴𝑋 ∧ ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ∈ 𝑋 ∧ ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ∈ 𝑋 )
65 1 7 3 dipsubdir ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴𝑋 ∧ ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ∈ 𝑋 ∧ ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) = ( ( 𝐴 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) − ( ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) )
66 4 64 65 mp2an ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) = ( ( 𝐴 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) − ( ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) )
67 5 9 6 3pm3.2i ( 𝐴𝑋𝐶 ∈ ℂ ∧ 𝐵𝑋 )
68 1 8 3 dipassr2 ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴𝑋𝐶 ∈ ℂ ∧ 𝐵𝑋 ) ) → ( 𝐴 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) )
69 4 67 68 mp2an ( 𝐴 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) )
70 69 oveq1i ( ( 𝐴 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) − ( ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) = ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) − ( ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) )
71 66 70 eqtri ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) = ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) − ( ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) )
72 63 71 oveq12i ( ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 𝐴 ) − ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) = ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 𝐴 ) ) ) − ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) − ( ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) )
73 13 43 49 subdii ( ( ∗ ‘ 𝐶 ) · ( ( 𝐵 𝑃 𝐴 ) − ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) = ( ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 𝐴 ) ) − ( ( ∗ ‘ 𝐶 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) )
74 73 oveq2i ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) − ( ( ∗ ‘ 𝐶 ) · ( ( 𝐵 𝑃 𝐴 ) − ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) ) = ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) − ( ( ( ∗ ‘ 𝐶 ) · ( 𝐵 𝑃 𝐴 ) ) − ( ( ∗ ‘ 𝐶 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) )
75 53 72 74 3eqtr4i ( ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 𝐴 ) − ( ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) 𝑃 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) = ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) − ( ( ∗ ‘ 𝐶 ) · ( ( 𝐵 𝑃 𝐴 ) − ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) )
76 22 24 75 3eqtr3i ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( ∗ ‘ 𝐶 ) 𝑆 𝐵 ) ) ) ↑ 2 ) = ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) − ( ( ∗ ‘ 𝐶 ) · ( ( 𝐵 𝑃 𝐴 ) − ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) )
77 19 76 breqtri 0 ≤ ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) − ( ( ∗ ‘ 𝐶 ) · ( ( 𝐵 𝑃 𝐴 ) − ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) )
78 43 49 subeq0i ( ( ( 𝐵 𝑃 𝐴 ) − ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) = 0 ↔ ( 𝐵 𝑃 𝐴 ) = ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) )
79 oveq2 ( ( ( 𝐵 𝑃 𝐴 ) − ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) = 0 → ( ( ∗ ‘ 𝐶 ) · ( ( 𝐵 𝑃 𝐴 ) − ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) = ( ( ∗ ‘ 𝐶 ) · 0 ) )
80 13 mul01i ( ( ∗ ‘ 𝐶 ) · 0 ) = 0
81 79 80 eqtrdi ( ( ( 𝐵 𝑃 𝐴 ) − ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) = 0 → ( ( ∗ ‘ 𝐶 ) · ( ( 𝐵 𝑃 𝐴 ) − ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) = 0 )
82 78 81 sylbir ( ( 𝐵 𝑃 𝐴 ) = ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) → ( ( ∗ ‘ 𝐶 ) · ( ( 𝐵 𝑃 𝐴 ) − ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) = 0 )
83 82 oveq2d ( ( 𝐵 𝑃 𝐴 ) = ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) → ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) − ( ( ∗ ‘ 𝐶 ) · ( ( 𝐵 𝑃 𝐴 ) − ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) ) = ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) − 0 ) )
84 39 resqcli ( ( 𝑁𝐴 ) ↑ 2 ) ∈ ℝ
85 84 recni ( ( 𝑁𝐴 ) ↑ 2 ) ∈ ℂ
86 85 45 subcli ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) ∈ ℂ
87 86 subid1i ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) − 0 ) = ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) )
88 83 87 eqtrdi ( ( 𝐵 𝑃 𝐴 ) = ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) → ( ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) − ( ( ∗ ‘ 𝐶 ) · ( ( 𝐵 𝑃 𝐴 ) − ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) ) = ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) )
89 77 88 breqtrid ( ( 𝐵 𝑃 𝐴 ) = ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) → 0 ≤ ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) )
90 84 10 subge0i ( 0 ≤ ( ( ( 𝑁𝐴 ) ↑ 2 ) − ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) ↔ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ≤ ( ( 𝑁𝐴 ) ↑ 2 ) )
91 89 90 sylib ( ( 𝐵 𝑃 𝐴 ) = ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) → ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ≤ ( ( 𝑁𝐴 ) ↑ 2 ) )
92 46 resqcli ( ( 𝑁𝐵 ) ↑ 2 ) ∈ ℝ
93 46 sqge0i 0 ≤ ( ( 𝑁𝐵 ) ↑ 2 )
94 92 93 pm3.2i ( ( ( 𝑁𝐵 ) ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( ( 𝑁𝐵 ) ↑ 2 ) )
95 10 84 94 3pm3.2i ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ ( ( 𝑁𝐴 ) ↑ 2 ) ∈ ℝ ∧ ( ( ( 𝑁𝐵 ) ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( ( 𝑁𝐵 ) ↑ 2 ) ) )
96 lemul1a ( ( ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ ( ( 𝑁𝐴 ) ↑ 2 ) ∈ ℝ ∧ ( ( ( 𝑁𝐵 ) ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ≤ ( ( 𝑁𝐴 ) ↑ 2 ) ) → ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) ≤ ( ( ( 𝑁𝐴 ) ↑ 2 ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) )
97 95 96 mpan ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ≤ ( ( 𝑁𝐴 ) ↑ 2 ) → ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) ≤ ( ( ( 𝑁𝐴 ) ↑ 2 ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) )
98 91 97 syl ( ( 𝐵 𝑃 𝐴 ) = ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) → ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) ≤ ( ( ( 𝑁𝐴 ) ↑ 2 ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) )
99 40 47 sqmuli ( ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) ↑ 2 ) = ( ( ( 𝑁𝐴 ) ↑ 2 ) · ( ( 𝑁𝐵 ) ↑ 2 ) )
100 98 99 breqtrrdi ( ( 𝐵 𝑃 𝐴 ) = ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) → ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) ≤ ( ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) ↑ 2 ) )
101 10 92 mulge0i ( ( 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∧ 0 ≤ ( ( 𝑁𝐵 ) ↑ 2 ) ) → 0 ≤ ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) )
102 11 93 101 mp2an 0 ≤ ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) · ( ( 𝑁𝐵 ) ↑ 2 ) )
103 39 46 remulcli ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) ∈ ℝ
104 103 sqge0i 0 ≤ ( ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) ↑ 2 )
105 10 92 remulcli ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) ∈ ℝ
106 103 resqcli ( ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) ↑ 2 ) ∈ ℝ
107 105 106 sqrtlei ( ( 0 ≤ ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) ∧ 0 ≤ ( ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) ↑ 2 ) ) → ( ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) ≤ ( ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) ↑ 2 ) ↔ ( √ ‘ ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ≤ ( √ ‘ ( ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) ↑ 2 ) ) ) )
108 102 104 107 mp2an ( ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) ≤ ( ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) ↑ 2 ) ↔ ( √ ‘ ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ≤ ( √ ‘ ( ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) ↑ 2 ) ) )
109 100 108 sylib ( ( 𝐵 𝑃 𝐴 ) = ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) → ( √ ‘ ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ≤ ( √ ‘ ( ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) ↑ 2 ) ) )
110 1 3 dipcl ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
111 12 5 6 110 mp3an ( 𝐴 𝑃 𝐵 ) ∈ ℂ
112 9 111 mulcomi ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝐴 𝑃 𝐵 ) · 𝐶 )
113 112 oveq1i ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) = ( ( ( 𝐴 𝑃 𝐵 ) · 𝐶 ) · ( ( 𝑁𝐵 ) ↑ 2 ) )
114 92 recni ( ( 𝑁𝐵 ) ↑ 2 ) ∈ ℂ
115 111 9 114 mulassi ( ( ( 𝐴 𝑃 𝐵 ) · 𝐶 ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) = ( ( 𝐴 𝑃 𝐵 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) )
116 113 115 eqtri ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) = ( ( 𝐴 𝑃 𝐵 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) )
117 116 fveq2i ( √ ‘ ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) = ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) )
118 1 2 nvge0 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → 0 ≤ ( 𝑁𝐴 ) )
119 12 5 118 mp2an 0 ≤ ( 𝑁𝐴 )
120 1 2 nvge0 ( ( 𝑈 ∈ NrmCVec ∧ 𝐵𝑋 ) → 0 ≤ ( 𝑁𝐵 ) )
121 12 6 120 mp2an 0 ≤ ( 𝑁𝐵 )
122 39 46 mulge0i ( ( 0 ≤ ( 𝑁𝐴 ) ∧ 0 ≤ ( 𝑁𝐵 ) ) → 0 ≤ ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) )
123 119 121 122 mp2an 0 ≤ ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) )
124 103 sqrtsqi ( 0 ≤ ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) → ( √ ‘ ( ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) ↑ 2 ) ) = ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) )
125 123 124 ax-mp ( √ ‘ ( ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) ↑ 2 ) ) = ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) )
126 109 117 125 3brtr3g ( ( 𝐵 𝑃 𝐴 ) = ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) → ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( 𝐶 · ( ( 𝑁𝐵 ) ↑ 2 ) ) ) ) ≤ ( ( 𝑁𝐴 ) · ( 𝑁𝐵 ) ) )