:: Subspaces and Cosets of Subspace of Real Unitary Space
:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama
::
:: Received October 9, 2002
:: Copyright (c) 2002-2026 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 BHSP_1, RLSUB_1, STRUCT_0, TARSKI, SUPINF_2, ALGSTR_0, REALSET1,
RLVECT_1, RELAT_1, ZFMISC_1, NUMBERS, ARYTM_3, FUNCT_1, REAL_1, PROB_2,
ARYTM_1, SUBSET_1, XBOOLE_0, BINOP_1, CARD_1, XXREAL_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, ALGSTR_0, ORDINAL1,
NUMBERS, XCMPLX_0, XREAL_0, MCART_1, RELAT_1, FUNCT_1, REAL_1, FUNCT_2,
DOMAIN_1, BINOP_1, REALSET1, RLVECT_1, RLSUB_1, BHSP_1, XXREAL_0;
constructors PARTFUN1, BINOP_1, XXREAL_0, REAL_1, REALSET1, RLSUB_1, BHSP_1,
VALUED_1, RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, NUMBERS, MEMBERED,
REALSET1, STRUCT_0, BHSP_1, VALUED_0, ALGSTR_0, XREAL_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, ALGSTR_0, BHSP_1;
equalities RLVECT_1, REALSET1, BINOP_1, STRUCT_0, ALGSTR_0, BHSP_1;
expansions RLVECT_1, TARSKI, XBOOLE_0, STRUCT_0;
theorems BHSP_1, RLVECT_1, FUNCT_1, TARSKI, FUNCT_2, ZFMISC_1, XBOOLE_0,
RELAT_1, RELSET_1, RLSUB_1, XBOOLE_1, XCMPLX_0, STRUCT_0, ALGSTR_0,
XREAL_0;
schemes XBOOLE_0;
begin :: Definition and Axioms of the Subspace of Real Unitary Space
definition
let V be RealUnitarySpace;
mode Subspace of V -> RealUnitarySpace means
:Def1:
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:]) & the scalar
of it = (the scalar of V)||the carrier of it;
existence
proof
take V;
A1: dom(the scalar of V) = [:the carrier of V, the carrier of V:] by
FUNCT_2:def 1;
dom(the addF of V) = [:the carrier of V, the carrier of V:] & dom(the
Mult of V) = [:REAL, the carrier of V:] by FUNCT_2:def 1;
hence thesis by A1,RELAT_1:69;
end;
end;
theorem
for V being RealUnitarySpace, W1,W2 being Subspace of V, x being object
st x in W1 & W1 is Subspace of W2 holds x in W2
proof
let V be RealUnitarySpace;
let W1,W2 be Subspace of V;
let x be object;
assume x in W1 & W1 is Subspace of W2;
then x in the carrier of W1 & the carrier of W1 c= the carrier of W2 by Def1;
hence thesis;
end;
theorem Th2:
for V being RealUnitarySpace, W being Subspace of V, x being object
st x in W holds x in V
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let x be object;
assume x in W;
then
A1: x in the carrier of W;
the carrier of W c= the carrier of V by Def1;
hence thesis by A1;
end;
theorem Th3:
for V being RealUnitarySpace, W being Subspace of V, w being
VECTOR of W holds w is VECTOR of V
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let w be VECTOR of W;
w in V by Th2,RLVECT_1:1;
hence thesis;
end;
theorem
for V being RealUnitarySpace, W being Subspace of V holds 0.W = 0.V by Def1;
theorem
for V being RealUnitarySpace, W1,W2 being Subspace of V holds 0.W1 = 0.W2
proof
let V be RealUnitarySpace;
let W1,W2 being Subspace of V;
0.W1 = 0.V by Def1;
hence thesis by Def1;
end;
theorem Th6:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let u,v be VECTOR of V;
let w1,w2 be VECTOR of W;
assume
A1: v = w1 & u = w2;
w1 + w2 = ((the addF of V)||the carrier of W).[w1,w2] by Def1;
hence thesis by A1,FUNCT_1:49;
end;
theorem Th7:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let v be VECTOR of V;
let w be VECTOR of W;
let a be Real;
assume
A1: w = v;
reconsider aa=a as Element of REAL by XREAL_0:def 1;
aa * w = ((the Mult of V) | [:REAL, the carrier of W:]).[aa,w] by Def1;
hence thesis by A1,FUNCT_1:49;
end;
theorem
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let v1,v2 be VECTOR of V;
let w1,w2 be VECTOR of W;
reconsider ww1 = w1, ww2 = w2 as VECTOR of V by Th3;
assume w1 = v1 & w2 = v2;
then
A1: v1 .|. v2 = (the scalar of V).[ww1,ww2];
w1 .|. w2 = (the scalar of W).[w1,w2]
.= ((the scalar of V)||the carrier of W).[w1,w2] by Def1;
hence thesis by A1,FUNCT_1:49;
end;
theorem Th9:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let v be VECTOR of V;
let w be VECTOR of W;
A1: - v = (- 1) * v & - w = (- 1) * w by RLVECT_1:16;
assume w = v;
hence thesis by A1,Th7;
end;
theorem Th10:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let u,v be VECTOR of V;
let w1,w2 be VECTOR of W;
assume that
A1: w1 = v and
A2: w2 = u;
- w2 = - u by A2,Th9;
hence thesis by A1,Th6;
end;
theorem Th11:
for V being RealUnitarySpace, W being Subspace of V holds 0.V in W
proof
let V be RealUnitarySpace;
let W be Subspace of V;
0.W in W;
hence thesis by Def1;
end;
theorem
for V being RealUnitarySpace, W1,W2 being Subspace of V holds 0.W1 in W2
proof
let V be RealUnitarySpace;
let W1,W2 be Subspace of V;
0.W1 = 0.V by Def1;
hence thesis by Th11;
end;
theorem
for V being RealUnitarySpace, W being Subspace of V holds 0.W in V by Th2,
RLVECT_1:1;
Lm1: for V being RealUnitarySpace, W being Subspace of V, V1,V2 being Subset
of V st the carrier of W = V1 holds V1 is linearly-closed
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let V1,V2 be Subset of V;
set VW = the carrier of W;
reconsider WW = W as RealUnitarySpace;
assume
A1: the carrier of W = V1;
A2: for a being Real, v being VECTOR of V st v in V1 holds a * v in V1
proof
let a be Real, v be VECTOR of V;
assume v in V1;
then reconsider vv = v as VECTOR of WW by A1;
reconsider vw = a * vv as Element of VW;
vw in V1 by A1;
hence thesis by Th7;
end;
for v,u being VECTOR of V st v in V1 & u in V1 holds v + u in V1
proof
let v,u be VECTOR of V;
assume v in V1 & u in V1;
then reconsider vv = v, uu = u as VECTOR of WW by A1;
reconsider vw = vv + uu as Element of VW;
vw in V1 by A1;
hence thesis by Th6;
end;
hence thesis by A2,RLSUB_1:def 1;
end;
theorem Th14:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
reconsider VW = the carrier of W as Subset of V by Def1;
let u,v be VECTOR of V;
assume u in W & v in W;
then
A1: u in the carrier of W & v in the carrier of W;
VW is linearly-closed by Lm1;
then u + v in the carrier of W by A1,RLSUB_1:def 1;
hence thesis;
end;
theorem Th15:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
reconsider VW = the carrier of W as Subset of V by Def1;
let v be VECTOR of V;
let a be Real;
assume v in W;
then
A1: v in the carrier of W;
reconsider aa=a as Real;
VW is linearly-closed by Lm1;
then aa * v in the carrier of W by A1,RLSUB_1:def 1;
hence thesis;
end;
theorem Th16:
for V being RealUnitarySpace, W being Subspace of V, v being
VECTOR of V st v in W holds - v in W
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let v be VECTOR of V;
assume v in W;
then (- 1) * v in W by Th15;
hence thesis by RLVECT_1:16;
end;
theorem Th17:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let u,v be VECTOR of V;
assume that
A1: u in W and
A2: v in W;
- v in W by A2,Th16;
hence thesis by A1,Th14;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
theorem Th18:
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
addF of V)||V1 & M = (the Mult of V) | [:REAL,V1:] & S = (the scalar of V)||V1
holds UNITSTR (# D,d1,A,M,S #) is Subspace of V
proof
let V be RealUnitarySpace;
let V1 be Subset of V;
let D be non empty set;
let d1 be Element of D;
let A be BinOp of D;
let M be Function of [:REAL, D:], D;
let S be Function of [:D, D:], REAL;
assume that
A1: V1 = D and
A2: d1 = 0.V and
A3: A = (the addF of V)||V1 and
A4: M = (the Mult of V) | [:REAL,V1:] and
A5: S = (the scalar of V)||V1;
UNITSTR (# D,d1,A,M,S #) is Subspace of V
proof
set W = UNITSTR (# D,d1,A,M,S #);
A6: for a being Real, x being VECTOR of W
holds a * x = (the Mult of V).[a,x]
proof let a be Real, x be VECTOR of W;
reconsider a as Element of REAL by XREAL_0:def 1;
a * x = (the Mult of V).[a,x] by A1,A4,FUNCT_1:49;
hence thesis;
end;
A7: for x,y being VECTOR of W holds x .|. y = (the scalar of V).[x,y]
by A1,A5,FUNCT_1:49;
A8: for x,y being VECTOR of W holds x + y = (the addF of V).[x,y] by A1,A3,
FUNCT_1:49;
A9: W is RealUnitarySpace-like vector-distributive scalar-distributive
scalar-associative scalar-unital Abelian
add-associative right_zeroed right_complementable
proof
set SV = the scalar of V;
set MV = the Mult of V;
set AV = the addF of V;
A10: for x being VECTOR of W holds jj * x = x
proof
let x be VECTOR of W;
reconsider y = x as VECTOR of V by A1,TARSKI:def 3;
thus jj * x = jj * y by A6
.= x by RLVECT_1:def 8;
end;
A11: for a,b being Real, x being VECTOR of W holds (a * b) * x =
a * (b * x)
proof
let a,b be Real;
let x be VECTOR of W;
reconsider y = x as VECTOR of V by A1,TARSKI:def 3;
reconsider a,b as Element of REAL by XREAL_0:def 1;
(a * b) * x = (a * b) * y by A6
.= a * (b * y) by RLVECT_1:def 7
.= MV.[a,b * x] by A6
.= a * (b * x) by A1,A4,FUNCT_1:49;
hence thesis;
end;
A12: for a being Real, x,y being VECTOR of W holds a * (x + y) =
a * x + a * y
proof
let a be Real;
let x,y be VECTOR of W;
reconsider x1 = x, y1 = y as VECTOR of V by A1,TARSKI:def 3;
reconsider a as Element of REAL by XREAL_0:def 1;
a * (x + y) = MV.[a,x + y] by A1,A4,FUNCT_1:49
.= a * (x1 + y1) by A8
.= a * x1 + a * y1 by RLVECT_1:def 5
.= AV.[MV.[a,x1],a * y] by A6
.= AV.[a * x, a * y] by A6
.= a * x + a * y by A1,A3,FUNCT_1:49;
hence thesis;
end;
A13: for x being VECTOR of W holds x + 0.W = x
proof
let x be VECTOR of W;
reconsider y = x as VECTOR of V by A1,TARSKI:def 3;
thus x + 0.W = y + 0.V by A2,A8
.= x by RLVECT_1:4;
end;
thus W is RealUnitarySpace-like
proof
let x,y,z be VECTOR of W;
reconsider z1 = z as VECTOR of V by A1,TARSKI:def 3;
reconsider y1 = y as VECTOR of V by A1,TARSKI:def 3;
reconsider x1 = x as VECTOR of V by A1,TARSKI:def 3;
let a be Real;
A14: x = 0.W implies x .|. x = 0
proof
assume x = 0.W;
then x1 .|. x1 = 0 by A2,BHSP_1:def 2;
then SV.[x1,x1] = 0;
hence thesis by A7;
end;
x .|. x = 0 implies x = 0.W
proof
assume x .|. x = 0;
then SV.[x1,x1] = 0 by A7;
then x1 .|. x1 = 0;
hence thesis by A2,BHSP_1:def 2;
end;
hence x .|. x = 0 iff x = 0.W by A14;
0 <= x1 .|. x1 by BHSP_1:def 2;
then 0 <= SV.[x1,x1];
hence 0 <= x .|. x by A7;
SV.[x1,y1] = y1 .|. x1 by BHSP_1:def 1;
then SV.[x1,y1] = SV.[y1,x1];
then x .|. y = SV.[y1,x1] by A7;
hence x .|. y = y .|. x by A7;
A15: (x + y) .|. z = SV.[x+y, z] by A7
.= SV.[x1+y1, z] by A8
.= (x1 + y1) .|. z1
.= x1 .|. z1 + y1 .|. z1 by BHSP_1:def 2;
x .|. z + y .|. z = SV.[x, z] + (y .|. z) by A7
.= (SV.[x, z]) + (SV.[y, z]) by A7
.= x1 .|. z1 + y1 .|. z1;
hence (x+y) .|. z = x .|. z + y .|. z by A15;
A16: a * ( x .|. y ) = a * SV.[x,y] by A7
.= a * (x1 .|. y1);
(a*x) .|. y = SV.[(a*x), y] by A7
.= SV.[(a*x1), y] by A6
.= (a*x1) .|. y1
.= a * ( x1 .|. y1 ) by BHSP_1:def 2;
hence thesis by A16;
end;
A17: for a,b being Real, x being VECTOR of W holds (a + b) * x =
a * x + b * x
proof
let a,b be Real;
let x be VECTOR of W;
reconsider y = x as VECTOR of V by A1,TARSKI:def 3;
reconsider a,b as Real;
(a + b) * x = (a + b) * y by A6
.= a * y + b * y by RLVECT_1:def 6
.= AV.[MV.[a,y],b * x] by A6
.= AV.[a * x,b * x] by A6
.= a * x + b * x by A1,A3,FUNCT_1:49;
hence thesis;
end;
A18: W is right_complementable
proof
let x be VECTOR of W;
reconsider x1 = x as VECTOR of V by A1,TARSKI:def 3;
consider v being VECTOR of V such that
A19: x1 + v = 0.V by ALGSTR_0:def 11;
v = - x1 by A19,RLVECT_1:def 10
.= (- 1) * x1 by RLVECT_1:16
.= (- jj) * x by A6;
then reconsider y = v as VECTOR of W;
take y;
thus thesis by A2,A8,A19;
end;
A20: for x,y being Element of W holds x + y = y + x
proof
let x,y be Element of W;
reconsider x1 = x, y1 = y as VECTOR of V by A1,TARSKI:def 3;
thus x + y = x1 + y1 by A8
.= y1 + x1
.= y + x by A8;
end;
for x,y,z being VECTOR of W holds (x + y) + z = x + (y + z)
proof
let x,y,z be VECTOR of W;
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1,TARSKI:def 3;
thus (x + y) + z = AV.[x + y,z1] by A8
.= (x1 + y1) + z1 by A8
.= x1 + (y1 + z1) by RLVECT_1:def 3
.= AV.[x1,y + z] by A8
.= x + (y + z) by A8;
end;
hence thesis by A20,A13,A18,A12,A17,A11,A10;
end;
0.W = 0.V by A2;
hence thesis by A1,A3,A4,A5,A9,Def1;
end;
hence thesis;
end;
theorem Th19:
for V being RealUnitarySpace holds V is Subspace of V
proof
let V be RealUnitarySpace;
thus the carrier of V c= the carrier of V & 0.V = 0.V;
thus thesis by RELSET_1:19;
end;
theorem Th20:
for V,X being strict RealUnitarySpace holds V is Subspace of X &
X is Subspace of V implies V = X
proof
let V,X be strict RealUnitarySpace;
assume that
A1: V is Subspace of X and
A2: X is Subspace of V;
set VX = the carrier of X;
set VV = the carrier of V;
VV c= VX & VX c= VV by A1,A2,Def1;
then
A3: VV = VX;
set MX = the Mult of X;
set MV = the Mult of V;
MV = MX | [:REAL,VV:] & MX = MV | [:REAL,VX:] by A1,A2,Def1;
then
A4: MV = MX by A3,RELAT_1:72;
set AX = the addF of X;
set AV = the addF of V;
AV = AX||VV & AX = AV||VX by A1,A2,Def1;
then
A5: AV = AX by A3,RELAT_1:72;
set SX = the scalar of X;
set SV = the scalar of V;
A6: SX = SV||VX by A2,Def1;
0.V = 0.X & SV = SX||VV by A1,Def1;
hence thesis by A3,A5,A4,A6,RELAT_1:72;
end;
theorem Th21:
for V,X,Y being RealUnitarySpace st V is Subspace of X & X is
Subspace of Y holds V is Subspace of Y
proof
let V,X,Y be RealUnitarySpace;
assume that
A1: V is Subspace of X and
A2: X is Subspace of Y;
the carrier of V c= the carrier of X & the carrier of X c= the carrier
of Y by A1,A2,Def1;
hence the carrier of V c= the carrier of Y;
0.V = 0.X by A1,Def1;
hence 0.V = 0.Y by A2,Def1;
thus the addF of V = (the addF of Y)||the carrier of V
proof
set AY = the addF of Y;
set VX = the carrier of X;
set AX = the addF of X;
set VV = the carrier of V;
set AV = the addF of V;
VV c= VX by A1,Def1;
then
A3: [:VV,VV:] c= [:VX,VX:] by ZFMISC_1:96;
AV = AX||VV by A1,Def1;
then AV = (AY||VX)||VV by A2,Def1;
hence thesis by A3,FUNCT_1:51;
end;
thus the Mult of V = (the Mult of Y) | [:REAL, the carrier of V:]
proof
set MY = the Mult of Y;
set VX = the carrier of X;
set MX = the Mult of X;
set VV = the carrier of V;
set MV = the Mult of V;
VV c= VX by A1,Def1;
then
A4: [:REAL,VV:] c= [:REAL,VX:] by ZFMISC_1:95;
MV = MX | [:REAL,VV:] by A1,Def1;
then MV = (MY | [:REAL,VX:]) | [:REAL,VV:] by A2,Def1;
hence thesis by A4,FUNCT_1:51;
end;
set SY = the scalar of Y;
set SX = the scalar of X;
set SV = the scalar of V;
set VX = the carrier of X;
set VV = the carrier of V;
VV c= VX by A1,Def1;
then
A5: [:VV,VV:] c= [:VX,VX:] by ZFMISC_1:96;
SV = SX||VV by A1,Def1;
then SV = SY||VX||VV by A2,Def1;
hence thesis by A5,FUNCT_1:51;
end;
theorem Th22:
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
proof
let V be RealUnitarySpace;
let W1,W2 be Subspace of V;
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
set AV = the addF of V;
set MV = the Mult of V;
set SV = the scalar of V;
assume
A1: the carrier of W1 c= the carrier of W2;
then
A2: [:VW1,VW1:] c= [:VW2,VW2:] by ZFMISC_1:96;
0.W1 = 0.V by Def1;
hence the carrier of W1 c= the carrier of W2 & 0.W1 = 0.W2 by A1,Def1;
the addF of W1 = AV||VW1 & the addF of W2 = AV||VW2 by Def1;
hence the addF of W1 = (the addF of W2)||the carrier of W1 by A2,FUNCT_1:51;
A3: [:REAL,VW1:] c= [:REAL,VW2:] by A1,ZFMISC_1:95;
the Mult of W1 = MV | [:REAL,VW1:] & the Mult of W2 = MV | [:REAL,VW2 :]
by Def1;
hence the Mult of W1 = (the Mult of W2) | [:REAL, the carrier of W1:] by A3,
FUNCT_1:51;
A4: [:VW1,VW1:] c= [:VW2,VW2:] by A1,ZFMISC_1:96;
the scalar of W1 = SV||VW1 & the scalar of W2 = SV||VW2 by Def1;
hence thesis by A4,FUNCT_1:51;
end;
theorem
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
proof
let V be RealUnitarySpace;
let W1,W2 be Subspace of V;
assume
A1: for v being VECTOR of V st v in W1 holds v in W2;
the carrier of W1 c= the carrier of W2
proof
let x be object;
assume
A2: x in the carrier of W1;
the carrier of W1 c= the carrier of V by Def1;
then reconsider v = x as VECTOR of V by A2;
v in W1 by A2;
then v in W2 by A1;
hence thesis;
end;
hence thesis by Th22;
end;
registration
let V be RealUnitarySpace;
cluster strict for Subspace of V;
existence
proof
the carrier of V is Subset of V iff the carrier of V c= the carrier of V;
then reconsider V1 = the carrier of V as Subset of V;
A1: the scalar of V = (the scalar of V)||V1 by RELSET_1:19;
the addF of V = (the addF of V)||V1 & the Mult of V = (the Mult of V)
| [: REAL,V1:] by RELSET_1:19;
then
UNITSTR(#the carrier of V,0.V,the addF of V,the Mult of V, the scalar
of V #) is Subspace of V by A1,Th18;
hence thesis;
end;
end;
theorem Th24:
for V being RealUnitarySpace, W1,W2 being strict Subspace of V
st the carrier of W1 = the carrier of W2 holds W1 = W2
proof
let V be RealUnitarySpace;
let W1,W2 be strict Subspace of V;
assume the carrier of W1 = the carrier of W2;
then W1 is Subspace of W2 & W2 is Subspace of W1 by Th22;
hence thesis by Th20;
end;
theorem Th25:
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
proof
let V be RealUnitarySpace;
let W1,W2 be strict Subspace of V;
assume
A1: for v being VECTOR of V holds v in W1 iff v in W2;
for x being object holds x in the carrier of W1 iff x in the carrier of W2
proof
let x be object;
thus x in the carrier of W1 implies x in the carrier of W2
proof
assume
A2: x in the carrier of W1;
the carrier of W1 c= the carrier of V by Def1;
then reconsider v = x as VECTOR of V by A2;
v in W1 by A2;
then v in W2 by A1;
hence thesis;
end;
assume
A3: x in the carrier of W2;
the carrier of W2 c= the carrier of V by Def1;
then reconsider v = x as VECTOR of V by A3;
v in W2 by A3;
then v in W1 by A1;
hence thesis;
end;
then the carrier of W1 = the carrier of W2 by TARSKI:2;
hence thesis by Th24;
end;
theorem
for V being strict RealUnitarySpace, W being strict Subspace of V st
the carrier of W = the carrier of V holds W = V
proof
let V be strict RealUnitarySpace;
let W be strict Subspace of V;
assume
A1: the carrier of W = the carrier of V;
V is Subspace of V by Th19;
hence thesis by A1,Th24;
end;
theorem
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
proof
let V be strict RealUnitarySpace;
let W be strict Subspace of V;
assume
A1: for v being VECTOR of V holds v in W iff v in V;
V is Subspace of V by Th19;
hence thesis by A1,Th25;
end;
theorem
for V being RealUnitarySpace, W being Subspace of V, V1 being Subset
of V st the carrier of W = V1 holds V1 is linearly-closed by Lm1;
theorem Th29:
for V being RealUnitarySpace, V1 being Subset of V st V1 <> {} &
V1 is linearly-closed holds ex W being strict Subspace of V st V1 = the carrier
of W
proof
let V be RealUnitarySpace;
let V1 be Subset of V;
assume that
A1: V1 <> {} and
A2: V1 is linearly-closed;
reconsider D = V1 as non empty set by A1;
reconsider d1 = 0.V as Element of D by A2,RLSUB_1:1;
set S = (the scalar of V)||V1;
set VV = the carrier of V;
set M = (the Mult of V) | [:REAL,V1:];
dom(the Mult of V) = [:REAL,VV:] by FUNCT_2:def 1;
then
A3: dom M = [:REAL,VV:] /\ [:REAL,V1:] by RELAT_1:61;
[:REAL,V1:] c= [:REAL,VV:] by ZFMISC_1:95;
then
A4: dom M = [:REAL,D:] by A3,XBOOLE_1:28;
now
let y be object;
thus y in D implies ex x being object st x in dom M & y = M.x
proof
assume
A5: y in D;
then reconsider v1 = y as Element of VV;
A6: [jj,y] in [:REAL,D:] by A5,ZFMISC_1:87;
then M.[1,y] = 1 * v1 by FUNCT_1:49
.= y by RLVECT_1:def 8;
hence thesis by A4,A6;
end;
given x being object such that
A7: x in dom M and
A8: y = M.x;
consider x1,x2 being object such that
A9: x1 in REAL and
A10: x2 in D and
A11: x = [x1,x2] by A4,A7,ZFMISC_1:def 2;
reconsider xx1 = x1 as Real by A9;
reconsider v2 = x2 as Element of VV by A10;
[x1,x2] in [:REAL,V1:] by A9,A10,ZFMISC_1:87;
then y = xx1 * v2 by A8,A11,FUNCT_1:49;
hence y in D by A2,A10,RLSUB_1:def 1;
end;
then D = rng M by FUNCT_1:def 3;
then reconsider M as Function of [:REAL,D:],D by A4,FUNCT_2:def 1,RELSET_1:4;
set A = (the addF of V)||V1;
dom(the addF of V) = [:VV,VV:] by FUNCT_2:def 1;
then
A12: dom A = [:VV,VV:] /\ [:V1,V1:] by RELAT_1:61;
then reconsider S as Function of [:D,D:],REAL by FUNCT_2:32;
A13: dom A = [:D,D:] by A12,XBOOLE_1:28;
now
let y be object;
thus y in D implies ex x being object st x in dom A & y = A.x
proof
assume
A14: y in D;
then reconsider v1 = y, v0 = d1 as Element of VV;
A15: [d1,y] in [:D,D:] by A14,ZFMISC_1:87;
then A.[d1,y] = v0 + v1 by FUNCT_1:49
.= y by RLVECT_1:4;
hence thesis by A13,A15;
end;
given x being object such that
A16: x in dom A and
A17: y = A.x;
consider x1,x2 being object such that
A18: x1 in D & x2 in D and
A19: x = [x1,x2] by A13,A16,ZFMISC_1:def 2;
reconsider v1 = x1, v2 = x2 as Element of VV by A18;
[x1,x2] in [:V1,V1:] by A18,ZFMISC_1:87;
then y = v1 + v2 by A17,A19,FUNCT_1:49;
hence y in D by A2,A18,RLSUB_1:def 1;
end;
then D = rng A by FUNCT_1:def 3;
then reconsider A as Function of [:D,D:],D by A13,FUNCT_2:def 1,RELSET_1:4;
set W = UNITSTR (# D,d1,A,M,S #);
W is Subspace of V by Th18;
hence thesis;
end;
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
:Def2:
the carrier of it = {0.V};
correctness by Th24,Th29,RLSUB_1:4;
end;
definition
let V being RealUnitarySpace;
func (Omega).V -> strict Subspace of V equals
the UNITSTR of V;
coherence
proof
set W = the UNITSTR of V;
A1: for u,v,w being VECTOR of W holds (u + v) + w = u + (v + w)
proof
let u,v,w be VECTOR of W;
reconsider u9=u,v9=v,w9=w as VECTOR of V;
thus (u + v) + w = (u9 + v9) + w9 .= u9 + (v9 + w9) by RLVECT_1:def 3
.= u + (v + w);
end;
A2: for v being VECTOR of W holds v + 0.W = v
proof
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
thus v + 0.W = v9 + 0.V .= v by RLVECT_1:4;
end;
A3: W is right_complementable
proof
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
consider w9 being VECTOR of V such that
A4: v9 + w9 = 0.V by ALGSTR_0:def 11;
reconsider w=w9 as VECTOR of W;
take w;
thus thesis by A4;
end;
A5: for v being VECTOR of W holds jj * v = v
proof
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
thus jj * v = 1 * v9 .= v by RLVECT_1:def 8;
end;
A6: for a,b be Real, v being VECTOR of W holds (a + b) * v = a * v
+ b * v
proof
let a,b be Real;
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
thus (a + b) * v = (a + b) * v9 .= a * v9 + b * v9 by RLVECT_1:def 6
.= a * v + b * v;
end;
A7: for a be Real ,v,w being VECTOR of W holds a * (v + w) = a * v
+ a * w
proof
let a be Real;
let v,w be VECTOR of W;
reconsider v9=v,w9=w as VECTOR of V;
thus a * (v + w) = a * (v9 + w9) .= a * v9 + a * w9 by RLVECT_1:def 5
.= a * v + a * w;
end;
A8: for a be Real,v,w be VECTOR of W, v9,w9 be VECTOR of V
st v = v9 & w = w9
holds v+w = v9+w9 & a*v = a*v9 & v .|. w = v9 .|. w9;
A9: for v,w being VECTOR of W holds v + w = w + v
proof
let v,w be VECTOR of W;
reconsider v9=v,w9=w as VECTOR of V;
thus v + w = w9 + v9 by A8
.= w + v;
end;
A10: 0.W = 0.V;
A11: W is RealUnitarySpace-like
proof
let x,y,z be VECTOR of W;
let a be Real;
reconsider x9 = x as VECTOR of V;
reconsider y9 = y as VECTOR of V;
reconsider z9 = z as VECTOR of V;
A12: (x+y) .|. z = (x9+y9) .|. z9
.= x9 .|. z9 + y9 .|. z9 by BHSP_1:def 2;
x9 .|. x9 = x .|. x;
hence x .|. x = 0 iff x = 0.W by A10,BHSP_1:def 2;
x9 .|. x9 = x .|. x;
hence 0 <= x .|. x by BHSP_1:def 2;
x9 .|. y9 = x .|. y;
hence x .|. y = y .|. x by A8;
thus (x+y) .|. z = x .|. z + y .|. z by A12;
(a*x) .|. y = (a*x9) .|. y9
.= a * (x9 .|. y9) by BHSP_1:def 2;
hence (a*x) .|. y = a * ( x .|. y );
end;
for a,b be Real, v being VECTOR of W holds (a * b) * v = a * (
b * v)
proof
let a,b be Real;
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
thus (a * b) * v = (a * b) * v9 .= a * (b * v9) by RLVECT_1:def 7
.= a * (b * v);
end;
then reconsider W as RealUnitarySpace by A9,A1,A2,A3,A7,A6,A5,A11,
RLVECT_1: def 2,def 3,def 4,def 5,def 6,def 7,def 8;
A13: the scalar of W = (the scalar of V)||the carrier of W & the addF of W
= (the addF of V)||the carrier of W by RELSET_1:19;
0.W = 0.V & the Mult of W = (the Mult of V)|([:REAL, the carrier of W
:]) by RELSET_1:19;
hence thesis by A13,Def1;
end;
end;
begin :: Theorems of Zero Subspace and Improper Subspace
theorem Th30:
for V being RealUnitarySpace, W being Subspace of V holds (0).W = (0).V
proof
let V be RealUnitarySpace;
let W be Subspace of V;
the carrier of (0).W = {0.W} & the carrier of (0).V = {0.V} by Def2;
then
A1: the carrier of (0).W = the carrier of (0).V by Def1;
(0).W is Subspace of V by Th21;
hence thesis by A1,Th24;
end;
theorem Th31:
for V being RealUnitarySpace, W1,W2 being Subspace of V holds (0).W1 = (0).W2
proof
let V be RealUnitarySpace;
let W1,W2 be Subspace of V;
(0).W1 = (0).V by Th30;
hence thesis by Th30;
end;
theorem
for V being RealUnitarySpace, W being Subspace of V holds (0).W is
Subspace of V by Th21;
theorem
for V being RealUnitarySpace, W being Subspace of V holds (0).V is
Subspace of W
proof
let V be RealUnitarySpace;
let W be Subspace of V;
the carrier of (0).V = {0.V} by Def2
.= {0.W} by Def1;
hence thesis by Th22;
end;
theorem
for V being RealUnitarySpace, W1,W2 being Subspace of V holds (0).W1
is Subspace of W2
proof
let V be RealUnitarySpace;
let W1,W2 be Subspace of V;
(0).W1 = (0).W2 by Th31;
hence thesis;
end;
theorem
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
{v + u where u is VECTOR of V : u in W};
coherence
proof
set Y = {v + u where u is VECTOR of V : u in W};
defpred P[object] means ex u being VECTOR of V st $1 = v + u & u in W;
consider X being set such that
A1: for x being object holds x in X iff x in the carrier of V & P[x] from
XBOOLE_0:sch 1;
X c= the carrier of V
by A1;
then reconsider X as Subset of V;
A2: Y c= X
proof
let x be object;
assume x in Y;
then ex u being VECTOR of V st x = v + u & u in W;
hence thesis by A1;
end;
X c= Y
proof
let x be object;
assume x in X;
then ex u being VECTOR of V st x = v + u & u in W by A1;
hence thesis;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
end;
Lm2: for V being RealUnitarySpace, W being Subspace of V holds 0.V + W = the
carrier of W
proof
let V be RealUnitarySpace;
let W be Subspace of V;
set A = {0.V + u where u is VECTOR of V : u in W};
A1: the carrier of W c= A
proof
let x be object;
assume x in the carrier of W;
then
A2: x in W;
then x in V by Th2;
then reconsider y = x as Element of V;
0.V + y = x by RLVECT_1:4;
hence thesis by A2;
end;
A c= the carrier of W
proof
let x be object;
assume x in A;
then consider u being VECTOR of V such that
A3: x = 0.V + u and
A4: u in W;
x = u by A3,RLVECT_1:4;
hence thesis by A4;
end;
hence thesis by A1;
end;
definition
let V be RealUnitarySpace;
let W be Subspace of V;
mode Coset of W -> Subset of V means
:Def5:
ex v be VECTOR of V st it = v + W;
existence
proof
reconsider VW = the carrier of W as Subset of V by Def1;
take VW;
take 0.V;
thus thesis by Lm2;
end;
end;
begin :: Theorems of the Cosets
theorem Th36:
for V being RealUnitarySpace, W being Subspace of V, v being
VECTOR of V holds 0.V in v + W iff v in W
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let v be VECTOR of V;
thus 0.V in v + W implies v in W
proof
assume 0.V in v + W;
then consider u being VECTOR of V such that
A1: 0.V = v + u and
A2: u in W;
v = - u by A1,RLVECT_1:def 10;
hence thesis by A2,Th16;
end;
assume v in W;
then
A3: - v in W by Th16;
0.V = v - v by RLVECT_1:15
.= v + (- v);
hence thesis by A3;
end;
theorem Th37:
for V being RealUnitarySpace, W being Subspace of V, v being
VECTOR of V holds v in v + W
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let v be VECTOR of V;
v + 0.V = v & 0.V in W by Th11,RLVECT_1:4;
hence thesis;
end;
theorem
for V being RealUnitarySpace, W being Subspace of V holds 0.V + W =
the carrier of W by Lm2;
theorem Th39:
for V being RealUnitarySpace, v being VECTOR of V holds v + (0). V = {v}
proof
let V be RealUnitarySpace;
let v be VECTOR of V;
thus v + (0).V c= {v}
proof
let x be object;
assume x in v + (0).V;
then consider u being VECTOR of V such that
A1: x = v + u and
A2: u in (0).V;
A3: the carrier of (0).V = {0.V} by Def2;
u in the carrier of (0).V by A2;
then u = 0.V by A3,TARSKI:def 1;
then x = v by A1,RLVECT_1:4;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {v};
then
A4: x = v by TARSKI:def 1;
0.V in (0).V & v = v + 0.V by Th11,RLVECT_1:4;
hence thesis by A4;
end;
Lm3: 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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let v be VECTOR of V;
0.V in W & v + 0.V = v by Th11,RLVECT_1:4;
then
A1: v in {v + u where u is VECTOR of V : u in W};
thus v in W implies v + W = the carrier of W
proof
assume
A2: v in W;
thus v + W c= the carrier of W
proof
let x be object;
assume x in v + W;
then consider u being VECTOR of V such that
A3: x = v + u and
A4: u in W;
v + u in W by A2,A4,Th14;
hence thesis by A3;
end;
let x be object;
assume x in the carrier of W;
then reconsider y = x, z = v as Element of W by A2;
reconsider y1 = y, z1 = z as VECTOR of V by Th3;
A5: z + (y - z) = (y + z) - z by RLVECT_1:def 3
.= y + (z - z) by RLVECT_1:def 3
.= y + 0.W by RLVECT_1:15
.= x by RLVECT_1:4;
y - z in W;
then
A6: y1 - z1 in W by Th10;
y - z = y1 - z1 by Th10;
then z1 + (y1 - z1) = x by A5,Th6;
hence thesis by A6;
end;
assume
A7: v + W = the carrier of W;
assume not v in W;
hence thesis by A7,A1;
end;
theorem Th40:
for V being RealUnitarySpace, v being VECTOR of V holds v +
(Omega).V = the carrier of V
by STRUCT_0:def 5,Lm3;
theorem Th41:
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
by Th36,Lm3;
theorem
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 by Lm3;
theorem Th43:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let v be VECTOR of V;
let a be Real;
assume
A1: v in W;
thus (a * v) + W c= the carrier of W
proof
let x be object;
assume x in (a * v) + W;
then consider u being VECTOR of V such that
A2: x = a * v + u and
A3: u in W;
a * v in W by A1,Th15;
then a * v + u in W by A3,Th14;
hence thesis by A2;
end;
let x be object;
assume
A4: x in the carrier of W;
then
A5: x in W;
the carrier of W c= the carrier of V by Def1;
then reconsider y = x as Element of V by A4;
A6: a * v + (y - a * v) = (y + a * v) - a * v by RLVECT_1:def 3
.= y + (a * v - a * v) by RLVECT_1:def 3
.= y + 0.V by RLVECT_1:15
.= x by RLVECT_1:4;
a * v in W by A1,Th15;
then y - a * v in W by A5,Th17;
hence thesis by A6;
end;
theorem Th44:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let v be VECTOR of V;
let a be Real;
assume that
A1: a <> 0 and
A2: (a * v) + W = the carrier of W;
assume not v in W;
then not 1 * v in W by RLVECT_1:def 8;
then not (a" * a) * v in W by A1,XCMPLX_0:def 7;
then not a" * (a * v) in W by RLVECT_1:def 7;
then
A3: not a * v in W by Th15;
0.V in W & a * v + 0.V = a * v by Th11,RLVECT_1:4;
then a * v in {a * v + u where u is VECTOR of V : u in W};
hence contradiction by A2,A3;
end;
theorem Th45:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let v be VECTOR of V;
v in W iff ((- jj) * v) + W = the carrier of W by Th43,Th44;
hence thesis by RLVECT_1:16;
end;
theorem Th46:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let u,v be VECTOR of V;
thus u in W implies v + W = (v + u) + W
proof
assume
A1: u in W;
thus v + W c= (v + u) + W
proof
let x be object;
assume x in v + W;
then consider v1 being VECTOR of V such that
A2: x = v + v1 and
A3: v1 in W;
A4: (v + u) + (v1 - u) = v + (u + (v1 - u)) by RLVECT_1:def 3
.= v + ((v1 + u) - u) by RLVECT_1:def 3
.= v + (v1 + (u - u)) by RLVECT_1:def 3
.= v + (v1 + 0.V) by RLVECT_1:15
.= x by A2,RLVECT_1:4;
v1 - u in W by A1,A3,Th17;
hence thesis by A4;
end;
let x be object;
assume x in (v + u) + W;
then consider v2 being VECTOR of V such that
A5: x = (v + u) + v2 and
A6: v2 in W;
A7: x = v + (u + v2) by A5,RLVECT_1:def 3;
u + v2 in W by A1,A6,Th14;
hence thesis by A7;
end;
assume
A8: v + W = (v + u) + W;
0.V in W & v + 0.V = v by Th11,RLVECT_1:4;
then v in (v + u) + W by A8;
then consider u1 being VECTOR of V such that
A9: v = (v + u) + u1 and
A10: u1 in W;
v = v + 0.V & v = v + (u + u1) by A9,RLVECT_1:4,def 3;
then u + u1 = 0.V by RLVECT_1:8;
then u = - u1 by RLVECT_1:def 10;
hence thesis by A10,Th16;
end;
theorem
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let u,v be VECTOR of V;
A1: - u in W implies u in W
proof
assume - u in W;
then - (- u) in W by Th16;
hence thesis by RLVECT_1:17;
end;
- u in W iff v + W = (v + (- u)) + W by Th46;
hence thesis by A1,Th16;
end;
theorem Th48:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let u,v be VECTOR of V;
thus v in u + W implies u + W = v + W
proof
assume v in u + W;
then consider z being VECTOR of V such that
A1: v = u + z and
A2: z in W;
thus u + W c= v + W
proof
let x be object;
assume x in u + W;
then consider v1 being VECTOR of V such that
A3: x = u + v1 and
A4: v1 in W;
v - z = u + (z - z) by A1,RLVECT_1:def 3
.= u + 0.V by RLVECT_1:15
.= u by RLVECT_1:4;
then
A5: x = v + (v1 + (- z)) by A3,RLVECT_1:def 3
.= v + (v1 - z);
v1 - z in W by A2,A4,Th17;
hence thesis by A5;
end;
let x be object;
assume x in v + W;
then consider v2 being VECTOR of V such that
A6: x = v + v2 & v2 in W;
z + v2 in W & x = u + (z + v2) by A1,A2,A6,Th14,RLVECT_1:def 3;
hence thesis;
end;
thus thesis by Th37;
end;
theorem Th49:
for V being RealUnitarySpace, W being Subspace of V, v being
VECTOR of V holds v + W = (- v) + W iff v in W
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let v be VECTOR of V;
thus v + W = (- v) + W implies v in W
proof
assume v + W = (- v) + W;
then v in (- v) + W by Th37;
then consider u being VECTOR of V such that
A1: v = - v + u and
A2: u in W;
0.V = v - (- v + u) by A1,RLVECT_1:15
.= (v - (- v)) - u by RLVECT_1:27
.= (v + v) - u by RLVECT_1:17
.= (1 * v + v) - u by RLVECT_1:def 8
.= (1 * v + 1 * v) - u by RLVECT_1:def 8
.= ((1 + 1) * v) - u by RLVECT_1:def 6
.= 2 * v - u;
then 2" * (2 * v) = 2" * u by RLVECT_1:21;
then (2" * 2) * v = 2" * u by RLVECT_1:def 7;
then v = 2" * u by RLVECT_1:def 8;
hence thesis by A2,Th15;
end;
assume
A3: v in W;
then v + W = the carrier of W by Lm3;
hence thesis by A3,Th45;
end;
theorem Th50:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let u,v1,v2 be VECTOR of V;
assume that
A1: u in v1 + W and
A2: u in v2 + W;
consider x1 being VECTOR of V such that
A3: u = v1 + x1 and
A4: x1 in W by A1;
consider x2 being VECTOR of V such that
A5: u = v2 + x2 and
A6: x2 in W by A2;
thus v1 + W c= v2 + W
proof
let x be object;
assume x in v1 + W;
then consider u1 being VECTOR of V such that
A7: x = v1 + u1 and
A8: u1 in W;
x2 - x1 in W by A4,A6,Th17;
then
A9: (x2 - x1) + u1 in W by A8,Th14;
u - x1 = v1 + (x1 - x1) by A3,RLVECT_1:def 3
.= v1 + 0.V by RLVECT_1:15
.= v1 by RLVECT_1:4;
then x = (v2 + (x2 - x1)) + u1 by A5,A7,RLVECT_1:def 3
.= v2 + ((x2 - x1) + u1) by RLVECT_1:def 3;
hence thesis by A9;
end;
let x be object;
assume x in v2 + W;
then consider u1 being VECTOR of V such that
A10: x = v2 + u1 and
A11: u1 in W;
x1 - x2 in W by A4,A6,Th17;
then
A12: (x1 - x2) + u1 in W by A11,Th14;
u - x2 = v2 + (x2 - x2) by A5,RLVECT_1:def 3
.= v2 + 0.V by RLVECT_1:15
.= v2 by RLVECT_1:4;
then x = (v1 + (x1 - x2)) + u1 by A3,A10,RLVECT_1:def 3
.= v1 + ((x1 - x2) + u1) by RLVECT_1:def 3;
hence thesis by A12;
end;
theorem
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
by Th50,Th49;
theorem Th52:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let v be VECTOR of V;
let a be Real;
assume that
A1: a <> 1 and
A2: a * v in v + W;
A3: a - 1 <> 0 by A1;
consider u being VECTOR of V such that
A4: a * v = v + u and
A5: u in W by A2;
u = u + 0.V by RLVECT_1:4
.= u + (v - v) by RLVECT_1:15
.= a * v - v by A4,RLVECT_1:def 3
.= a * v - 1 * v by RLVECT_1:def 8
.= (a - 1) * v by RLVECT_1:35;
then (a - 1)" * u = ((a - 1)" * (a - 1)) * v by RLVECT_1:def 7;
then 1 * v = (a - 1)" * u by A3,XCMPLX_0:def 7;
then v = (a - 1)" * u by RLVECT_1:def 8;
hence thesis by A5,Th15;
end;
theorem Th53:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let v be VECTOR of V;
let a be Real;
assume v in W;
then
A1: (a - 1) * v in W by Th15;
a * v = ((a - 1) + 1) * v .= (a - 1) * v + 1 * v by RLVECT_1:def 6
.= v + (a - 1) * v by RLVECT_1:def 8;
hence thesis by A1;
end;
theorem
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of
V holds - v in v + W iff v in W
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let v be VECTOR of V;
(- jj) * v = - v by RLVECT_1:16;
hence thesis by Th52,Th53;
end;
theorem Th55:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let u,v be VECTOR of V;
thus u + v in v + W implies u in W
proof
assume u + v in v + W;
then ex v1 being VECTOR of V st u + v = v + v1 & v1 in W;
hence thesis by RLVECT_1:8;
end;
assume u in W;
hence thesis;
end;
theorem
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let u,v be VECTOR of V;
A1: v - u = (- u) + v;
A2: - u in W implies - (- u) in W by Th16;
u in W implies - u in W by Th16;
hence thesis by A1,A2,Th55,RLVECT_1:17;
end;
theorem Th57:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let u,v be VECTOR of V;
thus u in v + W implies ex v1 being VECTOR of V st v1 in W & u = v + v1
proof
assume u in v + W;
then ex v1 being VECTOR of V st u = v + v1 & v1 in W;
hence thesis;
end;
given v1 being VECTOR of V such that
A1: v1 in W & u = v + v1;
thus thesis by A1;
end;
theorem
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let u,v be VECTOR of V;
thus u in v + W implies ex v1 being VECTOR of V st v1 in W & u = v - v1
proof
assume u in v + W;
then consider v1 being VECTOR of V such that
A1: u = v + v1 and
A2: v1 in W;
take x = - v1;
thus x in W by A2,Th16;
thus thesis by A1,RLVECT_1:17;
end;
given v1 being VECTOR of V such that
A3: v1 in W and
A4: u = v - v1;
- v1 in W by A3,Th16;
hence thesis by A4;
end;
theorem Th59:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let v1,v2 be VECTOR of V;
thus (ex v being VECTOR of V st v1 in v + W & v2 in v + W) implies v1 - v2
in W
proof
given v be VECTOR of V such that
A1: v1 in v + W and
A2: v2 in v + W;
consider u2 being VECTOR of V such that
A3: u2 in W and
A4: v2 = v + u2 by A2,Th57;
consider u1 being VECTOR of V such that
A5: u1 in W and
A6: v1 = v + u1 by A1,Th57;
v1 - v2 = (u1 + v) + ((- v) - u2) by A6,A4,RLVECT_1:30
.= ((u1 + v) + (- v)) - u2 by RLVECT_1:def 3
.= (u1 + (v + (- v))) - u2 by RLVECT_1:def 3
.= (u1 + 0.V) - u2 by RLVECT_1:5
.= u1 - u2 by RLVECT_1:4;
hence thesis by A5,A3,Th17;
end;
assume v1 - v2 in W;
then
A7: - (v1 - v2) in W by Th16;
take v1;
thus v1 in v1 + W by Th37;
v1 + (- (v1 - v2)) = v1 + ((- v1) + v2) by RLVECT_1:33
.= (v1 + (- v1)) + v2 by RLVECT_1:def 3
.= 0.V + v2 by RLVECT_1:5
.= v2 by RLVECT_1:4;
hence thesis by A7;
end;
theorem Th60:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let u,v be VECTOR of V;
assume v + W = u + W;
then v in u + W by Th37;
then consider u1 being VECTOR of V such that
A1: v = u + u1 and
A2: u1 in W;
take v1 = u - v;
0.V = (u + u1) - v by A1,RLVECT_1:15
.= u1 + (u - v) by RLVECT_1:def 3;
then v1 = - u1 by RLVECT_1:def 10;
hence v1 in W by A2,Th16;
thus v + v1 = (u + v) - v by RLVECT_1:def 3
.= u + (v - v) by RLVECT_1:def 3
.= u + 0.V by RLVECT_1:15
.= u by RLVECT_1:4;
end;
theorem Th61:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let u,v be VECTOR of V;
assume v + W = u + W;
then u in v + W by Th37;
then consider u1 being VECTOR of V such that
A1: u = v + u1 and
A2: u1 in W;
take v1 = v - u;
0.V = (v + u1) - u by A1,RLVECT_1:15
.= u1 + (v - u) by RLVECT_1:def 3;
then v1 = - u1 by RLVECT_1:def 10;
hence v1 in W by A2,Th16;
thus v - v1 = (v - v) + u by RLVECT_1:29
.= 0.V + u by RLVECT_1:15
.= u by RLVECT_1:4;
end;
theorem Th62:
for V being RealUnitarySpace, W1,W2 being strict Subspace of V,
v being VECTOR of V holds v + W1 = v + W2 iff W1 = W2
proof
let V be RealUnitarySpace;
let W1,W2 be strict Subspace of V;
let v be VECTOR of V;
thus v + W1 = v + W2 implies W1 = W2
proof
assume
A1: v + W1 = v + W2;
the carrier of W1 = the carrier of W2
proof
A2: the carrier of W1 c= the carrier of V by Def1;
thus the carrier of W1 c= the carrier of W2
proof
let x be object;
assume
A3: x in the carrier of W1;
then reconsider y = x as Element of V by A2;
set z = v + y;
x in W1 by A3;
then z in v + W2 by A1;
then consider u being VECTOR of V such that
A4: z = v + u and
A5: u in W2;
y = u by A4,RLVECT_1:8;
hence thesis by A5;
end;
let x be object;
assume
A6: x in the carrier of W2;
the carrier of W2 c= the carrier of V by Def1;
then reconsider y = x as Element of V by A6;
set z = v + y;
x in W2 by A6;
then z in v + W1 by A1;
then consider u being VECTOR of V such that
A7: z = v + u and
A8: u in W1;
y = u by A7,RLVECT_1:8;
hence thesis by A8;
end;
hence thesis by Th24;
end;
thus thesis;
end;
theorem Th63:
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
proof
let V be RealUnitarySpace;
let W1,W2 be strict Subspace of V;
let u,v be VECTOR of V;
assume
A1: v + W1 = u + W2;
set V2 = the carrier of W2;
set V1 = the carrier of W1;
assume
A2: W1 <> W2;
A3: now
set x = the Element of V1 \ V2;
assume V1 \ V2 <> {};
then x in V1 by XBOOLE_0:def 5;
then
A4: x in W1;
then x in V by Th2;
then reconsider x as Element of V;
set z = v + x;
z in u + W2 by A1,A4;
then consider u1 being VECTOR of V such that
A5: z = u + u1 and
A6: u1 in W2;
x = 0.V + x by RLVECT_1:4
.= v - v + x by RLVECT_1:15
.= - v + (u + u1) by A5,RLVECT_1:def 3;
then
A7: (v + (- v + (u + u1))) + W1 = v + W1 by A4,Th46;
v + (- v + (u + u1)) = (v - v) + (u + u1) by RLVECT_1:def 3
.= 0.V + (u + u1) by RLVECT_1:15
.= u + u1 by RLVECT_1:4;
then (u + u1) + W2 = (u + u1) + W1 by A1,A6,A7,Th46;
hence thesis by A2,Th62;
end;
A8: now
set x = the Element of V2 \ V1;
assume V2 \ V1 <> {};
then x in V2 by XBOOLE_0:def 5;
then
A9: x in W2;
then x in V by Th2;
then reconsider x as Element of V;
set z = u + x;
z in v + W1 by A1,A9;
then consider u1 being VECTOR of V such that
A10: z = v + u1 and
A11: u1 in W1;
x = 0.V + x by RLVECT_1:4
.= u - u + x by RLVECT_1:15
.= - u + (v + u1) by A10,RLVECT_1:def 3;
then
A12: (u + (- u + (v + u1))) + W2 = u + W2 by A9,Th46;
u + (- u + (v + u1)) = (u - u) + (v + u1) by RLVECT_1:def 3
.= 0.V + (v + u1) by RLVECT_1:15
.= v + u1 by RLVECT_1:4;
then (v + u1) + W1 = (v + u1) + W2 by A1,A11,A12,Th46;
hence thesis by A2,Th62;
end;
V1 <> V2 by A2,Th24;
then not V1 c= V2 or not V2 c= V1;
hence thesis by A3,A8,XBOOLE_1:37;
end;
theorem
for V being RealUnitarySpace, W being Subspace of V, C being Coset of
W holds C is linearly-closed iff C = the carrier of W
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let C be Coset of W;
thus C is linearly-closed implies C = the carrier of W
proof
assume
A1: C is linearly-closed;
consider v being VECTOR of V such that
A2: C = v + W by Def5;
C <> {} by A2,Th37;
then 0.V in v + W by A1,A2,RLSUB_1:1;
hence thesis by A2,Th41;
end;
thus thesis by Lm1;
end;
theorem
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
proof
let V be RealUnitarySpace;
let W1,W2 be strict Subspace of V;
let C1 be Coset of W1;
let C2 be Coset of W2;
( ex v1 being VECTOR of V st C1 = v1 + W1)& ex v2 being VECTOR of V st
C2 = v2 + W2 by Def5;
hence thesis by Th63;
end;
theorem
for V being RealUnitarySpace, v being VECTOR of V holds {v} is Coset of (0).V
proof
let V be RealUnitarySpace;
let v be VECTOR of V;
v + (0).V = {v} by Th39;
hence thesis by Def5;
end;
theorem
for V being RealUnitarySpace, V1 being Subset of V holds V1 is Coset
of (0).V implies ex v being VECTOR of V st V1 = {v}
proof
let V be RealUnitarySpace;
let V1 be Subset of V;
assume V1 is Coset of (0).V;
then consider v being VECTOR of V such that
A1: V1 = v + (0).V by Def5;
take v;
thus thesis by A1,Th39;
end;
theorem
for V being RealUnitarySpace, W being Subspace of V holds the carrier
of W is Coset of W
proof
let V be RealUnitarySpace;
let W be Subspace of V;
the carrier of W = 0.V + W by Lm2;
hence thesis by Def5;
end;
theorem
for V being RealUnitarySpace holds the carrier of V is Coset of (Omega).V
proof
let V be RealUnitarySpace;
set v = the VECTOR of V;
the carrier of V is Subset of V iff the carrier of V c= the carrier of V;
then reconsider A = the carrier of V as Subset of V;
A = v + (Omega).V by Th40;
hence thesis by Def5;
end;
theorem
for V being RealUnitarySpace, V1 being Subset of V st V1 is Coset of
(Omega).V holds V1 = the carrier of V
proof
let V be RealUnitarySpace;
let V1 be Subset of V;
assume V1 is Coset of (Omega).V;
then ex v being VECTOR of V st V1 = v + (Omega).V by Def5;
hence thesis by Th40;
end;
theorem
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let C be Coset of W;
ex v being VECTOR of V st C = v + W by Def5;
hence thesis by Th41;
end;
theorem Th72:
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let C be Coset of W;
let u be VECTOR of V;
thus u in C implies C = u + W
proof
assume
A1: u in C;
ex v being VECTOR of V st C = v + W by Def5;
hence thesis by A1,Th48;
end;
thus thesis by Th37;
end;
theorem
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let C be Coset of W;
let u,v be VECTOR of V;
assume u in C & v in C;
then C = u + W & C = v + W by Th72;
hence thesis by Th60;
end;
theorem
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let C be Coset of W;
let u,v be VECTOR of V;
assume u in C & v in C;
then C = u + W & C = v + W by Th72;
hence thesis by Th61;
end;
theorem
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let v1,v2 be VECTOR of V;
thus (ex C being Coset of W st v1 in C & v2 in C) implies v1 - v2 in W
proof
given C be Coset of W such that
A1: v1 in C & v2 in C;
ex v being VECTOR of V st C = v + W by Def5;
hence thesis by A1,Th59;
end;
assume v1 - v2 in W;
then consider v being VECTOR of V such that
A2: v1 in v + W & v2 in v + W by Th59;
reconsider C = v + W as Coset of W by Def5;
take C;
thus thesis by A2;
end;
theorem
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
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let u be VECTOR of V;
let B,C be Coset of W;
assume
A1: u in B & u in C;
( ex v1 being VECTOR of V st B = v1 + W)& ex v2 being VECTOR of V st C =
v2 + W by Def5;
hence thesis by A1,Th50;
end;