Metamath Proof Explorer

Theorem nvabs

Description: Norm difference property of a normed complex vector space. Problem 3 of Kreyszig p. 64. (Contributed by NM, 4-Dec-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nvabs.1 
|- X = ( BaseSet ` U )
nvabs.2 
|- G = ( +v ` U )
nvabs.4 
|- S = ( .sOLD ` U )
nvabs.6 
|- N = ( normCV ` U )
Assertion nvabs 
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( abs ` ( ( N ` A ) - ( N ` B ) ) ) <_ ( N ` ( A G ( -u 1 S B ) ) ) )

Proof

Step Hyp Ref Expression
1 nvabs.1 
 |-  X = ( BaseSet ` U )
2 nvabs.2 
 |-  G = ( +v ` U )
3 nvabs.4 
 |-  S = ( .sOLD ` U )
4 nvabs.6 
 |-  N = ( normCV ` U )
5 1 2 3 4 nvdif 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G ( -u 1 S B ) ) ) = ( N ` ( B G ( -u 1 S A ) ) ) )
6 5 negeqd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> -u ( N ` ( A G ( -u 1 S B ) ) ) = -u ( N ` ( B G ( -u 1 S A ) ) ) )
7 1 4 nvcl 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( N ` B ) e. RR )
8 7 3adant2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` B ) e. RR )
9 1 4 nvcl 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) e. RR )
10 9 3adant3 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` A ) e. RR )
11 simp1 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> U e. NrmCVec )
12 neg1cn 
 |-  -u 1 e. CC
13 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ A e. X ) -> ( -u 1 S A ) e. X )
14 12 13 mp3an2 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( -u 1 S A ) e. X )
15 14 3adant2 
 |-  ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( -u 1 S A ) e. X )
16 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ B e. X /\ ( -u 1 S A ) e. X ) -> ( B G ( -u 1 S A ) ) e. X )
17 15 16 syld3an3 
 |-  ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( B G ( -u 1 S A ) ) e. X )
18 17 3com23 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( B G ( -u 1 S A ) ) e. X )
19 1 4 nvcl 
 |-  ( ( U e. NrmCVec /\ ( B G ( -u 1 S A ) ) e. X ) -> ( N ` ( B G ( -u 1 S A ) ) ) e. RR )
20 11 18 19 syl2anc 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( B G ( -u 1 S A ) ) ) e. RR )
21 20 renegcld 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> -u ( N ` ( B G ( -u 1 S A ) ) ) e. RR )
22 1 2 nvcom 
 |-  ( ( U e. NrmCVec /\ A e. X /\ ( B G ( -u 1 S A ) ) e. X ) -> ( A G ( B G ( -u 1 S A ) ) ) = ( ( B G ( -u 1 S A ) ) G A ) )
23 18 22 syld3an3 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( B G ( -u 1 S A ) ) ) = ( ( B G ( -u 1 S A ) ) G A ) )
24 simprr 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> B e. X )
25 14 adantrr 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( -u 1 S A ) e. X )
26 simprl 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> A e. X )
27 24 25 26 3jca 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( B e. X /\ ( -u 1 S A ) e. X /\ A e. X ) )
28 1 2 nvass 
 |-  ( ( U e. NrmCVec /\ ( B e. X /\ ( -u 1 S A ) e. X /\ A e. X ) ) -> ( ( B G ( -u 1 S A ) ) G A ) = ( B G ( ( -u 1 S A ) G A ) ) )
