Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

Subspaces and Cosets of Subspaces in Real Linear Space

by
Wojciech A. Trybulec

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

environ

vocabulary RLVECT_1, BOOLE, ARYTM_1, RELAT_1, FUNCT_1, BINOP_1, RLSUB_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, REAL_1, MCART_1,
FUNCT_1, RELSET_1, FUNCT_2, DOMAIN_1, BINOP_1, STRUCT_0, RLVECT_1;
constructors REAL_1, DOMAIN_1, RLVECT_1, PARTFUN1, MEMBERED, XBOOLE_0;
clusters FUNCT_1, RLVECT_1, STRUCT_0, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1,
XBOOLE_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;

begin

reserve V,X,Y for RealLinearSpace;
reserve u,u1,u2,v,v1,v2 for VECTOR of V;
reserve a,b for Real;
reserve V1,V2,V3 for Subset of V;
reserve x for set;

::
::  Introduction of predicate lineary closed subsets of the carrier.
::

definition let V; let V1;
attr V1 is lineary-closed means
:: RLSUB_1:def 1

(for v,u st v in V1 & u in V1 holds v + u in V1) &
(for a,v st v in V1 holds a * v in V1);
end;

canceled 3;

theorem :: RLSUB_1:4
V1 <> {} & V1 is lineary-closed implies 0.V in V1;

theorem :: RLSUB_1:5
V1 is lineary-closed implies (for v st v in V1 holds - v in V1);

theorem :: RLSUB_1:6
V1 is lineary-closed implies
(for v,u st v in V1 & u in V1 holds v - u in V1);

theorem :: RLSUB_1:7
{0.V} is lineary-closed;

theorem :: RLSUB_1:8
the carrier of V = V1 implies V1 is lineary-closed;

theorem :: RLSUB_1:9
V1 is lineary-closed & V2 is lineary-closed &
V3 = {v + u : v in V1 & u in V2} implies V3 is lineary-closed;

theorem :: RLSUB_1:10
V1 is lineary-closed & V2 is lineary-closed implies
V1 /\ V2 is lineary-closed;

definition let V;
mode Subspace of V -> RealLinearSpace means
:: RLSUB_1:def 2

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

reserve W,W1,W2 for Subspace of V;
reserve w,w1,w2 for VECTOR of W;

::
::  Axioms of the subspaces of real linear spaces.
::

canceled 5;

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

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

theorem :: RLSUB_1:18
w is VECTOR of V;

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

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

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

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

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

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

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

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

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

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

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

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

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

reserve D for non empty set;
reserve d1 for Element of D;
reserve A for BinOp of D;
reserve M for Function of [:REAL,D:],D;

