mmtheorems83 - 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-10687

Statement List for Metamath Proof Explorer - 8201-8300 - Page 83 of 107

Type	Label	Description
Statement
Theorem	nvabl 8201	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 8202	The vector addition operation of a normed complex vector space is a group.
|- G = (+v` U)   =>   |- (U e. NrmCVec -> G e. Grp)
Theorem	nvgf 8203	Mapping for the vector addition operation.
|- X = (Base` U)   &   |- G = (+v` U)   =>   |- (U e. NrmCVec -> G:(X X. X)-->X)
Theorem	nvsf 8204	Mapping for the scalar multiplication operation.
|- X = (Base` U)   &   |- S = (.s` U)   =>   |- (U e. NrmCVec -> S:(CC X. X)-->X)
Theorem	nvgcl 8205	Closure law for the vector addition (group) operation of a normed complex vector space.
|- X = (Base` U)   &   |- G = (+v` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AGB) e. X)
Theorem	nvcom 8206	The vector addition (group) operation is commutative.
|- X = (Base` U)   &   |- G = (+v` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AGB) = (BGA))
Theorem	nvass 8207	The vector addition (group) operation is associative.
|- X = (Base` U)   &   |- G = (+v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGB)GC) = (AG(BGC)))
Theorem	nvadd12 8208	Commutative/associative law for vector addition.
|- X = (Base` U)   &   |- G = (+v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> (AG(BGC)) = (BG(AGC)))
Theorem	nvadd23 8209	Commutative/associative law for vector addition.
|- X = (Base` U)   &   |- G = (+v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGB)GC) = ((AGC)GB))
Theorem	nvrcan 8210	Right cancellation law for vector addition.
|- X = (Base` U)   &   |- G = (+v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGC) = (BGC) <-> A = B))
Theorem	nvlcan 8211	Left cancellation law for vector addition.
|- X = (Base` U)   &   |- G = (+v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((CGA) = (CGB) <-> A = B))
Theorem	nvadd4 8212	Rearrangement of 4 terms in a vector sum.
|- X = (Base` 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 8213	Closure law for the scalar product operation of a normed complex vector space.
|- X = (Base` U)   &   |- S = (.s` U)   =>   |- ((U e. NrmCVec /\ A e. CC /\ B e. X) -> (ASB) e. X)
Theorem	nvsid 8214	Identity element for the scalar product of a normed complex vector space.
|- X = (Base` U)   &   |- S = (.s` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (1SA) = A)
Theorem	nvsass 8215	Associative law for the scalar product of a normed complex vector space.
|- X = (Base` U)   &   |- S = (.s` U)   =>   |- ((U e. NrmCVec /\ (A e. CC /\ B e. CC /\ C e. X)) -> ((A x. B)SC) = (AS(BSC)))
Theorem	nvscom 8216	Commutative law for the scalar product of a normed complex vector space.
|- X = (Base` U)   &   |- S = (.s` U)   =>   |- ((U e. NrmCVec /\ (A e. CC /\ B e. CC /\ C e. X)) -> (AS(BSC)) = (BS(ASC)))
Theorem	nvdi 8217	Distributive law for the scalar product of a complex vector space.
|- X = (Base` 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 8218	Distributive law for the scalar product of a complex vector space.
|- X = (Base` 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 8219	A vector plus itself is two times the vector.
|- X = (Base` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (AGA) = (2SA))
Theorem	vsfval 8220	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 8221	Closure law for the zero vector of a normed complex vector space.
|- X = (Base` U)   &   |- Z = (0v` U)   =>   |- (U e. NrmCVec -> Z e. X)
Theorem	nv0rid 8222	The zero vector is a right identity element.
|- X = (Base` U)   &   |- G = (+v` U)   &   |- Z = (0v` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (AGZ) = A)
Theorem	nv0lid 8223	The zero vector is a left identity element.
|- X = (Base` U)   &   |- G = (+v` U)   &   |- Z = (0v` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (ZGA) = A)
Theorem	nv0 8224	Zero times a vector is the zero vector.
|- X = (Base` U)   &   |- S = (.s` U)   &   |- Z = (0v` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (0SA) = Z)
Theorem	nvsz 8225	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 8226	Minus 1 times a vector is the underlying group's inverse element. Equation 2 of [Kreyszig] p. 51.
|- X = (Base` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   &   |- M = (inv` G)   =>   |- ((U e. NrmCVec /\ A e. X) -> (-u1SA) = (M` A))
Theorem	invfval 8227	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 8228	Vector subtraction in terms of group division operation.
|- X = (Base` U)   &   |- G = (+v` U)   &   |- M = (-v` U)   &   |- N = ( /g ` G)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AMB) = (ANB))
Theorem	nvmval 8229	Value of vector subtraction on a normed complex vector space.
|- X = (Base` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AMB) = (AG(-u1SB)))
Theorem	nvmfval 8230	Value of the function for the vector subtraction operation on a normed complex vector space.
|- X = (Base` 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 8231	Two ways to express the negative of a vector.
|- X = (Base` U)   &   |- M = (-v` U)   &   |- S = (.s` U)   &   |- Z = (0v` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (ZMA) = (-u1SA))
Theorem	nvmf 8232	Mapping for the vector subtraction operation.
|- X = (Base` U)   &   |- M = (-v` U)   =>   |- (U e. NrmCVec -> M:(X X. X)-->X)
Theorem	nvmcl 8233	Closure law for the vector subtraction operation of a normed complex vector space.
|- X = (Base` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AMB) e. X)
Theorem	nvnnncan1 8234	Vector space analog of nnncan1t 5458.
|- X = (Base` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) -> ((AMB)M(AMC)) = (CMB))
Theorem	nvnnncan2 8235	Vector space analog of nnncan2t 5459.
|- X = (Base` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ (A e. X /\ B e. X /\ C e. X)) ->