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 = ⋅ 𝑠OLD ⁡ U
nvabs.6 ⊢ N = norm CV ⁡ U
Assertion nvabs ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ⁡ A − N ⁡ B ≤ N ⁡ A G -1 S B

Proof

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