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 |
|
oveq2 |
|- ( B = ( 0vec ` U ) -> ( A P B ) = ( A P ( 0vec ` U ) ) ) |
8 |
4
|
phnvi |
|- U e. NrmCVec |
9 |
|
eqid |
|- ( 0vec ` U ) = ( 0vec ` U ) |
10 |
1 9 3
|
dip0r |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( A P ( 0vec ` U ) ) = 0 ) |
11 |
8 5 10
|
mp2an |
|- ( A P ( 0vec ` U ) ) = 0 |
12 |
7 11
|
eqtrdi |
|- ( B = ( 0vec ` U ) -> ( A P B ) = 0 ) |
13 |
12
|
abs00bd |
|- ( B = ( 0vec ` U ) -> ( abs ` ( A P B ) ) = 0 ) |
14 |
1 2
|
nvge0 |
|- ( ( U e. NrmCVec /\ A e. X ) -> 0 <_ ( N ` A ) ) |
15 |
8 5 14
|
mp2an |
|- 0 <_ ( N ` A ) |
16 |
1 2
|
nvge0 |
|- ( ( U e. NrmCVec /\ B e. X ) -> 0 <_ ( N ` B ) ) |
17 |
8 6 16
|
mp2an |
|- 0 <_ ( N ` B ) |
18 |
1 2 8 5
|
nvcli |
|- ( N ` A ) e. RR |
19 |
1 2 8 6
|
nvcli |
|- ( N ` B ) e. RR |
20 |
18 19
|
mulge0i |
|- ( ( 0 <_ ( N ` A ) /\ 0 <_ ( N ` B ) ) -> 0 <_ ( ( N ` A ) x. ( N ` B ) ) ) |
21 |
15 17 20
|
mp2an |
|- 0 <_ ( ( N ` A ) x. ( N ` B ) ) |
22 |
13 21
|
eqbrtrdi |
|- ( B = ( 0vec ` U ) -> ( abs ` ( A P B ) ) <_ ( ( N ` A ) x. ( N ` B ) ) ) |
23 |
1 3
|
dipcl |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) e. CC ) |
24 |
8 5 6 23
|
mp3an |
|- ( A P B ) e. CC |
25 |
|
absval |
|- ( ( A P B ) e. CC -> ( abs ` ( A P B ) ) = ( sqrt ` ( ( A P B ) x. ( * ` ( A P B ) ) ) ) ) |
26 |
24 25
|
ax-mp |
|- ( abs ` ( A P B ) ) = ( sqrt ` ( ( A P B ) x. ( * ` ( A P B ) ) ) ) |
27 |
19
|
recni |
|- ( N ` B ) e. CC |
28 |
27
|
sqeq0i |
|- ( ( ( N ` B ) ^ 2 ) = 0 <-> ( N ` B ) = 0 ) |
29 |
1 9 2
|
nvz |
|- ( ( U e. NrmCVec /\ B e. X ) -> ( ( N ` B ) = 0 <-> B = ( 0vec ` U ) ) ) |
30 |
8 6 29
|
mp2an |
|- ( ( N ` B ) = 0 <-> B = ( 0vec ` U ) ) |
31 |
28 30
|
bitri |
|- ( ( ( N ` B ) ^ 2 ) = 0 <-> B = ( 0vec ` U ) ) |
32 |
31
|
necon3bii |
|- ( ( ( N ` B ) ^ 2 ) =/= 0 <-> B =/= ( 0vec ` U ) ) |
33 |
1 3
|
dipcl |
|- ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( B P A ) e. CC ) |
34 |
8 6 5 33
|
mp3an |
|- ( B P A ) e. CC |
35 |
19
|
resqcli |
|- ( ( N ` B ) ^ 2 ) e. RR |
36 |
35
|
recni |
|- ( ( N ` B ) ^ 2 ) e. CC |
37 |
34 36
|
divcan1zi |
|- ( ( ( N ` B ) ^ 2 ) =/= 0 -> ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( ( N ` B ) ^ 2 ) ) = ( B P A ) ) |
38 |
32 37
|
sylbir |
|- ( B =/= ( 0vec ` U ) -> ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( ( N ` B ) ^ 2 ) ) = ( B P A ) ) |
39 |
1 3
|
dipcj |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( * ` ( A P B ) ) = ( B P A ) ) |
40 |
8 5 6 39
|
mp3an |
|- ( * ` ( A P B ) ) = ( B P A ) |
41 |
38 40
|
eqtr4di |
|- ( B =/= ( 0vec ` U ) -> ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( ( N ` B ) ^ 2 ) ) = ( * ` ( A P B ) ) ) |
42 |
41
|
oveq2d |
|- ( B =/= ( 0vec ` U ) -> ( ( A P B ) x. ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( ( N ` B ) ^ 2 ) ) ) = ( ( A P B ) x. ( * ` ( A P B ) ) ) ) |
43 |
42
|
fveq2d |
|- ( B =/= ( 0vec ` U ) -> ( sqrt ` ( ( A P B ) x. ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( ( N ` B ) ^ 2 ) ) ) ) = ( sqrt ` ( ( A P B ) x. ( * ` ( A P B ) ) ) ) ) |
44 |
26 43
|
eqtr4id |
|- ( B =/= ( 0vec ` U ) -> ( abs ` ( A P B ) ) = ( sqrt ` ( ( A P B ) x. ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( ( N ` B ) ^ 2 ) ) ) ) ) |
45 |
38
|
eqcomd |
|- ( B =/= ( 0vec ` U ) -> ( B P A ) = ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( ( N ` B ) ^ 2 ) ) ) |
46 |
34 36
|
divclzi |
|- ( ( ( N ` B ) ^ 2 ) =/= 0 -> ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) e. CC ) |
47 |
32 46
|
sylbir |
|- ( B =/= ( 0vec ` U ) -> ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) e. CC ) |
48 |
|
div23 |
|- ( ( ( B P A ) e. CC /\ ( A P B ) e. CC /\ ( ( ( N ` B ) ^ 2 ) e. CC /\ ( ( N ` B ) ^ 2 ) =/= 0 ) ) -> ( ( ( B P A ) x. ( A P B ) ) / ( ( N ` B ) ^ 2 ) ) = ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( A P B ) ) ) |
49 |
34 24 48
|
mp3an12 |
|- ( ( ( ( N ` B ) ^ 2 ) e. CC /\ ( ( N ` B ) ^ 2 ) =/= 0 ) -> ( ( ( B P A ) x. ( A P B ) ) / ( ( N ` B ) ^ 2 ) ) = ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( A P B ) ) ) |
50 |
36 49
|
mpan |
|- ( ( ( N ` B ) ^ 2 ) =/= 0 -> ( ( ( B P A ) x. ( A P B ) ) / ( ( N ` B ) ^ 2 ) ) = ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( A P B ) ) ) |
51 |
32 50
|
sylbir |
|- ( B =/= ( 0vec ` U ) -> ( ( ( B P A ) x. ( A P B ) ) / ( ( N ` B ) ^ 2 ) ) = ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( A P B ) ) ) |
52 |
1 3
|
ipipcj |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A P B ) x. ( B P A ) ) = ( ( abs ` ( A P B ) ) ^ 2 ) ) |
53 |
8 5 6 52
|
mp3an |
|- ( ( A P B ) x. ( B P A ) ) = ( ( abs ` ( A P B ) ) ^ 2 ) |
54 |
24 34 53
|
mulcomli |
|- ( ( B P A ) x. ( A P B ) ) = ( ( abs ` ( A P B ) ) ^ 2 ) |
55 |
54
|
oveq1i |
|- ( ( ( B P A ) x. ( A P B ) ) / ( ( N ` B ) ^ 2 ) ) = ( ( ( abs ` ( A P B ) ) ^ 2 ) / ( ( N ` B ) ^ 2 ) ) |
56 |
51 55
|
eqtr3di |
|- ( B =/= ( 0vec ` U ) -> ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( A P B ) ) = ( ( ( abs ` ( A P B ) ) ^ 2 ) / ( ( N ` B ) ^ 2 ) ) ) |
57 |
24
|
abscli |
|- ( abs ` ( A P B ) ) e. RR |
58 |
57
|
resqcli |
|- ( ( abs ` ( A P B ) ) ^ 2 ) e. RR |
59 |
58 35
|
redivclzi |
|- ( ( ( N ` B ) ^ 2 ) =/= 0 -> ( ( ( abs ` ( A P B ) ) ^ 2 ) / ( ( N ` B ) ^ 2 ) ) e. RR ) |
60 |
32 59
|
sylbir |
|- ( B =/= ( 0vec ` U ) -> ( ( ( abs ` ( A P B ) ) ^ 2 ) / ( ( N ` B ) ^ 2 ) ) e. RR ) |
61 |
56 60
|
eqeltrd |
|- ( B =/= ( 0vec ` U ) -> ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( A P B ) ) e. RR ) |
62 |
30
|
necon3bii |
|- ( ( N ` B ) =/= 0 <-> B =/= ( 0vec ` U ) ) |
63 |
19
|
sqgt0i |
|- ( ( N ` B ) =/= 0 -> 0 < ( ( N ` B ) ^ 2 ) ) |
64 |
62 63
|
sylbir |
|- ( B =/= ( 0vec ` U ) -> 0 < ( ( N ` B ) ^ 2 ) ) |
65 |
57
|
sqge0i |
|- 0 <_ ( ( abs ` ( A P B ) ) ^ 2 ) |
66 |
|
divge0 |
|- ( ( ( ( ( abs ` ( A P B ) ) ^ 2 ) e. RR /\ 0 <_ ( ( abs ` ( A P B ) ) ^ 2 ) ) /\ ( ( ( N ` B ) ^ 2 ) e. RR /\ 0 < ( ( N ` B ) ^ 2 ) ) ) -> 0 <_ ( ( ( abs ` ( A P B ) ) ^ 2 ) / ( ( N ` B ) ^ 2 ) ) ) |
67 |
58 65 66
|
mpanl12 |
|- ( ( ( ( N ` B ) ^ 2 ) e. RR /\ 0 < ( ( N ` B ) ^ 2 ) ) -> 0 <_ ( ( ( abs ` ( A P B ) ) ^ 2 ) / ( ( N ` B ) ^ 2 ) ) ) |
68 |
35 64 67
|
sylancr |
|- ( B =/= ( 0vec ` U ) -> 0 <_ ( ( ( abs ` ( A P B ) ) ^ 2 ) / ( ( N ` B ) ^ 2 ) ) ) |
69 |
68 56
|
breqtrrd |
|- ( B =/= ( 0vec ` U ) -> 0 <_ ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( A P B ) ) ) |
70 |
|
eqid |
|- ( -v ` U ) = ( -v ` U ) |
71 |
|
eqid |
|- ( .sOLD ` U ) = ( .sOLD ` U ) |
72 |
1 2 3 4 5 6 70 71
|
siilem2 |
|- ( ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) e. CC /\ ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( A P B ) ) e. RR /\ 0 <_ ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( A P B ) ) ) -> ( ( B P A ) = ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( ( N ` B ) ^ 2 ) ) -> ( sqrt ` ( ( A P B ) x. ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( ( N ` B ) ^ 2 ) ) ) ) <_ ( ( N ` A ) x. ( N ` B ) ) ) ) |
73 |
47 61 69 72
|
syl3anc |
|- ( B =/= ( 0vec ` U ) -> ( ( B P A ) = ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( ( N ` B ) ^ 2 ) ) -> ( sqrt ` ( ( A P B ) x. ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( ( N ` B ) ^ 2 ) ) ) ) <_ ( ( N ` A ) x. ( N ` B ) ) ) ) |
74 |
45 73
|
mpd |
|- ( B =/= ( 0vec ` U ) -> ( sqrt ` ( ( A P B ) x. ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( ( N ` B ) ^ 2 ) ) ) ) <_ ( ( N ` A ) x. ( N ` B ) ) ) |
75 |
44 74
|
eqbrtrd |
|- ( B =/= ( 0vec ` U ) -> ( abs ` ( A P B ) ) <_ ( ( N ` A ) x. ( N ` B ) ) ) |
76 |
22 75
|
pm2.61ine |
|- ( abs ` ( A P B ) ) <_ ( ( N ` A ) x. ( N ` B ) ) |