theorem :: RLSUB_1:32
V1 = D &
d1 = 0.V &
A = (the add of V) | [:V1,V1:] &
M = (the Mult of V) | [:REAL,V1:] implies
RLSStruct (# D,d1,A,M #) is Subspace of V;

theorem :: RLSUB_1:33
V is Subspace of V;

theorem :: RLSUB_1:34
for V,X being strict RealLinearSpace holds
V is Subspace of X & X is Subspace of V implies V = X;

theorem :: RLSUB_1:35
V is Subspace of X & X is Subspace of Y implies V is Subspace of Y;

theorem :: RLSUB_1:36
the carrier of W1 c= the carrier of W2 implies W1 is Subspace of W2;

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

definition let V;
cluster strict Subspace of V;
end;

theorem :: RLSUB_1:38
for W1,W2 being strict Subspace of V holds
the carrier of W1 = the carrier of W2 implies W1 = W2;

theorem :: RLSUB_1:39
for W1,W2 being strict Subspace of V holds
(for v holds v in W1 iff v in W2) implies W1 = W2;

theorem :: RLSUB_1:40
for V being strict RealLinearSpace, W being strict Subspace of V holds
the carrier of W = the carrier of V implies W = V;

theorem :: RLSUB_1:41
for V being strict RealLinearSpace, W being strict Subspace of V holds
(for v being VECTOR of V holds v in W iff v in V) implies W = V;

theorem :: RLSUB_1:42
the carrier of W = V1 implies V1 is lineary-closed;

theorem :: RLSUB_1:43
V1 <> {} & V1 is lineary-closed implies
(ex W being strict Subspace of V st V1 = the carrier of W);

::
::  Definition of zero subspace and improper subspace of real linear space.
::

definition let V;
func (0).V -> strict Subspace of V means
:: RLSUB_1:def 3
the carrier of it = {0.V};
end;

definition let V;
func (Omega).V -> strict Subspace of V equals
:: RLSUB_1:def 4
the RLSStruct of V;
end;

::
::  Definitional theorems of zero subspace and improper subspace.
::

canceled 4;

theorem :: RLSUB_1:48
(0).W = (0).V;

theorem :: RLSUB_1:49
(0).W1 = (0).W2;

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

theorem :: RLSUB_1:51
(0).V is Subspace of W;

theorem :: RLSUB_1:52
(0).W1 is Subspace of W2;

canceled;

theorem :: RLSUB_1:54
for V being strict RealLinearSpace holds V is Subspace of (Omega).V;

::
::  Introduction of the cosets of subspace.
::

definition let V; let v,W;
func v + W -> Subset of V equals
:: RLSUB_1:def 5
{v + u : u in W};
end;

definition let V; let W;
mode Coset of W -> Subset of V means
:: RLSUB_1:def 6
ex v st it = v + W;
end;

reserve B,C for Coset of W;

::
::  Definitional theorems of the cosets.
::

canceled 3;

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

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

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

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

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

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

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

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

theorem :: RLSUB_1:66
a <> 0 & (a * v) + W = the carrier of W implies v in W;

theorem :: RLSUB_1:67
v in W iff - v + W = the carrier of W;

theorem :: RLSUB_1:68
u in W iff v + W = (v + u) + W;

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

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

theorem :: RLSUB_1:71
v + W = (- v) + W iff v in W;

theorem :: RLSUB_1:72
u in v1 + W & u in v2 + W implies v1 + W = v2 + W;

theorem :: RLSUB_1:73
u in v + W & u in (- v) + W implies v in W;

theorem :: RLSUB_1:74
a <> 1 & a * v in v + W implies v in W;

theorem :: RLSUB_1:75
v in W implies a * v in v + W;

theorem :: RLSUB_1:76
- v in v + W iff v in W;

theorem :: RLSUB_1:77
u + v in v + W iff u in W;

theorem :: RLSUB_1:78
v - u in v + W iff u in W;

theorem :: RLSUB_1:79
u in v + W iff
(ex v1 st v1 in W & u = v + v1);

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

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

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

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

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

theorem :: RLSUB_1:85
for W1,W2 being strict Subspace of V holds
v + W1 = u + W2 implies W1 = W2;

::
::  Theorems concerning cosets of subspace
::  regarded as subsets of the carrier.
::

theorem :: RLSUB_1:86
C is lineary-closed iff C = the carrier of W;

theorem :: RLSUB_1:87
for W1,W2 being strict Subspace of V,
C1 being Coset of W1, C2 being Coset of W2 holds
C1 = C2 implies W1 = W2;

theorem :: RLSUB_1:88
{v} is Coset of (0).V;

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

theorem :: RLSUB_1:90
the carrier of W is Coset of W;

theorem :: RLSUB_1:91
the carrier of V is Coset of (Omega).V;

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

theorem :: RLSUB_1:93
0.V in C iff C = the carrier of W;

theorem :: RLSUB_1:94
u in C iff C = u + W;

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

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

theorem :: RLSUB_1:97
(ex C st v1 in C & v2 in C) iff v1 - v2 in W;

theorem :: RLSUB_1:98
u in B & u in C implies B = C;