Metamath Proof Explorer


Theorem siilem1

Description: Lemma for sii . (Contributed by NM, 23-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses siii.1
|- X = ( BaseSet ` U )
siii.6
|- N = ( normCV ` U )
siii.7
|- P = ( .iOLD ` U )
siii.9
|- U e. CPreHilOLD
siii.a
|- A e. X
siii.b
|- B e. X
sii1.3
|- M = ( -v ` U )
sii1.4
|- S = ( .sOLD ` U )
sii1.c
|- C e. CC
sii1.r
|- ( C x. ( A P B ) ) e. RR
sii1.z
|- 0 <_ ( C x. ( A P B ) )
Assertion siilem1
|- ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( sqrt ` ( ( A P B ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) <_ ( ( N ` A ) x. ( N ` B ) ) )

Proof

Step Hyp Ref Expression
1 siii.1
 |-  X = ( BaseSet ` U )
2 siii.6
 |-  N = ( normCV ` U )
3 siii.7
 |-  P = ( .iOLD ` U )
4 siii.9
 |-  U e. CPreHilOLD
5 siii.a
 |-  A e. X
6 siii.b
 |-  B e. X
7 sii1.3
 |-  M = ( -v ` U )
8 sii1.4
 |-  S = ( .sOLD ` U )
9 sii1.c
 |-  C e. CC
10 sii1.r
 |-  ( C x. ( A P B ) ) e. RR
11 sii1.z
 |-  0 <_ ( C x. ( A P B ) )
12 4 phnvi
 |-  U e. NrmCVec
13 9 cjcli
 |-  ( * ` C ) e. CC
14 1 8 nvscl
 |-  ( ( U e. NrmCVec /\ ( * ` C ) e. CC /\ B e. X ) -> ( ( * ` C ) S B ) e. X )
15 12 13 6 14 mp3an
 |-  ( ( * ` C ) S B ) e. X
16 1 7 nvmcl
 |-  ( ( U e. NrmCVec /\ A e. X /\ ( ( * ` C ) S B ) e. X ) -> ( A M ( ( * ` C ) S B ) ) e. X )
17 12 5 15 16 mp3an
 |-  ( A M ( ( * ` C ) S B ) ) e. X
18 1 2 12 17 nvcli
 |-  ( N ` ( A M ( ( * ` C ) S B ) ) ) e. RR
19 18 sqge0i
 |-  0 <_ ( ( N ` ( A M ( ( * ` C ) S B ) ) ) ^ 2 )
