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 = \cdot_{𝑠OLD} (U)$
	nvabs.6	$⊢ N = {norm}_{CV} (U)$
Assertion	nvabs	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to \|N (A) - N (B)\| \leq 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 = \cdot_{𝑠OLD} (U)$
4		nvabs.6	$⊢ N = {norm}_{CV} (U)$
5	1 2 3 4	nvdif	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A G (-1 S B)) = N (B G (-1 S A))$
6	5	negeqd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to - N (A G (-1 S B)) = - N (B G (-1 S A))$
7	1 4	nvcl	$⊢ (U \in NrmCVec \land B \in X) \to N (B) \in ℝ$
8	7	3adant2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (B) \in ℝ$
9	1 4	nvcl	$⊢ (U \in NrmCVec \land A \in X) \to N (A) \in ℝ$
10	9	3adant3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A) \in ℝ$
11		simp1	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to U \in NrmCVec$
12		neg1cn	$⊢ - 1 \in ℂ$
13	1 3	nvscl	$⊢ (U \in NrmCVec \land - 1 \in ℂ \land A \in X) \to -1 S A \in X$
14	12 13	mp3an2	$⊢ (U \in NrmCVec \land A \in X) \to -1 S A \in X$
15	14	3adant2	$⊢ (U \in NrmCVec \land B \in X \land A \in X) \to -1 S A \in X$
16	1 2	nvgcl	$⊢ (U \in NrmCVec \land B \in X \land -1 S A \in X) \to B G (-1 S A) \in X$
17	15 16	syld3an3	$⊢ (U \in NrmCVec \land B \in X \land A \in X) \to B G (-1 S A) \in X$
18	17	3com23	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to B G (-1 S A) \in X$
19	1 4	nvcl	$⊢ (U \in NrmCVec \land B G (-1 S A) \in X) \to N (B G (-1 S A)) \in ℝ$
20	11 18 19	syl2anc	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (B G (-1 S A)) \in ℝ$
21	20	renegcld	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to - N (B G (-1 S A)) \in ℝ$
22	1 2	nvcom	$⊢ (U \in NrmCVec \land A \in X \land B G (-1 S A) \in X) \to A G (B G (-1 S A)) = (B G (-1 S A)) G A$
23	18 22	syld3an3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A G (B G (-1 S A)) = (B G (-1 S A)) G A$
24		simprr	$⊢ (U \in NrmCVec \land (A \in X \land B \in X)) \to B \in X$
25	14	adantrr	$⊢ (U \in NrmCVec \land (A \in X \land B \in X)) \to -1 S A \in X$
26		simprl	$⊢ (U \in NrmCVec \land (A \in X \land B \in X)) \to A \in X$
27	24 25 26	3jca	$⊢ (U \in NrmCVec \land (A \in X \land B \in X)) \to (B \in X \land -1 S A \in X \land A \in X)$
28	1 2	nvass	$⊢ (U \in NrmCVec \land (B \in X \land -1 S A \in X \land A \in X)) \to (B G (-1 S A)) G A = B G ((-1 S A) G A)$
29	27 28	syldan	$⊢ (U \in NrmCVec \land (A \in X \land B \in X)) \to (B G (-1 S A)) G A = B G ((-1 S A) G A)$
30	29	3impb	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (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 \in NrmCVec \land A \in X) \to (-1 S A) G A = 0_{vec} (U)$
33	32	3adant3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (-1 S A) G A = 0_{vec} (U)$
34	33	oveq2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to B G ((-1 S A) G A) = B G 0_{vec} (U)$
35	1 2 31	nv0rid	$⊢ (U \in NrmCVec \land B \in X) \to B G 0_{vec} (U) = B$
36	35	3adant2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to B G 0_{vec} (U) = B$
37	30 34 36	3eqtrd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (B G (-1 S A)) G A = B$
38	23 37	eqtrd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A G (B G (-1 S A)) = B$
39	38	fveq2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A G (B G (-1 S A))) = N (B)$
40	1 2 4	nvtri	$⊢ (U \in NrmCVec \land A \in X \land B G (-1 S A) \in X) \to N (A G (B G (-1 S A))) \leq N (A) + N (B G (-1 S A))$
41	18 40	syld3an3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A G (B G (-1 S A))) \leq N (A) + N (B G (-1 S A))$
42	39 41	eqbrtrrd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (B) \leq N (A) + N (B G (-1 S A))$
43	10	recnd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A) \in ℂ$
44	20	recnd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (B G (-1 S A)) \in ℂ$
45	43 44	subnegd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A) - (- N (B G (-1 S A))) = N (A) + N (B G (-1 S A))$
46	42 45	breqtrrd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (B) \leq N (A) - (- N (B G (-1 S A)))$
47	8 10 21 46	lesubd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to - N (B G (-1 S A)) \leq N (A) - N (B)$
48	6 47	eqbrtrd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to - N (A G (-1 S B)) \leq N (A) - N (B)$
49		simp2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A \in X$
50	1 3	nvscl	$⊢ (U \in NrmCVec \land - 1 \in ℂ \land B \in X) \to -1 S B \in X$
51	12 50	mp3an2	$⊢ (U \in NrmCVec \land B \in X) \to -1 S B \in X$
52	51	3adant2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to -1 S B \in X$
53		simp3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to B \in X$
54	1 2	nvass	$⊢ (U \in NrmCVec \land (A \in X \land -1 S B \in X \land B \in X)) \to (A G (-1 S B)) G B = A G ((-1 S B) G B)$
55	11 49 52 53 54	syl13anc	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (A G (-1 S B)) G B = A G ((-1 S B) G B)$
56	1 2 3 31	nvlinv	$⊢ (U \in NrmCVec \land B \in X) \to (-1 S B) G B = 0_{vec} (U)$
57	56	3adant2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (-1 S B) G B = 0_{vec} (U)$
58	57	oveq2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A G ((-1 S B) G B) = A G 0_{vec} (U)$
59	1 2 31	nv0rid	$⊢ (U \in NrmCVec \land A \in X) \to A G 0_{vec} (U) = A$
60	59	3adant3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A G 0_{vec} (U) = A$
61	55 58 60	3eqtrd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (A G (-1 S B)) G B = A$
62	61	fveq2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N ((A G (-1 S B)) G B) = N (A)$
63	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land -1 S B \in X) \to A G (-1 S B) \in X$
64	52 63	syld3an3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A G (-1 S B) \in X$
65	1 2 4	nvtri	$⊢ (U \in NrmCVec \land A G (-1 S B) \in X \land B \in X) \to N ((A G (-1 S B)) G B) \leq N (A G (-1 S B)) + N (B)$
66	64 65	syld3an2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N ((A G (-1 S B)) G B) \leq N (A G (-1 S B)) + N (B)$
67	62 66	eqbrtrrd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A) \leq N (A G (-1 S B)) + N (B)$
68	1 4	nvcl	$⊢ (U \in NrmCVec \land A G (-1 S B) \in X) \to N (A G (-1 S B)) \in ℝ$
69	11 64 68	syl2anc	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A G (-1 S B)) \in ℝ$
70	10 8 69	lesubaddd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (N (A) - N (B) \leq N (A G (-1 S B)) \leftrightarrow N (A) \leq N (A G (-1 S B)) + N (B))$
71	67 70	mpbird	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A) - N (B) \leq N (A G (-1 S B))$
72	10 8	resubcld	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A) - N (B) \in ℝ$
73	72 69	absled	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (\|N (A) - N (B)\| \leq N (A G (-1 S B)) \leftrightarrow (- N (A G (-1 S B)) \leq N (A) - N (B) \land N (A) - N (B) \leq N (A G (-1 S B))))$
74	48 71 73	mpbir2and	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to \|N (A) - N (B)\| \leq N (A G (-1 S B))$

Metamath Proof Explorer

Theorem nvabs

Proof