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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvabs.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
nvabs.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
nvabs.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion nvabs ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) )

Proof

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