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