This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )