:: The Vector Space of Subsets of a Set Based on Disjoint Union
:: by Jesse Alama
::
:: Received October 9, 2007
:: Copyright (c) 2007 Association of Mizar Users
environ
vocabularies FINSET_1, BSPACE, FUNCT_1, CARD_1, SUBSET_1, TARSKI, BOOLE,
RELAT_1, NAT_1, GROUP_1, FINSEQ_1, FINSEQ_2, QC_LANG1, BINOP_1, VECTSP_1,
RLVECT_1, RLVECT_3, RLVECT_2, SEQ_1, FINSEQ_4, FUNCT_4, ORDINAL2,
MATRLIN, VECTSP_9, INT_3, REALSET1, ARYTM;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, DOMAIN_1, RELSET_1,
FUNCT_1, NUMBERS, NAT_1, INT_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_7,
XXREAL_0, CARD_1, FINSET_1, FINSEQ_1, FINSEQOP, CARD_2, REALSET1,
STRUCT_0, GROUP_1, RLVECT_1, VECTSP_1, VECTSP_6, VECTSP_7,
VECTSP_9, INT_3, RANKNULL;
constructors NAT_1, FINSEQOP, HAHNBAN, VECTSP_7, VECTSP_9, REALSET1, WELLORD2,
NAT_D, FUNCT_7, BINOP_1, CARD_2, RANKNULL, INT_3, GR_CY_1;
registrations RELAT_1, STRUCT_0, CARD_1, FINSET_1, FINSEQ_1, REALSET1,
SUBSET_1, XBOOLE_0, VECTSP_1, ORDINAL1, XREAL_0, INT_1;
requirements NUMERALS, BOOLE, ARITHM, SUBSET, REAL;
definitions TARSKI, FUNCT_1, FINSEQ_1, CARD_1, VECTSP_6, XBOOLE_0, VECTSP_1,
RLVECT_1, STRUCT_0, FINSEQ_2, BINOP_1, INT_3;
theorems TARSKI, ZFMISC_1, FINSET_1, FINSEQ_1, FUNCT_1, VECTSP_7, VECTSP_9,
CARD_2, XBOOLE_1, FUNCT_2, SUBSET_1, XBOOLE_0, VECTSP_1, RLVECT_1,
VECTSP_4, VECTSP_6, STRUCT_0, CARD_1, FUNCOP_1, FUNCT_7, FINSEQ_2, NAT_1,
WELLORD2, RANKNULL, MATRIX_3, INT_2, INT_3, GR_CY_1, NAT_D, REALSET1,
ORDINAL1, PARTFUN1, FINSEQ_3;
schemes FINSEQ_1, FINSET_1, BINOP_1, FINSEQ_2, CLASSES1;
begin
definition
let S be 1-sorted;
func <*>S -> FinSequence of S equals
<*>([#]S);
coherence;
end;
:: exactly as in FINSEQ_2
reserve S for 1-sorted,
d for Element of S,
i for Element of NAT,
p for FinSequence,
b,X for set;
:: copied from FINSEQ_2:13
theorem
for p being FinSequence of S st i in dom p holds p.i in S
proof
let p be FinSequence of S;
assume i in dom p;
hence p.i in the carrier of S by FINSEQ_2:13;
end;
:: copied from FINSEQ_2:14
theorem
(for i being Nat st i in dom p holds p.i in S) implies p is FinSequence of S
proof
assume
A1: for i being Nat st i in dom p holds p.i in S;
for i being Nat st i in dom p holds p.i in the carrier of S
proof
let i be Nat;
assume i in dom p;
then p.i in S by A1;
hence thesis by STRUCT_0:def 5;
end;
hence thesis by FINSEQ_2:14;
end;
scheme IndSeqS{S() -> 1-sorted, P[set]}:
for p being FinSequence of S() holds P[p]
provided
A1: P[<*> S()]
and
A2: for p being FinSequence of S() for x being Element of S()
st P[p] holds P[p^<*x*>]
proof
A3: P[<*>the carrier of S()] by A1;
thus for p being FinSequence of the carrier of S() holds P[p]
from FINSEQ_2:sch 2(A3,A2);
end;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: The two-element field Z_2
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
begin
definition
func Z_2 -> Field equals
INT.Ring(2);
coherence by INT_2:44,INT_3:22;
end;
theorem
[#]Z_2 = {0,1} by CARD_1:88;
theorem
for a being Element of Z_2 holds a = 0 or a = 1 by CARD_1:88,TARSKI:def 2;
theorem Th5:
0.Z_2 = 0 by FUNCT_7:def 1,GR_CY_1:12;
theorem Th6:
1.Z_2 = 1 by INT_3:24;
theorem Th7:
1.Z_2 + 1.Z_2 = 0.Z_2
proof
1.Z_2 + 1.Z_2 = (1+1) mod 2 by Th6,GR_CY_1:def 5
.= 0 by NAT_D:25;
hence thesis by FUNCT_7:def 1;
end;
theorem
for x being Element of Z_2 holds x = 0.Z_2 iff x <> 1.Z_2
by Th5,Th6,CARD_1:88,TARSKI:def 2;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Set-theoretical Preliminaries
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
begin
definition
let X,x be set;
func X@x -> Element of Z_2 equals
:Def3:
1.Z_2 if x in X otherwise 0.Z_2;
coherence;
consistency;
end;
theorem
for X,x being set holds X@x = 1.Z_2 iff x in X by Def3;
theorem
for X,x being set holds X@x = 0.Z_2 iff not x in X by Def3;
theorem
for X,x being set holds X@x <> 0.Z_2 iff X@x = 1.Z_2
by Th5,Th6,CARD_1:88,TARSKI:def 2;
theorem
for X,x,y being set holds X@x = X@y iff (x in X iff y in X)
proof
let X,x,y be set;
thus X@x = X@y implies (x in X iff y in X)
proof
assume
A1: X@x = X@y;
thus x in X implies y in X
proof
assume x in X;
then X@x = 1.Z_2 by Def3;
hence thesis by A1,Def3;
end;
assume y in X;
then X@y = 1.Z_2 by Def3;
hence thesis by A1,Def3;
end;
assume
A2: x in X iff y in X;
per cases by Th5,Th6,CARD_1:88,TARSKI:def 2;
suppose X@x = 0.Z_2;
hence thesis by A2,Def3;
end;
suppose X@x = 1.Z_2;
hence thesis by A2,Def3;
end;
end;
theorem
for X,Y,x being set holds X@x = Y@x iff (x in X iff x in Y)
proof
let X,Y,x be set;
thus X@x = Y@x implies (x in X iff x in Y)
proof
assume
A1: X@x = Y@x;
thus x in X implies x in Y
proof
assume x in X;
then X@x = 1.Z_2 by Def3;
hence thesis by A1,Def3;
end;
assume x in Y;
then Y@x = 1.Z_2 by Def3;
hence thesis by A1,Def3;
end;
thus (x in X iff x in Y) implies X@x = Y@x
proof
assume
A2: x in X iff x in Y;
per cases by Th5,Th6,CARD_1:88,TARSKI:def 2;
suppose X@x = 0.Z_2;
hence thesis by A2,Def3;
end;
suppose X@x = 1.Z_2;
hence thesis by A2,Def3;
end;
end;
end;
theorem
for x being set holds {}@x = 0.Z_2 by Def3;
theorem Th15:
for X being set, u,v being Subset of X, x being Element of X
holds (u \+\ v)@x = u@x + v@x
proof
let X be set, u,v be Subset of X, x be Element of X;
per cases;
suppose
A1: x in u \+\ v;
then
A2: (u \+\ v)@x = 1.Z_2 by Def3;
per cases;
suppose
A3: x in u;
then
A4: not x in v by A1,XBOOLE_0:1;
A5: u@x = 1.Z_2 by A3,Def3;
v@x = 0.Z_2 by A4,Def3;
hence thesis by A2,A5,RLVECT_1:10;
end;
suppose
A6: not x in u;
then
A7: x in v by A1,XBOOLE_0:1;
A8: u@x = 0.Z_2 by A6,Def3;
v@x = 1.Z_2 by A7,Def3;
hence thesis by A2,A8,RLVECT_1:10;
end;
end;
suppose
A9: not x in u \+\ v;
then
A10: (u \+\ v)@x = 0.Z_2 by Def3;
per cases;
suppose
A11: x in u;
then
A12: x in v by A9,XBOOLE_0:1;
u@x = 1.Z_2 by A11,Def3;
hence thesis by A10,A12,Def3,Th7;
end;
suppose
A13: not x in u;
then
A14: not x in v by A9,XBOOLE_0:1;
A15: u@x = 0.Z_2 by A13,Def3;
v@x = 0.Z_2 by A14,Def3;
hence thesis by A10,A15,RLVECT_1:10;
end;
end;
end;
theorem
for X,Y being set holds X = Y iff for x being set holds X@x = Y@x
proof
let X,Y be set;
thus X = Y implies for x being set holds X@x = Y@x;
thus (for x being set holds X@x = Y@x) implies X = Y
proof
assume
A1: for x being set holds X@x = Y@x;
thus X c= Y
proof
let y be set such that
A2: y in X;
X@y = 1.Z_2 by A2,Def3;
then Y@y = 1.Z_2 by A1;
hence thesis by Def3;
end;
let y be set such that
A3: y in Y;
Y@y = 1.Z_2 by A3,Def3;
then X@y = 1.Z_2 by A1;
hence thesis by Def3;
end;
end;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: The Boolean Bector Space of Subsets of a Set
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
begin
definition
let X be set, a be Element of Z_2, c be Subset of X;
func a \*\ c -> Subset of X equals
:Def4:
c if a = 1.Z_2, {}X if a = 0.Z_2;
consistency;
coherence;
end;
definition
let X be set;
func bspace-sum(X) -> BinOp of bool X means
:Def5:
for c,d being Subset of X
holds it.(c,d) = c \+\ d;
existence
proof
defpred P[set,set,set] means
ex a,b being Subset of X st $1 = a & $2 = b & $3 = a \+\ b;
A1: for x,y being set st x in bool X & y in bool X ex z being set
st z in bool X & P[x,y,z]
proof
let x,y be set such that
A2: x in bool X and
A3: y in bool X;
reconsider x,y as Subset of X by A2,A3;
set z = x \+\ y;
take z;
thus thesis;
end;
consider f being Function of [:bool X,bool X:],bool X such that
A4: for x,y being set st x in bool X & y in bool X
holds P[x,y,f.(x,y)] from BINOP_1:sch 1(A1);
reconsider f as BinOp of bool X;
A5: for c,d being Subset of X holds f.(c,d) = c \+\ d
proof
let c,d be Subset of X;
consider a,b being Subset of X such that
A6: c = a and
A7: d = b and
A8: f.(c,d) = a \+\ b by A4;
thus thesis by A6,A7,A8;
end;
take f;
thus thesis by A5;
end;
uniqueness
proof
let f,g be BinOp of bool X such that
A9: for c,d being Subset of X holds f.(c,d) = c \+\ d and
A10: for c,d being Subset of X holds g.(c,d) = c \+\ d;
dom f = [:bool X,bool X:] by FUNCT_2:def 1;
then
A11: dom f = dom g by FUNCT_2:def 1;
for x being set st x in dom f holds f.x = g.x
proof
let x be set such that
A12: x in dom f;
consider y,z being set such that
A13: y in bool X and
A14: z in bool X and
A15: x = [y,z] by A12,ZFMISC_1:def 2;
reconsider y as Subset of X by A13;
reconsider z as Subset of X by A14;
f.(y,z) = y \+\ z & g.(y,z) = y \+\ z by A9,A10;
hence thesis by A15;
end;
hence thesis by A11,FUNCT_1:9;
end;
end;
theorem Th17:
for a being Element of Z_2, c,d being Subset of X
holds a \*\ (c \+\ d) = (a \*\ c) \+\ (a \*\ d)
proof
let a be Element of Z_2, c,d be Subset of X;
per cases by Th5,Th6,CARD_1:88,TARSKI:def 2;
suppose a = 0.Z_2;
then a \*\ (c \+\ d) = {}X & a \*\ c = {}X & a \*\ d = {}X by Def4;
hence thesis;
end;
suppose a = 1.Z_2;
then a \*\ (c \+\ d) = c \+\ d & a \*\ c = c & a \*\ d = d by Def4;
hence thesis;
end;
end;
theorem Th18:
for a,b being Element of Z_2, c being Subset of X
holds (a+b) \*\ c = (a \*\ c) \+\ (b \*\ c)
proof
let a,b be Element of Z_2, c be Subset of X;
per cases by Th5,Th6,CARD_1:88,TARSKI:def 2;
suppose
A1: a = 0.Z_2;
then a \*\ c = {}X by Def4;
hence thesis by A1,RLVECT_1:10;
end;
suppose
A2: a = 1.Z_2;
per cases by Th5,Th6,CARD_1:88,TARSKI:def 2;
suppose
A3: b = 0.Z_2;
then b \*\ c = {}X by Def4;
hence thesis by A3,RLVECT_1:10;
end;
suppose
A4: b = 1.Z_2;
then
A5: b \*\ c = c by Def4;
c \+\ c = {}X by XBOOLE_1:92;
hence thesis by A2,A4,A5,Def4,Th7;
end;
end;
end;
theorem
for c being Subset of X holds (1.Z_2) \*\ c = c by Def4;
theorem Th20:
for a,b being Element of Z_2, c being Subset of X
holds a \*\ (b \*\ c) = (a*b) \*\ c
proof
let a,b be Element of Z_2, c be Subset of X;
per cases by Th5,Th6,CARD_1:88,TARSKI:def 2;
suppose
A1: a = 0.Z_2;
then
A2: a*b = 0.Z_2 by VECTSP_1:39;
a \*\ (b \*\ c) = {}X by A1,Def4;
hence thesis by A2,Def4;
end;
suppose
A3: a = 1.Z_2;
then a \*\ (b \*\ c) = b \*\ c by Def4;
hence thesis by A3,VECTSP_1:def 16;
end;
end;
definition
let X be set;
func
bspace-scalar-mult(X) -> Function of [:the carrier of Z_2,bool X:],bool X
means
:Def6:
for a being Element of Z_2, c being Subset of X
holds it.(a,c) = a \*\ c;
existence
proof
defpred P[set,set,set] means ex a being Element of Z_2,
c being Subset of X st $1 = a & $2 = c & $3 = a \*\ c;
A1: for x,y being set st x in the carrier of Z_2 & y in bool X ex z being set
st z in bool X & P[x,y,z]
proof
let x,y be set such that
A2: x in the carrier of Z_2 and
A3: y in bool X;
reconsider x as Element of Z_2 by A2;
reconsider y as Subset of X by A3;
set z = x \*\ y;
take z;
thus thesis;
end;
consider f being Function of [:the carrier of Z_2,bool X:],bool X such that
A4: for x,y being set st x in the carrier of Z_2 & y in bool X
holds P[x,y,f.(x,y)] from BINOP_1:sch 1(A1);
A5: for a being Element of Z_2, c being Subset of X holds f.(a,c) = a \*\ c
proof
let a be Element of Z_2, c be Subset of X;
consider a' being Element of Z_2, c' being Subset of X such that
A6: a = a' and
A7: c = c' and
A8: f.(a,c) = a' \*\ c' by A4;
thus thesis by A6,A7,A8;
end;
take f;
thus thesis by A5;
end;
uniqueness
proof
let f,g be Function of [:the carrier of Z_2,bool X:],bool X such that
A9: for a being Element of Z_2, c being Subset of X
holds f.(a,c) = a \*\ c and
A10: for a being Element of Z_2, c being Subset of X holds g.(a,c) = a \*\ c;
dom f = [:the carrier of Z_2,bool X:] by FUNCT_2:def 1;
then
A11: dom f = dom g by FUNCT_2:def 1;
for x being set st x in dom f holds f.x = g.x
proof
let x be set such that
A12: x in dom f;
consider y,z being set such that
A13: y in the carrier of Z_2 and
A14: z in bool X and
A15: x = [y,z] by A12,ZFMISC_1:def 2;
reconsider y as Element of Z_2 by A13;
reconsider z as Subset of X by A14;
f.(y,z) = y \*\ z & g.(y,z) = y \*\ z by A9,A10;
hence thesis by A15;
end;
hence thesis by A11,FUNCT_1:9;
end;
end;
definition
let X be set;
func bspace(X) -> non empty VectSpStr over Z_2 equals
VectSpStr (# bool X,
bspace-sum(X), {}X, bspace-scalar-mult(X) #);
coherence;
end;
Lm1: for a,b,c being Element of bspace(X), A,B,C being Subset of X
st a = A & b = B & c = C holds a+(b+c) = A \+\ (B \+\ C)
& (a+b)+c = (A \+\ B) \+\ C
proof
let a,b,c be Element of bspace(X);
let A,B,C be Subset of X;
assume
A1: a = A & b = B & c = C;
thus a+(b+c) = A \+\ (B \+\ C)
proof
b+c = B \+\ C by A1,Def5;
hence thesis by A1,Def5;
end;
thus (a+b)+c = (A \+\ B) \+\ C
proof
a+b = A \+\ B by A1,Def5;
hence thesis by A1,Def5;
end;
end;
Lm2: for a,b being Element of Z_2, x,y being Element of bspace(X),
c,d being Subset of X st x = c & y = d holds (a*x)+(b*y)
= (a \*\ c) \+\ (b \*\ d) & a*(x+y) = a \*\ (c \+\ d) &
(a+b)*x = (a+b) \*\ c & (a*b)*x = (a*b) \*\ c & a*(b*x) = a \*\ (b \*\ c)
proof
let a,b be Element of Z_2, x,y be Element of bspace(X), c,d be Subset of X
such that
A1: x = c and
A2: y = d;
thus (a*x)+(b*y) = (a \*\ c) \+\ (b \*\ d)
proof
A3: a*x = a \*\ c by A1,Def6;
b*y = b \*\ d by A2,Def6;
hence thesis by A3,Def5;
end;
thus a*(x+y) = a \*\ (c \+\ d)
proof
A4: x+y = c \+\ d by A1,A2,Def5;
thus thesis by A4,Def6;
end;
thus (a+b)*x = (a+b) \*\ c by A1,Def6;
thus (a*b)*x = (a*b) \*\ c by A1,Def6;
thus a*(b*x) = a \*\ (b \*\ c)
proof
b*x = b \*\ c by A1,Def6;
hence thesis by Def6;
end;
end;
theorem Th21:
bspace(X) is Abelian
proof
let x,y be Element of bspace(X);
reconsider A = x, B = y as Subset of X;
x+y = B \+\ A by Def5
.= y+x by Def5;
hence thesis;
end;
theorem Th22:
bspace(X) is add-associative
proof
let x,y,z be Element of bspace(X);
reconsider A = x, B = y, C = z as Subset of X;
x+(y+z) = A \+\ (B \+\ C) by Lm1
.= (A \+\ B) \+\ C by XBOOLE_1:91
.= (x+y)+z by Lm1;
hence thesis;
end;
theorem Th23:
bspace(X) is right_zeroed
proof
let x be Element of bspace(X);
reconsider A = x as Subset of X;
reconsider Z = 0.bspace(X) as Subset of X;
x+0.bspace(X) = A \+\ Z by Def5
.= x;
hence thesis;
end;
theorem Th24:
bspace(X) is right_complementable
proof
let x be Element of bspace(X);
reconsider A = x as Subset of X;
A1: A \+\ A = {}X by XBOOLE_1:92;
take x;
thus thesis by A1,Def5;
end;
theorem Th25:
for a being Element of Z_2, x,y being Element of bspace(X)
holds a*(x+y) = (a*x)+(a*y)
proof
let a be Element of Z_2, x,y be Element of bspace(X);
reconsider c = x, d = y as Subset of X;
a*(x+y) = a \*\ (c \+\ d) by Lm2
.= (a \*\ c) \+\ (a \*\ d) by Th17
.= (a*x)+(a*y) by Lm2;
hence thesis;
end;
theorem Th26:
for a,b being Element of Z_2, x being Element of bspace(X)
holds (a+b)*x = (a*x)+(b*x)
proof
let a,b be Element of Z_2, x be Element of bspace(X);
reconsider c = x as Subset of X;
(a+b)*x = (a+b) \*\ c by Lm2
.= (a \*\ c) \+\ (b \*\ c) by Th18
.= (a*x)+(b*x) by Lm2;
hence thesis;
end;
theorem Th27:
for a,b being Element of Z_2, x being Element of bspace(X)
holds (a*b)*x = a*(b*x)
proof
let a,b be Element of Z_2, x be Element of bspace(X);
reconsider c = x as Subset of X;
(a*b)*x = (a*b) \*\ c by Lm2
.= a \*\ (b \*\ c) by Th20
.= a*(b*x) by Lm2;
hence thesis;
end;
theorem Th28:
for x being Element of bspace(X) holds (1_Z_2)*x = x
proof
let x be Element of bspace(X);
reconsider c = x as Subset of X;
(1_Z_2)*x = (1_Z_2) \*\ c by Def6
.= c by Def4;
hence thesis;
end;
theorem Th29:
bspace(X) is VectSp-like
proof
let a,b be Element of Z_2, x,y be Element of bspace(X);
thus a*(x+y) = (a*x)+(a*y) by Th25;
thus (a+b)*x = (a*x)+(b*x) by Th26;
thus (a*b)*x = a*(b*x) by Th27;
thus (1.Z_2)*x = x by Th28;
end;
registration
let X be set;
cluster bspace(X) -> VectSp-like Abelian right_complementable
add-associative right_zeroed;
coherence by Th21,Th22,Th23,Th24,Th29;
end;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: The Linear Independence and Linear Span of Singleton Subsets
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
begin
definition
let X be set;
attr X is Singleton means
:Def8:
X is non empty trivial;
end;
registration
cluster Singleton -> non empty trivial set;
coherence by Def8;
cluster non empty trivial -> Singleton set;
coherence by Def8;
end;
definition
let X be set, f be Subset of X;
redefine attr f is Singleton means
:Def9:
ex x being set st x in X & f = {x};
compatibility
proof
thus f is Singleton implies ex x being set st x in X & f = {x}
proof
assume f is Singleton;
then f is non empty trivial by Def8;
then consider x being set such that
A1: f = {x} by REALSET1:def 4;
take x;
x in f by A1,TARSKI:def 1;
hence x in X;
thus thesis by A1;
end;
thus thesis;
end;
end;
definition
let X be set;
func singletons(X) equals
{ f where f is Subset of X : f is Singleton };
coherence;
end;
definition
let X be set;
redefine func singletons(X) -> Subset of bspace(X);
coherence
proof
set S = singletons(X);
S c= bool(X)
proof
let f be set such that
A1: f in S;
consider g being Subset of X such that
A2: f = g and g is Singleton by A1;
reconsider f as Subset of X by A2;
f is Element of bool(X);
hence thesis;
end;
hence thesis;
end;
end;
registration
let X be non empty set;
cluster singletons(X) -> non empty;
coherence
proof
consider x being Element of X;
{x} in singletons(X);
hence thesis;
end;
end;
theorem Th30:
for X being non empty set, f being Subset of X
st f is Element of singletons(X) holds f is Singleton
proof
let X be non empty set, f be Subset of X such that
A1: f is Element of singletons(X);
f in singletons(X) by A1;
then consider g being Subset of X such that
A2: g = f and
A3: g is Singleton;
thus thesis by A2,A3;
end;
definition
let F be Field, V be VectSp of F, l be Linear_Combination of V,
x be Element of V;
redefine func l.x -> Element of F;
coherence
proof
l.x in [#]F;
hence thesis;
end;
end;
definition
let X be non empty set, s be FinSequence of bspace(X), x be Element of X;
func s@x -> FinSequence of Z_2 means
:Def11:
len it = len s
& for j being Nat st 1 <= j & j <= len s holds it.j = (s.j)@x;
existence
proof
deffunc F(set) = (s.$1)@x;
consider p being FinSequence such that
A1: len p = len s and
A2: for k being Nat st k in dom p holds p.k = F(k) from FINSEQ_1:sch 2;
A3: for j being Nat st 1 <= j & j <= len s holds p.j = (s.j)@x
proof
let j be Nat such that
A4: 1 <= j and
A5: j <= len s;
j in dom p by A4,A5,FINSEQ_3:27,A1;
hence thesis by A2;
end;
rng p c= the carrier of Z_2
proof
let y be set such that
A6: y in rng p;
consider a being set such that
A7: a in dom p and
A8: p.a = y by A6,FUNCT_1:def 5;
a is Nat by A7,ORDINAL1:def 13;
then p.a = (s.a)@x by A2,A7;
hence thesis by A8;
end;
then reconsider p as FinSequence of Z_2 by FINSEQ_1:def 4;
take p;
thus thesis by A1,A3;
end;
uniqueness
proof
let f,g be FinSequence of Z_2 such that
A9: len f = len s & for j being Nat st 1 <= j & j <= len s
holds f.j = (s.j)@x and
A10: len g = len s & for j being Nat st 1 <= j & j <= len s
holds g.j = (s.j)@x;
for k being Nat st 1 <= k & k <= len f holds f.k = g.k
proof
let k be Nat such that
A11: 1 <= k and
A12: k <= len f;
f.k = (s.k)@x & g.k = (s.k)@x by A9,A10,A11,A12;
hence thesis;
end;
hence thesis by A9,A10,FINSEQ_1:18;
end;
end;
theorem Th31:
for X being non empty set, x being Element of X
holds (<*>(bspace(X)))@x = <*>Z_2
proof
let X be non empty set, x be Element of X;
set V = bspace(X);
set L = (<*>V)@x;
len L = len <*>V by Def11
.= 0 by CARD_1:47;
hence thesis by CARD_2:59;
end;
theorem Th32:
for X being set, u,v being Element of bspace(X), x being Element of X
holds (u + v)@x = u@x + v@x
proof
let X be set, u,v be Element of bspace(X), x be Element of X;
reconsider u' = u, v' = v as Subset of X;
(u + v)@x = (u' \+\ v')@x by Def5
.= (u'@x) + (v'@x) by Th15;
hence thesis;
end;
theorem Th33:
for X being non empty set, s being FinSequence of bspace(X),
f being Element of bspace(X), x being Element of X
holds (s ^ <*f*>)@x = (s@x) ^ <*f@x*>
proof
let X be non empty set, s be FinSequence of bspace(X),
f be Element of bspace(X), x be Element of X;
set L = (s ^ <*f*>)@x;
set R = (s@x) ^ <*f@x*>;
A1: len L = len (s ^ <*f*>) by Def11
.= (len s) + (len <*f*>) by FINSEQ_1:35
.= (len s) + 1 by FINSEQ_1:56;
A2: len ((s@x) ^ <*f@x*>) = (len (s@x)) + (len <*f@x*>) by FINSEQ_1:35
.= (len s) + (len <*f@x*>) by Def11
.= (len s) + 1 by FINSEQ_1:56;
for k being Nat st 1 <= k & k <= len L holds L.k = R.k
proof
let k be Nat such that
A3: 1 <= k and
A4: k <= len L;
A5: k in NAT by ORDINAL1:def 13;
per cases by A1,A4,NAT_1:8;
suppose
A6: k <= len s;
k <= len (s ^ <*f*>) by A4,Def11;
then
A7: L.k = ((s ^ <*f*>).k)@x by A3,Def11;
dom (s@x) = Seg (len (s@x)) by FINSEQ_1:def 3
.= Seg (len s) by Def11;
then k in dom (s@x) by A3,A5,A6;
then
A8: R.k = (s@x).k by FINSEQ_1:def 7
.= (s.k)@x by A3,A6,Def11;
dom s = Seg (len s) by FINSEQ_1:def 3;
then k in dom s by A3,A5,A6;
hence thesis by A7,A8,FINSEQ_1:def 7;
end;
suppose
A9: k = len L;
A10: k <= len (s ^ <*f*>) by A4,Def11;
A11: len (s@x) = len s by Def11;
dom (<*f@x*>) = {1} by FINSEQ_1:4,def 8;
then 1 in dom (<*f@x*>) by TARSKI:def 1;
then
A12: R.k = <*f@x*>.1 by A1,A9,A11,FINSEQ_1:def 7
.= f@x by FINSEQ_1:def 8;
dom (<*f*>) = {1} by FINSEQ_1:4,def 8;
then 1 in dom (<*f*>) by TARSKI:def 1;
then (s ^ <*f*>).k = <*f*>.1 by A1,A9,FINSEQ_1:def 7
.= f by FINSEQ_1:def 8;
hence thesis by A3,A10,A12,Def11;
end;
end;
hence thesis by A1,A2,FINSEQ_1:18;
end;
theorem Th34:
for X being non empty set, s being FinSequence of bspace(X),
x being Element of X holds (Sum s)@x = Sum (s@x)
proof
let X be non empty set, s be FinSequence of bspace(X), x be Element of X;
set V = bspace(X);
defpred Q[FinSequence of V] means (Sum ($1))@x = Sum (($1)@x);
A1: Q[<*>V]
proof
set e = <*>V;
reconsider z = 0.V as Subset of X;
A2: Sum e = 0.V by RLVECT_1:60;
A3: e@x = <*>Z_2 by Th31;
z@x = 0.Z_2 by Def3;
hence thesis by A2,A3,RLVECT_1:60;
end;
A4: for p being FinSequence of V, f being Element of V st Q[p]
holds Q[p ^ <*f*>]
proof
let p be FinSequence of V, f be Element of V such that
A5: Q[p];
(Sum (p ^ <*f*>))@x = ((Sum p) + (Sum <*f*>))@x by RLVECT_1:58
.= ((Sum p) + f)@x by RLVECT_1:61
.= (Sum p)@x + f@x by Th32
.= Sum (p@x) + Sum (<*f@x*>) by A5,RLVECT_1:61
.= Sum (p@x ^ <*f@x*>) by RLVECT_1:58
.= Sum ((p ^ <*f*>)@x) by Th33;
hence thesis;
end;
for p being FinSequence of V holds Q[p] from IndSeqS(A1,A4);
hence thesis;
end;
theorem Th35:
for X being non empty set, l being Linear_Combination of bspace(X),
x being Element of bspace(X) st x in Carrier l holds l.x = 1_Z_2
proof
let X be non empty set, l be Linear_Combination of bspace(X),
x be Element of bspace(X) such that
A1: x in Carrier l;
l.x <> 0.Z_2 by A1,VECTSP_6:20;
hence thesis by Th5,Th6,CARD_1:88,TARSKI:def 2;
end;
theorem Th36:
singletons {} = {}
proof
set X = {};
assume singletons(X) <> {};
then consider f being set such that
A1: f in singletons(X) by XBOOLE_0:def 1;
consider g being Subset of X such that g = f and
A2: g is Singleton by A1;
consider x being set such that
A3: x in X and g = {x} by A2,Def9;
thus thesis by A3;
end;
theorem Th37:
singletons(X) is linearly-independent
proof
per cases;
suppose
A1: X is empty;
{} = {}(the carrier of bspace(X));
hence thesis by A1,Th36,VECTSP_7:4;
end;
suppose X is non empty;
then reconsider X as non empty set;
set V = bspace(X);
set S = singletons(X);
for l being Linear_Combination of S st Sum l = 0.V holds Carrier l = {}
proof
let l be Linear_Combination of S such that
A2: Sum l = 0.V;
set C = Carrier l;
reconsider s = Sum l as Subset of X;
assume C <> {};
then consider f being Element of V such that
A3: f in C by SUBSET_1:10;
reconsider f as Subset of X;
C c= S by VECTSP_6:def 7;
then f is Singleton by A3,Th30;
then consider x being set such that
A4: x in X and
A5: f = {x} by Def9;
x in f by A5,TARSKI:def 1;
then
A6: f@x = 1.Z_2 by Def3;
reconsider x as Element of X by A4;
A7: s@x = 0.Z_2 by A2,Def3;
A8: for g being Subset of X st g <> f & g in C holds g@x = 0.Z_2
proof
let g be Subset of X such that
A9: g <> f and
A10: g in C;
C c= S by VECTSP_6:def 7;
then g is Singleton by A10,Th30;
then consider y being set such that
A11: y in X and
A12: g = {y} by Def9;
reconsider y as Element of X by A11;
now
assume g@x <> 0.Z_2;
then x in {y} by A12,Def3;
hence contradiction by A5,A9,A12,TARSKI:def 1;
end;
hence thesis;
end;
reconsider g = f as Element of V;
reconsider m = l!(C \ {g}) as Linear_Combination of C \ {g};
reconsider n = l!{g} as Linear_Combination of {g};
reconsider t = Sum m, u = Sum n as Subset of X;
A13: l!(Carrier l) = l by RANKNULL:24;
A14: {g} c= Carrier l by A3,ZFMISC_1:37;
reconsider l as Linear_Combination of C by A13;
l = n + m by A14,RANKNULL:27;
then Sum l = (Sum m) + (Sum n) by VECTSP_6:77;
then s = t \+\ u by Def5;
then
A15: s@x = t@x + u@x by Th15;
A16: t@x = 0
proof
A17: for F being FinSequence of V st F is one-to-one & rng F = Carrier m
holds (m (#) F)@x = (len F) |-> 0.Z_2
proof
let F be FinSequence of V such that F is one-to-one and
A18: rng F = Carrier m;
set L = (m (#) F)@x;
set R = (len F) |-> 0.Z_2;
A19: len (m (#) F) = len F by VECTSP_6:def 8;
then
A20: len L = len F by Def11;
dom R = Seg (len F) by FUNCOP_1:19;
then
A21: len L = len R by A20,FINSEQ_1:def 3;
for k being Nat st 1 <= k & k <= len L holds L.k = R.k
proof
let k be Nat such that
A22: 1 <= k and
A23: k <= len L;
len (m (#) F) = len F by VECTSP_6:def 8;
then
A24: dom (m (#) F) = Seg (len F) by FINSEQ_1:def 3;
A25: k in NAT by ORDINAL1:def 13;
then k in dom (m (#) F) by A20,A22,A23,A24;
then
A26: (m (#) F).k = m.(F/.k)*(F/.k) by VECTSP_6:def 8;
dom F = Seg (len F) by FINSEQ_1:def 3;
then
A27: k in dom F by A20,A22,A23,A25;
then
A28: F/.k = F.k by PARTFUN1:def 8;
then
A29: F/.k in Carrier m by A18,A27,FUNCT_1:12;
reconsider Fk = F/.k as Subset of X;
m.(F/.k) = 1_Z_2 by A18,A27,A28,Th35,FUNCT_1:12;
then
A30: (m (#) F).k = Fk by A26,VECTSP_1:def 26;
A31: Carrier m = C \ {f}
proof
thus Carrier m c= C \ {f} by VECTSP_6:def 7;
thus C \ {f} c= Carrier m
proof
let y be set such that
A32: y in C \ {f};
A33: y in C by A32,XBOOLE_0:def 4;
reconsider y as Element of V by A32;
now
assume
A34: not y in Carrier m;
m.y = l.y by A32,RANKNULL:25;
then l.y = 0.Z_2 by A34;
hence contradiction by A33,VECTSP_6:20;
end;
hence thesis;
end;
end;
A35: Fk <> f
proof
assume Fk = f;
then not f in {f} by A29,A31,XBOOLE_0:def 4;
hence contradiction by TARSKI:def 1;
end;
A36: Fk in C by A29,A31,XBOOLE_0:def 4;
A37: L.k = ((m (#) F).k)@x by A19,A20,A22,A23,Def11
.= 0.Z_2 by A8,A30,A35,A36;
k in Seg (len F) by A20,A22,A23,A25;
hence thesis by A37,FUNCOP_1:13;
end;
hence thesis by A21,FINSEQ_1:18;
end;
consider F being FinSequence of V such that
A38: F is one-to-one and
A39: rng F = Carrier m and
A40: t = Sum (m (#) F) by VECTSP_6:def 9;
A41: (Sum (m (#) F))@x = Sum ((m (#) F)@x) by Th34;
(m (#) F)@x = (len F) |-> 0.Z_2 by A17,A38,A39;
hence thesis by A40,A41,Th5,MATRIX_3:13;
end;
u = f
proof
A42: Sum n = (n.g)*g by VECTSP_6:43;
g in {g} by TARSKI:def 1;
then
A43: n.g = l.g by RANKNULL:25;
l.g <> 0.Z_2 by A3,VECTSP_6:20;
then
A44: l.g = 1_Z_2 by Th5,Th6,CARD_1:88,TARSKI:def 2;
thus thesis by A42,A43,A44,VECTSP_1:def 26;
end;
hence thesis by A6,A7,A15,A16,Th5,RLVECT_1:10;
end;
hence thesis by VECTSP_7:def 1;
end;
end;
theorem
for f being Element of bspace(X) st (ex x being set st x in X & f = {x})
holds f in singletons(X);
theorem Th39:
for X being finite set, A being Subset of X
ex l being Linear_Combination of singletons(X) st Sum l = A
proof
let X be finite set, A be Subset of X;
set V = bspace(X);
set S = singletons(X);
defpred P[set] means $1 is Subset of X
implies ex l being Linear_Combination of S st Sum l = $1;
A1: A is finite;
A2: P[{}]
proof
assume {} is Subset of X;
reconsider l = ZeroLC(V) as Linear_Combination of S by VECTSP_6:26;
A3: Sum l = 0.V by VECTSP_6:41;
take l;
thus thesis by A3;
end;
A4: for x,B being set st x in A & B c= A & P[B] holds P[B \/ {x}]
proof
let x,B be set such that x in A and B c= A and
A5: P[B];
assume
A6: B \/ {x} is Subset of X;
then reconsider B as Subset of X by XBOOLE_1:11;
consider l being Linear_Combination of S such that
A7: Sum l = B by A5;
per cases;
suppose
A8: x in B;
take l;
thus thesis by A7,A8,ZFMISC_1:46;
end;
suppose
A9: not x in B;
reconsider f = {x} as Element of V by A6,XBOOLE_1:11;
reconsider g = f as Subset of X;
reconsider z = ZeroLC(V) as Linear_Combination of {}V by VECTSP_6:26;
set m = z +* (f,1_Z_2);
m is Linear_Combination of {}V \/ {f} by RANKNULL:23;
then reconsider m = z +* (f,1_Z_2) as Linear_Combination of {f};
dom z = [#]V by FUNCT_2:169;
then
A10: m.f = 1_Z_2 by FUNCT_7:33;
A11: B misses {x} by A9,ZFMISC_1:56;
f in S;
then {f} c= S by ZFMISC_1:37;
then m is Linear_Combination of S by VECTSP_6:25;
then reconsider n = l + m as Linear_Combination of S by VECTSP_6:52;
A12: Sum n = (Sum l) + (Sum m) by VECTSP_6:77
.= (Sum l) + (m.f)*f by VECTSP_6:43
.= (Sum l) + f by A10,VECTSP_1:def 26
.= B \+\ g by A7,Def5
.= (B \/ {x}) \ (B /\ {x}) by XBOOLE_1:101
.= (B \/ {x}) \ {} by A11,XBOOLE_0:def 7
.= B \/ {x};
take n;
thus thesis by A12;
end;
end;
P[A] from FINSET_1:sch 2(A1,A2,A4);
hence thesis;
end;
theorem Th40:
for X being finite set holds Lin(singletons(X)) = bspace(X)
proof
let X be finite set;
set V = bspace(X);
set S = singletons(X);
for v being Element of V holds v in Lin(S)
proof
let v be Element of V;
reconsider f = v as Subset of X;
consider A being set such that
A1: A c= X and
A2: f = A;
reconsider A as Subset of X by A1;
consider l being Linear_Combination of S such that
A3: Sum l = A by Th39;
thus thesis by A2,A3,VECTSP_7:12;
end;
hence thesis by VECTSP_4:40;
end;
theorem Th41:
for X being finite set holds singletons(X) is Basis of bspace(X)
proof
let X be finite set;
A1: singletons(X) is linearly-independent by Th37;
Lin(singletons(X)) = bspace(X) by Th40;
hence thesis by A1,VECTSP_7:def 3;
end;
registration
let X be finite set;
cluster singletons(X) -> finite;
coherence by FINSET_1:13;
end;
registration
let X be finite set;
cluster bspace(X) -> finite-dimensional;
coherence
proof
set S = singletons(X);
A1: S is Basis of bspace(X) by Th41;
thus thesis by A1,VECTSP_9:def 1;
end;
end;
theorem
Card (singletons X) = Card X
proof
defpred P[set,set] means $1 in X & $2 = {$1};
A1: for x,y1,y2 being set st x in X & P[x,y1] & P[x,y2] holds y1 = y2;
A2: for x being set st x in X holds ex y being set st P[x,y];
consider f being Function such that
A3: dom f = X and
A4: for x being set st x in X holds P[x,f.x] from CLASSES1:sch 1(A2);
A5: f is one-to-one
proof
let x1,x2 be set such that
A6: x1 in dom f and
A7: x2 in dom f and
A8: f.x1 = f.x2;
A9: P[x1,f.x1] by A3,A4,A6;
P[x2,f.x2] by A3,A4,A7;
hence thesis by A8,A9,ZFMISC_1:6;
end;
rng f = singletons(X)
proof
thus rng f c= singletons(X)
proof
let y be set such that
A10: y in rng f;
consider x being set such that
A11: x in dom f and
A12: y = f.x by A10,FUNCT_1:def 5;
A13: f.x = {x} by A3,A4,A11;
then reconsider fx = f.x as Subset of X by A3,A11,ZFMISC_1:37;
fx is Singleton by A13;
hence thesis by A12;
end;
let y be set such that
A14: y in singletons(X);
consider z being Subset of X such that
A15: y = z and
A16: z is Singleton by A14;
reconsider y as Subset of X by A15;
consider x being set such that
A17: x in X and
A18: y = {x} by A15,A16,Def9;
reconsider x as Element of X by A17;
y = f.x by A4,A17,A18;
hence thesis by A3,A17,FUNCT_1:12;
end;
then X,singletons(X) are_equipotent by A3,A5,WELLORD2:def 4;
hence thesis by CARD_1:21;
end;
theorem
Card [#](bspace X) = exp(2,Card(X)) by CARD_2:44;
theorem
dim bspace {} = 0
proof
Card [#]bspace {} = 1 by CARD_2:60,ZFMISC_1:1;
hence thesis by RANKNULL:5;
end;