:: Subspaces and Cosets of Subspaces in Vector Space
:: by Wojciech A. Trybulec
::
:: Received July 27, 1990
:: Copyright (c) 1990-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 RLVECT_1, ALGSTR_0, BINOP_1, VECTSP_1, LATTICES, XBOOLE_0,
SUBSET_1, ARYTM_1, RELAT_1, ARYTM_3, RLSUB_1, SUPINF_2, GROUP_1,
STRUCT_0, TARSKI, REALSET1, ZFMISC_1, FUNCT_1, MESFUNC1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, REALSET1, FUNCT_1,
FUNCT_2, STRUCT_0, ALGSTR_0, DOMAIN_1, BINOP_1, RLVECT_1, GROUP_1,
VECTSP_1;
constructors PARTFUN1, BINOP_1, REALSET1, VECTSP_1, RLVECT_1, RELSET_1,
GROUP_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, REALSET1, STRUCT_0, VECTSP_1,
RELAT_1, ALGSTR_0;
requirements SUBSET, BOOLE;
definitions TARSKI, RLVECT_1, XBOOLE_0, ALGSTR_0, VECTSP_1;
equalities BINOP_1, REALSET1, STRUCT_0, ALGSTR_0, VECTSP_1;
expansions TARSKI, XBOOLE_0, STRUCT_0;
theorems FUNCT_1, FUNCT_2, TARSKI, VECTSP_1, ZFMISC_1, RLVECT_1, RELAT_1,
VECTSP_2, RELSET_1, XBOOLE_0, XBOOLE_1, ALGSTR_0;
schemes XBOOLE_0;
begin
reserve x,y,y1,y2 for object;
Lm1: for GF be add-associative right_zeroed right_complementable Abelian
commutative associative well-unital distributive non empty doubleLoopStr, V
be Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over GF, a,b being Element of GF, v being Element of V holds (
a - b) * v = a * v - b * v
proof
let GF be add-associative right_zeroed right_complementable Abelian
commutative associative well-unital distributive non empty doubleLoopStr, V
be Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over GF, a,b be Element of GF, v be Element of V;
thus (a - b) * v = a * v + (- b) * v by VECTSP_1:def 15
.= a * v - b * v by VECTSP_1:21;
end;
definition
let GF be non empty multMagma;
let V be non empty ModuleStr over GF;
let V1 be Subset of V;
attr V1 is linearly-closed means
(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;
theorem Th1:
for GF be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr, V be
Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over GF, V1 be Subset of V st V1 <> {} & V1 is linearly-closed
holds 0.V in V1
proof
let GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF, V1 be Subset of V;
assume that
A1: V1 <> {} and
A2: V1 is linearly-closed;
set x = the Element of V1;
reconsider x as Element of V by A1,TARSKI:def 3;
0.GF * x in V1 by A1,A2;
hence thesis by VECTSP_1:14;
end;
theorem Th2:
for GF be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr, V be
Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over GF, V1 be Subset of V st V1 is linearly-closed for v
being Element of V st v in V1 holds - v in V1
proof
let GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF, V1 be Subset of V;
assume
A1: V1 is linearly-closed;
let v be Element of V;
assume v in V1;
then (- 1_GF) * v in V1 by A1;
hence thesis by VECTSP_1:14;
end;
theorem
for GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF, V1 be Subset of V st V1 is linearly-closed for v,u being
Element of V st v in V1 & u in V1 holds v - u in V1
proof
let GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF, V1 be Subset of V;
assume
A1: V1 is linearly-closed;
let v,u be Element of V;
assume that
A2: v in V1 and
A3: u in V1;
- u in V1 by A1,A3,Th2;
hence thesis by A1,A2;
end;
theorem Th4:
for GF be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr, V be
Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over GF holds {0.V} is linearly-closed
proof
let GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF;
thus for v,u being Element of V st v in {0.V} & u in {0.V} holds v + u in {
0.V}
proof
let v,u be Element of V;
assume v in {0.V} & u in {0.V};
then v = 0.V & u = 0.V by TARSKI:def 1;
then v + u = 0.V by RLVECT_1:4;
hence thesis by TARSKI:def 1;
end;
let a be Element of GF;
let v be Element of V;
assume
A1: v in {0.V};
then v = 0.V by TARSKI:def 1;
hence thesis by A1,VECTSP_1:14;
end;
theorem
for GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF, V1 be Subset of V st the carrier of V = V1 holds V1 is
linearly-closed;
theorem
for GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF, V1,V2,V3 be Subset of V st V1 is linearly-closed & V2 is
linearly-closed & V3 = {v + u where v is Element of V, u is Element of V : v in
V1 & u in V2} holds V3 is linearly-closed
proof
let GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF, V1,V2,V3 be Subset of V;
assume that
A1: V1 is linearly-closed & V2 is linearly-closed and
A2: V3 = {v + u where v is Element of V, u is Element of V : v in V1 & u
in V2};
thus for v,u being Element of V st v in V3 & u in V3 holds v + u in V3
proof
let v,u be Element of V;
assume that
A3: v in V3 and
A4: u in V3;
consider v1,v2 being Element of V such that
A5: v = v1 + v2 and
A6: v1 in V1 & v2 in V2 by A2,A3;
consider u1,u2 being Element of V such that
A7: u = u1 + u2 and
A8: u1 in V1 & u2 in V2 by A2,A4;
A9: v + u = ((v1 + v2) + u1) + u2 by A5,A7,RLVECT_1:def 3
.= ((v1 + u1) + v2) + u2 by RLVECT_1:def 3
.= (v1 + u1) + (v2 + u2) by RLVECT_1:def 3;
v1 + u1 in V1 & v2 + u2 in V2 by A1,A6,A8;
hence thesis by A2,A9;
end;
let a be Element of GF;
let v be Element of V;
assume v in V3;
then consider v1,v2 being Element of V such that
A10: v = v1 + v2 and
A11: v1 in V1 & v2 in V2 by A2;
A12: a * v = a * v1 + a * v2 by A10,VECTSP_1:def 14;
a * v1 in V1 & a * v2 in V2 by A1,A11;
hence thesis by A2,A12;
end;
theorem
for GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF, V1,V2 be Subset of V st V1 is linearly-closed & V2 is
linearly-closed holds V1 /\ V2 is linearly-closed
proof
let GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF, V1,V2 be Subset of V;
assume that
A1: V1 is linearly-closed and
A2: V2 is linearly-closed;
thus for v,u being Element of V st v in V1 /\ V2 & u in V1 /\ V2 holds v + u
in V1 /\ V2
proof
let v,u be Element of V;
assume
A3: v in V1 /\ V2 & u in V1 /\ V2;
then v in V2 & u in V2 by XBOOLE_0:def 4;
then
A4: v + u in V2 by A2;
v in V1 & u in V1 by A3,XBOOLE_0:def 4;
then v + u in V1 by A1;
hence thesis by A4,XBOOLE_0:def 4;
end;
let a be Element of GF;
let v be Element of V;
assume
A5: v in V1 /\ V2;
then v in V2 by XBOOLE_0:def 4;
then
A6: a * v in V2 by A2;
v in V1 by A5,XBOOLE_0:def 4;
then a * v in V1 by A1;
hence thesis by A6,XBOOLE_0:def 4;
end;
definition
let GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF;
mode Subspace of V -> Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over GF means
:Def2:
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 lmult of it = (the lmult of V) |([:the carrier of
GF, the carrier of it:] qua set);
existence
proof
take V;
thus the carrier of V c= the carrier of V & 0.V = 0.V;
thus thesis by RELSET_1:19;
end;
end;
reserve GF for add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr,
V,X,Y for Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr 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;
theorem
x in W1 & W1 is Subspace of W2 implies x in W2
proof
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 Def2;
hence thesis;
end;
theorem Th9:
x in W implies x in V
proof
assume x in W;
then
A1: x in the carrier of W;
the carrier of W c= the carrier of V by Def2;
hence thesis by A1;
end;
theorem Th10:
w is Element of V
proof
w in V by Th9,RLVECT_1:1;
hence thesis;
end;
theorem
0.W = 0.V by Def2;
theorem
0.W1 = 0.W2
proof
thus 0.W1 = 0.V by Def2
.= 0.W2 by Def2;
end;
theorem Th13:
w1 = v & w2 = u implies w1 + w2 = v + u
proof
assume
A1: v = w1 & u = w2;
w1 + w2 = ((the addF of V)||the carrier of W).[w1,w2] by Def2;
hence thesis by A1,FUNCT_1:49;
end;
theorem Th14:
w = v implies a * w = a * v
proof
assume
A1: w = v;
a * w = ((the lmult of V) | ([:the carrier of GF, the carrier of W:] qua
set) ).[a,w] by Def2;
hence thesis by A1,FUNCT_1:49;
end;
theorem Th15:
w = v implies - v = - w
proof
A1: - v = (- 1_GF) * v & - w = (- 1_GF) * w by VECTSP_1:14;
assume w = v;
hence thesis by A1,Th14;
end;
theorem Th16:
w1 = v & w2 = u implies w1 - w2 = v - u
proof
assume that
A1: w1 = v and
A2: w2 = u;
- w2 = - u by A2,Th15;
hence thesis by A1,Th13;
end;
Lm2: the carrier of W = V1 implies V1 is linearly-closed
proof
set VW = the carrier of W;
reconsider WW = W as Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over GF;
assume
A1: the carrier of W = V1;
thus for v,u st v in V1 & u in V1 holds v + u in V1
proof
let v,u;
assume v in V1 & u in V1;
then reconsider vv = v, uu = u as Element of WW by A1;
reconsider vw = vv + uu as Element of VW;
vw in V1 by A1;
hence thesis by Th13;
end;
let a,v;
assume v in V1;
then reconsider vv = v as Element of WW by A1;
reconsider vw = a * vv as Element of VW;
vw in V1 by A1;
hence thesis by Th14;
end;
theorem Th17:
0.V in W
proof
0.W in W;
hence thesis by Def2;
end;
theorem
0.W1 in W2
proof
0.W1 = 0.V by Def2;
hence thesis by Th17;
end;
theorem
0.W in V by Th9,RLVECT_1:1;
theorem Th20:
u in W & v in W implies u + v in W
proof
reconsider VW = the carrier of W as Subset of V by Def2;
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 Lm2;
then u + v in the carrier of W by A1;
hence thesis;
end;
theorem Th21:
v in W implies a * v in W
proof
reconsider VW = the carrier of W as Subset of V by Def2;
assume v in W;
then
A1: v in the carrier of W;
VW is linearly-closed by Lm2;
then a * v in the carrier of W by A1;
hence thesis;
end;
theorem Th22:
v in W implies - v in W
proof
assume v in W;
then (- 1_GF) * v in W by Th21;
hence thesis by VECTSP_1:14;
end;
theorem Th23:
u in W & v in W implies u - v in W
proof
assume that
A1: u in W and
A2: v in W;
- v in W by A2,Th22;
hence thesis by A1,Th20;
end;
theorem Th24:
V is Subspace of V
proof
A1: the lmult of V = (the lmult of V) |([:the carrier of GF, the carrier of
V:] qua set) by RELSET_1:19;
0.V = 0.V & the addF of V = (the addF of V)||the carrier of V by RELSET_1:19;
hence thesis by A1,Def2;
end;
theorem Th25:
for X,V being strict Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over GF holds V is
Subspace of X & X is Subspace of V implies V = X
proof
let X,V be strict Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over GF;
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,Def2;
then
A3: VV = VX;
set AX = the addF of X;
set AV = the addF of V;
AV = AX||VV & AX = AV||VX by A1,A2,Def2;
then
A4: AV = AX by A3;
set MX = the lmult of X;
set MV = the lmult of V;
A5: MX = MV |([:the carrier of GF,VX:] qua set) by A2,Def2;
0.V = 0.X & MV = MX |([:the carrier of GF,VV:] qua set) by A1,Def2;
hence thesis by A3,A4,A5;
end;
theorem Th26:
V is Subspace of X & X is Subspace of Y implies V is Subspace of Y
proof
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,Def2;
then
A3: the carrier of V c= the carrier of Y;
A4: 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,Def2;
then
A5: [:VV,VV:] c= [:VX,VX:] by ZFMISC_1:96;
AV = AX||VV by A1,Def2;
then AV = AY||VX||VV by A2,Def2;
hence thesis by A5,FUNCT_1:51;
end;
set MY = the lmult of Y;
set MX = the lmult of X;
set MV = the lmult of V;
set VX = the carrier of X;
set VV = the carrier of V;
VV c= VX by A1,Def2;
then
A6: [:the carrier of GF,VV:] c= [:the carrier of GF,the carrier of X:] by
ZFMISC_1:95;
MV = MX |([:the carrier of GF,VV:] qua set) by A1,Def2;
then MV = MY |([:the carrier of GF,VX:] qua set) |([:the carrier of GF,VV:]
qua set) by A2,Def2;
then
A7: MV = MY |([:the carrier of GF,VV:] qua set) by A6,FUNCT_1:51;
0.V = 0.X by A1,Def2;
then 0.V = 0.Y by A2,Def2;
hence thesis by A3,A4,A7,Def2;
end;
theorem Th27:
the carrier of W1 c= the carrier of W2 implies W1 is Subspace of W2
proof
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
set MW1 = the lmult of W1;
set MW2 = the lmult of W2;
set AV = the addF of V;
set MV = the lmult of V;
A1: (the addF of W1) = AV||VW1 & (the addF of W2) = AV||VW2 by Def2;
assume
A2: the carrier of W1 c= the carrier of W2;
then [:VW1,VW1:] c= [:VW2,VW2:] by ZFMISC_1:96;
then
A3: the addF of W1 = (the addF of W2)||the carrier of W1 by A1,FUNCT_1:51;
A4: MW1 = MV |([:the carrier of GF,VW1:] qua set) & MW2 = MV |([:the carrier
of GF,VW2:] qua set) by Def2;
[:the carrier of GF,VW1:] c= [:the carrier of GF,VW2:] by A2,ZFMISC_1:95;
then
A5: MW1 = MW2 |([:the carrier of GF,VW1:] qua set) by A4,FUNCT_1:51;
0.W1 = 0.V & 0.W2 = 0.V by Def2;
hence thesis by A2,A3,A5,Def2;
end;
theorem Th28:
(for v st v in W1 holds v in W2) implies W1 is Subspace of W2
proof
assume
A1: for 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 Def2;
then reconsider v = x as Element of V by A2;
v in W1 by A2;
then v in W2 by A1;
hence thesis;
end;
hence thesis by Th27;
end;
registration
let GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over GF;
cluster strict for Subspace of V;
existence
proof
set M = the lmult of V;
set W = ModuleStr (# the carrier of V,the addF of V,0.V,M #);
A1: W is vector-distributive
proof
let a be Element of GF;
let v,w be Element of W;
reconsider x = v, y = w as Element of V;
thus a * (v + w) = a * (x + y) .= a * x + a * y by VECTSP_1:def 14
.= a * v + a * w;
end;
A2: W is scalar-distributive
proof
let a,b be Element of GF;
let v be Element of W;
reconsider x = v as Element of V;
thus (a + b) * v = (a + b) * x .= a * x + b * x by VECTSP_1:def 15
.= a * v + b * v;
end;
A3: W is scalar-associative
proof
let a,b be Element of GF;
let v be Element of W;
reconsider x = v as Element of V;
thus a * b * v = a * b * x .= a * (b * x) by VECTSP_1:def 16
.= a * (b * v);
end;
A4: W is scalar-unital
proof
let v be Element of W;
reconsider x = v as Element of V;
thus 1.GF * v = 1_GF * x .= v;
end;
A5: for a,b be Element of W for x,y be Element of V st x = a & b = y holds
a + b = x + y;
W is Abelian add-associative right_zeroed right_complementable
proof
thus W is Abelian
proof
let a,b be Element of W;
reconsider x = a, y = b as Element of V;
thus a + b = y + x by A5
.= b + a;
end;
hereby
let a,b,c be Element of W;
reconsider x = a, y = b, z = c as Element of V;
thus a + b + c = x + y + z .= x + (y + z) by RLVECT_1:def 3
.= a + (b + c);
end;
hereby
let a be Element of W;
reconsider x = a as Element of V;
thus a + 0.W = x + 0.V .= a by RLVECT_1:4;
end;
let a be Element of W;
reconsider x = a as Element of V;
reconsider b = (comp V).x as Element of W;
take b;
thus a + b = x + - x by VECTSP_1:def 13
.= 0.W by RLVECT_1:5;
end;
then reconsider
W as Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over GF by A1,A2,A3,A4;
A6: 0.W = 0.V & the addF of W = (the addF of V)||the carrier of W by
RELSET_1:19;
the lmult of W = (the lmult of V) | ([:the carrier of GF, the carrier
of W:] qua set) by RELSET_1:19;
then reconsider W as Subspace of V by A6,Def2;
take W;
thus thesis;
end;
end;
theorem Th29:
for W1,W2 being strict Subspace of V st the carrier of W1 = the
carrier of W2 holds W1 = W2
proof
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 Th27;
hence thesis by Th25;
end;
theorem Th30:
for W1,W2 being strict Subspace of V st (for v holds v in W1 iff
v in W2) holds W1 = W2
proof
let W1,W2 be strict Subspace of V;
assume
A1: for 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 Def2;
then reconsider v = x as Element 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 Def2;
then reconsider v = x as Element 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 Th29;
end;
theorem
for V being strict Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over GF, W being strict
Subspace of V holds the carrier of W = the carrier of V implies W = V
proof
let V be strict Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over GF, W be strict Subspace of V;
assume
A1: the carrier of W = the carrier of V;
V is Subspace of V by Th24;
hence thesis by A1,Th29;
end;
theorem
for V being strict Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over GF, W being strict
Subspace of V holds (for v being Element of V holds v in W) implies W = V
proof
let V be strict Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over GF, W be strict Subspace of V;
assume for v being Element of V holds v in W;
then
A1: for v be Element of V holds ( v in W iff v in V);
V is Subspace of V by Th24;
hence thesis by A1,Th30;
end;
theorem
the carrier of W = V1 implies V1 is linearly-closed by Lm2;
theorem Th34:
V1 <> {} & V1 is linearly-closed implies ex W being strict
Subspace of V st V1 = the carrier of W
proof
assume that
A1: V1 <> {} and
A2: V1 is linearly-closed;
reconsider D = V1 as non empty set by A1;
reconsider d = 0.V as Element of D by A2,Th1;
set VV = the carrier of V;
set C = (comp V) | D;
dom(comp V) = VV by FUNCT_2:def 1;
then
A3: dom C = D by RELAT_1:62;
A4: rng C c= D
proof
let x be object;
assume x in rng C;
then consider y being object such that
A5: y in dom C and
A6: C.y = x by FUNCT_1:def 3;
reconsider y as Element of V by A3,A5;
x = (comp V).y by A5,A6,FUNCT_1:47
.= - y by VECTSP_1:def 13;
hence thesis by A2,A3,A5,Th2;
end;
set M = (the lmult of V) |([:the carrier of GF,D:] qua set);
dom(the lmult of V) = [:the carrier of GF,VV:] by FUNCT_2:def 1;
then
A7: dom M = [:the carrier of GF,D:] by RELAT_1:62,ZFMISC_1:96;
A8: rng M c= D
proof
let x be object;
assume x in rng M;
then consider y being object such that
A9: y in dom M and
A10: M.y = x by FUNCT_1:def 3;
consider y1,y2 being object such that
A11: [y1,y2] = y by A7,A9,RELAT_1:def 1;
reconsider y1 as Element of GF by A7,A9,A11,ZFMISC_1:87;
A12: y2 in V1 by A7,A9,A11,ZFMISC_1:87;
then reconsider y2 as Element of V;
x = y1 * y2 by A9,A10,A11,FUNCT_1:47;
hence thesis by A2,A12;
end;
set A = (the addF of V)||D;
dom(the addF of V) = [:VV,VV:] by FUNCT_2:def 1;
then
A13: dom A = [:D,D:] by RELAT_1:62,ZFMISC_1:96;
A14: rng A c= D
proof
let x be object;
assume x in rng A;
then consider y being object such that
A15: y in dom A and
A16: A.y = x by FUNCT_1:def 3;
consider y1,y2 being object such that
A17: [y1,y2] = y by A13,A15,RELAT_1:def 1;
A18: y1 in D & y2 in D by A13,A15,A17,ZFMISC_1:87;
then reconsider y1,y2 as Element of V;
x = y1 + y2 by A15,A16,A17,FUNCT_1:47;
hence thesis by A2,A18;
end;
reconsider M as Function of [:the carrier of GF,D:], D by A7,A8,FUNCT_2:def 1
,RELSET_1:4;
reconsider C as UnOp of D by A3,A4,FUNCT_2:def 1,RELSET_1:4;
reconsider A as BinOp of D by A13,A14,FUNCT_2:def 1,RELSET_1:4;
set W = ModuleStr (# D,A,d,M #);
A19: for a,b be Element of W for x,y be Element of V st x = a & b = y holds
a + b = x + y
proof
let a,b be Element of W;
let x,y be Element of V such that
A20: x = a & b = y;
thus a + b = A.[a,b] .= x + y by A13,A20,FUNCT_1:47;
end;
A21: W is Abelian add-associative right_zeroed right_complementable
proof
thus W is Abelian
proof
let a,b be Element of W;
reconsider x = a, y = b as Element of V by TARSKI:def 3;
thus a + b = y + x by A19
.= b + a by A19;
end;
hereby
let a,b,c be Element of W;
reconsider x = a, y = b, z = c as Element of V by TARSKI:def 3;
A22: b + c = y + z by A19;
a + b = x + y by A19;
hence a + b + c = x + y + z by A19
.= x + (y + z) by RLVECT_1:def 3
.= a + (b + c) by A19,A22;
end;
hereby
let a be Element of W;
reconsider x = a as Element of V by TARSKI:def 3;
thus a + 0.W = x + 0.V by A19
.= a by RLVECT_1:4;
end;
let a be Element of W;
reconsider x = a as Element of V by TARSKI:def 3;
reconsider a9 = a as Element of D;
reconsider b = C.a9 as Element of D;
reconsider b as Element of W;
take b;
thus a + b = x + (comp V).x by A3,A19,FUNCT_1:47
.= x + - x by VECTSP_1:def 13
.= 0.W by RLVECT_1:5;
end;
A23: W is vector-distributive
proof
let a be Element of GF;
let v,w be Element of W;
reconsider x = v, y = w as Element of V by TARSKI:def 3;
A24: now
let a be Element of GF;
let x be Element of W;
let y be Element of V;
assume
A25: y = x;
[a,x] in dom M by A7;
hence a * x = a * y by A25,FUNCT_1:47;
end;
then
A26: a * v = a * x;
A27: a * w = a * y by A24;
v + w = x + y by A19;
hence a * (v + w) = a * (x + y) by A24
.= a * x + a * y by VECTSP_1:def 14
.= a * v + a * w by A19,A26,A27;
end;
A28: W is scalar-distributive
proof
let a,b be Element of GF;
let v be Element of W;
reconsider x = v as Element of V by TARSKI:def 3;
A29: now
let a be Element of GF;
let x be Element of W;
let y be Element of V;
assume
A30: y = x;
[a,x] in dom M by A7;
hence a * x = a * y by A30,FUNCT_1:47;
end;
then
A31: a * v = a * x;
A32: b * v = b * x by A29;
thus (a + b) * v = (a + b) * x by A29
.= a * x + b * x by VECTSP_1:def 15
.= a * v + b * v by A19,A32,A31;
end;
A33: W is scalar-associative
proof
let a,b be Element of GF;
let v be Element of W;
reconsider x = v as Element of V by TARSKI:def 3;
A34: now
let a be Element of GF;
let x be Element of W;
let y be Element of V;
assume
A35: y = x;
[a,x] in dom M by A7;
hence a * x = a * y by A35,FUNCT_1:47;
end;
then A36: b * v = b * x;
thus a * b * v = a * b * x by A34
.= a * (b * x) by VECTSP_1:def 16
.= a * (b * v) by A34,A36;
end;
W is scalar-unital
proof
let v be Element of W;
reconsider x = v as Element of V by TARSKI:def 3;
now
let a be Element of GF;
let x be Element of W;
let y be Element of V;
assume
A37: y = x;
[a,x] in dom M by A7;
hence a * x = a * y by A37,FUNCT_1:47;
end;
hence 1.GF * v = 1_GF * x
.= v;
end;
then reconsider
W as Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over GF by A21,A23,A28,A33;
0.W = 0.V;
then reconsider W as strict Subspace of V by Def2;
take W;
thus thesis;
end;
definition
let GF;
let V;
func (0).V -> strict Subspace of V means
:Def3:
the carrier of it = {0.V};
correctness by Th4,Th29,Th34;
end;
definition
let GF;
let V;
func (Omega).V -> strict Subspace of V equals
the ModuleStr of V;
coherence
proof
set W = the ModuleStr of V;
A1: W is vector-distributive
proof
let x be Element of GF, v,w be Element of W;
reconsider v9 = v, w9 = w as Element of V;
thus x*(v+w) = x*(v9+w9) .= x*v9+x*w9 by VECTSP_1:def 14
.= x*v+x*w;
end;
A2: W is scalar-distributive
proof
let x,y be Element of GF, v be Element of W;
reconsider v9 = v as Element of V;
thus (x+y)*v = (x+y)*v9 .= x*v9+y*v9 by VECTSP_1:def 15
.= x*v+y*v;
end;
A3: W is scalar-associative
proof
let x,y be Element of GF, v be Element of W;
reconsider v9 = v as Element of V;
thus (x*y)*v = (x*y)*v9 .= x*(y*v9) by VECTSP_1:def 16
.= x*(y*v);
end;
A4: W is scalar-unital
proof
let v be Element of W;
reconsider v9 = v as Element of V;
thus (1.GF)*v = (1_GF)*v9 .= v;
end;
A5: for a for v,w be Element of W, v9,w9 be Element of V st v=v9 & w=w9
holds v+w = v9+w9 & a*v = a*v9;
W is Abelian add-associative right_zeroed right_complementable
proof
thus W is Abelian
proof
let x,y be Element of W;
reconsider x9 = x, y9 = y as Element of V;
thus x+y = y9+x9 by A5
.= y+x;
end;
hereby
let x,y,z be Element of W;
reconsider x9 = x, y9 = y, z9 = z as Element of V;
thus (x+y)+z = (x9+y9)+z9 .= x9+(y9+z9) by RLVECT_1:def 3
.= x+(y+z);
end;
hereby
let x be Element of W;
reconsider x9 = x as Element of V;
thus x+(0.W) = x9+0.V .= x by RLVECT_1:4;
end;
let x be Element of W;
reconsider x9 = x as Element of V;
consider b being Element of V such that
A6: x9 + b = 0.V by ALGSTR_0:def 11;
reconsider b9 = b as Element of W;
take b9;
thus thesis by A6;
end;
then reconsider
W as Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over GF by A4,A1,A2,A3;
A7: the lmult of W = (the lmult of V) |([:the carrier of GF, the carrier of
W:] qua set) by RELSET_1:19;
0.W = 0.V & the addF of W= (the addF of V)||the carrier of W by RELSET_1:19
;
hence thesis by A7,Def2;
end;
end;
theorem
x in (0).V iff x = 0.V
proof
thus x in (0).V implies x = 0.V
proof
assume x in (0).V;
then x in the carrier of (0).V;
then x in {0.V} by Def3;
hence thesis by TARSKI:def 1;
end;
thus thesis by Th17;
end;
theorem Th36:
(0).W = (0).V
proof
the carrier of (0).W = {0.W} & the carrier of (0).V = {0.V} by Def3;
then
A1: the carrier of (0).W = the carrier of (0).V by Def2;
(0).W is Subspace of V by Th26;
hence thesis by A1,Th29;
end;
theorem Th37:
(0).W1 = (0).W2
proof
(0).W1 = (0).V by Th36;
hence thesis by Th36;
end;
theorem
(0).W is Subspace of V by Th26;
theorem
(0).V is Subspace of W
proof
(0).W = (0).V by Th36;
hence thesis;
end;
theorem
(0).W1 is Subspace of W2
proof
(0).W1 = (0).W2 by Th37;
hence thesis;
end;
theorem
for V being Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over GF holds V is
Subspace of (Omega).V
proof
let V be Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over GF;
reconsider VS = V as Subspace of V by Th24;
for v being Vector of V st v in VS holds v in (Omega).V;
hence thesis by Th28;
end;
definition
let GF;
let V;
let v,W;
func v + W -> Subset of V equals
{v + u : u in W};
coherence
proof
set Y = {v + u : u in W};
defpred Sep[object] means ex u 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 & Sep[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 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 st x = v + u & u in W by A1;
hence thesis;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
end;
Lm3: 0.V + W = the carrier of W
proof
set A = {0.V + u : 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 Th9;
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 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 GF;
let V;
let W;
mode Coset of W -> Subset of V means
:Def6:
ex v st it = v + W;
existence
proof
reconsider VW = the carrier of W as Subset of V by Def2;
take VW;
take 0.V;
thus thesis by Lm3;
end;
end;
reserve B,C for Coset of W;
theorem Th42:
x in v + W iff ex u st u in W & x = v + u
proof
thus x in v + W implies ex u st u in W & x = v + u
proof
assume x in v + W;
then consider u such that
A1: x = v + u & u in W;
take u;
thus thesis by A1;
end;
given u such that
A2: u in W & x = v + u;
thus thesis by A2;
end;
theorem Th43:
0.V in v + W iff v in W
proof
thus 0.V in v + W implies v in W
proof
assume 0.V in v + W;
then consider u such that
A1: 0.V = v + u and
A2: u in W;
v = - u by A1,VECTSP_1:16;
hence thesis by A2,Th22;
end;
assume v in W;
then
A3: - v in W by Th22;
0.V = v + (- v) by VECTSP_1:19;
hence thesis by A3;
end;
theorem Th44:
v in v + W
proof
v + 0.V = v & 0.V in W by Th17,RLVECT_1:4;
hence thesis;
end;
theorem
0.V + W = the carrier of W by Lm3;
theorem Th46:
v + (0).V = {v}
proof
thus v + (0).V c= {v}
proof
let x be object;
assume x in v + (0).V;
then consider u such that
A1: x = v + u and
A2: u in (0).V;
A3: the carrier of (0).V = {0.V} by Def3;
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 Th17,RLVECT_1:4;
hence thesis by A4;
end;
Lm4: v in W iff v + W = the carrier of W
proof
0.V in W & v + 0.V = v by Th17,RLVECT_1:4;
then
A1: v in {v + u : 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 such that
A3: x = v + u and
A4: u in W;
v + u in W by A2,A4,Th20;
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 Element of V by Th10;
A5: z + (y - z) = y + (z + (- z)) by RLVECT_1:def 3
.= y + 0.W by VECTSP_1:19
.= x by RLVECT_1:4;
y - z in W;
then
A6: y1 - z1 in W by Th16;
y - z = y1 - z1 by Th16;
then z1 + (y1 - z1) = x by A5,Th13;
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 Th47:
v + (Omega).V = the carrier of V
by RLVECT_1:1,Lm4;
theorem Th48:
0.V in v + W iff v + W = the carrier of W
by Th43,Lm4;
theorem
v in W iff v + W = the carrier of W by Lm4;
theorem Th50:
v in W implies (a * v) + W = the carrier of W
by Th21,Lm4;
theorem Th51:
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
proof
let GF be Field, V be VectSp of GF, a be Element of GF, v be Element of V, W
be Subspace of V;
assume that
A1: a <> 0.GF and
A2: (a * v) + W = the carrier of W;
assume not v in W;
then not 1_GF * v in W;
then not (a" * a) * v in W by A1,VECTSP_1:def 10;
then not a" * (a * v) in W by VECTSP_1:def 16;
then
A3: not a * v in W by Th21;
0.V in W & a * v + 0.V = a * v by Th17,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
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
proof
let GF be Field, V be VectSp of GF, v be Element of V, W be Subspace of V;
- 1_GF <> 0.GF by VECTSP_2:3;
then v in W iff ((- 1_GF) * v) + W = the carrier of W by Th50,Th51;
hence thesis by VECTSP_1:14;
end;
theorem Th53:
u in W iff v + W = (v + u) + W
proof
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 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 VECTSP_1:19
.= x by A2,RLVECT_1:4;
v1 - u in W by A1,A3,Th23;
hence thesis by A4;
end;
let x be object;
assume x in (v + u) + W;
then consider v2 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,Th20;
hence thesis by A7;
end;
assume
A8: v + W = (v + u) + W;
0.V in W & v + 0.V = v by Th17,RLVECT_1:4;
then v in (v + u) + W by A8;
then consider u1 such that
A9: v = (v + u) + u1 and
A10: u1 in W;
v = v + (u + u1) by A9,RLVECT_1:def 3;
then u + u1 = 0.V by RLVECT_1:9;
then u = - u1 by VECTSP_1:16;
hence thesis by A10,Th22;
end;
theorem
u in W iff v + W = (v - u) + W
proof
A1: - u in W implies u in W
proof
assume - u in W;
then - (- u) in W by Th22;
hence thesis by RLVECT_1:17;
end;
- u in W iff v + W = (v + (- u)) + W by Th53;
hence thesis by A1,Th22;
end;
theorem Th55:
v in u + W iff u + W = v + W
proof
thus v in u + W implies u + W = v + W
proof
assume v in u + W;
then consider z being Element 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 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 VECTSP_1:19
.= 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,Th23;
hence thesis by A5;
end;
let x be object;
assume x in v + W;
then consider v2 such that
A6: x = v + v2 & v2 in W;
z + v2 in W & x = u + (z + v2) by A1,A2,A6,Th20,RLVECT_1:def 3;
hence thesis;
end;
thus thesis by Th44;
end;
theorem Th56:
u in v1 + W & u in v2 + W implies v1 + W = v2 + W
proof
assume that
A1: u in v1 + W and
A2: u in v2 + W;
thus v1 + W = u + W by A1,Th55
.= v2 + W by A2,Th55;
end;
theorem
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
proof
let GF be Field, V be VectSp of GF, a be Element of GF, v be Element of V, W
be Subspace of V;
assume that
A1: a <> 1_GF and
A2: a * v in v + W;
A3: a - 1_GF <> 0.GF by A1,RLVECT_1:21;
consider u being Element 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 VECTSP_1:19
.= a * v - v by A4,RLVECT_1:def 3
.= a * v - 1_GF * v
.= (a - 1_GF) * v by Lm1;
then (a - 1_GF)" * u = ((a - 1_GF)" * (a - 1_GF)) * v by VECTSP_1:def 16;
then 1_GF * v = (a - 1_GF)" * u by A3,VECTSP_1:def 10;
then v = (a - 1_GF)" * u;
hence thesis by A5,Th21;
end;
theorem Th58:
v in W implies a * v in v + W
proof
assume v in W;
then v + W = the carrier of W & a*v in W by Lm4,Th21;
hence thesis;
end;
theorem
v in W implies - v in v + W
proof
assume v in W;
then (- 1_GF) * v in v + W by Th58;
hence thesis by VECTSP_1:14;
end;
theorem Th60:
u + v in v + W iff u in W
proof
thus u + v in v + W implies u in W
proof
assume u + v in v + W;
then ex v1 st u + v = v + v1 & v1 in W;
hence thesis by RLVECT_1:8;
end;
assume u in W;
hence thesis;
end;
theorem
v - u in v + W iff u in W
proof
A1: v - u = (- u) + v;
A2: - u in W implies - (- u) in W by Th22;
u in W implies - u in W by Th22;
hence thesis by A1,A2,Th60,RLVECT_1:17;
end;
theorem
u in v + W iff ex v1 st v1 in W & u = v - v1
proof
thus u in v + W implies ex v1 st v1 in W & u = v - v1
proof
assume u in v + W;
then consider v1 such that
A1: u = v + v1 and
A2: v1 in W;
take x = - v1;
thus x in W by A2,Th22;
thus thesis by A1,RLVECT_1:17;
end;
given v1 such that
A3: v1 in W and
A4: u = v - v1;
- v1 in W by A3,Th22;
hence thesis by A4;
end;
theorem Th63:
(ex v st v1 in v + W & v2 in v + W) iff v1 - v2 in W
proof
thus (ex v st v1 in v + W & v2 in v + W) implies v1 - v2 in W
proof
given v such that
A1: v1 in v + W and
A2: v2 in v + W;
consider u2 such that
A3: u2 in W and
A4: v2 = v + u2 by A2,Th42;
consider u1 such that
A5: u1 in W and
A6: v1 = v + u1 by A1,Th42;
v1 - v2 = (u1 + v) + ((- v) - u2) by A6,A4,VECTSP_1:17
.= ((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,Th23;
end;
assume v1 - v2 in W;
then
A7: - (v1 - v2) in W by Th22;
take v1;
thus v1 in v1 + W by Th44;
v1 + (- (v1 - v2)) = v1 + ((- v1) + v2) by VECTSP_1:17
.= (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 Th64:
v + W = u + W implies ex v1 st v1 in W & v + v1 = u
proof
assume v + W = u + W;
then v in u + W by Th44;
then consider u1 such that
A1: v = u + u1 and
A2: u1 in W;
take v1 = u - v;
0.V = (u + u1) - v by A1,VECTSP_1:19
.= u1 + (u - v) by RLVECT_1:def 3;
then v1 = - u1 by VECTSP_1:16;
hence v1 in W by A2,Th22;
thus v + v1 = (u + v) - v by RLVECT_1:def 3
.= u + (v - v) by RLVECT_1:def 3
.= u + 0.V by VECTSP_1:19
.= u by RLVECT_1:4;
end;
theorem Th65:
v + W = u + W implies ex v1 st v1 in W & v - v1 = u
proof
assume v + W = u + W;
then u in v + W by Th44;
then consider u1 such that
A1: u = v + u1 and
A2: u1 in W;
take v1 = v - u;
0.V = (v + u1) - u by A1,VECTSP_1:19
.= u1 + (v - u) by RLVECT_1:def 3;
then v1 = - u1 by VECTSP_1:16;
hence v1 in W by A2,Th22;
thus v - v1 = (v - v) + u by RLVECT_1:29
.= 0.V + u by VECTSP_1:19
.= u by RLVECT_1:4;
end;
theorem Th66:
for W1,W2 being strict Subspace of V holds v + W1 = v + W2 iff W1 = W2
proof
let W1,W2 be strict Subspace 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 Def2;
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 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 Def2;
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 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 Th29;
end;
thus thesis;
end;
theorem Th67:
for W1,W2 being strict Subspace of V st v + W1 = u + W2 holds W1 = W2
proof
let W1,W2 be strict Subspace 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 Th9;
then reconsider x as Element of V;
set z = v + x;
z in u + W2 by A1,A4;
then consider u1 such that
A5: z = u + u1 and
A6: u1 in W2;
x = 0.V + x by RLVECT_1:4
.= (v + (- v)) + x by VECTSP_1:19
.= - v + (u + u1) by A5,RLVECT_1:def 3;
then
A7: (v + (- v + (u + u1))) + W1 = v + W1 by A4,Th53;
v + (- v + (u + u1)) = (v + (- v)) + (u + u1) by RLVECT_1:def 3
.= 0.V + (u + u1) by VECTSP_1:19
.= u + u1 by RLVECT_1:4;
then (u + u1) + W2 = (u + u1) + W1 by A1,A6,A7,Th53;
hence thesis by A2,Th66;
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 Th9;
then reconsider x as Element of V;
set z = u + x;
z in v + W1 by A1,A9;
then consider u1 such that
A10: z = v + u1 and
A11: u1 in W1;
x = 0.V + x by RLVECT_1:4
.= (u + (- u)) + x by VECTSP_1:19
.= - u + (v + u1) by A10,RLVECT_1:def 3;
then
A12: (u + (- u + (v + u1))) + W2 = u + W2 by A9,Th53;
u + (- u + (v + u1)) = (u + (- u)) + (v + u1) by RLVECT_1:def 3
.= 0.V + (v + u1) by VECTSP_1:19
.= v + u1 by RLVECT_1:4;
then (v + u1) + W1 = (v + u1) + W2 by A1,A11,A12,Th53;
hence thesis by A2,Th66;
end;
V1 <> V2 by A2,Th29;
then not V1 c= V2 or not V2 c= V1;
hence thesis by A3,A8,XBOOLE_1:37;
end;
theorem
ex C st v in C
proof
reconsider C = v + W as Coset of W by Def6;
take C;
thus thesis by Th44;
end;
theorem
C is linearly-closed iff C = the carrier of W
proof
thus C is linearly-closed implies C = the carrier of W
proof
assume
A1: C is linearly-closed;
consider v such that
A2: C = v + W by Def6;
C <> {} by A2,Th44;
then 0.V in v + W by A1,A2,Th1;
hence thesis by A2,Th48;
end;
thus thesis by Lm2;
end;
theorem
for W1,W2 being strict Subspace of V, C1 being Coset of W1, C2 being
Coset of W2 st C1 = C2 holds W1 = W2
proof
let W1,W2 be strict Subspace of V, C1 be Coset of W1, C2 be Coset of W2;
( ex v1 st C1 = v1 + W1)& ex v2 st C2 = v2 + W2 by Def6;
hence thesis by Th67;
end;
theorem
{v} is Coset of (0).V
proof
v + (0).V = {v} by Th46;
hence thesis by Def6;
end;
theorem
V1 is Coset of (0).V implies ex v st V1 = {v}
proof
assume V1 is Coset of (0).V;
then consider v such that
A1: V1 = v + (0).V by Def6;
take v;
thus thesis by A1,Th46;
end;
theorem
the carrier of W is Coset of W
proof
the carrier of W = 0.V + W by Lm3;
hence thesis by Def6;
end;
theorem
the carrier of V is Coset of (Omega).V
proof
set v = the Element of V;
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 Th47;
hence thesis by Def6;
end;
theorem
V1 is Coset of (Omega).V implies V1 = the carrier of V
proof
assume V1 is Coset of (Omega).V;
then ex v st V1 = v + (Omega).V by Def6;
hence thesis by Th47;
end;
theorem
0.V in C iff C = the carrier of W
proof
ex v st C = v + W by Def6;
hence thesis by Th48;
end;
theorem Th77:
u in C iff C = u + W
proof
thus u in C implies C = u + W
proof
assume
A1: u in C;
ex v st C = v + W by Def6;
hence thesis by A1,Th55;
end;
thus thesis by Th44;
end;
theorem
u in C & v in C implies ex v1 st v1 in W & u + v1 = v
proof
assume u in C & v in C;
then C = u + W & C = v + W by Th77;
hence thesis by Th64;
end;
theorem
u in C & v in C implies ex v1 st v1 in W & u - v1 = v
proof
assume u in C & v in C;
then C = u + W & C = v + W by Th77;
hence thesis by Th65;
end;
theorem
(ex C st v1 in C & v2 in C) iff v1 - v2 in W
proof
thus (ex C st v1 in C & v2 in C) implies v1 - v2 in W
proof
given C such that
A1: v1 in C & v2 in C;
ex v st C = v + W by Def6;
hence thesis by A1,Th63;
end;
assume v1 - v2 in W;
then consider v such that
A2: v1 in v + W & v2 in v + W by Th63;
reconsider C = v + W as Coset of W by Def6;
take C;
thus thesis by A2;
end;
theorem
u in B & u in C implies B = C
proof
assume
A1: u in B & u in C;
( ex v1 st B = v1 + W)& ex v2 st C = v2 + W by Def6;
hence thesis by A1,Th56;
end;
::
:: Auxiliary theorems.
::
theorem
for GF be add-associative right_zeroed right_complementable Abelian
commutative associative well-unital distributive non empty doubleLoopStr, V
be Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over GF, a,b being Element of GF, v being Element of V holds (
a - b) * v = a * v - b * v by Lm1;