Theorem nvabs 8301

Description: Norm difference property of a normed complex vector space. Problem 3 of [Kreyszig] p. 64.

Hypotheses

Ref	Expression
nvabs.1	|- X = (Base` U)
nvabs.2	|- G = (+v` U)
nvabs.4	|- S = (.s` U)
nvabs.6	|- N = (norm` U)

Assertion

Ref	Expression
nvabs	|- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (abs` ((N` A) - (N` B))) <_ (N` (AG(-u1SB))))

Proof of Theorem nvabs

Step	Hyp	Ref	Expression
1		nvabs.1	. . . . . 6 |- X = (Base` U)
2		nvabs.2	. . . . . 6 |- G = (+v` U)
3		nvabs.4	. . . . . 6 |- S = (.s` U)
4		nvabs.6	. . . . . 6 |- N = (norm` U)
5	1, 2, 3, 4	nvdif 8293	. . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(-u1SB))) = (N` (BG(-u1SA))))
6	5	negeqd 5361	. . . 4 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> -u(N` (AG(-u1SB))) = -u(N` (BG(-u1SA))))
7	1, 2	nvcom 8240	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ (BG(-u1SA)) e. X) -> (AG(BG(-u1SA))) = ((BG(-u1SA))GA))
8	1, 2	nvgcl 8239	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ B e. X /\ (-u1SA) e. X) -> (BG(-u1SA)) e. X)
9		ax1cn 5269	. . . . . . . . . . . . . . 15 |- 1 e. CC
10	9	negcl 5369	. . . . . . . . . . . . . 14 |- -u1 e. CC
11	1, 3	nvscl 8247	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ -u1 e. CC /\ A e. X) -> (-u1SA) e. X)
12	10, 11	mp3an2 904	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ A e. X) -> (-u1SA) e. X)
13	12	3adant2 798	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ B e. X /\ A e. X) -> (-u1SA) e. X)
14	8, 13	syld3an3 870	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ B e. X /\ A e. X) -> (BG(-u1SA)) e. X)
15	14	3com23 839	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (BG(-u1SA)) e. X)
16	7, 15	syld3an3 870	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AG(BG(-u1SA))) = ((BG(-u1SA))GA))
17		simprr 415	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ (A e. X /\ B e. X)) -> B e. X)
18	12	adantrr 395	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ (A e. X /\ B e. X)) -> (-u1SA) e. X)
19		simprl 414	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ (A e. X /\ B e. X)) -> A e. X)
20	17, 18, 19	3jca 819	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ (A e. X /\ B e. X)) -> (B e. X /\ (-u1SA) e. X /\ A e. X))
21	1, 2	nvass 8241	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ (B e. X /\ (-u1SA) e. X /\ A e. X)) -> ((BG(-u1SA))GA) = (BG((-u1SA)GA)))
22	20, 21	syldan 467	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ (A e. X /\ B e. X)) -> ((BG(-u1SA))GA) = (BG((-u1SA)GA)))
23	22	3impb 829	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((BG(-u1SA))GA) = (BG((-u1SA)GA)))
24		eqid 1475	. . . . . . . . . . . . 13 |- (0v` U) = (0v` U)
25	1, 2, 3, 24	nvlinv 8274	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ A e. X) -> ((-u1SA)GA) = (0v` U))
26	25	3adant3 799	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((-u1SA)GA) = (0v` U))
27	26	opreq2d 3976	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (BG((-u1SA)GA)) = (BG(0v` U)))
28	1, 2, 24	nv0rid 8256	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ B e. X) -> (BG(0v` U)) = B)
29	28	3adant2 798	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (BG(0v` U)) = B)
30	23, 27, 29	3eqtrd 1511	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((BG(-u1SA))GA) = B)
31	16, 30	eqtrd 1507	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AG(BG(-u1SA))) = B)
32	31	fveq2d 3728	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(BG(-u1SA)))) = (N` B))
33	1, 2, 4	nvtri 8298	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ (BG(-u1SA)) e. X) -> (N` (AG(BG(-u1SA)))) <_ ((N` A) + (N` (BG(-u1SA)))))
34	33, 15	syld3an3 870	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(BG(-u1SA)))) <_ ((N` A) + (N` (BG(-u1SA)))))
35	32, 34	eqbrtrrd 2637	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` B) <_ ((N` A) + (N` (BG(-u1SA)))))
36		subnegt 5394	. . . . . . 7 |- (((N` A) e. CC /\ (N` (BG(-u1SA))) e. CC) -> ((N` A) - -u(N` (BG(-u1SA)))) = ((N` A) + (N` (BG(-u1SA)))))
37	1, 4	nvcl 8287	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X) -> (N` A) e. RR)
38	37	3adant3 799	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` A) e. RR)
39	38	recnd 5315	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` A) e. CC)
40	1, 4	nvcl 8287	. . . . . . . . 9 |- ((U e. NrmCVec /\ (BG(-u1SA)) e. X) -> (N` (BG(-u1SA))) e. RR)
41		3simp1 788	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> U e. NrmCVec)
42	40, 41, 15	sylanc 471	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (BG(-u1SA))) e. RR)
43	42	recnd 5315	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (BG(-u1SA))) e. CC)
44	36, 39, 43	sylanc 471	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` A) - -u(N` (BG(-u1SA)))) = ((N` A) + (N` (BG(-u1SA)))))
45	35, 44	breqtrrd 2641	. . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` B) <_ ((N` A) - -u(N` (BG(-u1SA)))))
46		lesubt 5636	. . . . . 6 |- ((-u(N` (BG(-u1SA))) e. RR /\ (N` A) e. RR /\ (N` B) e. RR) -> (-u(N` (BG(-u1SA))) <_ ((N` A) - (N` B)) <-> (N` B) <_ ((N` A) - -u(N` (BG(-u1SA))))))
47		renegclt 5437	. . . . . . 7 |- ((N` (BG(-u1SA))) e. RR -> -u(N` (BG(-u1SA))) e. RR)
48	42, 47	syl 10	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> -u(N` (BG(-u1SA))) e. RR)
49	1, 4	nvcl 8287	. . . . . . 7 |- ((U e. NrmCVec /\ B e. X) -> (N` B) e. RR)
50	49	3adant2 798	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` B) e. RR)
51	46, 48, 38, 50	syl3anc 858	. . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (-u(N` (BG(-u1SA))) <_ ((N` A) - (N` B)) <-> (N` B) <_ ((N` A) - -u(N` (BG(-u1SA))))))
52	45, 51	mpbird 196	. . . 4 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> -u(N` (BG(-u1SA))) <_ ((N` A) - (N` B)))
53	6, 52	eqbrtrd 2635	. . 3 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> -u(N` (AG(-u1SB))) <_ ((N` A) - (N` B)))
54	1, 2	nvass 8241	. . . . . . . 8 |- ((U e. NrmCVec /\ (A e. X /\ (-u1SB) e. X /\ B e. X)) -> ((AG(-u1SB))GB) = (AG((-u1SB)GB)))
55		3simp2 789	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> A e. X)
56	1, 3	nvscl 8247	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ -u1 e. CC /\ B e. X) -> (-u1SB) e. X)
57	10, 56	mp3an2 904	. . . . . . . . . 10 |- ((U e. NrmCVec /\ B e. X) -> (-u1SB) e. X)
58	57	3adant2 798	. . . . . . . . 9 |- (