Metamath Proof Explorer


Theorem siii

Description: Inference from sii . (Contributed by NM, 20-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
Assertion siii
|- ( abs ` ( A P B ) ) <_ ( ( 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 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 ) )