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 ) ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )