Theorem nvi 8229

Description: The properties of a normed complex vector space, which is a vector space accompanied by a norm.

Hypotheses

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

Assertion

Ref	Expression
nvi	|- (U e. NrmCVec -> (<.G, S>. e. CVec /\ N:X-->RR /\ A.x e. X (((N` x) = 0 -> x = Z) /\ A.y e. CC (N` (ySx)) = ((abs` y) x. (N` x)) /\ A.y e. X (N` (xGy)) <_ ((N` x) + (N` y)))))

Distinct variable groups:   x,y,G   x,N,y   x,S,y   x,X,y   x,Z

Proof of Theorem nvi

Step	Hyp	Ref	Expression
1		df-nv 8207	. . 3 |- NrmCVec = {<.<.g, s>., n>. | (<.g, s>. e. CVec /\ n:ran g-->RR /\ A.x e. ran g(((n` x) = 0 -> x = (Id` g)) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. ran g(n` (xgy)) <_ ((n` x) + (n` y))))}
2	1	eleq2i 1541	. 2 |- (U e. NrmCVec <-> U e. {<.<.g, s>., n>. | (<.g, s>. e. CVec /\ n:ran g-->RR /\ A.x e. ran g(((n` x) = 0 -> x = (Id` g)) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. ran g(n` (xgy)) <_ ((n` x) + (n` y))))})
3		id 59	. . . . 5 |- (g = (1st` (1st` U)) -> g = (1st` (1st` U)))
4		nvi.2	. . . . . 6 |- G = (+v` U)
5	4	vafval 8218	. . . . 5 |- G = (1st` (1st` U))
6	3, 5	syl6eqr 1528	. . . 4 |- (g = (1st` (1st` U)) -> g = G)
7		opeq1 2491	. . . . . 6 |- (g = G -> <.g, s>. = <.G, s>.)
8	7	eleq1d 1543	. . . . 5 |- (g = G -> (<.g, s>. e. CVec <-> <.G, s>. e. CVec))
9		rneq 3345	. . . . . . 7 |- (g = G -> ran g = ran G)
10		nvi.1	. . . . . . . 8 |- X = (Base` U)
11	10, 4	bafval 8219	. . . . . . 7 |- X = ran G
12	9, 11	syl6eqr 1528	. . . . . 6 |- (g = G -> ran g = X)
13		feq2 3627	. . . . . 6 |- (ran g = X -> (n:ran g-->RR <-> n:X-->RR))
14	12, 13	syl 10	. . . . 5 |- (g = G -> (n:ran g-->RR <-> n:X-->RR))
15		fveq2 3730	. . . . . . . . . 10 |- (g = G -> (Id` g) = (Id` G))
16		nvi.5	. . . . . . . . . . 11 |- Z = (0v` U)
17	4, 16	0vfval 8221	. . . . . . . . . 10 |- Z = (Id` G)
18	15, 17	syl6eqr 1528	. . . . . . . . 9 |- (g = G -> (Id` g) = Z)
19	18	eqeq2d 1489	. . . . . . . 8 |- (g = G -> (x = (Id` g) <-> x = Z))
20	19	imbi2d 614	. . . . . . 7 |- (g = G -> (((n` x) = 0 -> x = (Id` g)) <-> ((n` x) = 0 -> x = Z)))
21		opreq 3973	. . . . . . . . . 10 |- (g = G -> (xgy) = (xGy))
22	21	fveq2d 3734	. . . . . . . . 9 |- (g = G -> (n` (xgy)) = (n` (xGy)))
23	22	breq1d 2634	. . . . . . . 8 |- (g = G -> ((n` (xgy)) <_ ((n` x) + (n` y)) <-> (n` (xGy)) <_ ((n` x) + (n` y))))
24	12, 23	raleq12d 1797	. . . . . . 7 |- (g = G -> (A.y e. ran g(n` (xgy)) <_ ((n` x) + (n` y)) <-> A.y e. X (n` (xGy)) <_ ((n` x) + (n` y))))
25	20, 24	3anbi13d 897	. . . . . 6 |- (g = G -> ((((n` x) = 0 -> x = (Id` g)) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. ran g(n` (xgy)) <_ ((n` x) + (n` y))) <-> (((n` x) = 0 -> x = Z) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. X (n` (xGy)) <_ ((n` x) + (n` y)))))
26	12, 25	raleq12d 1797	. . . . 5 |- (g = G -> (A.x e. ran g(((n` x) = 0 -> x = (Id` g)) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. ran g(n` (xgy)) <_ ((n` x) + (n` y))) <-> A.x e. X (((n` x) = 0 -> x = Z) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. X (n` (xGy)) <_ ((n` x) + (n` y)))))
27	8, 14, 26	3anbi123d 895	. . . 4 |- (g = G -> ((<.g, s>. e. CVec /\ n:ran g-->RR /\ A.x e. ran g(((n` x) = 0 -> x = (Id` g)) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. ran g(n` (xgy)) <_ ((n` x) + (n` y)))) <-> (<.G, s>. e. CVec /\ n:X-->RR /\ A.x e. X (((n` x) = 0 -> x = Z) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. X (n` (xGy)) <_ ((n` x) + (n` y))))))
28	6, 27	syl 10	. . 3 |- (g = (1st` (1st` U)) -> ((<.g, s>. e. CVec /\ n:ran g-->RR /\ A.x e. ran g(((n` x) = 0 -> x = (Id` g)) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. ran g(n` (xgy)) <_ ((n` x) + (n` y)))) <-> (<.G, s>. e. CVec /\ n:X-->RR /\ A.x e. X (((n` x) = 0 -> x = Z) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. X (n` (xGy)) <_ ((n` x) + (n` y))))))
29		id 59	. . . . 5 |- (s = (2nd` (1st` U)) -> s = (2nd` (1st` U)))
30		nvi.4	. . . . . 6 |- S = (.s` U)
31	30	smfval 8220	. . . . 5 |- S = (2nd` (1st` U))
32	29, 31	syl6eqr 1528	. . . 4 |- (s = (2nd` (1st` U)) -> s = S)
33		opeq2 2492	. . . . . 6 |- (s = S -> <.G, s>. = <.G, S>.)
34	33	eleq1d 1543	. . . . 5 |- (s = S -> (<.G, s>. e. CVec <-> <.G, S>. e. CVec))
35		opreq 3973	. . . . . . . . . 10 |- (s = S -> (ysx) = (ySx))
36	35	fveq2d 3734	. . . . . . . . 9 |- (s = S -> (n` (ysx)) = (n` (ySx)))
37	36	eqeq1d 1486	. . . . . . . 8 |- (s = S -> ((n` (ysx)) = ((abs` y) x. (n` x)) <-> (n` (ySx)) = ((abs` y) x. (n` x))))
38	37	ralbidv 1666	. . . . . . 7 |- (s = S -> (A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) <-> A.y e. CC (n` (ySx)) = ((abs` y) x. (n` x))))
39	38	3anbi2d 900	. . . . . 6 |- (s = S -> ((((n` x) = 0 -> x = Z) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. X (n` (xGy)) <_ ((n` x) + (n` y))) <-> (((n` x) = 0 -> x = Z) /\ A.y e. CC (n` (ySx)) = ((abs` y) x. (n` x)) /\ A.y e. X (n` (xGy)) <_ ((n` x) + (n` y)))))
40	39	ralbidv 1666	. . . . 5 |- (s = S -> (A.x e. X (((n` x) = 0 -> x = Z) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. X (n` (xGy)) <_ ((n` x) + (n` y))) <-> A.x e. X (((n` x) = 0 -> x = Z) /\ A.y e. CC (n` (ySx)) = ((abs` y) x. (n` x)) /\ A.y e. X (