Theorem nvabs 8297

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 8289	. . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(-u1SB))) = (N` (BG(-u1SA))))
6	5	negeqd 5373	. . . 4 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> -u(N` (AG(-u1SB))) = -u(N` (BG(-u1SA))))
7	1, 2	nvcom 8236	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ (BG(-u1SA)) e. X) -> (AG(BG(-u1SA))) = ((BG(-u1SA))GA))
8	1, 2	nvgcl 8235	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ B e. X /\ (-u1SA) e. X) -> (BG(-u1SA)) e. X)
9		ax1cn 5281	. . . . . . . . . . . . . . 15 |- 1 e. CC
10	9	negcl 5381	. . . . . . . . . . . . . 14 |- -u1 e. CC
11	1, 3	nvscl 8243	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ -u1 e. CC /\ A e. X) -> (-u1SA) e. X)
12	10, 11	mp3an2 906	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ A e. X) -> (-u1SA) e. X)
13	12	3adant2 800	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ B e. X /\ A e. X) -> (-u1SA) e. X)
14	8, 13	syld3an3 872	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ B e. X /\ A e. X) -> (BG(-u1SA)) e. X)
15	14	3com23 841	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (BG(-u1SA)) e. X)
16	7, 15	syld3an3 872	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AG(BG(-u1SA))) = ((BG(-u1SA))GA))
17		simprr 417	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ (A e. X /\ B e. X)) -> B e. X)
18	12	adantrr 397	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ (A e. X /\ B e. X)) -> (-u1SA) e. X)
19		simprl 416	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ (A e. X /\ B e. X)) -> A e. X)
20	17, 18, 19	3jca 821	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ (A e. X /\ B e. X)) -> (B e. X /\ (-u1SA) e. X /\ A e. X))
21	1, 2	nvass 8237	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ (B e. X /\ (-u1SA) e. X /\ A e. X)) -> ((BG(-u1SA))GA) = (BG((-u1SA)GA)))
22	20, 21	syldan 469	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ (A e. X /\ B e. X)) -> ((BG(-u1SA))GA) = (BG((-u1SA)GA)))
23	22	3impb 831	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((BG(-u1SA))GA) = (BG((-u1SA)GA)))
24		eqid 1478	. . . . . . . . . . . . 13 |- (0v` U) = (0v` U)
25	1, 2, 3, 24	nvlinv 8270	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ A e. X) -> ((-u1SA)GA) = (0v` U))
26	25	3adant3 801	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((-u1SA)GA) = (0v` U))
27	26	opreq2d 3982	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (BG((-u1SA)GA)) = (BG(0v` U)))
28	1, 2, 24	nv0rid 8252	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ B e. X) -> (BG(0v` U)) = B)
29	28	3adant2 800	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (BG(0v` U)) = B)
30	23, 27, 29	3eqtrd 1514	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((BG(-u1SA))GA) = B)
31	16, 30	eqtrd 1510	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AG(BG(-u1SA))) = B)
32	31	fveq2d 3734	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(BG(-u1SA)))) = (N` B))
33	1, 2, 4	nvtri 8294	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ (BG(-u1SA)) e. X) -> (N` (AG(BG(-u1SA)))) <_ ((N` A) + (N` (BG(-u1SA)))))
34	33, 15	syld3an3 872	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(BG(-u1SA)))) <_ ((N` A) + (N` (BG(-u1SA)))))
35	32, 34	eqbrtrrd 2642	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` B) <_ ((N` A) + (N` (BG(-u1SA)))))
36		subnegt 5406	. . . . . . 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 8283	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X) -> (N` A) e. RR)
38	37	3adant3 801	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` A) e. RR)
39	38	recnd 5327	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` A) e. CC)
40	1, 4	nvcl 8283	. . . . . . . . 9 |- ((U e. NrmCVec /\ (BG(-u1SA)) e. X) -> (N` (BG(-u1SA))) e. RR)
41		3simp1 790	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> U e. NrmCVec)
42	40, 41, 15	sylanc 473	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (BG(-u1SA))) e. RR)
43	42	recnd 5327	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (BG(-u1SA))) e. CC)
44	36, 39, 43	sylanc 473	. . . . . 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 2646	. . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` B) <_ ((N` A) - -u(N` (BG(-u1SA)))))
46		lesubt 5648	. . . . . 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 5449	. . . . . . 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 8283	. . . . . . 7 |- ((U e. NrmCVec /\ B e. X) -> (N` B) e. RR)
50	49	3adant2 800	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` B) e. RR)
51	46, 48, 38, 50	syl3anc 860	. . . . 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 2640	. . 3 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> -u(N` (AG(-u1SB))) <_ ((N` A) - (N` B)))
54	1, 2	nvass 8237	. . . . . . . 8 |- ((U e. NrmCVec /\ (A e. X /\ (-u1SB) e. X /\ B e. X)) -> ((AG(-u1SB))GB) = (AG((-u1SB)GB)))
55		3simp2 791	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> A e. X)
56	1, 3	nvscl 8243	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ -u1 e. CC /\ B e. X) -> (-u1SB) e. X)
57	10, 56	mp3an2 906	. . . . . . . . . 10 |- ((U e. NrmCVec /\ B e. X) -> (-u1SB) e. X)
58	57	3adant2 800	. . . . . . . . 9 |- (