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