mmtheorems96 - 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-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 9501-9600 - Page 96 of 175

Type	Label	Description
Statement
Theorem	vccl 9501	Closure of the scalar product of a complex vector space.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ A e. CC /\ B e. X) -> (ASB) e. X)
Theorem	vcid 9502	Identity element for the scalar product of a complex vector space.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ A e. X) -> (1SA) = A)
Theorem	vcdi 9503	Distributive law for the scalar product of a complex vector space.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ (A e. CC /\ B e. X /\ C e. X)) -> (AS(BGC)) = ((ASB)G(ASC)))
Theorem	vcdir 9504	Distributive law for the scalar product of a complex vector space.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ (A e. CC /\ B e. CC /\ C e. X)) -> ((A + B)SC) = ((ASC)G(BSC)))
Theorem	vcass 9505	Associative law for the scalar product of a complex vector space.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ (A e. CC /\ B e. CC /\ C e. X)) -> ((A x. B)SC) = (AS(BSC)))
Theorem	vc2 9506	A vector plus itself is two times the vector.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ A e. X) -> (AGA) = (2SA))
Theorem	vcsubdir 9507	Subtractive distributive law for the scalar product of a complex vector space.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ (A e. CC /\ B e. CC /\ C e. X)) -> ((A - B)SC) = ((ASC)G(-u1S(BSC))))
Theorem	vcabl 9508	Vector addition is an Abelian group operation.
|- G = (1st` W)   =>   |- (W e. CVec -> G e. Abel)
Theorem	vcgrp 9509	Vector addition is a group operation.
|- G = (1st` W)   =>   |- (W e. CVec -> G e. Grp)
Theorem	vcgcl 9510	Closure law for the vector addition (group) operation of a complex vector space.
|- G = (1st` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ A e. X /\ B e. X) -> (AGB) e. X)
Theorem	vccom 9511	Vector addition is commutative.
|- G = (1st` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ A e. X /\ B e. X) -> (AGB) = (BGA))
Theorem	vcaass 9512	Vector addition is associative.
|- G = (1st` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGB)GC) = (AG(BGC)))
Theorem	vca23 9513	Commutative/associative law that swaps the last two terms in a triple vector sum.
|- G = (1st` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGB)GC) = ((AGC)GB))
Theorem	vca4 9514	Rearrangement of 4 terms in a vector sum.
|- G = (1st` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ (A e. X /\ B e. X) /\ (C e. X /\ D e. X)) -> ((AGB)G(CGD)) = ((AGC)G(BGD)))
Theorem	vcrcan 9515	Right cancellation law for vector addition.
|- G = (1st` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGC) = (BGC) <-> A = B))
Theorem	vclcan 9516	Left cancellation law for vector addition.
|- G = (1st` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((CGA) = (CGB) <-> A = B))
Theorem	vczcl 9517	The zero vector is a vector.
|- G = (1st` W)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- (W e. CVec -> Z e. X)
Theorem	vc0rid 9518	The zero vector is a right identity element.
|- G = (1st` W)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- ((W e. CVec /\ A e. X) -> (AGZ) = A)
Theorem	vc0lid 9519	The zero vector is a left identity element.
|- G = (1st` W)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- ((W e. CVec /\ A e. X) -> (ZGA) = A)
Theorem	vc0 9520	Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- ((W e. CVec /\ A e. X) -> (0SA) = Z)
Theorem	vcz 9521	Anything times the zero vector is the zero vector. Equation 1b of [Kreyszig] p. 51.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- ((W e. CVec /\ A e. CC) -> (ASZ) = Z)
Theorem	vcm 9522	Minus 1 times a vector is the underlying group's inverse element. Equation 2 of [Kreyszig] p. 51.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   &   |- M = (inv` G)   =>   |- ((W e. CVec /\ A e. X) -> (-u1SA) = (M` A))
Theorem	vcrinv 9523	A vector minus itself.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- ((W e. CVec /\ A e. X) -> (AG(-u1SA)) = Z)
Theorem	vclinv 9524	Minus a vector plus itself.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- ((W e. CVec /\ A e. X) -> ((-u1SA)GA) = Z)
Theorem	vcnegneg 9525	Double negative of a vector.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ A e. X) -> (-u1S(-u1SA)) = A)
Theorem	vcnegsubdi2 9526	Distribution of negative over vector subtraction.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ A e. X /\ B e. X) -> (-u1S(AG(-u1SB))) = (BG(-u1SA)))
Theorem	vcsub4 9527	Rearrangement of 4 terms in a mixed vector addition and subtraction.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ (A e. X /\ B e. X) /\ (C e. X /\ D e. X)) -> ((AGB)G(-u1S(CGD))) = ((AG(-u1SC))G(BG(-u1SD))))
Theorem	isvclem 9528	Lemma for isvc 9532.
Theorem	vcoprnelem 9529	Lemma for vcoprne 9530.
Theorem	vcoprne 9530	The operations of a complex vector space cannot be identical.
|- (<.G, S>. e. CVec -> G =/= S)
Theorem	vcex 9531	The components of a complex vector space are sets.
|- (<.G, S>. e. CVec -> (G e. _V /\ S e. _V))
Theorem	isvc 9532	The predicate "is a complex vector space."
|- X = ran G   =>   |- (<.G, S>. e. CVec <-> (G e. Abel /\ S:(CC X. X)-->X /\ A.x e. X ((1Sx) = x /\ A.y e. CC (A.z e. X (yS(xGz)) = ((ySx)G(ySz)) /\ A.z e. CC (((y + z)Sx) = ((ySx)G(zSx)) /\ ((y x. z)Sx) = (yS(zSx)))))))
Theorem	isvci 9533	Properties that determine a complex vector space.
|- G e. Abel   &   |- dom G = (X X. X)   &   |- S:(CC X. X)-->X   &   |- (x e. X -> (1Sx) = x)   &   |- ((y e. CC /\ x e. X /\ z e. X) -> (yS(xGz)) = ((ySx)G(ySz)))   &   |- ((y e. CC /\ z e. CC /\ x e. X) -> ((y + z)Sx) = ((ySx)G(zSx)))   &   |- ((y e. CC /\ z e. CC /\ x e. X) -> ((y x. z)Sx) = (yS(zSx)))   &   |- W = <.G, S>.   =>   |- W e. CVec
Examples of complex vector spaces
Theorem	cnvc 9534	The set of complex numbers is a complex vector space. The vector operation is +, and the scalar product is x..
|- <. + , x. >. e. CVec
Normed complex vector spaces
Definition and basic properties
Syntax	cnv 9535	Extend class notation with the class of all normed complex vector spaces.
class NrmCVec
Syntax	cpv 9536	Extend class notation with vector addition in a normed complex vector space. In the literature, the subscript "v" is omitted, but we need it to avoid ambiguity with complex number addition + caddc 6389.
class +v
Syntax	cba 9537	Extend class notation with the base set of a normed complex vector space. (Note that BaseSet is capitalized because, once it is fixed for a particular vector space U, it is not a function, unlike e.g. norm. This is our typical convention.)
class BaseSet
Syntax	cns 9538	Extend class notation with scalar multiplication in a normed complex vector space. In the literature scalar multiplication is usually indicated by juxtaposition, but we need an explicit symbol to prevent ambiguity.
class .s
Syntax	cn0v 9539	Extend class notation with zero vector in a normed complex vector space.
class 0v
Syntax	cnsb 9540	Extend class notation with vector subtraction in a normed complex vector space.
class -v
Syntax	cnm 9541	Extend class notation with the norm function in a normed complex vector space. In the literature, the norm of A is usually written "|| A ||", but we use function notation to take advantage of our existing theorems about functions.
class norm
Syntax	cims 9542	Extend class notation with the class of the induced metrics on normed complex vector spaces.
class IndMet
Definition	df-nv 9543	Define the class of all normed complex vector spaces.
|- 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))))}
Theorem	nvss 9544	Structure of the class of all normed complex vectors spaces.
|- NrmCVec C_ ((_V X. _V) X. _V)
Theorem	nvvcop 9545	A normed complex vector space is a vector space.
|- (<.<.G, S>., N>. e. NrmCVec -> <.G, S>. e. CVec)
Definition	df-va 9546	Define vector addition on a normed complex vector space.
|- +v = (1st o. 1st)
Definition	df-ba 9547	Define the base set of a normed complex vector space.
|- BaseSet = {<.x, y>. | y = ran (+v` x)}
Definition	df-sm 9548	Define scalar multiplication on a normed complex vector space.
|- .s = (2nd o. 1st)
Definition	df-0v 9549	Define the zero vector in a normed complex vector space.
|- 0v = (Id o. +v)
Definition	df-vs 9550	Define vector subtraction on a normed complex vector space.
|- -v = ( /g o. +v)
Definition	df-nm 9551	Define the norm function in a normed complex vector space.
|- norm = 2nd
Definition	df-ims 9552	Define the induced metric on a normed complex vector space.
|- IndMet = {<.u, d>. | (u e. NrmCVec /\ d = ((norm` u) o. (-v` u)))}
Theorem	nvrel 9553	The class of all normed complex vectors spaces is a relation.
|- Rel NrmCVec
Theorem	vafval 9554	Value of the function for the vector addition (group) operation on a normed complex vector space.
|- G = (+v` U)   =>   |- G = (1st` (1st` U))
Theorem	bafval 9555	Value of the function for the base set of a normed complex vector space.
|- X = (BaseSet` U)   &   |- G = (+v` U)   =>   |- X = ran G
Theorem	smfval 9556	Value of the function for the scalar multiplication operation on a normed complex vector space.
|- S = (.s` U)   =>   |- S = (2nd` (1st` U))
Theorem	0vfval 9557	Value of the function for the zero vector on a normed complex vector space.
|- G = (+v` U)   &   |- Z = (0v` U)   =>   |- Z = (Id` G)
Theorem	nmfval 9558	Value of the norm function in a normed complex vector space.
|- N = (norm` U)   =>   |- N = (2nd` U)
Theorem	nvop2 9559	A normed complex vector space is an ordered pair of a vector space and a norm operation.
|- W = (1st` U)   &   |- N = (norm` U)   =>   |- (U e. NrmCVec -> U = <.W, N>.)
Theorem	nvvop 9560	The vector space component of a normed complex vector space is an ordered pair of the underlying group and a scalar product.
|- W = (1st` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   =>   |- (U e. NrmCVec -> W = <.G, S>.)
Theorem	isnvlem 9561	Lemma for isnv 9563.
Theorem	nvex 9562	The components of a normed complex vector space are sets.
|- (<.<.G, S>., N>. e. NrmCVec -> (G e. _V /\ S e. _V /\ N e. _V))
Theorem	isnv 9563	The predicate "is a normed complex vector space."
|- X = ran G   &   |- Z = (Id` G)   =>   |- (<.<.G, S>., N>. 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)))))
Theorem	isnvi 9564	Properties that determine a normed complex vector space.
|- X = ran G   &   |- Z = (Id` G)   &   |- <.G, S>. e. CVec   &   |- N:X-->RR   &   |- ((x e. X /\ (N` x) = 0) -> x = Z)   &   |- ((y e. CC /\ x e. X) -> (N` (ySx)) = ((abs` y) x. (N` x)))   &   |- ((x e. X /\ y e. X) -> (N` (xGy)) <_ ((N` x) + (N` y)))   &   |- U = <.<.G, S>., N>.   =>   |- U e. NrmCVec
Theorem	nvi 9565	The properties of a normed complex vector space, which is a vector space accompanied by a norm.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   &   |- Z = (0v` U)   &   |- N = (norm` U)   =>   |- (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)))))
Theorem	nvvc 9566	The vector space component of a normed complex vector space.
|- W = (1st` U)   =>   |- (U e. NrmCVec -> W e. CVec)
Theorem	nvabl 9567	The vector addition operation of a normed complex vector space is an Abelian group.
|- G = (+v` U)   =>   |- (U e. NrmCVec -> G e. Abel)
Theorem	nvgrp 9568	The vector addition operation of a normed complex vector space is a group.
|- G = (+v` U)   =>   |- (U e. NrmCVec -> G e. Grp)
Theorem	nvgf 9569	Mapping for the vector addition operation.
|- X = (BaseSet` U)   &   |- G = (+v` U)   =>   |- (U e. NrmCVec -> G:(X X. X)-->X)
Theorem	nvsf 9570	Mapping for the scalar multiplication operation.
|- X = (BaseSet` U)   &   |- S = (.s` U)   =>   |- (U e. NrmCVec -> S:(CC X. X)-->X)
Theorem	nvgcl 9571	Closure law for the vector addition (group) operation of a normed complex vector space.
|- X = (BaseSet` U)   &   |- G = (+v` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AGB) e. X)
Theorem	nvcom 9572	The vector addition (group) operation is commutative.
|- X = (BaseSet` U)   &   |- G = (+v` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AGB) = (BGA))
Theorem	nvass 9573	The vector addition (group) operation is associative.
|- X = (BaseSet` U)   &   |- G = (+v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGB)GC) = (AG(BGC)))
Theorem	nvadd12 9574	Commutative/associative law for vector addition.
|- X = (BaseSet` U)   &   |- G = (+v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> (AG(BGC)) = (BG(AGC)))
Theorem	nvadd23 9575	Commutative/associative law for vector addition.
|- X = (BaseSet` U)   &   |- G = (+v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGB)GC) = ((AGC)GB))
Theorem	nvrcan 9576	Right cancellation law for vector addition.
|- X = (BaseSet` U)   &   |- G = (+v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGC) = (BGC) <-> A = B))
Theorem	nvlcan 9577	Left cancellation law for vector addition.
|- X = (BaseSet` U)   &   |- G = (+v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((CGA) = (CGB) <-> A = B))
Theorem	nvadd4 9578	Rearrangement of 4 terms in a vector sum.
|- X = (BaseSet` U)   &   |- G = (+v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X) /\ (C e. X /\ D e. X)) -> ((AGB)G(CGD)) = ((AGC)G(BGD)))
Theorem	nvscl 9579	Closure law for the scalar product operation of a normed complex vector space.
|- X = (BaseSet` U)   &   |- S = (.s` U)   =>   |- ((U e. NrmCVec /\ A e. CC /\ B e. X) -> (ASB) e. X)
Theorem	nvsid 9580	Identity element for the scalar product of a normed complex vector space.
|- X = (BaseSet` U)   &   |- S = (.s` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (1SA) = A)
Theorem	nvsass 9581	Associative law for the scalar product of a normed complex vector space.
|- X = (BaseSet` U)   &   |- S = (.s` U)   =>   |- ((U e. NrmCVec /\ (A e. CC /\ B e. CC /\ C e. X)) -> ((A x. B)SC) = (AS(BSC)))
Theorem	nvscom 9582	Commutative law for the scalar product of a normed complex vector space.
|- X = (BaseSet` U)   &   |- S = (.s` U)   =>   |- ((U e. NrmCVec /\ (A e. CC /\ B e. CC /\ C e. X)) -> (AS(BSC)) = (BS(ASC)))
Theorem	nvdi 9583	Distributive law for the scalar product of a complex vector space.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   =>   |- ((U e. NrmCVec /\ (A e. CC /\ B e. X /\ C e. X)) -> (AS(BGC)) = ((ASB)G(ASC)))
Theorem	nvdir 9584	Distributive law for the scalar product of a complex vector space.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   =>   |- ((U e. NrmCVec /\ (A e. CC /\ B e. CC /\ C e. X)) -> ((A + B)SC) = ((ASC)G(BSC)))
Theorem	nv2 9585	A vector plus itself is two times the vector.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (AGA) = (2SA))
Theorem	vsfval 9586	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 9587	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 9588	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 9589	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 9590	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 9591	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 9592	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 9593	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 9594	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 9595	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 9596	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 9597	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 9598	Mapping for the vector subtraction operation.
|- X = (BaseSet` U)   &   |- M = (-v` U)   =>   |- (U e. NrmCVec -> M:(X X. X)-->X)
Theorem	nvmcl 9599	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 9600	Vector space analog of nnncan1 6632.
|- X = (BaseSet` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((AMB)M(AMC)) = (CMB))