29 27 28 syldan 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( ( B G ( -u 1 S A ) ) G A ) = ( B G ( ( -u 1 S A ) G A ) ) )
30 29 3impb 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( B G ( -u 1 S A ) ) G A ) = ( B G ( ( -u 1 S A ) G A ) ) )
31 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
32 1 2 3 31 nvlinv 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( ( -u 1 S A ) G A ) = ( 0vec ` U ) )
33 32 3adant3 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( -u 1 S A ) G A ) = ( 0vec ` U ) )
34 33 oveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( B G ( ( -u 1 S A ) G A ) ) = ( B G ( 0vec ` U ) ) )
35 1 2 31 nv0rid 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( B G ( 0vec ` U ) ) = B )
36 35 3adant2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( B G ( 0vec ` U ) ) = B )
37 30 34 36 3eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( B G ( -u 1 S A ) ) G A ) = B )
38 23 37 eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( B G ( -u 1 S A ) ) ) = B )
39 38 fveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G ( B G ( -u 1 S A ) ) ) ) = ( N ` B ) )
40 1 2 4 nvtri 
 |-  ( ( U e. NrmCVec /\ A e. X /\ ( B G ( -u 1 S A ) ) e. X ) -> ( N ` ( A G ( B G ( -u 1 S A ) ) ) ) <_ ( ( N ` A ) + ( N ` ( B G ( -u 1 S A ) ) ) ) )
41 18 40 syld3an3 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G ( B G ( -u 1 S A ) ) ) ) <_ ( ( N ` A ) + ( N ` ( B G ( -u 1 S A ) ) ) ) )
42 39 41 eqbrtrrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` B ) <_ ( ( N ` A ) + ( N ` ( B G ( -u 1 S A ) ) ) ) )
43 10 recnd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` A ) e. CC )
44 20 recnd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( B G ( -u 1 S A ) ) ) e. CC )
45 43 44 subnegd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` A ) - -u ( N ` ( B G ( -u 1 S A ) ) ) ) = ( ( N ` A ) + ( N ` ( B G ( -u 1 S A ) ) ) ) )
46 42 45 breqtrrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` B ) <_ ( ( N ` A ) - -u ( N ` ( B G ( -u 1 S A ) ) ) ) )
47 8 10 21 46 lesubd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> -u ( N ` ( B G ( -u 1 S A ) ) ) <_ ( ( N ` A ) - ( N ` B ) ) )
48 6 47 eqbrtrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> -u ( N ` ( A G ( -u 1 S B ) ) ) <_ ( ( N ` A ) - ( N ` B ) ) )
49 simp2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> A e. X )
50 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ B e. X ) -> ( -u 1 S B ) e. X )
51 12 50 mp3an2 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( -u 1 S B ) e. X )
52 51 3adant2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( -u 1 S B ) e. X )
53 simp3 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> B e. X )
54 1 2 nvass 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ ( -u 1 S B ) e. X /\ B e. X ) ) -> ( ( A G ( -u 1 S B ) ) G B ) = ( A G ( ( -u 1 S B ) G B ) ) )
55 11 49 52 53 54 syl13anc 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A G ( -u 1 S B ) ) G B ) = ( A G ( ( -u 1 S B ) G B ) ) )
56 1 2 3 31 nvlinv 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( ( -u 1 S B ) G B ) = ( 0vec ` U ) )
57 56 3adant2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( -u 1 S B ) G B ) = ( 0vec ` U ) )
58 57 oveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( ( -u 1 S B ) G B ) ) = ( A G ( 0vec ` U ) ) )
59 1 2 31 nv0rid 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( A G ( 0vec ` U ) ) = A )
60 59 3adant3 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( 0vec ` U ) ) = A )
61 55 58 60 3eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A G ( -u 1 S B ) ) G B ) = A )
62 61 fveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( ( A G ( -u 1 S B ) ) G B ) ) = ( N ` A ) )
63 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ ( -u 1 S B ) e. X ) -> ( A G ( -u 1 S B ) ) e. X )
64 52 63 syld3an3 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( -u 1 S B ) ) e. X )
65 1 2 4 nvtri 
 |-  ( ( U e. NrmCVec /\ ( A G ( -u 1 S B ) ) e. X /\ B e. X ) -> ( N ` ( ( A G ( -u 1 S B ) ) G B ) ) <_ ( ( N ` ( A G ( -u 1 S B ) ) ) + ( N ` B ) ) )
66 64 65 syld3an2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( ( A G ( -u 1 S B ) ) G B ) ) <_ ( ( N ` ( A G ( -u 1 S B ) ) ) + ( N ` B ) ) )
67 62 66 eqbrtrrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` A ) <_ ( ( N ` ( A G ( -u 1 S B ) ) ) + ( N ` B ) ) )
68 1 4 nvcl 
 |-  ( ( U e. NrmCVec /\ ( A G ( -u 1 S B ) ) e. X ) -> ( N ` ( A G ( -u 1 S B ) ) ) e. RR )
69 11 64 68 syl2anc 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G ( -u 1 S B ) ) ) e. RR )
70 10 8 69 lesubaddd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( N ` A ) - ( N ` B ) ) <_ ( N ` ( A G ( -u 1 S B ) ) ) <-> ( N ` A ) <_ ( ( N ` ( A G ( -u 1 S B ) ) ) + ( N ` B ) ) ) )
71 67 70 mpbird 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` A ) - ( N ` B ) ) <_ ( N ` ( A G ( -u 1 S B ) ) ) )
72 10 8 resubcld 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` A ) - ( N ` B ) ) e. RR )
73 72 69 absled 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( abs ` ( ( N ` A ) - ( N ` B ) ) ) <_ ( N ` ( A G ( -u 1 S B ) ) ) <-> ( -u ( N ` ( A G ( -u 1 S B ) ) ) <_ ( ( N ` A ) - ( N ` B ) ) /\ ( ( N ` A ) - ( N ` B ) ) <_ ( N ` ( A G ( -u 1 S B ) ) ) ) ) )
74 48 71 73 mpbir2and 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( abs ` ( ( N ` A ) - ( N ` B ) ) ) <_ ( N ` ( A G ( -u 1 S B ) ) ) )