mmtheorems86 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 8501-8600 - Page 86 of 123

Type	Label	Description
Statement
Theorem	vsfval 8501	Value of the function for the vector subtraction operation on a normed complex vector space.
|- G = (+v` U)   &   |- M = (-v` U)   =>   |- M = ( /g ` G)
Theorem	nvzcl 8502	Closure law for the zero vector of a normed complex vector space.
|- X = (BaseSet` U)   &   |- Z = (0v` U)   =>   |- (U e. NrmCVec -> Z e. X)
Theorem	nv0rid 8503	The zero vector is a right identity element.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- Z = (0v` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (AGZ) = A)
Theorem	nv0lid 8504	The zero vector is a left identity element.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- Z = (0v` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (ZGA) = A)
Theorem	nv0 8505	Zero times a vector is the zero vector.
|- X = (BaseSet` U)   &   |- S = (.s` U)   &   |- Z = (0v` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (0SA) = Z)
Theorem	nvsz 8506	Anything times the zero vector is the zero vector.
|- S = (.s` U)   &   |- Z = (0v` U)   =>   |- ((U e. NrmCVec /\ A e. CC) -> (ASZ) = Z)
Theorem	nvinv 8507	Minus 1 times a vector is the underlying group's inverse element. Equation 2 of [Kreyszig] p. 51.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   &   |- M = (inv` G)   =>   |- ((U e. NrmCVec /\ A e. X) -> (-u1SA) = (M` A))
Theorem	invfval 8508	Function for the negative of a vector on a normed complex vector space, in terms of the underlying addition group inverse. (We currently do not have a separate notation for the negative of a vector.)
|- G = (+v` U)   &   |- S = (.s` U)   &   |- N = (S o. `'(2nd |` ({-u1} X. V)))   =>   |- (U e. NrmCVec -> N = (inv` G))
Theorem	nvm 8509	Vector subtraction in terms of group division operation.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- M = (-v` U)   &   |- N = ( /g ` G)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AMB) = (ANB))
Theorem	nvmval 8510	Value of vector subtraction on a normed complex vector space.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AMB) = (AG(-u1SB)))
Theorem	nvmfval 8511	Value of the function for the vector subtraction operation on a normed complex vector space.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   &   |- M = (-v` U)   =>   |- (U e. NrmCVec -> M = {<.<.x, y>., z>. | ((x e. X /\ y e. X) /\ z = (xG(-u1Sy)))})
Theorem	nvzs 8512	Two ways to express the negative of a vector.
|- X = (BaseSet` U)   &   |- M = (-v` U)   &   |- S = (.s` U)   &   |- Z = (0v` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (ZMA) = (-u1SA))
Theorem	nvmf 8513	Mapping for the vector subtraction operation.
|- X = (BaseSet` U)   &   |- M = (-v` U)   =>   |- (U e. NrmCVec -> M:(X X. X)-->X)
Theorem	nvmcl 8514	Closure law for the vector subtraction operation of a normed complex vector space.
|- X = (BaseSet` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AMB) e. X)
Theorem	nvnnncan1 8515	Vector space analog of nnncan1 5621.
|- X = (BaseSet` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((AMB)M(AMC)) = (CMB))
Theorem	nvnnncan2 8516	Vector space analog of nnncan2 5622.
|- X = (BaseSet` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((AMC)M(BMC)) = (AMB))
Theorem	nvmdi 8517	Distributive law for scalar product over subtraction.
|- X = (BaseSet` U)   &   |- M = (-v` U)   &   |- S = (.s` U)   =>   |- ((U e. NrmCVec /\ (A e. CC /\ B e. X /\ C e. X)) -> (AS(BMC)) = ((ASB)M(ASC)))
Theorem	nvnegneg 8518	Double negative of a vector.
|- X = (BaseSet` U)   &   |- S = (.s` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (-u1S(-u1SA)) = A)
Theorem	nvmul0or 8519	If a scalar product is zero, one of its factors must be zero.
|- X = (BaseSet` U)   &   |- S = (.s` U)   &   |- Z = (0v` U)   =>   |- ((U e. NrmCVec /\ A e. CC /\ B e. X) -> ((ASB) = Z <-> (A = 0 \/ B = Z)))
Theorem	nvrinv 8520	A vector minus itself.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   &   |- Z = (0v` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (AG(-u1SA)) = Z)
Theorem	nvlinv 8521	Minus a vector plus itself.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   &   |- Z = (0v` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> ((-u1SA)GA) = Z)
Theorem	nvsubadd 8522	Relationship between vector subtraction and addition.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((AMB) = C <-> (BGC) = A))
Theorem	nvpncan2 8523	Cancellation law for vector subtraction.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((AGB)MA) = B)
Theorem	nvpncan 8524	Cancellation law for vector subtraction.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((AGB)MB) = A)
Theorem	nvaddsubass 8525	Associative-type law for vector addition and subtraction.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGB)MC) = (AG(BMC)))
Theorem	nvaddsub 8526	Commutative/associative law for vector addition and subtraction.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGB)MC) = ((AMC)GB))
Theorem	nvnpcan 8527	Cancellation law for a normed complex vector space.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((AMB)GB) = A)
Theorem	nvaddsub4 8528	Rearrangement of 4 terms in a mixed vector addition and subtraction.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X) /\ (C e. X /\ D e. X)) -> ((AGB)M(CGD)) = ((AMC)G(BMD)))
Theorem	nvsubsub23 8529	Swap subtrahend and result of vector subtraction.
|- X = (BaseSet` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((AMB) = C <-> (AMC) = B))
Theorem	nvnncan 8530	Cancellation law for a normed complex vector space.
|- X = (BaseSet` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AM(AMB)) = B)
Theorem	nvmeq0 8531	The difference between two vectors is zero iff they are equal.
|- X = (BaseSet` U)   &   |- M = (-v` U)   &   |- Z = (0v` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((AMB) = Z <-> A = B))
Theorem	nvmid 8532	A vector minus itself is the zero vector.
|- X = (BaseSet` U)   &   |- M = (-v` U)   &   |- Z = (0v` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (AMA) = Z)
Theorem	nvf 8533	Mapping for the norm function.
|- X = (BaseSet` U)   &   |- N = (norm` U)   =>   |- (U e. NrmCVec -> N:X-->RR)
Theorem	nvcl 8534	The norm of a normed complex vector space is a real number.
|- X = (BaseSet` U)   &   |- N = (norm` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (N` A) e. RR)
Theorem	nvcli 8535	The norm of a normed complex vector space is a real number.
|- X = (BaseSet` U)   &   |- N = (norm` U)   &   |- U e. NrmCVec   &   |- A e. X   =>   |- (N` A) e. RR
Theorem	nvdm 8536	Two ways to express the set of vectors in a normed complex vector space.
|- G = (+v` U)   &   |- N = (norm` U)   =>   |- (U e. NrmCVec -> (X = dom N <-> X = ran G))
Theorem	nvs 8537	Proportionality property of the norm of a scalar product in a normed complex vector space.
|- X = (BaseSet` U)   &   |- S = (.s` U)   &   |- N = (norm` U)   =>   |- ((U e. NrmCVec /\ A e. CC /\ B e. X) -> (N` (ASB)) = ((abs` A) x. (N` B)))
Theorem	nvsge0 8538	The norm of a scalar product with a nonnegative real.
|- X = (BaseSet` U)   &   |- S = (.s` U)   &   |- N = (norm` U)   =>   |- ((U e. NrmCVec /\ (A e. RR /\ 0 <_ A) /\ B e. X) -> (N` (ASB)) = (A x. (N` B)))
Theorem	nvm1 8539	The norm of the negative of a vector.
|- X = (BaseSet` U)   &   |- S = (.s` U)   &   |- N = (norm` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (N` (-u1SA)) = (N` A))
Theorem	nvdif 8540	The norm of the difference between two vectors.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   &   |- N = (norm` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(-u1SB))) = (N` (BG(-u1SA))))
Theorem	nvpi 8541	The norm of a vector plus the imaginary scalar product of another.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   &   |- N = (norm` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(iSB))) = (N` (BG(-uiSA))))
Theorem	nvsub 8542	The norm of the difference between two vectors.
|- X = (BaseSet` U)   &   |- M = (-v` U)   &   |- N = (norm` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AMB)) = (N` (BMA)))
Theorem	nvz0 8543	The norm of a zero vector is zero.
|- Z = (0v` U)   &   |- N = (norm` U)   =>   |- (U e. NrmCVec -> (N` Z) = 0)
Theorem	nvz 8544	The norm of a vector is zero iff the vector is zero. First part of Problem 2 of [Kreyszig] p. 64.
|- X = (BaseSet` U)   &   |- Z = (0v` U)   &   |- N = (norm` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> ((N` A) = 0 <-> A = Z))
Theorem	nvtri 8545	Triangle inequality for the norm of a normed complex vector space.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- N = (norm` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AGB)) <_ ((N` A) + (N` B)))
Theorem	nvmtri 8546	Triangle inequality for the norm of a vector difference.
|- X = (BaseSet` U)   &   |- M = (-v` U)   &   |- N = (norm` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AMB)) <_ ((N` A) + (N` B)))
Theorem	nvmtri2 8547	Triangle inequality for the norm of a vector difference.
|- X = (BaseSet` U)   &   |- M = (-v` U)   &   |- N = (norm` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> (N` (AMC)) <_ ((N` (AMB)) + (N` (BMC))))
Theorem	nvabs 8548	Norm difference property of a normed complex vector space. Problem 3 of [Kreyszig] p. 64.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   &   |- N = (norm` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (abs` ((N` A) - (N` B))) <_ (N` (AG(-u1SB))))
Theorem	nvge0 8549	The norm of a normed complex vector space is nonnegative. Second part of Problem 2 of [Kreyszig] p. 64.
|- X = (BaseSet` U)   &   |- N = (norm` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> 0 <_ (N` A))
Theorem	nvgt0 8550	A nonzero norm is positive.
|- X = (BaseSet` U)   &   |- Z = (0v` U)   &   |- N = (norm` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (A =/= Z <-> 0 < (N` A)))
Theorem	nv1 8551	From any nonzero vector, construct a vector whose norm is one.
|- X = (BaseSet` U)   &   |- S = (.s` U)   &   |- Z = (0v` U)   &   |- N = (norm` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ A =/= Z) -> (N` ((1 / (N` A))SA)) = 1)
Theorem	nvop 8552	A complex inner product space in terms of ordered pair components.
|- G = (+v` U)   &   |- S = (.s` U)   &   |- N = (norm` U)   =>   |- (U e. NrmCVec -> U = <.<.G, S>., N>.)
Theorem	nvoprne 8553	The vector addition and scalar product operations are not identical.
|- (<.<.G, S>., N>. e. NrmCVec -> G =/= S)
Examples of normed complex vector spaces
Theorem	cnnv 8554	The set of complex numbers is a normed complex vector space. The vector operation is +, the scalar product is x., and the norm function is abs. (Contributed by Steve Rodriguez, 3-Dec-2006.)
|- U = <.<. + , x. >., abs>.   =>   |- U e. NrmCVec
Theorem	cnnvg 8555	The vector addition (group) operation of the normed complex vector space of complex numbers.
|- U = <.<. + , x. >., abs>.   =>   |- + = (+v` U)
Theorem	cnnvba 8556	The base set of the normed complex vector space of complex numbers.
|- U = <.<. + , x. >., abs>.   =>   |- CC = (BaseSet` U)
Theorem	cnnvdemo 8557	Derive the associative law for complex number addition axaddass 5431 to demonstrate the use of cnnv 8554, cnnvg 8555, and cnnvba 8556.
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A + B) + C) = (A + (B + C)))
Theorem	cnnvs 8558	The scalar product operation of the normed complex vector space of complex numbers.
|- U = <.<. + , x. >., abs>.   =>   |- x. = (.s` U)
Theorem	cnnvnm 8559	The norm operation of the normed complex vector space of complex numbers.
|- U = <.<. + , x. >., abs>.   =>   |- abs = (norm` U)
Theorem	cnnvm 8560	The vector subtraction operation of the normed complex vector space of complex numbers.
|- U = <.<. + , x. >., abs>.   =>   |- - = (-v` U)
Theorem	elimnv 8561	Hypothesis elimination lemma for normed complex vector spaces to assist weak deduction theorem.
|- X = (BaseSet` U)   &   |- Z = (0v` U)   &   |- U e. NrmCVec   =>   |- if(A e. X, A, Z) e. X
Theorem	elimnvu 8562	Hypothesis elimination lemma for normed complex vector spaces to assist weak deduction theorem.
|- if(U e. NrmCVec, U, <.<. + , x. >., abs>.) e. NrmCVec
Induced metric of a normed complex vector space
Theorem	imsval 8563	Value of the induced metric of a normed complex vector space.
|- M = (-v` U)   &   |- N = (norm` U)   &   |- D = (IndMet` U)   =>   |- (U e. NrmCVec -> D = (N o. M))
Theorem	imsdval 8564	Value of the induced metric (distance function) of a normed complex vector space. Equation 1 of [Kreyszig] p. 59.
|- X = (BaseSet` U)   &   |- M = (-v` U)   &   |- N = (norm` U)   &   |- D = (IndMet` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (ADB) = (N` (AMB)))
Theorem	imsdval2 8565	Value of the distance function of the induced metric of a normed complex vector space. Equation 1 of [Kreyszig] p. 59.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   &   |- N = (norm` U)   &   |- D = (IndMet` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (ADB) = (N` (AG(-u1SB))))
Theorem	nvnd 8566	The norm of a normed complex vector space expressed in terms of the distance function of its induced metric. Problem 1 of [Kreyszig] p. 63.
|- X = (BaseSet` U)   &   |- Z = (0v` U)   &   |- N = (norm` U)   &   |- D = (IndMet` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (N` A) = (ADZ))
Theorem	imsdf 8567	Mapping for the induced metric distance function of a normed complex vector space.
|- X = (BaseSet` U)   &   |- D = (IndMet` U)   =>   |- (U e. NrmCVec -> D:(X X. X)-->RR)
Theorem	imsba 8568	Base set of the induced metric space of a normed complex vector space.
|- X = (BaseSet` U)   &   |- D = (IndMet` U)   =>   |- (U e. NrmCVec -> X = dom dom D)
Theorem	imsbai 8569	Base set of the induced metric space of a normed complex vector space.
|- X = (BaseSet` U)   &   |- D = (IndMet` U)   &   |- U e. NrmCVec   =>   |- X = dom dom D
Theorem	imsmetlem 8570	Lemma for imsmet 8571.
Theorem	imsmet 8571	The induced metric of a normed complex vector space is a metric space. Part of Definition 2.2-1 of [Kreyszig] p. 58.
|- D = (IndMet` U)   =>   |- (U e. NrmCVec -> D e. Met)
Theorem	nvelbl 8572	Membership of a vector in a ball.
|- X = (BaseSet` U)   &   |- M = (-v` U)   &   |- N = (norm` U)   &   |- D = (IndMet` U)   =>   |- (((U e. NrmCVec /\ P e. X /\ A e. X) /\ (R e. RR /\ 0 < R)) -> (A e. (P( ball ` D)R) <-> (N` (AMP)) < R))
Theorem	nvelbl2 8573	Membership of an off-center vector in a ball.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- N = (norm` U)   &   |- D = (IndMet` U)   =>   |- (((U e. NrmCVec /\ P e. X /\ A e. X) /\ (R e. RR /\ 0 < R)) -> ((PGA) e. (P( ball ` D)R) <-> (N` A) < R))
Theorem	nvcnf 8574	A continuous function is an operation (normed complex vector space version of cnf 7972).
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- C = (IndMet` U)   &   |- D = (IndMet` W)   &   |- J = (Open` C)   &   |- K = (Open` D)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) -> F:X-->Y)
Theorem	nvcnpf 8575	A continuous function is an operation (normed complex vector space version of cnpf 7973).
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- C = (IndMet` U)   &   |- D = (IndMet` W)   &   |- J = (Open` C)   &   |- K = (Open` D)   =>   |- (((U e. NrmCVec /\ W e. NrmCVec /\ P e. X) /\ F e. ((J CnP K)` P)) -> F:X-->Y)
Theorem	nvcni 8576	Epsilon-delta property of a continuous operator. (Normed complex vector space version of metcni 8105.)
|- X = (BaseSet` U)   &   |- M = (norm` U)   &   |- N = (norm` W)   &   |- R = (-v` U)   &   |- S = (-v` W)   &   |- C = (IndMet` U)   &   |- D = (IndMet` W)   &   |- J = (Open` C)   &   |- K = (Open` D)   =>   |- (((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) /\ (P e. X /\ A e. RR /\ 0 < A)) -> E.x e. RR (0 < x /\ A.y e. X ((M` (PRy)) < x -> (N` ((F` P)S(F` y))) < A)))
Theorem	nvcni2 8577	Epsilon-delta property of a continuous operator. (Normed complex vector space version of metcni 8105.)
|- X = (BaseSet` U)   &   |- M = (norm` U)   &   |- N = (norm` W)   &   |- R = (-v` U)   &   |- S = (-v` W)   &   |- C = (IndMet` U)   &   |- D = (IndMet` W)   &   |- J = (Open` C)   &   |- K = (Open` D)   =>   |- (((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) /\ (P e. X /\ A e. RR /\ 0 < A)) -> E.x e. RR (0 < x /\ A.y e. X ((M` (PRy)) <_ x -> (N` ((F` P)S(F` y))) <_ A)))
Theorem	nvcni3 8578	Epsilon-delta property of a continuous operator. (Normed complex vector space version of metcni 8105.)
|- X = (BaseSet` U)   &   |- M = (norm` U)   &   |- N = (norm` W)   &   |- R = (-v` U)   &   |- S = (-v` W)   &   |- C = (IndMet` U)   &   |- D = (IndMet` W)   &   |- J = (Open` C)   &   |- K = (Open` D)   =>   |- (((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) /\ (P e. X /\ A e. RR /\ 0 < A)) -> E.x e. RR (0 < x /\ A.y e. X ((M` (yRP)) < x -> (N` ((F` y)S(F` P))) < A)))
Theorem	nvlmcl 8579	Closure of the limit of a converging vector sequence.
|- X = (BaseSet` U)   &   |- D = (IndMet` U)   &   |- P e. V   =>   |- ((U e. NrmCVec /\ F(~~>m` D)P) -> P e. X)
Theorem	nvlmle 8580	If the norm of each member of a converging sequence is less than or equal to a given amount, so is the norm of the convergence value.
|- X = (BaseSet` U)   &   |- N = (norm` U)   &   |- D = (IndMet` U)   &   |- P e. V   =>   |- (((U e. NrmCVec /\ F:NN-->X /\ F(~~>m` D)P) /\ (R e. RR /\ A.k e. NN (N` (F` k)) <_ R)) -> (N` P) <_ R)
Theorem	cnims 8581	The metric induced on the complex numbers. cnmet 8115 proves that it is a metric. (Contributed by Steve Rodriguez, 5-Dec-2006; revised by nm 15-Jan-2008.)
|- U = <.<. + , x. >., abs>.   &   |- D = (abs o. - )   =>   |- D = (IndMet` U)
Theorem	vacnlem1 8582	Lemma for vacn 8588.
Theorem	vacnlem2 8583	Lemma for vacn 8588.
Theorem	vacnlem3 8584	Lemma for vacn 8588.
Theorem	vacnlem4 8585	Lemma for vacn 8588.
Theorem	vacnlem5 8586	Lemma for vacn 8588.
Theorem	vacnlem6 8587	Lemma for vacn 8588.
Theorem	vacn 8588	Vector addition is continuous. (Contributed by Jeffrey Hankins, 16-Jun-2009.)
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- C = (IndMet` U)   &   |- D = {<.<.x, y>., z>. | ((x e. (X X. X) /\ y e. (X X. X)) /\ z = sup({((1st` x)C(1st` y)), ((2nd` x)C(2nd` y))}, RR, < ))}   &   |- J = (Open` C)   &   |- K = (Open` D)   =>   |- (U e. NrmCVec -> G e. (K Cn J))
Theorem	sqcn 8589	The square function on complex numbers is continuous.
|- D = (IndMet` <.<. + , x. >., abs>.)   &   |- J = (Open` D)   &   |- F = {<.x, y>. | (x e. CC /\ y = (x^2))}   =>   |- F e. (J Cn J)
Theorem	sqcn2 8590	The square function on complex numbers is continuous.
|- D = (abs o. - )   &   |- J = (Open` D)   &   |- F = {<.w, v>. | (w e. CC /\ v = (w^2))}   =>   |- F e. (J Cn J)
Theorem	nmcnilem 8591	Lemma for nmcni 8592.
Theorem	nmcni 8592	The norm of a normed complex vector space is a continuous function.
|- N = (norm` U)   &   |- C = (IndMet` U)   &   |- D = ((abs o. - ) |` (RR X. RR))   &   |- J = (Open` C)   &   |- K = (Open` D)   &   |- U e. NrmCVec   =>   |- N e. (J Cn K)
Theorem	nmcn 8593	The norm of a normed complex vector space is a continuous function.
|- N = (norm` U)   &   |- C = (IndMet` U)   &   |- D = ((abs o. - ) |` (RR X. RR))   &   |- J = (Open` C)   &   |- K = (Open` D)   =>   |- (U e. NrmCVec -> N e. (J Cn K))
Theorem	nmcn2 8594	The norm of a normed complex vector space is a continuous function to RR.
|- N = (norm` U)   &   |- D = (IndMet` U)   &   |- J = (Open` D)   =>   |- (U e. NrmCVec -> N e. (J Cn (topGen` ran (,))))
Theorem	nmcn3 8595	The norm of a normed complex vector space is a continuous function to CC.
|- N = (norm` U)   &   |- D = (IndMet` U)   &   |- J = (Open` D)   &   |- K = (Open` (IndMet` <.<. + , x. >., abs>.))   =>   |- (U e. NrmCVec -> N e. (J Cn K))
Theorem	nmcnc 8596	The norm of a normed complex vector space is a continuous function to CC. (For RR, see nmcn 8593.)
|- N = (norm` U)   &   |- C = (IndMet` U)   &   |- D = (abs o. - )   &   |- J = (Open` C)   &   |- K = (Open` D)   =>   |- (U e. NrmCVec -> N e. (J Cn K))
Theorem	abscn 8597	The absolute value function on complex numbers is continuous.
|- C = (abs o. - )   &   |- R = ((abs o. - ) |` (RR X. RR))   &   |- J = (Open` C)   &   |- K = (Open` R)   =>   |- abs e. (J Cn K)
Theorem	abscncfALT 8598	Absolute value is continuous. Alternate proof of abscncf 7480.
|- abs e. (CC-cn->RR)
Theorem	va1cnlem 8599	Lemma for va1cn 8600.
Theorem	va1cn 8600	Vector addition is continuous in its first operand.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- D = (IndMet` U)   &   |- J = (Open` D)   &   |- F = {<.w, v>. | (w e. X /\ v = (wGA))}   &   |- U e. NrmCVec   =>   |- (A e. X -> F e. (J Cn J))