Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

### Subspaces and Cosets of Subspace of Real Unitary Space

by
Noboru Endou,
Takashi Mitsuishi, and
Yasunari Shidama

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

```environ

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

begin :: Definition and Axioms of the Subspace of Real Unitary Space

definition
let V be RealUnitarySpace;
mode Subspace of V -> RealUnitarySpace means
:: RUSUB_1:def 1

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:]) &
the scalar of it
= (the scalar of V)|([:the carrier of it, the carrier of it:]);
end;

theorem :: RUSUB_1:1
for V being RealUnitarySpace, W1,W2 being Subspace of V, x being set st
x in W1 & W1 is Subspace of W2 holds x in W2;

theorem :: RUSUB_1:2
for V being RealUnitarySpace, W being Subspace of V, x being set st x in W
holds x in V;

theorem :: RUSUB_1:3
for V being RealUnitarySpace, W being Subspace of V, w being VECTOR of W holds
w is VECTOR of V;

theorem :: RUSUB_1:4
for V being RealUnitarySpace, W being Subspace of V holds 0.W = 0.V;

theorem :: RUSUB_1:5
for V being RealUnitarySpace, W1,W2 being Subspace of V holds 0.W1 = 0.W2;

theorem :: RUSUB_1:6
for V being RealUnitarySpace, W being Subspace of V,
u,v being VECTOR of V, w1,w2 being VECTOR of W st
w1 = v & w2 = u holds w1 + w2 = v + u;

theorem :: RUSUB_1:7
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V,
w being VECTOR of W, a being Real st w = v holds a * w = a * v;

theorem :: RUSUB_1:8
for V being RealUnitarySpace, W being Subspace of V, v1,v2 being VECTOR of V,
w1,w2 being VECTOR of W st w1 = v1 & w2 = v2 holds w1 .|. w2 = v1 .|. v2;

theorem :: RUSUB_1:9
for V being RealUnitarySpace, W being Subspace of V,
v being VECTOR of V, w being VECTOR of W st w = v holds - v = - w;

theorem :: RUSUB_1:10
for V being RealUnitarySpace, W being Subspace of V,
u,v being VECTOR of V, w1,w2 being VECTOR of W st w1 = v & w2 = u
holds w1 - w2 = v - u;

theorem :: RUSUB_1:11
for V being RealUnitarySpace, W being Subspace of V holds
0.V in W;

theorem :: RUSUB_1:12
for V being RealUnitarySpace, W1,W2 being Subspace of V holds
0.W1 in W2;

theorem :: RUSUB_1:13
for V being RealUnitarySpace, W being Subspace of V holds
0.W in V;

theorem :: RUSUB_1:14
for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V
st u in W & v in W holds u + v in W;

theorem :: RUSUB_1:15
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V,
a being Real st v in W holds a * v in W;

theorem :: RUSUB_1:16
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V
st v in W holds - v in W;

theorem :: RUSUB_1:17
for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V
st u in W & v in W holds u - v in W;

theorem :: RUSUB_1:18
for V being RealUnitarySpace, V1 being Subset of V,
D being non empty set, d1 being Element of D, A being BinOp of D,
M being Function of [:REAL, D:], D, S being Function of [:D,D:],REAL st
V1 = D &
d1 = 0.V &
A = (the add of V) | [:V1,V1:] &
M = (the Mult of V) | [:REAL,V1:] &
S = (the scalar of V) | [:V1,V1:] holds
UNITSTR (# D,d1,A,M,S #) is Subspace of V;

theorem :: RUSUB_1:19
for V being RealUnitarySpace holds V is Subspace of V;

theorem :: RUSUB_1:20
for V,X being strict RealUnitarySpace holds
V is Subspace of X & X is Subspace of V implies V = X;

theorem :: RUSUB_1:21
for V,X,Y being RealUnitarySpace st
V is Subspace of X & X is Subspace of Y holds V is Subspace of Y;

theorem :: RUSUB_1:22
for V being RealUnitarySpace, W1,W2 being Subspace of V st
the carrier of W1 c= the carrier of W2 holds W1 is Subspace of W2;

theorem :: RUSUB_1:23
for V being RealUnitarySpace, W1,W2 being Subspace of V st
(for v being VECTOR of V st v in W1 holds v in W2) holds
W1 is Subspace of W2;

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

theorem :: RUSUB_1:24
for V being RealUnitarySpace, W1,W2 being strict Subspace of V st
the carrier of W1 = the carrier of W2 holds W1 = W2;

theorem :: RUSUB_1:25
for V being RealUnitarySpace, W1,W2 being strict Subspace of V st
(for v being VECTOR of V holds v in W1 iff v in W2) holds W1 = W2;

theorem :: RUSUB_1:26
for V being strict RealUnitarySpace, W being strict Subspace of V st
the carrier of W = the carrier of V holds W = V;

theorem :: RUSUB_1:27
for V being strict RealUnitarySpace, W being strict Subspace of V st
(for v being VECTOR of V holds v in W iff v in V) holds W = V;

theorem :: RUSUB_1:28
for V being RealUnitarySpace, W being Subspace of V,
V1 being Subset of V st
the carrier of W = V1 holds V1 is lineary-closed;

theorem :: RUSUB_1:29
for V being RealUnitarySpace, W being Subspace of V,
V1 being Subset of V st
V1 <> {} & V1 is lineary-closed holds
(ex W being strict Subspace of V st V1 = the carrier of W);

begin
:: Definition of Zero Subspace and Improper Subspace of Real Unitary Space

definition
let V being RealUnitarySpace;
func (0).V -> strict Subspace of V means
:: RUSUB_1:def 2

the carrier of it = {0.V};
end;

definition
let V being RealUnitarySpace;
func (Omega).V -> strict Subspace of V equals
:: RUSUB_1:def 3

the UNITSTR of V;
end;

begin :: Theorems of Zero Subspace and Improper Subspace

theorem :: RUSUB_1:30
for V being RealUnitarySpace, W being Subspace of V holds
(0).W = (0).V;

theorem :: RUSUB_1:31
for V being RealUnitarySpace, W1,W2 being Subspace of V holds
(0).W1 = (0).W2;

theorem :: RUSUB_1:32
for V being RealUnitarySpace, W being Subspace of V holds
(0).W is Subspace of V;

theorem :: RUSUB_1:33
for V being RealUnitarySpace, W being Subspace of V holds
(0).V is Subspace of W;

theorem :: RUSUB_1:34
for V being RealUnitarySpace, W1,W2 being Subspace of V holds
(0).W1 is Subspace of W2;

theorem :: RUSUB_1:35
for V being strict RealUnitarySpace holds V is Subspace of (Omega).V;

begin :: The Cosets of Subspace of Real Unitary Space

definition
let V be RealUnitarySpace, v be VECTOR of V, W be Subspace of V;
func v + W -> Subset of V equals
:: RUSUB_1:def 4

{v + u where u is VECTOR of V : u in W};
end;

definition
let V be RealUnitarySpace; let W be Subspace of V;
mode Coset of W -> Subset of V means
:: RUSUB_1:def 5

ex v be VECTOR of V st it = v + W;
end;

begin :: Theorems of the Cosets

theorem :: RUSUB_1:36
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds
0.V in v + W iff v in W;

theorem :: RUSUB_1:37
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds
v in v + W;

theorem :: RUSUB_1:38
for V being RealUnitarySpace, W being Subspace of V holds
0.V + W = the carrier of W;

theorem :: RUSUB_1:39
for V being RealUnitarySpace, v being VECTOR of V holds
v + (0).V = {v};

theorem :: RUSUB_1:40
for V being RealUnitarySpace, v being VECTOR of V holds
v + (Omega).V = the carrier of V;

theorem :: RUSUB_1:41
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds
0.V in v + W iff v + W = the carrier of W;

theorem :: RUSUB_1:42
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V
holds
v in W iff v + W = the carrier of W;

theorem :: RUSUB_1:43
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V,
a being Real st v in W holds (a * v) + W = the carrier of W;

theorem :: RUSUB_1:44
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V,
a being Real st a <> 0 & (a * v) + W = the carrier of W holds v in W;

theorem :: RUSUB_1:45
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds
v in W iff - v + W = the carrier of W;

theorem :: RUSUB_1:46
for V being RealUnitarySpace, W being Subspace of V,
u,v being VECTOR of V holds u in W iff v + W = (v + u) + W;

theorem :: RUSUB_1:47
for V being RealUnitarySpace, W being Subspace of V,
u,v being VECTOR of V holds u in W iff v + W = (v - u) + W;

theorem :: RUSUB_1:48
for V being RealUnitarySpace, W being Subspace of V,
u,v being VECTOR of V holds v in u + W iff u + W = v + W;

theorem :: RUSUB_1:49
for V being RealUnitarySpace, W being Subspace of V,
v being VECTOR of V holds v + W = (- v) + W iff v in W;

theorem :: RUSUB_1:50
for V being RealUnitarySpace, W being Subspace of V,
u,v1,v2 being VECTOR of V st
u in v1 + W & u in v2 + W holds v1 + W = v2 + W;

theorem :: RUSUB_1:51
for V being RealUnitarySpace, W being Subspace of V,
u,v being VECTOR of V st u in v + W & u in (- v) + W holds v in W;

theorem :: RUSUB_1:52
for V being RealUnitarySpace, W being Subspace of V,
v being VECTOR of V, a being Real st a <> 1 & a * v in v + W holds v in W;

theorem :: RUSUB_1:53
for V being RealUnitarySpace, W being Subspace of V,
v being VECTOR of V, a being Real st v in W holds a * v in v + W;

theorem :: RUSUB_1:54
for V being RealUnitarySpace, W being Subspace of V,
v being VECTOR of V holds - v in v + W iff v in W;

theorem :: RUSUB_1:55
for V being RealUnitarySpace, W being Subspace of V,
u,v being VECTOR of V holds u + v in v + W iff u in W;

theorem :: RUSUB_1:56
for V being RealUnitarySpace, W being Subspace of V,
u,v being VECTOR of V holds v - u in v + W iff u in W;

theorem :: RUSUB_1:57
for V being RealUnitarySpace, W being Subspace of V,
u,v being VECTOR of V holds u in v + W iff
(ex v1 being VECTOR of V st v1 in W & u = v + v1);

theorem :: RUSUB_1:58
for V being RealUnitarySpace, W being Subspace of V,
u,v being VECTOR of V holds u in v + W iff
(ex v1 being VECTOR of V st v1 in W & u = v - v1);

theorem :: RUSUB_1:59
for V being RealUnitarySpace, W being Subspace of V,
v1,v2 being VECTOR of V holds
(ex v being VECTOR of V st v1 in v + W & v2 in v + W) iff v1 - v2 in W;

theorem :: RUSUB_1:60
for V being RealUnitarySpace, W being Subspace of V,
u,v being VECTOR of V st v + W = u + W holds
(ex v1 being VECTOR of V st v1 in W & v + v1 = u);

theorem :: RUSUB_1:61
for V being RealUnitarySpace, W being Subspace of V,
u,v being VECTOR of V st v + W = u + W holds
(ex v1 being VECTOR of V st v1 in W & v - v1 = u);

theorem :: RUSUB_1:62
for V being RealUnitarySpace, W1,W2 being strict Subspace of V,
v being VECTOR of V holds v + W1 = v + W2 iff W1 = W2;

theorem :: RUSUB_1:63
for V being RealUnitarySpace, W1,W2 being strict Subspace of V,
u,v being VECTOR of V st v + W1 = u + W2 holds W1 = W2;

theorem :: RUSUB_1:64
for V being RealUnitarySpace, W being Subspace of V, C being Coset of W holds
C is lineary-closed iff C = the carrier of W;

theorem :: RUSUB_1:65
for V being RealUnitarySpace, W1,W2 being strict Subspace of V,
C1 being Coset of W1, C2 being Coset of W2 holds
C1 = C2 implies W1 = W2;

theorem :: RUSUB_1:66
for V being RealUnitarySpace, W being Subspace of V,
C being Coset of W, v being VECTOR of V holds
{v} is Coset of (0).V;

theorem :: RUSUB_1:67
for V being RealUnitarySpace, W being Subspace of V,
V1 being Subset of V, v being VECTOR of V holds
V1 is Coset of (0).V implies (ex v being VECTOR of V st V1 = {v});

theorem :: RUSUB_1:68
for V being RealUnitarySpace, W being Subspace of V holds
the carrier of W is Coset of W;

theorem :: RUSUB_1:69
for V being RealUnitarySpace holds the carrier of V is Coset of (Omega).V;

theorem :: RUSUB_1:70
for V being RealUnitarySpace, W being Subspace of V,
V1 being Subset of V st V1 is Coset of (Omega).V holds
V1 = the carrier of V;

theorem :: RUSUB_1:71
for V being RealUnitarySpace, W being Subspace of V, C being Coset of W holds
0.V in C iff C = the carrier of W;

theorem :: RUSUB_1:72
for V being RealUnitarySpace, W being Subspace of V, C being Coset of W,
u being VECTOR of V holds u in C iff C = u + W;

theorem :: RUSUB_1:73
for V being RealUnitarySpace, W being Subspace of V, C being Coset of W,
u,v being VECTOR of V st u in C & v in C holds
(ex v1 being VECTOR of V st v1 in W & u + v1 = v);

theorem :: RUSUB_1:74
for V being RealUnitarySpace, W being Subspace of V, C being Coset of W,
u,v being VECTOR of V st u in C & v in C holds
(ex v1 being VECTOR of V st v1 in W & u - v1 = v);

theorem :: RUSUB_1:75
for V being RealUnitarySpace, W being Subspace of V,
v1,v2 being VECTOR of V holds
(ex C being Coset of W st v1 in C & v2 in C) iff v1 - v2 in W;

theorem :: RUSUB_1:76
for V being RealUnitarySpace, W being Subspace of V,
u being VECTOR of V, B,C being Coset of W st u in B & u in C holds B = C;

```