:: Subspaces and Cosets of Subspaces in Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received July 24, 1989
:: Copyright (c) 1990-2021 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, REAL_1, SUBSET_1, ARYTM_3, RELAT_1, XBOOLE_0, SUPINF_2,
CARD_1, ARYTM_1, STRUCT_0, TARSKI, ALGSTR_0, REALSET1, ZFMISC_1, NUMBERS,
FUNCT_1, BINOP_1, RLSUB_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, REAL_1, MCART_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, REALSET1,
DOMAIN_1, STRUCT_0, ALGSTR_0, RLVECT_1;
constructors PARTFUN1, BINOP_1, REAL_1, NAT_1, REALSET1, RLVECT_1, RELSET_1,
NUMBERS;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, NUMBERS, REALSET1,
STRUCT_0, RLVECT_1, ORDINAL1, ALGSTR_0, XREAL_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 for Real;
reserve V1,V2,V3 for Subset of V;
reserve x for object;
::
:: Introduction of predicate linearly closed subsets of the carrier.
::
definition
let V;
let V1;
attr V1 is linearly-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;
theorem :: RLSUB_1:1
V1 <> {} & V1 is linearly-closed implies 0.V in V1;
theorem :: RLSUB_1:2
V1 is linearly-closed implies for v st v in V1 holds - v in V1;
theorem :: RLSUB_1:3
V1 is linearly-closed implies for v,u st v in V1 & u in V1 holds v - u in V1;
theorem :: RLSUB_1:4
{0.V} is linearly-closed;
theorem :: RLSUB_1:5
the carrier of V = V1 implies V1 is linearly-closed;
theorem :: RLSUB_1:6
V1 is linearly-closed & V2 is linearly-closed & V3 = {v + u : v in V1
& u in V2} implies V3 is linearly-closed;
theorem :: RLSUB_1:7
V1 is linearly-closed & V2 is linearly-closed implies V1 /\ V2 is
linearly-closed;
definition
let V;
mode Subspace of V -> RealLinearSpace means
:: RLSUB_1: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 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.
::
theorem :: RLSUB_1:8
x in W1 & W1 is Subspace of W2 implies x in W2;
theorem :: RLSUB_1:9
x in W implies x in V;
theorem :: RLSUB_1:10
w is VECTOR of V;
theorem :: RLSUB_1:11
0.W = 0.V;
theorem :: RLSUB_1:12
0.W1 = 0.W2;
theorem :: RLSUB_1:13
w1 = v & w2 = u implies w1 + w2 = v + u;
theorem :: RLSUB_1:14
w = v implies a * w = a * v;
theorem :: RLSUB_1:15
w = v implies - v = - w;
theorem :: RLSUB_1:16
w1 = v & w2 = u implies w1 - w2 = v - u;
theorem :: RLSUB_1:17
0.V in W;
theorem :: RLSUB_1:18
0.W1 in W2;
theorem :: RLSUB_1:19
0.W in V;
theorem :: RLSUB_1:20
u in W & v in W implies u + v in W;
theorem :: RLSUB_1:21
v in W implies a * v in W;
theorem :: RLSUB_1:22
v in W implies - v in W;
theorem :: RLSUB_1:23
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:24
V1 = D & d1 = 0.V & A = (the addF of V)||V1 & M = (the Mult of V
) | [:REAL,V1:] implies RLSStruct (# D,d1,A,M #) is Subspace of V;
theorem :: RLSUB_1:25
V is Subspace of V;
theorem :: RLSUB_1:26
for V,X being strict RealLinearSpace holds V is Subspace of X &
X is Subspace of V implies V = X;
theorem :: RLSUB_1:27
V is Subspace of X & X is Subspace of Y implies V is Subspace of Y;
theorem :: RLSUB_1:28
the carrier of W1 c= the carrier of W2 implies W1 is Subspace of W2;
theorem :: RLSUB_1:29
(for v st v in W1 holds v in W2) implies W1 is Subspace of W2;
registration
let V;
cluster strict for Subspace of V;
end;
theorem :: RLSUB_1:30
for W1,W2 being strict Subspace of V holds the carrier of W1 =
the carrier of W2 implies W1 = W2;
theorem :: RLSUB_1:31
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:32
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:33
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:34
the carrier of W = V1 implies V1 is linearly-closed;
theorem :: RLSUB_1:35
V1 <> {} & V1 is linearly-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.
::
theorem :: RLSUB_1:36
(0).W = (0).V;
theorem :: RLSUB_1:37
(0).W1 = (0).W2;
theorem :: RLSUB_1:38
(0).W is Subspace of V;
theorem :: RLSUB_1:39
(0).V is Subspace of W;
theorem :: RLSUB_1:40
(0).W1 is Subspace of W2;
theorem :: RLSUB_1:41
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.
::
theorem :: RLSUB_1:42
0.V in v + W iff v in W;
theorem :: RLSUB_1:43
v in v + W;
theorem :: RLSUB_1:44
0.V + W = the carrier of W;
theorem :: RLSUB_1:45
v + (0).V = {v};
theorem :: RLSUB_1:46
v + (Omega).V = the carrier of V;
theorem :: RLSUB_1:47
0.V in v + W iff v + W = the carrier of W;
theorem :: RLSUB_1:48
v in W iff v + W = the carrier of W;
theorem :: RLSUB_1:49
v in W implies (a * v) + W = the carrier of W;
theorem :: RLSUB_1:50
a <> 0 & (a * v) + W = the carrier of W implies v in W;
theorem :: RLSUB_1:51
v in W iff - v + W = the carrier of W;
theorem :: RLSUB_1:52
u in W iff v + W = (v + u) + W;
theorem :: RLSUB_1:53
u in W iff v + W = (v - u) + W;
theorem :: RLSUB_1:54
v in u + W iff u + W = v + W;
theorem :: RLSUB_1:55
v + W = (- v) + W iff v in W;
theorem :: RLSUB_1:56
u in v1 + W & u in v2 + W implies v1 + W = v2 + W;
theorem :: RLSUB_1:57
u in v + W & u in (- v) + W implies v in W;
theorem :: RLSUB_1:58
a <> 1 & a * v in v + W implies v in W;
theorem :: RLSUB_1:59
v in W implies a * v in v + W;
theorem :: RLSUB_1:60
- v in v + W iff v in W;
theorem :: RLSUB_1:61
u + v in v + W iff u in W;
theorem :: RLSUB_1:62
v - u in v + W iff u in W;
theorem :: RLSUB_1:63
u in v + W iff ex v1 st v1 in W & u = v + v1;
theorem :: RLSUB_1:64
u in v + W iff ex v1 st v1 in W & u = v - v1;
theorem :: RLSUB_1:65
(ex v st v1 in v + W & v2 in v + W) iff v1 - v2 in W;
theorem :: RLSUB_1:66
v + W = u + W implies ex v1 st v1 in W & v + v1 = u;
theorem :: RLSUB_1:67
v + W = u + W implies ex v1 st v1 in W & v - v1 = u;
theorem :: RLSUB_1:68
for W1,W2 being strict Subspace of V holds v + W1 = v + W2 iff W1 = W2;
theorem :: RLSUB_1:69
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:70
C is linearly-closed iff C = the carrier of W;
theorem :: RLSUB_1:71
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:72
{v} is Coset of (0).V;
theorem :: RLSUB_1:73
V1 is Coset of (0).V implies ex v st V1 = {v};
theorem :: RLSUB_1:74
the carrier of W is Coset of W;
theorem :: RLSUB_1:75
the carrier of V is Coset of (Omega).V;
theorem :: RLSUB_1:76
V1 is Coset of (Omega).V implies V1 = the carrier of V;
theorem :: RLSUB_1:77
0.V in C iff C = the carrier of W;
theorem :: RLSUB_1:78
u in C iff C = u + W;
theorem :: RLSUB_1:79
u in C & v in C implies ex v1 st v1 in W & u + v1 = v;
theorem :: RLSUB_1:80
u in C & v in C implies ex v1 st v1 in W & u - v1 = v;
theorem :: RLSUB_1:81
(ex C st v1 in C & v2 in C) iff v1 - v2 in W;
theorem :: RLSUB_1:82
u in B & u in C implies B = C;