Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Subspaces and Cosets of Subspaces in Vector Space

by
Wojciech A. Trybulec

MML identifier: VECTSP_4
[ Mizar article, MML identifier index ]

```environ

vocabulary RLVECT_1, VECTSP_1, ARYTM_1, BINOP_1, LATTICES, RLSUB_1, BOOLE,
RELAT_1, FUNCT_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
STRUCT_0, DOMAIN_1, BINOP_1, RLVECT_1, VECTSP_1;
constructors GROUP_2, DOMAIN_1, BINOP_1, PARTFUN1, MEMBERED, XBOOLE_0;
clusters FUNCT_1, VECTSP_1, STRUCT_0, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1,
XBOOLE_0;
requirements SUBSET, BOOLE;

begin

reserve x,y,y1,y2 for set;

definition let GF be non empty HGrStr; let V be non empty VectSpStr over GF;
let V1 be Subset of V;
attr V1 is lineary-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;

canceled 3;

theorem :: VECTSP_4:4
for GF be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr),
right_complementable VectSp-like (non empty VectSpStr over GF),
V1 be Subset of V
st V1 <> {} & V1 is lineary-closed holds 0.V in V1;

theorem :: VECTSP_4:5
for GF be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr),
right_complementable VectSp-like (non empty VectSpStr over GF),
V1 be Subset of V
st V1 is lineary-closed
for v being Element of V st v in V1 holds - v in V1;

theorem :: VECTSP_4:6
for GF be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr),
right_complementable VectSp-like (non empty VectSpStr over GF),
V1 be Subset of V
st V1 is lineary-closed
for v,u being Element of V
st v in V1 & u in V1 holds v - u in V1;

theorem :: VECTSP_4:7
for GF be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr),
right_complementable VectSp-like (non empty VectSpStr over GF)
holds {0.V} is lineary-closed;

theorem :: VECTSP_4:8
for GF be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr),
right_complementable VectSp-like (non empty VectSpStr over GF),
V1 be Subset of V
st the carrier of V = V1 holds V1 is lineary-closed;

theorem :: VECTSP_4:9
for GF be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr),
right_complementable VectSp-like (non empty VectSpStr over GF),
V1,V2,V3 be Subset of V
st V1 is lineary-closed & V2 is lineary-closed &
V3 = {v + u where
v is Element of V,
u is Element of V
: v in V1 & u in V2}
holds V3 is lineary-closed;

theorem :: VECTSP_4:10
for GF be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr),
right_complementable VectSp-like (non empty VectSpStr over GF),
V1,V2 be Subset of V
st V1 is lineary-closed & V2 is lineary-closed
holds V1 /\ V2 is lineary-closed;

definition
let GF be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive
(non empty doubleLoopStr),
right_complementable VectSp-like (non empty VectSpStr over GF);
mode Subspace of V -> Abelian add-associative right_zeroed
right_complementable VectSp-like (non empty VectSpStr over GF) means
:: VECTSP_4:def 2

the carrier of it c= the carrier of V &
the Zero of it = the Zero of V &
(the add of V) | [:the carrier of it,the carrier of it:] &
the lmult of it =
(the lmult of V) | [:the carrier of GF, the carrier of it:];
end;

reserve GF for add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr),
right_complementable VectSp-like (non empty VectSpStr 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;

canceled 5;

theorem :: VECTSP_4:16
x in W1 & W1 is Subspace of W2 implies x in W2;

theorem :: VECTSP_4:17
x in W implies x in V;

theorem :: VECTSP_4:18
w is Element of V;

theorem :: VECTSP_4:19
0.W = 0.V;

theorem :: VECTSP_4:20
0.W1 = 0.W2;

theorem :: VECTSP_4:21
w1 = v & w2 = u implies w1 + w2 = v + u;

theorem :: VECTSP_4:22
w = v implies a * w = a * v;

theorem :: VECTSP_4:23
w = v implies - v = - w;

theorem :: VECTSP_4:24
w1 = v & w2 = u implies w1 - w2 = v - u;

theorem :: VECTSP_4:25
0.V in W;

theorem :: VECTSP_4:26
0.W1 in W2;

theorem :: VECTSP_4:27
0.W in V;

theorem :: VECTSP_4:28
u in W & v in W implies u + v in W;

theorem :: VECTSP_4:29
v in W implies a * v in W;

theorem :: VECTSP_4:30
v in W implies - v in W;

theorem :: VECTSP_4:31
u in W & v in W implies u - v in W;

theorem :: VECTSP_4:32
V is Subspace of V;

theorem :: VECTSP_4:33
for X,V being strict Abelian add-associative right_zeroed
right_complementable VectSp-like (non empty VectSpStr over GF)
holds V is Subspace of X & X is Subspace of V implies V = X;

theorem :: VECTSP_4:34
V is Subspace of X & X is Subspace of Y implies V is Subspace of Y;

theorem :: VECTSP_4:35
the carrier of W1 c= the carrier of W2 implies
W1 is Subspace of W2;

theorem :: VECTSP_4:36
(for v st v in W1 holds v in W2) implies W1 is Subspace of W2;

definition let GF be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive
(non empty doubleLoopStr),
right_complementable VectSp-like (non empty VectSpStr over GF);
cluster strict Subspace of V;
end;

theorem :: VECTSP_4:37
for W1,W2 being strict Subspace of V st
the carrier of W1 = the carrier of W2
holds W1 = W2;

theorem :: VECTSP_4:38
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:39
for V being strict Abelian add-associative right_zeroed
right_complementable VectSp-like (non empty VectSpStr over GF),
W being strict Subspace of V holds
the carrier of W = the carrier of V implies
W = V;

theorem :: VECTSP_4:40
for V being strict Abelian add-associative right_zeroed
right_complementable VectSp-like (non empty VectSpStr 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:41
the carrier of W = V1 implies V1 is lineary-closed;

theorem :: VECTSP_4:42
V1 <> {} & V1 is lineary-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 VectSpStr of V;
end;

canceled 3;

theorem :: VECTSP_4:46
x in (0).V iff x = 0.V;

theorem :: VECTSP_4:47
(0).W = (0).V;

theorem :: VECTSP_4:48
(0).W1 = (0).W2;

theorem :: VECTSP_4:49
(0).W is Subspace of V;

theorem :: VECTSP_4:50
(0).V is Subspace of W;

theorem :: VECTSP_4:51
(0).W1 is Subspace of W2;

canceled;

theorem :: VECTSP_4:53
for V being strict Abelian add-associative right_zeroed
right_complementable VectSp-like (non empty VectSpStr 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;

canceled 3;

theorem :: VECTSP_4:57
x in v + W iff ex u st u in W & x = v + u;

theorem :: VECTSP_4:58
0.V in v + W iff v in W;

theorem :: VECTSP_4:59
v in v + W;

theorem :: VECTSP_4:60
0.V + W = the carrier of W;

theorem :: VECTSP_4:61
v + (0).V = {v};

theorem :: VECTSP_4:62
v + (Omega).V = the carrier of V;

theorem :: VECTSP_4:63
0.V in v + W iff v + W = the carrier of W;

theorem :: VECTSP_4:64
v in W iff v + W = the carrier of W;

theorem :: VECTSP_4:65
v in W implies (a * v) + W = the carrier of W;

theorem :: VECTSP_4:66
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:67
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:68
u in W iff v + W = (v + u) + W;

theorem :: VECTSP_4:69
u in W iff v + W = (v - u) + W;

theorem :: VECTSP_4:70
v in u + W iff u + W = v + W;

theorem :: VECTSP_4:71
u in v1 + W & u in v2 + W implies v1 + W = v2 + W;

theorem :: VECTSP_4:72
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:73
v in W implies a * v in v + W;

theorem :: VECTSP_4:74
v in W implies - v in v + W;

theorem :: VECTSP_4:75
u + v in v + W iff u in W;

theorem :: VECTSP_4:76
v - u in v + W iff u in W;

canceled;

theorem :: VECTSP_4:78
u in v + W iff
(ex v1 st v1 in W & u = v - v1);

theorem :: VECTSP_4:79
(ex v st v1 in v + W & v2 in v + W) iff v1 - v2 in W;

theorem :: VECTSP_4:80
v + W = u + W implies
(ex v1 st v1 in W & v + v1 = u);

theorem :: VECTSP_4:81
v + W = u + W implies
(ex v1 st v1 in W & v - v1 = u);

theorem :: VECTSP_4:82
for W1,W2 being strict Subspace of V
holds v + W1 = v + W2 iff W1 = W2;

theorem :: VECTSP_4:83
for W1,W2 being strict Subspace of V st v + W1 = u + W2
holds W1 = W2;

theorem :: VECTSP_4:84
ex C st v in C;

theorem :: VECTSP_4:85
C is lineary-closed iff C = the carrier of W;

theorem :: VECTSP_4:86
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:87
{v} is Coset of (0).V;

theorem :: VECTSP_4:88
V1 is Coset of (0).V implies (ex v st V1 = {v});

theorem :: VECTSP_4:89
the carrier of W is Coset of W;

theorem :: VECTSP_4:90
the carrier of V is Coset of (Omega).V;

theorem :: VECTSP_4:91
V1 is Coset of (Omega).V implies V1 = the carrier of V;

theorem :: VECTSP_4:92
0.V in C iff C = the carrier of W;

theorem :: VECTSP_4:93
u in C iff C = u + W;

theorem :: VECTSP_4:94
u in C & v in C implies (ex v1 st v1 in W & u + v1 = v);

theorem :: VECTSP_4:95
u in C & v in C implies (ex v1 st v1 in W & u - v1 = v);

theorem :: VECTSP_4:96
(ex C st v1 in C & v2 in C) iff v1 - v2 in W;

theorem :: VECTSP_4:97
u in B & u in C implies B = C;

::
::  Auxiliary theorems.
::

canceled 5;

theorem :: VECTSP_4:103
for GF be add-associative right_zeroed right_complementable
Abelian commutative associative left_unital distributive
(non empty doubleLoopStr),