20 17 5 15 3pm3.2i
 |-  ( ( A M ( ( * ` C ) S B ) ) e. X /\ A e. X /\ ( ( * ` C ) S B ) e. X )
21 1 7 3 dipsubdi
 |-  ( ( U e. CPreHilOLD /\ ( ( A M ( ( * ` C ) S B ) ) e. X /\ A e. X /\ ( ( * ` C ) S B ) e. X ) ) -> ( ( A M ( ( * ` C ) S B ) ) P ( A M ( ( * ` C ) S B ) ) ) = ( ( ( A M ( ( * ` C ) S B ) ) P A ) - ( ( A M ( ( * ` C ) S B ) ) P ( ( * ` C ) S B ) ) ) )
22 4 20 21 mp2an
 |-  ( ( A M ( ( * ` C ) S B ) ) P ( A M ( ( * ` C ) S B ) ) ) = ( ( ( A M ( ( * ` C ) S B ) ) P A ) - ( ( A M ( ( * ` C ) S B ) ) P ( ( * ` C ) S B ) ) )
23 1 2 3 ipidsq
 |-  ( ( U e. NrmCVec /\ ( A M ( ( * ` C ) S B ) ) e. X ) -> ( ( A M ( ( * ` C ) S B ) ) P ( A M ( ( * ` C ) S B ) ) ) = ( ( N ` ( A M ( ( * ` C ) S B ) ) ) ^ 2 ) )
24 12 17 23 mp2an
 |-  ( ( A M ( ( * ` C ) S B ) ) P ( A M ( ( * ` C ) S B ) ) ) = ( ( N ` ( A M ( ( * ` C ) S B ) ) ) ^ 2 )
25 13 6 15 3pm3.2i
 |-  ( ( * ` C ) e. CC /\ B e. X /\ ( ( * ` C ) S B ) e. X )
26 1 8 3 dipass
 |-  ( ( U e. CPreHilOLD /\ ( ( * ` C ) e. CC /\ B e. X /\ ( ( * ` C ) S B ) e. X ) ) -> ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) = ( ( * ` C ) x. ( B P ( ( * ` C ) S B ) ) ) )
27 4 25 26 mp2an
 |-  ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) = ( ( * ` C ) x. ( B P ( ( * ` C ) S B ) ) )
28 6 9 6 3pm3.2i
 |-  ( B e. X /\ C e. CC /\ B e. X )
29 1 8 3 dipassr2
 |-  ( ( U e. CPreHilOLD /\ ( B e. X /\ C e. CC /\ B e. X ) ) -> ( B P ( ( * ` C ) S B ) ) = ( C x. ( B P B ) ) )
30 4 28 29 mp2an
 |-  ( B P ( ( * ` C ) S B ) ) = ( C x. ( B P B ) )
31 1 2 3 ipidsq
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( B P B ) = ( ( N ` B ) ^ 2 ) )
32 12 6 31 mp2an
 |-  ( B P B ) = ( ( N ` B ) ^ 2 )
33 32 oveq2i
 |-  ( C x. ( B P B ) ) = ( C x. ( ( N ` B ) ^ 2 ) )
34 30 33 eqtri
 |-  ( B P ( ( * ` C ) S B ) ) = ( C x. ( ( N ` B ) ^ 2 ) )
35 34 oveq2i
 |-  ( ( * ` C ) x. ( B P ( ( * ` C ) S B ) ) ) = ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) )
36 27 35 eqtri
 |-  ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) = ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) )
37 36 oveq2i
 |-  ( ( C x. ( A P B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) ) = ( ( C x. ( A P B ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) )
38 37 oveq2i
 |-  ( ( ( ( N ` A ) ^ 2 ) - ( ( * ` C ) x. ( B P A ) ) ) - ( ( C x. ( A P B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) ) ) = ( ( ( ( N ` A ) ^ 2 ) - ( ( * ` C ) x. ( B P A ) ) ) - ( ( C x. ( A P B ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) )
39 1 2 12 5 nvcli
 |-  ( N ` A ) e. RR
40 39 recni
 |-  ( N ` A ) e. CC
41 40 sqcli
 |-  ( ( N ` A ) ^ 2 ) e. CC
42 1 3 dipcl
 |-  ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( B P A ) e. CC )
43 12 6 5 42 mp3an
 |-  ( B P A ) e. CC
44 13 43 mulcli
 |-  ( ( * ` C ) x. ( B P A ) ) e. CC
45 10 recni
 |-  ( C x. ( A P B ) ) e. CC
46 1 2 12 6 nvcli
 |-  ( N ` B ) e. RR
47 46 recni
 |-  ( N ` B ) e. CC
48 47 sqcli
 |-  ( ( N ` B ) ^ 2 ) e. CC
49 9 48 mulcli
 |-  ( C x. ( ( N ` B ) ^ 2 ) ) e. CC
50 13 49 mulcli
 |-  ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) e. CC
51 sub4
 |-  ( ( ( ( ( N ` A ) ^ 2 ) e. CC /\ ( ( * ` C ) x. ( B P A ) ) e. CC ) /\ ( ( C x. ( A P B ) ) e. CC /\ ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) e. CC ) ) -> ( ( ( ( N ` A ) ^ 2 ) - ( ( * ` C ) x. ( B P A ) ) ) - ( ( C x. ( A P B ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) ) = ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( ( * ` C ) x. ( B P A ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) ) )
52 41 44 45 50 51 mp4an
 |-  ( ( ( ( N ` A ) ^ 2 ) - ( ( * ` C ) x. ( B P A ) ) ) - ( ( C x. ( A P B ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) ) = ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( ( * ` C ) x. ( B P A ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) )
53 38 52 eqtri
 |-  ( ( ( ( N ` A ) ^ 2 ) - ( ( * ` C ) x. ( B P A ) ) ) - ( ( C x. ( A P B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) ) ) = ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( ( * ` C ) x. ( B P A ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) )
54 5 15 5 3pm3.2i
 |-  ( A e. X /\ ( ( * ` C ) S B ) e. X /\ A e. X )
55 1 7 3 dipsubdir
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ ( ( * ` C ) S B ) e. X /\ A e. X ) ) -> ( ( A M ( ( * ` C ) S B ) ) P A ) = ( ( A P A ) - ( ( ( * ` C ) S B ) P A ) ) )
56 4 54 55 mp2an
 |-  ( ( A M ( ( * ` C ) S B ) ) P A ) = ( ( A P A ) - ( ( ( * ` C ) S B ) P A ) )
57 1 2 3 ipidsq
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( A P A ) = ( ( N ` A ) ^ 2 ) )
58 12 5 57 mp2an
 |-  ( A P A ) = ( ( N ` A ) ^ 2 )
59 13 6 5 3pm3.2i
 |-  ( ( * ` C ) e. CC /\ B e. X /\ A e. X )
60 1 8 3 dipass
 |-  ( ( U e. CPreHilOLD /\ ( ( * ` C ) e. CC /\ B e. X /\ A e. X ) ) -> ( ( ( * ` C ) S B ) P A ) = ( ( * ` C ) x. ( B P A ) ) )
61 4 59 60 mp2an
 |-  ( ( ( * ` C ) S B ) P A ) = ( ( * ` C ) x. ( B P A ) )
62 58 61 oveq12i
 |-  ( ( A P A ) - ( ( ( * ` C ) S B ) P A ) ) = ( ( ( N ` A ) ^ 2 ) - ( ( * ` C ) x. ( B P A ) ) )
63 56 62 eqtri
 |-  ( ( A M ( ( * ` C ) S B ) ) P A ) = ( ( ( N ` A ) ^ 2 ) - ( ( * ` C ) x. ( B P A ) ) )
64 5 15 15 3pm3.2i
 |-  ( A e. X /\ ( ( * ` C ) S B ) e. X /\ ( ( * ` C ) S B ) e. X )
65 1 7 3 dipsubdir
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ ( ( * ` C ) S B ) e. X /\ ( ( * ` C ) S B ) e. X ) ) -> ( ( A M ( ( * ` C ) S B ) ) P ( ( * ` C ) S B ) ) = ( ( A P ( ( * ` C ) S B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) ) )
66 4 64 65 mp2an
 |-  ( ( A M ( ( * ` C ) S B ) ) P ( ( * ` C ) S B ) ) = ( ( A P ( ( * ` C ) S B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) )
67 5 9 6 3pm3.2i
 |-  ( A e. X /\ C e. CC /\ B e. X )
68 1 8 3 dipassr2
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ C e. CC /\ B e. X ) ) -> ( A P ( ( * ` C ) S B ) ) = ( C x. ( A P B ) ) )
69 4 67 68 mp2an
 |-  ( A P ( ( * ` C ) S B ) ) = ( C x. ( A P B ) )
70 69 oveq1i
 |-  ( ( A P ( ( * ` C ) S B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) ) = ( ( C x. ( A P B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) )
71 66 70 eqtri
 |-  ( ( A M ( ( * ` C ) S B ) ) P ( ( * ` C ) S B ) ) = ( ( C x. ( A P B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) )
72 63 71 oveq12i
 |-  ( ( ( A M ( ( * ` C ) S B ) ) P A ) - ( ( A M ( ( * ` C ) S B ) ) P ( ( * ` C ) S B ) ) ) = ( ( ( ( N ` A ) ^ 2 ) - ( ( * ` C ) x. ( B P A ) ) ) - ( ( C x. ( A P B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) ) )
73 13 43 49 subdii
 |-  ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) = ( ( ( * ` C ) x. ( B P A ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) )
74 73 oveq2i
 |-  ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) ) = ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( ( * ` C ) x. ( B P A ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) )
75 53 72 74 3eqtr4i
 |-  ( ( ( A M ( ( * ` C ) S B ) ) P A ) - ( ( A M ( ( * ` C ) S B ) ) P ( ( * ` C ) S B ) ) ) = ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) )
76 22 24 75 3eqtr3i
 |-  ( ( N ` ( A M ( ( * ` C ) S B ) ) ) ^ 2 ) = ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) )
77 19 76 breqtri
 |-  0 <_ ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) )
78 43 49 subeq0i
 |-  ( ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) = 0 <-> ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) )
