mmtheorems156 - 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-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19026

Statement List for Metamath Proof Explorer - 15501-15600 - Page 156 of 191

Type	Label	Description
Statement
Theorem	ltrset 15501	A left translation is a set.
|- F = (x e. X |-> (AGx))   &   |- X = ran G   =>   |- (G e. GrpOp -> F e. _V)
Theorem	ltrran2 15502	The range of a left translation. The term A is a constant.
|- F = (x e. X |-> (AGx))   &   |- X = ran G   =>   |- ((G e. GrpOp /\ A e. X) -> ran F = X)
Theorem	ltrooo 15503	A left translation is a bijection. The term A is a constant.
|- F = (x e. X |-> (AGx))   &   |- X = ran G   =>   |- ((G e. GrpOp /\ A e. X) -> F:X-1-1-onto->X)
Theorem	ltrcmp 15504	Left translation expressed as a composite.
|- F = (x e. X |-> (AGx))   &   |- X = ran G   =>   |- ((G e. GrpOp /\ A e. X) -> F = (G o. {<.x, y>. | (x e. X /\ y = <.A, x>.)}))
Theorem	ltrinvlem 15505	The converse of a left translation. The term A is a constant.
|- F = (x e. X |-> (AGx))   &   |- X = ran G   &   |- D = ( /g ` G)   &   |- N = (inv` G)   =>   |- ((G e. GrpOp /\ A e. X) -> `'F = (x e. X |-> ((N` A)Gx)))
Theorem	cmpltr 15506	Composite of two left translations. The terms A and B are constant. Don't use. See cmpltr2 15507.
|- F = (x e. X |-> (AGx))   &   |- X = ran G   &   |- H = (x e. X |-> (BGx))   =>   |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (F o. H) = (x e. X |-> ((AGB)Gx)))
Theorem	cmpltr2 15507	Composite of two left translations. The terms A and B are constant.
|- F = (x e. X |-> (AGx))   &   |- X = ran G   &   |- H = (x e. X |-> (BGx))   =>   |- ((G e. GrpOp /\ A e. X /\ B e. X) -> (F o. H) = (x e. X |-> ((AGB)Gx)))
Theorem	reptertr2 15508	Replacement of x by the term A in a translation. B is a constant. Note that x and y can be the same.
|- F = (y e. X |-> (yGB))   &   |- H = (x e. X |-> A)   &   |- A e. _V   =>   |- (A.x e. X A e. X -> (F o. H) = (x e. X |-> (AGB)))
Theorem	reptertr3 15509	Replacement of x by the term A in a translation. B is a constant. Note that x and y can be the same.
|- F = (y e. X |-> (BGy))   &   |- H = (x e. X |-> A)   &   |- A e. _V   =>   |- (A.x e. X A e. X -> (F o. H) = (x e. X |-> (BGA)))
Theorem	reptertr4 15510	Replacement of x by the term A in a translation. B and C are constant.
|- F = (y e. X |-> ((BGy)GC))   &   |- H = (x e. X |-> A)   &   |- A e. _V   =>   |- (A.x e. X A e. X -> (F o. H) = (x e. X |-> ((BGA)GC)))
Theorem	cmperltr 15511	A right and left translation expressed as a composite. Note that x and y can't be the same.
|- F = (x e. X |-> ((AGx)GB))   &   |- E = (y e. X |-> (AGy))   &   |- H = (x e. X |-> (xGB))   &   |- X = ran G   =>   |- ((G e. GrpOp /\ A e. X /\ B e. X) -> F = (E o. H))
Theorem	cmprltr 15512	Composite of two right and left translations. Note that x and y can't be the same. See cmprltr2 15513 for a more general version.
|- F = (y e. X |-> ((AGy)GC))   &   |- E = (x e. X |-> ((BGx)GD))   &   |- X = ran G   =>   |- ((G e. GrpOp /\ (A e. X /\ B e. X) /\ (C e. X /\ D e. X)) -> (F o. E) = (x e. X |-> (((AGB)Gx)G(DGC))))
Theorem	cmprltr2 15513	Composite of two right and left translations. No restriction: x and z can be equal.
|- F = (z e. X |-> ((AGz)GC))   &   |- E = (x e. X |-> ((BGx)GD))   &   |- X = ran G   =>   |- ((G e. GrpOp /\ (A e. X /\ B e. X) /\ (C e. X /\ D e. X)) -> (F o. E) = (x e. X |-> (((AGB)Gx)G(DGC))))
Theorem	rltrdom 15514	The domain of a right and left translation.
|- F = (x e. X |-> ((AGx)GB))   &   |- X = ran G   =>   |- dom F = X
Theorem	rltrset 15515	A right and left translation is a set.
|- F = (x e. X |-> ((AGx)GB))   &   |- X = ran G   =>   |- (G e. GrpOp -> F e. _V)
Theorem	rltrran 15516	The range of a right and left translation. Note that A and B are constant.
|- F = (x e. X |-> ((AGx)GB))   &   |- X = ran G   =>   |- ((G e. GrpOp /\ A e. X /\ B e. X) -> ran F = X)
Theorem	rltrooo 15517	A right and left translation is a bijection.
|- F = (x e. X |-> ((AGx)GB))   &   |- X = ran G   =>   |- ((G e. GrpOp /\ A e. X /\ B e. X) -> F:X-1-1-onto->X)
Fields and Rings
Theorem	com2i 15518	Property of a commutative structure with two operation.
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   =>   |- (R e. Com2 -> A.a e. X A.b e. X (aHb) = (bHa))
Theorem	rngmgmbs3 15519	The domain of the first variable of an internal operation with a left and right identity element equals its base set.
|- ((G:(X X. X)-->X /\ E.u e. X A.x e. X ((xGu) = x /\ (uGx) = x)) -> dom dom G = X)
Theorem	rngdmdmrn 15520	In a unital ring the range of the multiplication equals the domain of the first variable.
|- H = (2nd` R)   =>   |- (R e. RingOps -> dom dom H = ran H)
Theorem	rnplrnml3 15521	In a unital ring the domain of the first operand of the addition equals the domain of the second operand of the addition.
|- G = (1st` R)   =>   |- (R e. RingOps -> dom dom G = ran dom G)
Theorem	ununr 15522	The unit of a unital ring is unique.
|- H = (2nd` R)   &   |- X = ran (1st` R)   =>   |- (R e. RingOps -> E!x e. X A.y e. X ((yHx) = y /\ (xHy) = y))
Theorem	rnginvcl 15523	The additive inverse of a unital ring element pertains to the unital ring.
|- X = ran G   &   |- N = (inv` G)   =>   |- ((<.G, H>. e. RingOps /\ A e. X) -> (N` A) e. X)
Theorem	multinv 15524	Multiplication by an additive inverse.
|- X = ran G   &   |- G = (1st` R)   &   |- H = (2nd` R)   =>   |- ((R e. RingOps /\ A e. X /\ B e. X) -> (((inv` G)` A)HB) = ((inv` G)` (AHB)))
Theorem	multinvb 15525	Multiplication by an additive inverse.
|- X = ran G   &   |- G = (1st` R)   &   |- H = (2nd` R)   =>   |- ((R e. RingOps /\ A e. X /\ B e. X) -> (AH((inv` G)` B)) = ((inv` G)` (AHB)))
Theorem	mult2inv 15526	Multiplication of two additive inverses.
|- X = ran G   &   |- G = (1st` R)   &   |- H = (2nd` R)   =>   |- ((R e. RingOps /\ A e. X /\ B e. X) -> (((inv` G)` A)H((inv` G)` B)) = (AHB))
Theorem	rngunval2 15527	The value of the unit of a ring.
|- X = ran (1st` R)   &   |- H = (2nd` R)   &   |- U = (Id` H)   =>   |- (R e. RingOps -> U = U.{u e. X | A.x e. X ((uHx) = x /\ (xHu) = x)})
Theorem	isfld 15528	The predicate "is a field".
|- ((G e. A /\ H e. B) -> (<.G, H>. e. Fld <-> (<.G, H>. e. DivRingOps /\ A.x e. ran GA.y e. ran G(xHy) = (yHx))))
Theorem	fldi 15529	The "axioms" of a field.
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- (R e. Fld -> ((G e. AbelOp /\ H:(X X. X)-->X) /\ (A.x e. X A.y e. X A.z e. X (((xHy)Hz) = (xH(yHz)) /\ (xH(yGz)) = ((xHy)G(xHz)) /\ ((xGy)Hz) = ((xHz)G(yHz))) /\ E.x e. X A.y e. X ((yHx) = y /\ (xHy) = y)) /\ ((H |` ((X \ {Z}) X. (X \ {Z}))) e. GrpOp /\ A.x e. X A.y e. X (xHy) = (yHx))))
Theorem	fldax1 15530	1st "axiom" of a field. The addition is an abelian group.
|- G = (1st` R)   =>   |- (R e. Fld -> G e. AbelOp)
Theorem	fldax2 15531	2nd "axiom" of a field. The multiplication is an internal operation.
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   =>   |- (R e. Fld -> H:(X X. X)-->X)
Theorem	fldax3 15532	3rd "axiom" of a field. The multiplication is associative.
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   =>   |- (R e. Fld -> A.x e. X A.y e. X A.z e. X ((xHy)Hz) = (xH(yHz)))
Theorem	fldax4 15533	4th "axiom" of a field. The multiplication is distributive.
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   =>   |- (R e. Fld -> A.x e. X A.y e. X A.z e. X (xH(yGz)) = ((xHy)G(xHz)))
Theorem	fldax5 15534	5th "axiom" of a field. Existence of a neutral element.
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   =>   |- (R e. Fld -> E.x e. X A.y e. X (yHx) = y)
Theorem	fldax6 15535	6th "axiom" of a field. The multiplication is a group on the underlying set deprived from zero.
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- (R e. Fld -> (H |` ((X \ {Z}) X. (X \ {Z}))) e. GrpOp)
Theorem	fldax7 15536	7th "axiom" of a field. The multiplication is commutative.
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   =>   |- (R e. Fld -> A.x e. X A.y e. X (xHy) = (yHx))
Theorem	zrfld 15537	The zero ring is not a field.
|- A e. B   =>   |- -. <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>. e. Fld
Theorem	zerdivemp1 15538	In a unitary ring a left invertible element is not a zero divisor.
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- Z = (Id` G)   &   |- X = ran G   &   |- U = (Id` H)   =>   |- ((R e. RingOps /\ A e. (X \ Z) /\ E.a e. X (aHA) = U) -> (B e. X -> ((AHB) = Z -> B = Z)))
Theorem	rngridfz 15539	In a unitary ring a left invertible element is different from zero iff 1 =/= 0.
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- Z = (Id` G)   &   |- X = ran G   &   |- U = (Id` H)   =>   |- ((R e. RingOps /\ A e. X /\ E.a e. X (aHA) = U) -> (A =/= Z <-> U =/= Z))
Theorem	zintdom 15540	ZZ is a commutative ring.
|- <. + , x. >. e. (RingOps i^i Com2)
Syntax	ctofld 15541	Extend class notation with the class of all totally ordered fields.
class Tofld
Definition	df-tofld 15542	Definition of a totally ordered field. Experimental.
|- Tofld = {<.<.g, h>., r>. | (<.g, h>. e. Fld /\ (r e. TosetRel /\ U.U.r = ran g) /\ A.x e. U.U.rA.y e. U.U.rA.z e. U.U.r((xry -> (xgz)r(ygz)) /\ ((Id` g)rz -> (xhz)r(yhz))))}
Syntax	czerodiv 15543	Extend class notation with the class of all the zero divisors.
class zeroDiv
Definition	df-zd 15544	Definition of the zero divisors of a ring. Experimental.
|- zeroDiv = {<.r, y>. | y = {a e. ran (1st` r) | (a =/= (Id` (1st` r)) /\ E.b e. ran (1st` r)(b =/= (Id` (1st` r)) /\ (a(2nd` r)b) = (Id` (1st` r))))}}
Generic modules and vector spaces
Syntax	cvec 15545	Extend class notation with the class of all generic vector spaces and modules.
class Vec
Definition	df-vec 15546	Definition of a vector space (<.g, h>. is a field ), or of a module (<.g, h>. is a ring ).
|- Vec = {z | E.gE.hE.aE.b(z = <.<.g, h>., <.a, b>.>. /\ (a e. AbelOp /\ b:(ran g X. ran a)-->ran a /\ A.u e. ran a(((Id` h)bu) = u /\ A.x e. ran g(A.v e. ran a(xb(uav)) = ((xbu)a(xbv)) /\ A.y e. ran g(((xgy)bu) = ((xbu)a(ybu)) /\ ((xhy)bu) = (xb(ybu)))))))}
Theorem	vecval1b 15547	The predicate "is a vector space" or "is a module".
|- X = ran G   &   |- W = ran A   =>   |- (((G e. M /\ H e. N /\ A e. O) /\ B e. P) -> (<.G, H>. Vec <.A, B>. <-> (A e. AbelOp /\ B:(X X. W)-->W /\ A.u e. W (((Id` H)Bu) = u /\ A.x e. X (A.v e. W (xB(uAv)) = ((xBu)A(xBv)) /\ A.y e. X (((xGy)Bu) = ((xBu)A(yBu)) /\ ((xHy)Bu) = (xB(yBu))))))))
Theorem	vecval3b 15548	The "axioms" of a vector space or module.
|- X = ran G   &   |- G = (1st` (1st` R))   &   |- H = (2nd` (1st` R))   &   |- A = (1st` (2nd` R))   &   |- B = (2nd` (2nd` R))   &   |- W = ran A   =>   |- (R e. Vec -> (A e. AbelOp /\ B:(X X. W)-->W /\ A.u e. W (((Id` H)Bu) = u /\ A.x e. X (A.v e. W (xB(uAv)) = ((xBu)A(xBv)) /\ A.y e. X (((xGy)Bu) = ((xBu)A(yBu)) /\ ((xHy)Bu) = (xB(yBu)))))))
Theorem	vecax1 15549	1st "axiom" of a vector space or module. The vector addition is an abelian group.
|- +w = (1st` (2nd` R))   =>   |- (R e. Vec -> +w e. AbelOp)
Theorem	vecax2 15550	2nd "axiom" of a vector space or module. Domain, codomain and functionality of the multiplication of a vector by a scalar.
|- X = ran (1st` (1st` R))   &   |- .w = (2nd` (2nd` R))   &   |- W = ran (1st` (2nd` R))   =>   |- (R e. Vec -> .w :(X X. W)-->W)
Theorem	vecax3 15551	3rd "axiom" of a vector space or module. Multiplication by 1.
|- .w = (2nd` (2nd` R))   &   |- W = ran (1st` (2nd` R))   &   |- 1t = (Id` (2nd` (1st` R)))   =>   |- (R e. Vec -> A.u e. W (1t .w u) = u)
Theorem	vecax4 15552	4th "axiom" of a vector space or module. Multiplication by a scalar distributes over vector addition.
|- X = ran (1st` (1st` R))   &   |- +w = (1st` (2nd` R))   &   |- .w = (2nd` (2nd` R))   &   |- W = ran (1st` (2nd` R))   =>   |- (R e. Vec -> A.u e. W A.x e. X A.v e. W (x.w (u+w v)) = ((x.w u)+w (x.w v)))
Theorem	vecax5 15553	5th "axiom" of a vector space or module. Multiplication by a sum of scalars.
|- X = ran (1st` (1st` R))   &   |- +t = (1st` (1st` R))   &   |- +w = (1st` (2nd` R))   &   |- .w = (2nd` (2nd` R))   &   |- W = ran (1st` (2nd` R))   =>   |- (R e. Vec -> A.u e. W A.x e. X A.y e. X ((x+t y).w u) = ((x.w u)+w (y.w u)))
Theorem	vecax6 15554	6th "axiom" of a vector space or module. Relation between scalar multiplication and vector multiplication.
|- X = ran (1st` (1st` R))   &   |- .t = (2nd` (1st` R))   &   |- .w = (2nd` (2nd` R))   &   |- W = ran (1st` (2nd` R))   =>   |- (R e. Vec -> A.u e. W A.x e. X A.y e. X ((x.t y).w u) = (x.w (y.w u)))
Theorem	vecax5b 15555	Multiplication by a sum of scalars.
|- X = ran (1st` (1st` R))   &   |- +t = (1st` (1st` R))   &   |- +w = (1st` (2nd` R))   &   |- .w = (2nd` (2nd` R))   &   |- W = ran (1st` (2nd` R))   =>   |- ((R e. Vec /\ (U e. W /\ A e. X /\ B e. X)) -> ((A+t B).w U) = ((A.w U)+w (B.w U)))
Theorem	claddinvvec 15556	Closure of the additive inverse of a vector.
|- W = ran (1st` (2nd` R))   &   |- ~w = (inv` (1st` (2nd` R)))   =>   |- ((R e. Vec /\ U e. W) -> (~w ` U) e. W)
Theorem	vec2inv 15557	Double inverse law for vector additive inverse.
|- W = ran (1st` (2nd` R))   &   |- ~w = (inv` (1st` (2nd` R)))   =>   |- ((R e. Vec /\ U e. W) -> (~w ` (~w ` U)) = U)
Theorem	sum2vv 15558	The sum of two vectors is a vector.
|- +w = (1st` (2nd` R))   &   |- W = ran +w    =>   |- ((R e. Vec /\ V1 e. W /\ V2 e. W) -> (V1+w V2) e. W)
Theorem	addnull1 15559	Addition of the null vector.
|- +w = (1st` (2nd` R))   &   |- W = ran +w    &   |- 0w = (Id` +w )   =>   |- ((R e. Vec /\ U e. W) -> (U+w 0w ) = U)
Theorem	addnull2 15560	Addition of the null vector.
|- +w = (1st` (2nd` R))   &   |- W = ran +w    &   |- 0w = (Id` +w )   =>   |- ((R e. Vec /\ U e. W) -> (0w +w U) = U)
Theorem	addvecass 15561	The addition of vectors is associative.
|- +w = (1st` (2nd` R))   &   |- W = ran +w    =>   |- ((R e. Vec /\ (V1 e. W /\ V2 e. W /\ V3 e. W)) -> (V1+w (V2+w V3)) = ((V1+w V2)+w V3))
Theorem	addvecom 15562	The addition of vectors is associative.
|- +w = (1st` (2nd` R))   &   |- W = ran +w    =>   |- ((R e. Vec /\ (V1 e. W /\ V2 e. W)) -> (V1+w V2) = (V2+w V1))
Theorem	invaddvec 15563	Additive inverse of a sum of vectors.
|- +w = (1st` (2nd` R))   &   |- W = ran +w    &   |- ~w = (inv` +w )   =>   |- ((R e. Vec /\ (V1 e. W /\ V2 e. W)) -> (~w ` (V1+w V2)) = ((~w ` V1)+w (~w ` V2)))
Theorem	prodvs 15564	The product of a vector by a scalar is a vector.
|- +w = (1st` (2nd` R))   &   |- .w = (2nd` (2nd` R))   &   |- W = ran +w    &   |- X = ran +t    &   |- +t = (1st` (1st` R))   =>   |- ((R e. Vec /\ A e. X /\ U e. W) -> (A.w U) e. W)
Theorem	vecsrcan 15565	Right cancellation law for vector subtraction.
|- -w = ( /g ` +w )   &   |- W = ran +w    &   |- +w = (1st` (2nd` R))   =>   |- ((R e. Vec /\ (V1 e. W /\ V2 e. W /\ V3 e. W)) -> ((V1-w V3) = (V2-w V3) <-> V1 = V2))
Theorem	vecslcan 15566	Left cancellation law for vector subtraction.
|- -w = ( /g ` +w )   &   |- W = ran +w    &   |- +w = (1st` (2nd` R))   =>   |- ((R e. Vec /\ (V1 e. W /\ V2 e. W /\ V3 e. W)) -> ((V3-w V1) = (V3-w V2) <-> V1 = V2))
Theorem	vwit 15567	A vector minus itself equals zero.
|- 0w = (Id` +w )   &   |- +w = (1st` (2nd` R))   &   |- -w = ( /g ` +w )   &   |- W = ran +w    =>   |- ((R e. Vec /\ U e. W) -> (U-w U) = 0w )
Theorem	sub2vec 15568	Definition of the subtraction of two vectors.
|- 0w = (Id` +w )   &   |- +w = (1st` (2nd` R))   &   |- -w = ( /g ` +w )   &   |- W = ran +w    &   |- ~w = (inv` +w )   =>   |- ((R e. Vec /\ (V1 e. W /\ V2 e. W)) -> (V1-w V2) = (V1+w (~w ` V2)))
Theorem	mvecrtol 15569	Moving a vector from the right member of an equation into the left member.
|- 0w = (Id` +w )   &   |- +w = (1st` (2nd` R))   &   |- -w = ( /g ` +w )   &   |- W = ran +w    =>   |- ((R e. Vec /\ (V1 e. W /\ V2 e. W)) -> (V1 = V2 <-> (V1-w V2) = 0w ))
Theorem	dblsubvec 15570	Double subtraction of vectors.
|- 0w = (Id` +w )   &   |- +w = (1st` (2nd` R))   &   |- -w = ( /g ` +w )   &   |- W = ran +w    =>   |- ((R e. Vec /\ (V1 e. W /\ V2 e. W /\ V3 e. W)) -> ((V1-w V2)-w V3) = (V1-w (V2+w V3)))
Theorem	vecrcan 15571	Right cancellation law for vector addition.
|- 0w = (Id` +w )   &   |- +w = (1st` (2nd` R))   &   |- -w = ( /g ` +w )   &   |- W = ran +w    &   |- +w = (1st` (2nd` R))   &   |- W = ran +w    =>   |- ((R e. Vec /\ (V1 e. W /\ V2 e. W /\ V3 e. W)) -> ((V1+w V3) = (V2+w V3) <-> V1 = V2))
Theorem	veclcan 15572	Left cancellation law for vector addition.
|- 0w = (Id` +w )   &   |- +w = (1st` (2nd` R))   &   |- -w = ( /g ` +w )   &   |- W = ran +w    &   |- +w = (1st` (2nd` R))   &   |- W = ran +w    =>   |- ((R e. Vec /\ (V1 e. W /\ V2 e. W /\ V3 e. W)) -> ((V3+w V1) = (V3+w V2) <-> V1 = V2))
Theorem	mvecrtol2 15573	Moving a vector from the right member of an equation into the left member.
|- 0w = (Id` +w )   &   |- +w = (1st` (2nd` R))   &   |- -w = ( /g ` +w )   &   |- W = ran +w    =>   |- ((R e. Vec /\ (V1 e. W /\ V2 e. W /\ V3 e. W)) -> (V1 = (V2+w V3) <-> (V1-w V2) = V3))
Theorem	prvs 15574	The product of a vector by a scalar is a vector.
|- X = ran (1st` (1st` R))   &   |- W = ran (1st` (2nd` R))   &   |- .w = (2nd` (2nd` R))   =>   |- ((R e. Vec /\ A e. X /\ U e. W) -> (A.w U) e. W)
Theorem	mulveczer 15575	Multiplication of a vector by zero.
|- W = ran (1st` (2nd` R))   &   |- 0t = (Id` +t )   &   |- +t = (1st` (1st` R))   &   |- .t = (2nd` (1st` R))   &   |- .w = (2nd` (2nd` R))   &   |- 0w = (Id` (1st` (2nd` R)))   =>   |- ((R e. Vec /\ <.+t , .t >. e. RingOps /\ U e. W) -> (0t .w U) = 0w )
Theorem	mulinvsca 15576	Multiplication by the inverse of a scalar.
|- X = ran +t    &   |- W = ran (1st` (2nd` R))   &   |- .w = (2nd` (2nd` R))   &   |- ~t = (inv` +t )   &   |- ~w = (inv` (1st` (2nd` R)))   &   |- +t = (1st` (1st` R))   &   |- .t = (2nd` (1st` R))   =>   |- ((R e. Vec /\ <.+t , .t >. e. RingOps /\ (A e. X /\ U e. W)) -> ((~t ` A).w U) = (~w ` (A.w U)))
Theorem	muldisc 15577	Multiplication by a difference of scalars.
|- X = ran (1st` (1st` R))   &   |- +t = (1st` (1st` R))   &   |- +w = (1st` (2nd` R))   &   |- .w = (2nd` (2nd` R))   &   |- W = ran (1st` (2nd` R))   &   |- -t = ( /g ` +t )   &   |- -w = ( /g ` +w )   &   |- .t = (2nd` (1st` R))   =>   |- ((R e. Vec /\ <.+t , .t >. e. RingOps) -> A.u e. W A.x e. X A.y e. X ((x-t y).w u) = ((x.w u)-w (y.w u)))
Theorem	vecax5c 15578	Multiplication by a difference of scalars.
|- X = ran +t    &   |- +t = (1st` (1st` R))   &   |- -t = ( /g ` +t )   &   |- +w = (1st` (2nd` R))   &   |- -w = ( /g ` +w )   &   |- .w = (2nd` (2nd` R))   &   |- W = ran +w    &   |- .t = (2nd` (1st` R))   =>   |- ((R e. Vec /\ <.+t , .t >. e. RingOps) -> ((U e. W /\ A e. X /\ B e. X) -> ((A-t B).w U) = ((A.w U)-w (B.w U))))
Theorem	svli2 15579	If a finite sequence of vectors U(k) are linearly independant, two combinations of those vectors are equal iff the scalars are equal.
|- X = ran +t    &   |- 0t = (Id` +t )   &   |- +t = (1st` (1st` R))   &   |- .t = (2nd` (1st` R))   &   |- 0w = (Id` +w )   &   |- +w = (1st` (2nd` R))   &   |- W = ran +w    &   |- .w = (2nd` (2nd` R))   =>   |- (((R e. Vec /\ <.+t , .t >. e. RingOps /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> (prod_k e. (1...N)+w (S1.w U) = prod_k e. (1...N)+w (S2.w U) <-> A.k e. (1...N)S1 = S2))
Syntax	csvec 15580	Extend class notation with the class of all generic subspace vector spaces and modules.
class SubVec
Definition	df-svs 15581	A sub-vector space v of a vector space x is a vector space that has the same scalar set than x, whose addition and whose multiplication are restrictions of those of x.
|- SubVec = {<.x, y>. | (x e. Vec /\ y = {v e. Vec | ((1st` v) = (1st` x) /\ (1st` (2nd` v)) C_ (1st` (2nd` x)) /\ (2nd` (2nd` v)) = ((2nd` (2nd` x)) |` (ran (1st` (1st` x)) X. ran (1st` (2nd` v)))))})}
Theorem	svs2 15582	A textbook definition. A sub-vector space of a vector space x is a subset that is itself a vector space under the inherited operations.
|- SubVec = {<.x, y>. | (x e. Vec /\ y = {v e. Vec | ((1st` v) = (1st` x) /\ E.w e. ~P ran (1st` (2nd` x))((1st` (2nd` v)) = ((1st` (2nd` x)) |` (w X. w)) /\ (2nd` (2nd` v)) = ((2nd` (2nd` x)) |` (ran (1st` (1st` x)) X. w))))})}
Theorem	svs3 15583	A very concise definition of a subspace of a vector space.
|- SubVec = {<.x, y>. | (x e. Vec /\ y = {v e. Vec | ((1st` v) = (1st` x) /\ (1st` (2nd` v)) C_ (1st` (2nd` x)) /\ (2nd` (2nd` v)) C_ (2nd` (2nd` x)))})}
Real vector spaces
Syntax	cvr 15584	Extend class notation with the class of all real vector spaces.
class RVec
Definition	df-vr 15585	Define the class of all real vector spaces. The definition of a RVec and a CVec don't much differ. There may be a way to get both in only one definition. A RVec seems mandatory if one wants to do classical cartesian geometry. We can't use a CVec instead. Changing the field changes important properties such as the dimension.
|- RVec = {<.g, s>. | (g e. AbelOp /\ s:(RR X. ran g)-->ran g /\ A.x e. ran g((1sx) = x /\ A.y e. RR (A.z e. ran g(ys(xgz)) = ((ysx)g(ysz)) /\ A.z e. RR (((y + z)sx) = ((ysx)g(zsx)) /\ ((y x. z)sx) = (ys(zsx))))))}
Theorem	vrrel 15586	The class of all real vector spaces is a relation.
|- Rel RVec
Theorem	vri 15587	The properties of a real 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 real 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. RVec -> (G e. AbelOp /\ S:(RR X. X)-->X /\ A.x e. X ((1Sx) = x /\ A.y e. RR (A.z e. X (yS(xGz)) = ((ySx)G(ySz)) /\ A.z e. RR (((y + z)Sx) = ((ySx)G(zSx)) /\ ((y x. z)Sx) = (yS(zSx)))))))
Matrices
Syntax	cmmat 15588	Addition of matrices.
class +m
Syntax	csmat 15589	Scalar multiplication of matrices.
class .m
Syntax	cxmat 15590	Multiplication of matrices.
class xm
Definition	df-amat 15591	Matrix addition. Meaningful if g is a Magma (a binary internal operation) at least. Experimental.
|- +m = {<.g, h>. | h = {<.<.m, n>., o>. | E.j e. NN E.k e. NN (m:((1...j) X. (1...k))-->dom dom g /\ n:((1...j) X. (1...k))-->dom dom g /\ o = (x e. (1...j), y e. (1...k) |-> ((m` <.x, y>.)g(n` <.x, y>.))))}}
Definition	df-smat 15592	Matrix left scalar multiplication. Meaningful if g is a binary external operation. Experimental.
|- .m = {<.g, h>. | h = {<.<.m, a>., o>. | E.j e. NN E.k e. NN (m:((1...j) X. (1...k))-->ran dom g /\ a e. dom dom g /\ o = (x e. (1...j), y e. (1...k) |-> (ag(m` <.x, y>.))))}}
Definition	df-mmat 15593	Matrix multiplication. Meaningful if <.g, h>. is a ring at least. prod3 here should be sum_ (to be traditional). But in set.mm sum_ is CC oriented and has a limit definition embedded and thus doesn't fit the needs of this generic definition. Experimental.
|- xm = {<.<.g, h>., f>. | f = {<.<.m, n>., o>. | E.j e. NN E.k e. NN E.l e. NN (m:((1...j) X. (1...k))-->dom dom g /\ n:((1...k) X. (1...l))-->dom dom g /\ o = (x e. (1...j), y e. (1...l) |-> prod3 z e. (1...k)g((m` <.x, z>.)h(n` <.z, y>.))))}}
Affine spaces
Syntax	raffsp 15594	Extend class notation with the class of all R affine spaces.
class RAffSp
Definition	df-raffsp 15595	Define a RR affine space id est a RR vector space x ( called the free vectors class ) together with a function y. y associates to each vector a bijection from a set t (called the space) to itself (here t is retrieved from the operation.) Technically speaking, y is a faithful (i.e. injective) and transitive group action (id est a group homomorphism whose range is the underlying set of a symmetry group ). Informally speaking the aim of all of that is to associate to each point of t a unique point of t through the "action" of a vector of x and thus to formalize the idea of translation. When we have embedded the idea of translation it is easy to define a repere and thus all the cartesian geometry is available.
|- RAffSp = {<.x, y>. | (x e. RVec /\ E.t(y e. ((1st` x) GrpHom (SymGrp` t)) /\ y:ran (1st` x)-1-1->t /\ A.a e. t A.b e. t E.v e. ran (1st` x)((y` v)` a) = b))}
Intervals of reals and extended reals
Theorem	iooirrsa 15596	An open interval is included in RR if A and B belong to RR*.
|- ((A e. RR* /\ B e. RR*) -> (A(,)B) C_ RR)
Theorem	clsrebb 15597	A closed interval is a set of extended reals.
|- (B e. _V -> (A[,]B) C_ RR*)
Theorem	bsi 15598	Membership to the set of open intervals implied the existence of two bounds in the set of the extended reals.
|- (A e. ran (,) -> E.x e. RR* E.y e. RR* A = (x(,)y))
Theorem	elioo1t3 15599	If an open interval has an element, then A < B.
|- (C e. (A(,)B) -> A < B)
Theorem	oisbmi 15600	An open interval with its upper bound equal to -oo is empty.
|- (A(,) -oo) = (/)