mmtheorems85 - 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 - 8401-8500 - Page 85 of 123

Type	Label	Description
Statement
Theorem	ring0cl 8401	A ring has an additive identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- (R e. Ring -> Z e. X)
Theorem	ring0rid 8402	The additive identity of a ring is a right identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- ((R e. Ring /\ A e. X) -> (AGZ) = A)
Theorem	ring0lid 8403	The additive identity of a ring is a left identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- ((R e. Ring /\ A e. X) -> (ZGA) = A)
Examples of rings
Theorem	cnring 8404	The set of complex numbers is a (unital) ring. (Contributed by Steve Rodriguez, 2-Feb-2007.)
|- <. + , x. >. e. Ring
Theorem	ringsn 8405	The trivial or zero ring defined on a singleton set {A} (see http://en.wikipedia.org/wiki/Trivial_ring). (Contributed by Steve Rodriguez, 10-Feb-2007.)
|- A e. V   =>   |- <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>. e. Ring
Division Rings
Definition and basic properties
Syntax	cdrng 8406	Extend class notation with the class of all division rings.
class DivRing
Definition	df-drng 8407	Define the class of all division rings (sometimes called skew fields). A division ring is a unital ring where every element except the additive identity has a multiplicative inverse.
|- DivRing = {<.g, h>. | (<.g, h>. e. Ring /\ (h |` ((ran g \ {(Id` g)}) X. (ran g \ {(Id` g)}))) e. Grp)}
Theorem	drngi 8408	The properties of a division ring.
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- (R e. DivRing -> (R e. Ring /\ (H |` ((X \ {Z}) X. (X \ {Z}))) e. Grp))
Star Fields
Definition and basic properties
Syntax	csfld 8409	Extend class notation with the class of all star fields.
class *-Fld
Definition	df-sfld 8410	Define the class of all star fields, which are all division rings with involutions.
|- *-Fld = {<.r, n>. | (r e. DivRing /\ n:ran (1st` r)-->ran (1st` r) /\ A.x e. dom nA.y e. dom n((n` (x(1st` r)y)) = ((n` x)(1st` r)(n` y)) /\ (n` (x(2nd` r)y)) = ((n` y)(2nd` r)(n` x)) /\ (n` (n` x)) = x))}
Complex vector spaces
Definition and basic properties
Syntax	cvc 8411	Extend class notation with the class of all complex vector spaces.
class CVec
Definition	df-vc 8412	Define the class of all complex vector spaces.
|- CVec = {<.g, s>. | (g e. Abel /\ s:(CC X. ran g)-->ran g /\ A.x e. ran g((1sx) = x /\ A.y e. CC (A.z e. ran g(ys(xgz)) = ((ysx)g(ysz)) /\ A.z e. CC (((y + z)sx) = ((ysx)g(zsx)) /\ ((y x. z)sx) = (ys(zsx))))))}
Theorem	vcrel 8413	The class of all complex vector spaces is a relation.
|- Rel CVec
Theorem	vci 8414	The properties of a complex vector space, which is an Abelian group (i.e. the vectors, with the operation of vector addition) accompanied by a scalar multiplication operation on the field of complex numbers. The variable W was chosen because V is already used for the universal class.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   =>   |- (W 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	vcsm 8415	Functionality of th scalar product of a complex vector space.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   =>   |- (W e. CVec -> S:(CC X. X)-->X)
Theorem	vccl 8416	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 8417	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 8418	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 8419	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 8420	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 8421	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 8422	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 8423	Vector addition is an Abelian group operation.
|- G = (1st` W)   =>   |- (W e. CVec -> G e. Abel)
Theorem	vcgrp 8424	Vector addition is a group operation.
|- G = (1st` W)   =>   |- (W e. CVec -> G e. Grp)
Theorem	vcgcl 8425	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 8426	Vector addition is commutative.
|- G = (1st` W)   &   |- X = ran G   =>   |- ((W e. CVec /\ A e. X /\ B e. X) -> (AGB) = (BGA))
Theorem	vcaass 8427	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 8428	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 8429	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 8430	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 8431	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 8432	The zero vector is a vector.
|- G = (1st` W)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- (W e. CVec -> Z e. X)
Theorem	vc0rid 8433	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 8434	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 8435	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 8436	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 8437	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 8438	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 8439	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 8440	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 8441	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 8442	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 8443	Lemma for isvc 8447.
Theorem	vcoprnelem 8444	Lemma for vcoprne 8445.
Theorem	vcoprne 8445	The operations of a complex vector space cannot be identical.
|- (<.G, S>. e. CVec -> G =/= S)
Theorem	vcex 8446	The components of a complex vector space are sets.
|- (<.G, S>. e. CVec -> (G e. V /\ S e. V))
Theorem	isvc 8447	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 8448	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 8449	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 8450	Extend class notation with the class of all normed complex vector spaces.
class NrmCVec
Syntax	cpv 8451	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 5391.
class +v
Syntax	cba 8452	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 8453	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 8454	Extend class notation with zero vector in a normed complex vector space.
class 0v
Syntax	cnsb 8455	Extend class notation with vector subtraction in a normed complex vector space.
class -v
Syntax	cnm 8456	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 8457	Extend class notation with the class of the induced metrics on normed complex vector spaces.
class IndMet
Definition	df-nv 8458	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 8459	Structure of the class of all normed complex vectors spaces.
|- NrmCVec (_ ((V X. V) X. V)
Theorem	nvvcop 8460	A normed complex vector space is a vector space.
|- (<.<.G, S>., N>. e. NrmCVec -> <.G, S>. e. CVec)
Definition	df-va 8461	Define vector addition on a normed complex vector space.
|- +v = (1st o. 1st)
Definition	df-ba 8462	Define the base set of a normed complex vector space.
|- BaseSet = {<.x, y>. | y = ran (+v` x)}
Definition	df-sm 8463	Define scalar multiplication on a normed complex vector space.
|- .s = (2nd o. 1st)
Definition	df-0v 8464	Define the zero vector in a normed complex vector space.
|- 0v = (Id o. +v)
Definition	df-vs 8465	Define vector subtraction on a normed complex vector space.
|- -v = ( /g o. +v)
Definition	df-nm 8466	Define the norm function in a normed complex vector space.
|- norm = 2nd
Definition	df-ims 8467	Define the induced metric on a normed complex vector space.
|- IndMet = {<.u, d>. | (u e. NrmCVec /\ d = ((norm` u) o. (-v` u)))}
Theorem	nvrel 8468	The class of all normed complex vectors spaces is a relation.
|- Rel NrmCVec
Theorem	vafval 8469	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 8470	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 8471	Value of the function for the scalar multiplication operation on a normed complex vector space.
|- S = (.s` U)   =>   |- S = (2nd` (1st` U))
Theorem	0vfval 8472	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 8473	Value of the norm function in a normed complex vector space.
|- N = (norm` U)   =>   |- N = (2nd` U)
Theorem	nvop2 8474	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 8475	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 8476	Lemma for isnv 8478.
Theorem	nvex 8477	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 8478	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 8479	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 8480	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 8481	The vector space component of a normed complex vector space.
|- W = (1st` U)   =>   |- (U e. NrmCVec -> W e. CVec)
Theorem	nvabl 8482	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 8483	The vector addition operation of a normed complex vector space is a group.
|- G = (+v` U)   =>   |- (U e. NrmCVec -> G e. Grp)
Theorem	nvgf 8484	Mapping for the vector addition operation.
|- X = (BaseSet` U)   &   |- G = (+v` U)   =>   |- (U e. NrmCVec -> G:(X X. X)-->X)
Theorem	nvsf 8485	Mapping for the scalar multiplication operation.
|- X = (BaseSet` U)   &   |- S = (.s` U)   =>   |- (U e. NrmCVec -> S:(CC X. X)-->X)
Theorem	nvgcl 8486	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 8487	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 8488	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 8489	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 8490	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 8491	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 8492	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 8493	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 8494	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 8495	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 8496	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 8497	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 8498	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 8499	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 8500	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))