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-10700 108 10701-10752

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

Type	Label	Description
Statement
Syntax	cba 8201	Extend class notation with the base set of a normed complex vector space. (Note that Base 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 Base
Syntax	cns 8202	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 8203	Extend class notation with zero vector in a normed complex vector space.
class 0v
Syntax	cnsb 8204	Extend class notation with vector subtraction in a normed complex vector space.
class −v
Syntax	cnm 8205	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 8206	Extend class notation with the class of the induced metrics on normed complex vector spaces.
class IndMet
Definition	df-nv 8207	Define the class of all normed complex vector spaces.
⊢ NrmCVec = {⟨⟨g, s⟩, n⟩∣(⟨g, s⟩ ∈ CVec ⋀ n:ran g–→ℝ ⋀ ∀x ∈ ran g(((n ‘x) = 0 → x = (Id ‘g)) ⋀ ∀y ∈ ℂ (n ‘(ysx)) = ((abs ‘y) · (n ‘x)) ⋀ ∀y ∈ ran g(n ‘(xgy)) ≤ ((n ‘x) + (n ‘y))))}
Theorem	nvss 8208	Structure of the class of all normed complex vectors spaces.
⊢ NrmCVec ⊆ ((V × V) × V)
Theorem	nvvcop 8209	A normed complex vector space is a vector space.
⊢ (⟨⟨G, S⟩, N⟩ ∈ NrmCVec → ⟨G, S⟩ ∈ CVec)
Definition	df-va 8210	Define vector addition on a normed complex vector space.
⊢ +v = (1st ∘ 1st )
Definition	df-ba 8211	Define the base set of a normed complex vector space.
⊢ Base = {⟨x, y⟩∣y = ran ( +v ‘x)}
Definition	df-sm 8212	Define scalar multiplication on a normed complex vector space.
⊢ ·s = (2nd ∘ 1st )
Definition	df-0v 8213	Define the zero vector in a normed complex vector space.
⊢ 0v = (Id ∘ +v )
Definition	df-vs 8214	Define vector subtraction on a normed complex vector space.
⊢ −v = ( /g ∘ +v )
Definition	df-nm 8215	Define the norm function in a normed complex vector space.
⊢ norm = 2nd
Definition	df-ims 8216	Define the induced metric on a normed complex vector space.
⊢ IndMet = {⟨u, d⟩∣(u ∈ NrmCVec ⋀ d = ((norm ‘u) ∘ ( −v ‘u)))}
Theorem	nvrel 8217	The class of all normed complex vectors spaces is a relation.
⊢ Rel NrmCVec
Theorem	vafval 8218	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 8219	Value of the function for the base set of a normed complex vector space.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    ⇒   ⊢ X = ran G
Theorem	smfval 8220	Value of the function for the scalar multiplication operation on a normed complex vector space.
⊢ S = ( ·s ‘U)    ⇒   ⊢ S = (2nd ‘(1st ‘U))
Theorem	0vfval 8221	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 8222	Value of the norm function in a normed complex vector space.
⊢ N = (norm ‘U)    ⇒   ⊢ N = (2nd ‘U)
Theorem	nvop2 8223	A normed complex vector space is an ordered pair of a vector space and a norm operation.
⊢ W = (1st ‘U)    &   ⊢ N = (norm ‘U)    ⇒   ⊢ (U ∈ NrmCVec → U = ⟨W, N⟩)
Theorem	nvvop 8224	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 ∈ NrmCVec → W = ⟨G, S⟩)
Theorem	isnvlem 8225	Lemma for isnv 8227.
Theorem	nvex 8226	The components of a normed complex vector space are sets.
⊢ (⟨⟨G, S⟩, N⟩ ∈ NrmCVec → (G ∈ V ⋀ S ∈ V ⋀ N ∈ V))
Theorem	isnv 8227	The predicate "is a normed complex vector space."
⊢ X = ran G    &   ⊢ Z = (Id ‘G)    ⇒   ⊢ (⟨⟨G, S⟩, N⟩ ∈ NrmCVec ↔ (⟨G, S⟩ ∈ CVec ⋀ N:X–→ℝ ⋀ ∀x ∈ X (((N ‘x) = 0 → x = Z) ⋀ ∀y ∈ ℂ (N ‘(ySx)) = ((abs ‘y) · (N ‘x)) ⋀ ∀y ∈ X (N ‘(xGy)) ≤ ((N ‘x) + (N ‘y)))))
Theorem	isnvi 8228	Properties that determine a normed complex vector space.
⊢ X = ran G    &   ⊢ Z = (Id ‘G)    &   ⊢ ⟨G, S⟩ ∈ CVec    &   ⊢ N:X–→ℝ    &   ⊢ ((x ∈ X ⋀ (N ‘x) = 0) → x = Z)    &   ⊢ ((y ∈ ℂ ⋀ x ∈ X) → (N ‘(ySx)) = ((abs ‘y) · (N ‘x)))    &   ⊢ ((x ∈ X ⋀ y ∈ X) → (N ‘(xGy)) ≤ ((N ‘x) + (N ‘y)))    &   ⊢ U = ⟨⟨G, S⟩, N⟩    ⇒   ⊢ U ∈ NrmCVec
Theorem	nvi 8229	The properties of a normed complex vector space, which is a vector space accompanied by a norm.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    &   ⊢ S = ( ·s ‘U)    &   ⊢ Z = (0v ‘U)    &   ⊢ N = (norm ‘U)    ⇒   ⊢ (U ∈ NrmCVec → (⟨G, S⟩ ∈ CVec ⋀ N:X–→ℝ ⋀ ∀x ∈ X (((N ‘x) = 0 → x = Z) ⋀ ∀y ∈ ℂ (N ‘(ySx)) = ((abs ‘y) · (N ‘x)) ⋀ ∀y ∈ X (N ‘(xGy)) ≤ ((N ‘x) + (N ‘y)))))
Theorem	nvvc 8230	The vector space component of a normed complex vector space.
⊢ W = (1st ‘U)    ⇒   ⊢ (U ∈ NrmCVec → W ∈ CVec)
Theorem	nvabl 8231	The vector addition operation of a normed complex vector space is an Abelian group.
⊢ G = ( +v ‘U)    ⇒   ⊢ (U ∈ NrmCVec → G ∈ Abel)
Theorem	nvgrp 8232	The vector addition operation of a normed complex vector space is a group.
⊢ G = ( +v ‘U)    ⇒   ⊢ (U ∈ NrmCVec → G ∈ Grp)
Theorem	nvgf 8233	Mapping for the vector addition operation.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    ⇒   ⊢ (U ∈ NrmCVec → G:(X × X)–→X)
Theorem	nvsf 8234	Mapping for the scalar multiplication operation.
⊢ X = (Base ‘U)    &   ⊢ S = ( ·s ‘U)    ⇒   ⊢ (U ∈ NrmCVec → S:(ℂ × X)–→X)
Theorem	nvgcl 8235	Closure law for the vector addition (group) operation of a normed complex vector space.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X ⋀ B ∈ X) → (AGB) ∈ X)
Theorem	nvcom 8236	The vector addition (group) operation is commutative.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X ⋀ B ∈ X) → (AGB) = (BGA))
Theorem	nvass 8237	The vector addition (group) operation is associative.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → ((AGB)GC) = (AG(BGC)))
Theorem	nvadd12 8238	Commutative/associative law for vector addition.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → (AG(BGC)) = (BG(AGC)))
Theorem	nvadd23 8239	Commutative/associative law for vector addition.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → ((AGB)GC) = ((AGC)GB))
Theorem	nvrcan 8240	Right cancellation law for vector addition.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → ((AGC) = (BGC) ↔ A = B))
Theorem	nvlcan 8241	Left cancellation law for vector addition.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → ((CGA) = (CGB) ↔ A = B))
Theorem	nvadd4 8242	Rearrangement of 4 terms in a vector sum.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ X ⋀ B ∈ X) ⋀ (C ∈ X ⋀ D ∈ X)) → ((AGB)G(CGD)) = ((AGC)G(BGD)))
Theorem	nvscl 8243	Closure law for the scalar product operation of a normed complex vector space.
⊢ X = (Base ‘U)    &   ⊢ S = ( ·s ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ ℂ ⋀ B ∈ X) → (ASB) ∈ X)
Theorem	nvsid 8244	Identity element for the scalar product of a normed complex vector space.
⊢ X = (Base ‘U)    &   ⊢ S = ( ·s ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X) → (1SA) = A)
Theorem	nvsass 8245	Associative law for the scalar product of a normed complex vector space.
⊢ X = (Base ‘U)    &   ⊢ S = ( ·s ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ X)) → ((A · B)SC) = (AS(BSC)))
Theorem	nvscom 8246	Commutative law for the scalar product of a normed complex vector space.
⊢ X = (Base ‘U)    &   ⊢ S = ( ·s ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ X)) → (AS(BSC)) = (BS(ASC)))
Theorem	nvdi 8247	Distributive law for the scalar product of a complex vector space.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    &   ⊢ S = ( ·s ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ ℂ ⋀ B ∈ X ⋀ C ∈ X)) → (AS(BGC)) = ((ASB)G(ASC)))
Theorem	nvdir 8248	Distributive law for the scalar product of a complex vector space.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    &   ⊢ S = ( ·s ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ X)) → ((A + B)SC) = ((ASC)G(BSC)))
Theorem	nv2 8249	A vector plus itself is two times the vector.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    &   ⊢ S = ( ·s ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X) → (AGA) = (2SA))
Theorem	vsfval 8250	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 8251	Closure law for the zero vector of a normed complex vector space.
⊢ X = (Base ‘U)    &   ⊢ Z = (0v ‘U)    ⇒   ⊢ (U ∈ NrmCVec → Z ∈ X)
Theorem	nv0rid 8252	The zero vector is a right identity element.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    &   ⊢ Z = (0v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X) → (AGZ) = A)
Theorem	nv0lid 8253	The zero vector is a left identity element.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    &   ⊢ Z = (0v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X) → (ZGA) = A)
Theorem	nv0 8254	Zero times a vector is the zero vector.
⊢ X = (Base ‘U)    &   ⊢ S = ( ·s ‘U)    &   ⊢ Z = (0v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X) → (0SA) = Z)
Theorem	nvsz 8255	Anything times the zero vector is the zero vector.
⊢ S = ( ·s ‘U)    &   ⊢ Z = (0v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ ℂ) → (ASZ) = Z)
Theorem	nvinv 8256	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 ∈ NrmCVec ⋀ A ∈ X) → (-1SA) = (M ‘A))
Theorem	invfval 8257	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 ∘ ◡(2nd ↾ ({-1} × V)))    ⇒   ⊢ (U ∈ NrmCVec → N = (inv ‘G))
Theorem	nvm 8258	Vector subtraction in terms of group division operation.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    &   ⊢ M = ( −v ‘U)    &   ⊢ N = ( /g ‘G)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X ⋀ B ∈ X) → (AMB) = (ANB))
Theorem	nvmval 8259	Value of vector subtraction on a normed complex vector space.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    &   ⊢ S = ( ·s ‘U)    &   ⊢ M = ( −v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X ⋀ B ∈ X) → (AMB) = (AG(-1SB)))
Theorem	nvmfval 8260	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 ∈ NrmCVec → M = {⟨⟨x, y⟩, z⟩∣((x ∈ X ⋀ y ∈ X) ⋀ z = (xG(-1Sy)))})
Theorem	nvzs 8261	Two ways to express the negative of a vector.
⊢ X = (Base ‘U)    &   ⊢ M = ( −v ‘U)    &   ⊢ S = ( ·s ‘U)    &   ⊢ Z = (0v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X) → (ZMA) = (-1SA))
Theorem	nvmf 8262	Mapping for the vector subtraction operation.
⊢ X = (Base ‘U)    &   ⊢ M = ( −v ‘U)    ⇒   ⊢ (U ∈ NrmCVec → M:(X × X)–→X)
Theorem	nvmcl 8263	Closure law for the vector subtraction operation of a normed complex vector space.
⊢ X = (Base ‘U)    &   ⊢ M = ( −v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X ⋀ B ∈ X) → (AMB) ∈ X)
Theorem	nvnnncan1 8264	Vector space analog of nnncan1t 5479.
⊢ X = (Base ‘U)    &   ⊢ M = ( −v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → ((AMB)M(AMC)) = (CMB))
Theorem	nvnnncan2 8265	Vector space analog of nnncan2t 5480.
⊢ X = (Base ‘U)    &   ⊢ M = ( −v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → ((AMC)M(BMC)) = (AMB))
Theorem	nvmdi 8266	Distributive law for scalar product over subtraction.
⊢ X = (Base ‘U)    &   ⊢ M = ( −v ‘U)    &   ⊢ S = ( ·s ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ ℂ ⋀ B ∈ X ⋀ C ∈ X)) → (AS(BMC)) = ((ASB)M(ASC)))
Theorem	nvnegneg 8267	Double negative of a vector.
⊢ X = (Base ‘U)    &   ⊢ S = ( ·s ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X) → (-1S(-1SA)) = A)
Theorem	nvmul0or 8268	If a scalar product is zero, one of its factors must be zero.
⊢ X = (Base ‘U)    &   ⊢ S = ( ·s ‘U)    &   ⊢ Z = (0v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ ℂ ⋀ B ∈ X) → ((ASB) = Z ↔ (A = 0 ⋁ B = Z)))
Theorem	nvrinv 8269	A vector minus itself.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    &   ⊢ S = ( ·s ‘U)    &   ⊢ Z = (0v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X) → (AG(-1SA)) = Z)
Theorem	nvlinv 8270	Minus a vector plus itself.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    &   ⊢ S = ( ·s ‘U)    &   ⊢ Z = (0v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X) → ((-1SA)GA) = Z)
Theorem	nvsubadd 8271	Relationship between vector subtraction and addition.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    &   ⊢ M = ( −v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → ((AMB) = C ↔ (BGC) = A))
Theorem	nvpncan2 8272	Cancellation law for vector subtraction.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    &   ⊢ M = ( −v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X ⋀ B ∈ X) → ((AGB)MA) = B)
Theorem	nvpncan 8273	Cancellation law for vector subtraction.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    &   ⊢ M = ( −v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X ⋀ B ∈ X) → ((AGB)MB) = A)
Theorem	nvaddsubass 8274	Associative-type law for vector addition and subtraction.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    &   ⊢ M = ( −v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → ((AGB)MC) = (AG(BMC)))
Theorem	nvaddsub 8275	Commutative/associative law for vector addition and subtraction.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    &   ⊢ M = ( −v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → ((AGB)MC) = ((AMC)GB))
Theorem	nvnpcan 8276	Cancellation law for a normed complex vector space.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    &   ⊢ M = ( −v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X ⋀ B ∈ X) → ((AMB)GB) = A)
Theorem	nvaddsub4 8277	Rearrangement of 4 terms in a mixed vector addition and subtraction.
⊢ X = (Base ‘U)    &   ⊢ G = ( +v ‘U)    &   ⊢ M = ( −v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ X ⋀ B ∈ X) ⋀ (C ∈ X ⋀ D ∈ X)) → ((AGB)M(CGD)) = ((AMC)G(BMD)))
Theorem	nvsubsub23 8278	Swap subtrahend and result of vector subtraction.
⊢ X = (Base ‘U)    &   ⊢ M = ( −v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → ((AMB) = C ↔ (AMC) = B))
Theorem	nvnncan 8279	Cancellation law for a normed complex vector space.
⊢ X = (Base ‘U)    &   ⊢ M = ( −v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X ⋀ B ∈ X) → (AM(AMB)) = B)
Theorem	nvmeq0 8280	The difference between two vectors is zero iff they are equal.
⊢ X = (Base ‘U)    &   ⊢ M = ( −v ‘U)    &   ⊢ Z = (0v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X ⋀ B ∈ X) → ((AMB) = Z ↔ A = B))
Theorem	nvmid 8281	A vector minus itself is the zero vector.
⊢ X = (Base ‘U)    &   ⊢ M = ( −v ‘U)    &   ⊢ Z = (0v ‘U)    ⇒   ⊢ ((U ∈ NrmCVec ⋀ A ∈ X) → (AMA) = Z)
Theorem	nvf 8282