:: Subspaces and Cosets of Subspaces in Vector Space
:: by Wojciech A. Trybulec
::
:: Received July 27, 1990
:: Copyright (c) 1990-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RLVECT_1, ALGSTR_0, BINOP_1, VECTSP_1, LATTICES, XBOOLE_0,
SUBSET_1, ARYTM_1, RELAT_1, ARYTM_3, RLSUB_1, SUPINF_2, GROUP_1,
STRUCT_0, TARSKI, REALSET1, ZFMISC_1, FUNCT_1, MESFUNC1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, REALSET1, FUNCT_1,
FUNCT_2, STRUCT_0, ALGSTR_0, DOMAIN_1, BINOP_1, RLVECT_1, GROUP_1,
VECTSP_1;
constructors PARTFUN1, BINOP_1, REALSET1, VECTSP_1, RLVECT_1, RELSET_1,
GROUP_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, REALSET1, STRUCT_0, VECTSP_1,
RELAT_1, ALGSTR_0;
requirements SUBSET, BOOLE;
begin
reserve x,y,y1,y2 for object;
definition
let GF be non empty multMagma;
let V be non empty ModuleStr over GF;
let V1 be Subset of V;
attr V1 is linearly-closed means
:: VECTSP_4:def 1
(for v,u being Element of V st v in
V1 & u in V1 holds v + u in V1) & for a being Element of GF, v being Element of
V st v in V1 holds a * v in V1;
end;
theorem :: VECTSP_4:1
for GF be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr, V be
Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over GF, V1 be Subset of V st V1 <> {} & V1 is linearly-closed
holds 0.V in V1;
theorem :: VECTSP_4:2
for GF be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr, V be
Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over GF, V1 be Subset of V st V1 is linearly-closed for v
being Element of V st v in V1 holds - v in V1;
theorem :: VECTSP_4:3
for GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF, V1 be Subset of V st V1 is linearly-closed for v,u being
Element of V st v in V1 & u in V1 holds v - u in V1;
theorem :: VECTSP_4:4
for GF be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr, V be
Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over GF holds {0.V} is linearly-closed;
theorem :: VECTSP_4:5
for GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF, V1 be Subset of V st the carrier of V = V1 holds V1 is
linearly-closed;
theorem :: VECTSP_4:6
for GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF, V1,V2,V3 be Subset of V st V1 is linearly-closed & V2 is
linearly-closed & V3 = {v + u where v is Element of V, u is Element of V : v in
V1 & u in V2} holds V3 is linearly-closed;
theorem :: VECTSP_4:7
for GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF, V1,V2 be Subset of V st V1 is linearly-closed & V2 is
linearly-closed holds V1 /\ V2 is linearly-closed;
definition
let GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF;
mode Subspace of V -> Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over GF means
:: VECTSP_4:def 2
the
carrier of it c= the carrier of V & 0.it = 0.V & the addF of it = (the addF of
V)||the carrier of it & the lmult of it = (the lmult of V) |([:the carrier of
GF, the carrier of it:] qua set);
end;
reserve GF for add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr,
V,X,Y for Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over GF;
reserve a for Element of GF;
reserve u,u1,u2,v,v1,v2 for Element of V;
reserve W,W1,W2 for Subspace of V;
reserve V1 for Subset of V;
reserve w,w1,w2 for Element of W;
theorem :: VECTSP_4:8
x in W1 & W1 is Subspace of W2 implies x in W2;
theorem :: VECTSP_4:9
x in W implies x in V;
theorem :: VECTSP_4:10
w is Element of V;
theorem :: VECTSP_4:11
0.W = 0.V;
theorem :: VECTSP_4:12
0.W1 = 0.W2;
theorem :: VECTSP_4:13
w1 = v & w2 = u implies w1 + w2 = v + u;
theorem :: VECTSP_4:14
w = v implies a * w = a * v;
theorem :: VECTSP_4:15
w = v implies - v = - w;
theorem :: VECTSP_4:16
w1 = v & w2 = u implies w1 - w2 = v - u;
theorem :: VECTSP_4:17
0.V in W;
theorem :: VECTSP_4:18
0.W1 in W2;
theorem :: VECTSP_4:19
0.W in V;
theorem :: VECTSP_4:20
u in W & v in W implies u + v in W;
theorem :: VECTSP_4:21
v in W implies a * v in W;
theorem :: VECTSP_4:22
v in W implies - v in W;
theorem :: VECTSP_4:23
u in W & v in W implies u - v in W;
theorem :: VECTSP_4:24
V is Subspace of V;
theorem :: VECTSP_4:25
for X,V being strict Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over GF holds V is
Subspace of X & X is Subspace of V implies V = X;
theorem :: VECTSP_4:26
V is Subspace of X & X is Subspace of Y implies V is Subspace of Y;
theorem :: VECTSP_4:27
the carrier of W1 c= the carrier of W2 implies W1 is Subspace of W2;
theorem :: VECTSP_4:28
(for v st v in W1 holds v in W2) implies W1 is Subspace of W2;
registration
let GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF;
cluster strict for Subspace of V;
end;
theorem :: VECTSP_4:29
for W1,W2 being strict Subspace of V st the carrier of W1 = the
carrier of W2 holds W1 = W2;
theorem :: VECTSP_4:30
for W1,W2 being strict Subspace of V st (for v holds v in W1 iff
v in W2) holds W1 = W2;
theorem :: VECTSP_4:31
for V being strict Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over GF, W being strict
Subspace of V holds the carrier of W = the carrier of V implies W = V;
theorem :: VECTSP_4:32
for V being strict Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over GF, W being strict
Subspace of V holds (for v being Element of V holds v in W) implies W = V;
theorem :: VECTSP_4:33
the carrier of W = V1 implies V1 is linearly-closed;
theorem :: VECTSP_4:34
V1 <> {} & V1 is linearly-closed implies ex W being strict
Subspace of V st V1 = the carrier of W;
definition
let GF;
let V;
func (0).V -> strict Subspace of V means
:: VECTSP_4:def 3
the carrier of it = {0.V};
end;
definition
let GF;
let V;
func (Omega).V -> strict Subspace of V equals
:: VECTSP_4:def 4
the ModuleStr of V;
end;
theorem :: VECTSP_4:35
x in (0).V iff x = 0.V;
theorem :: VECTSP_4:36
(0).W = (0).V;
theorem :: VECTSP_4:37
(0).W1 = (0).W2;
theorem :: VECTSP_4:38
(0).W is Subspace of V;
theorem :: VECTSP_4:39
(0).V is Subspace of W;
theorem :: VECTSP_4:40
(0).W1 is Subspace of W2;
theorem :: VECTSP_4:41
for V being Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over GF holds V is
Subspace of (Omega).V;
definition
let GF;
let V;
let v,W;
func v + W -> Subset of V equals
:: VECTSP_4:def 5
{v + u : u in W};
end;
definition
let GF;
let V;
let W;
mode Coset of W -> Subset of V means
:: VECTSP_4:def 6
ex v st it = v + W;
end;
reserve B,C for Coset of W;
theorem :: VECTSP_4:42
x in v + W iff ex u st u in W & x = v + u;
theorem :: VECTSP_4:43
0.V in v + W iff v in W;
theorem :: VECTSP_4:44
v in v + W;
theorem :: VECTSP_4:45
0.V + W = the carrier of W;
theorem :: VECTSP_4:46
v + (0).V = {v};
theorem :: VECTSP_4:47
v + (Omega).V = the carrier of V;
theorem :: VECTSP_4:48
0.V in v + W iff v + W = the carrier of W;
theorem :: VECTSP_4:49
v in W iff v + W = the carrier of W;
theorem :: VECTSP_4:50
v in W implies (a * v) + W = the carrier of W;
theorem :: VECTSP_4:51
for GF being Field, V being VectSp of GF, a being Element of GF,
v being Element of V, W being Subspace of V st a <> 0.GF & (a * v) + W = the
carrier of W holds v in W;
theorem :: VECTSP_4:52
for GF being Field, V being VectSp of GF, v being Element of V, W
being Subspace of V holds v in W iff - v + W = the carrier of W;
theorem :: VECTSP_4:53
u in W iff v + W = (v + u) + W;
theorem :: VECTSP_4:54
u in W iff v + W = (v - u) + W;
theorem :: VECTSP_4:55
v in u + W iff u + W = v + W;
theorem :: VECTSP_4:56
u in v1 + W & u in v2 + W implies v1 + W = v2 + W;
theorem :: VECTSP_4:57
for GF being Field, V being VectSp of GF, a being Element of GF, v
being Element of V, W being Subspace of V st a <> 1_GF & a * v in v + W holds v
in W;
theorem :: VECTSP_4:58
v in W implies a * v in v + W;
theorem :: VECTSP_4:59
v in W implies - v in v + W;
theorem :: VECTSP_4:60
u + v in v + W iff u in W;
theorem :: VECTSP_4:61
v - u in v + W iff u in W;
theorem :: VECTSP_4:62
u in v + W iff ex v1 st v1 in W & u = v - v1;
theorem :: VECTSP_4:63
(ex v st v1 in v + W & v2 in v + W) iff v1 - v2 in W;
theorem :: VECTSP_4:64
v + W = u + W implies ex v1 st v1 in W & v + v1 = u;
theorem :: VECTSP_4:65
v + W = u + W implies ex v1 st v1 in W & v - v1 = u;
theorem :: VECTSP_4:66
for W1,W2 being strict Subspace of V holds v + W1 = v + W2 iff W1 = W2;
theorem :: VECTSP_4:67
for W1,W2 being strict Subspace of V st v + W1 = u + W2 holds W1 = W2;
theorem :: VECTSP_4:68
ex C st v in C;
theorem :: VECTSP_4:69
C is linearly-closed iff C = the carrier of W;
theorem :: VECTSP_4:70
for W1,W2 being strict Subspace of V, C1 being Coset of W1, C2 being
Coset of W2 st C1 = C2 holds W1 = W2;
theorem :: VECTSP_4:71
{v} is Coset of (0).V;
theorem :: VECTSP_4:72
V1 is Coset of (0).V implies ex v st V1 = {v};
theorem :: VECTSP_4:73
the carrier of W is Coset of W;
theorem :: VECTSP_4:74
the carrier of V is Coset of (Omega).V;
theorem :: VECTSP_4:75
V1 is Coset of (Omega).V implies V1 = the carrier of V;
theorem :: VECTSP_4:76
0.V in C iff C = the carrier of W;
theorem :: VECTSP_4:77
u in C iff C = u + W;
theorem :: VECTSP_4:78
u in C & v in C implies ex v1 st v1 in W & u + v1 = v;
theorem :: VECTSP_4:79
u in C & v in C implies ex v1 st v1 in W & u - v1 = v;
theorem :: VECTSP_4:80
(ex C st v1 in C & v2 in C) iff v1 - v2 in W;
theorem :: VECTSP_4:81
u in B & u in C implies B = C;
::
:: Auxiliary theorems.
::
theorem :: VECTSP_4:82
for GF be add-associative right_zeroed right_complementable Abelian
commutative associative well-unital distributive non empty doubleLoopStr, V
be Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over GF, a,b being Element of GF, v being Element of V holds (
a - b) * v = a * v - b * v;