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 1 3 ipipcj 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A P B ) x. ( B P A ) ) = ( ( abs ` ( A P B ) ) ^ 2 ) )
49 8 5 6 48 mp3an 
 |-  ( ( A P B ) x. ( B P A ) ) = ( ( abs ` ( A P B ) ) ^ 2 )
50 24 34 49 mulcomli 
 |-  ( ( B P A ) x. ( A P B ) ) = ( ( abs ` ( A P B ) ) ^ 2 )
51 50 oveq1i 
 |-  ( ( ( B P A ) x. ( A P B ) ) / ( ( N ` B ) ^ 2 ) ) = ( ( ( abs ` ( A P B ) ) ^ 2 ) / ( ( N ` B ) ^ 2 ) )
52 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 ) ) )
53 34 24 52 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 ) ) )
54 36 53 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 ) ) )
55 32 54 sylbir 
 |-  ( B =/= ( 0vec ` U ) -> ( ( ( B P A ) x. ( A P B ) ) / ( ( N ` B ) ^ 2 ) ) = ( ( ( B P A ) / ( ( N ` B ) ^ 2 ) ) x. ( A P B ) ) )
56 51 55 syl5reqr 
 |-  ( 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 ) )