79 oveq2
 |-  ( ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) = 0 -> ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) = ( ( * ` C ) x. 0 ) )
80 13 mul01i
 |-  ( ( * ` C ) x. 0 ) = 0
81 79 80 eqtrdi
 |-  ( ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) = 0 -> ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) = 0 )
82 78 81 sylbir
 |-  ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) = 0 )
83 82 oveq2d
 |-  ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) ) = ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - 0 ) )
84 39 resqcli
 |-  ( ( N ` A ) ^ 2 ) e. RR
85 84 recni
 |-  ( ( N ` A ) ^ 2 ) e. CC
86 85 45 subcli
 |-  ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) e. CC
87 86 subid1i
 |-  ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - 0 ) = ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) )
88 83 87 eqtrdi
 |-  ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) ) = ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) )
89 77 88 breqtrid
 |-  ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> 0 <_ ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) )
90 84 10 subge0i
 |-  ( 0 <_ ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) <-> ( C x. ( A P B ) ) <_ ( ( N ` A ) ^ 2 ) )
91 89 90 sylib
 |-  ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( C x. ( A P B ) ) <_ ( ( N ` A ) ^ 2 ) )
92 46 resqcli
 |-  ( ( N ` B ) ^ 2 ) e. RR
93 46 sqge0i
 |-  0 <_ ( ( N ` B ) ^ 2 )
94 92 93 pm3.2i
 |-  ( ( ( N ` B ) ^ 2 ) e. RR /\ 0 <_ ( ( N ` B ) ^ 2 ) )
95 10 84 94 3pm3.2i
 |-  ( ( C x. ( A P B ) ) e. RR /\ ( ( N ` A ) ^ 2 ) e. RR /\ ( ( ( N ` B ) ^ 2 ) e. RR /\ 0 <_ ( ( N ` B ) ^ 2 ) ) )
96 lemul1a
 |-  ( ( ( ( C x. ( A P B ) ) e. RR /\ ( ( N ` A ) ^ 2 ) e. RR /\ ( ( ( N ` B ) ^ 2 ) e. RR /\ 0 <_ ( ( N ` B ) ^ 2 ) ) ) /\ ( C x. ( A P B ) ) <_ ( ( N ` A ) ^ 2 ) ) -> ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) <_ ( ( ( N ` A ) ^ 2 ) x. ( ( N ` B ) ^ 2 ) ) )
97 95 96 mpan
 |-  ( ( C x. ( A P B ) ) <_ ( ( N ` A ) ^ 2 ) -> ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) <_ ( ( ( N ` A ) ^ 2 ) x. ( ( N ` B ) ^ 2 ) ) )
98 91 97 syl
 |-  ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) <_ ( ( ( N ` A ) ^ 2 ) x. ( ( N ` B ) ^ 2 ) ) )
99 40 47 sqmuli
 |-  ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) = ( ( ( N ` A ) ^ 2 ) x. ( ( N ` B ) ^ 2 ) )
100 98 99 breqtrrdi
 |-  ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) <_ ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) )
101 10 92 mulge0i
 |-  ( ( 0 <_ ( C x. ( A P B ) ) /\ 0 <_ ( ( N ` B ) ^ 2 ) ) -> 0 <_ ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) )
102 11 93 101 mp2an
 |-  0 <_ ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) )
103 39 46 remulcli
 |-  ( ( N ` A ) x. ( N ` B ) ) e. RR
104 103 sqge0i
 |-  0 <_ ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 )
105 10 92 remulcli
 |-  ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) e. RR
106 103 resqcli
 |-  ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) e. RR
107 105 106 sqrtlei
 |-  ( ( 0 <_ ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) /\ 0 <_ ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) ) -> ( ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) <_ ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) <-> ( sqrt ` ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) ) <_ ( sqrt ` ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) ) ) )
108 102 104 107 mp2an
 |-  ( ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) <_ ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) <-> ( sqrt ` ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) ) <_ ( sqrt ` ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) ) )
109 100 108 sylib
 |-  ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( sqrt ` ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) ) <_ ( sqrt ` ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) ) )
110 1 3 dipcl
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) e. CC )
111 12 5 6 110 mp3an
 |-  ( A P B ) e. CC
112 9 111 mulcomi
 |-  ( C x. ( A P B ) ) = ( ( A P B ) x. C )
113 112 oveq1i
 |-  ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) = ( ( ( A P B ) x. C ) x. ( ( N ` B ) ^ 2 ) )
114 92 recni
 |-  ( ( N ` B ) ^ 2 ) e. CC
115 111 9 114 mulassi
 |-  ( ( ( A P B ) x. C ) x. ( ( N ` B ) ^ 2 ) ) = ( ( A P B ) x. ( C x. ( ( N ` B ) ^ 2 ) ) )
116 113 115 eqtri
 |-  ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) = ( ( A P B ) x. ( C x. ( ( N ` B ) ^ 2 ) ) )
117 116 fveq2i
 |-  ( sqrt ` ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) ) = ( sqrt ` ( ( A P B ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) )
118 1 2 nvge0
 |-  ( ( U e. NrmCVec /\ A e. X ) -> 0 <_ ( N ` A ) )
119 12 5 118 mp2an
 |-  0 <_ ( N ` A )
120 1 2 nvge0
 |-  ( ( U e. NrmCVec /\ B e. X ) -> 0 <_ ( N ` B ) )
121 12 6 120 mp2an
 |-  0 <_ ( N ` B )
122 39 46 mulge0i
 |-  ( ( 0 <_ ( N ` A ) /\ 0 <_ ( N ` B ) ) -> 0 <_ ( ( N ` A ) x. ( N ` B ) ) )
123 119 121 122 mp2an
 |-  0 <_ ( ( N ` A ) x. ( N ` B ) )
124 103 sqrtsqi
 |-  ( 0 <_ ( ( N ` A ) x. ( N ` B ) ) -> ( sqrt ` ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) ) = ( ( N ` A ) x. ( N ` B ) ) )
125 123 124 ax-mp
 |-  ( sqrt ` ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) ) = ( ( N ` A ) x. ( N ` B ) )
126 109 117 125 3brtr3g
 |-  ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( sqrt ` ( ( A P B ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) <_ ( ( N ` A ) x. ( N ` B ) ) )