:: The Vector Space of Subsets of a Set Based on Symmetric Difference
:: by Jesse Alama
::
:: Received October 9, 2007
:: Copyright (c) 2007-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 NUMBERS, STRUCT_0, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, NAT_1,
ORDINAL4, VECTSP_1, INT_3, CARD_1, SUPINF_2, MESFUNC1, ARYTM_3, INT_1,
QC_LANG1, XBOOLE_0, TARSKI, BINOP_1, ZFMISC_1, RLVECT_1, ALGSTR_0,
GROUP_1, RLVECT_2, XXREAL_0, CARD_3, RLVECT_3, REALSET1, VALUED_1,
FINSEQ_2, PARTFUN1, FINSET_1, FUNCT_4, RLVECT_5, ORDINAL2, BSPACE;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, DOMAIN_1, RELSET_1,
FUNCT_1, ORDINAL1, NUMBERS, NAT_1, INT_1, PARTFUN1, FUNCT_2, BINOP_1,
FUNCT_7, XXREAL_0, CARD_1, FINSET_1, FINSEQ_1, FINSEQ_2, FINSEQOP,
CARD_2, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, VECTSP_6,
VECTSP_7, MATRLIN, VECTSP_9, INT_3, RANKNULL;
constructors FINSEQOP, VECTSP_7, VECTSP_9, REALSET1, WELLORD2, NAT_D, FUNCT_7,
CARD_2, RANKNULL, INT_3, GR_CY_1, RELSET_1, BINOP_2, BINOP_1;
registrations STRUCT_0, CARD_1, FINSET_1, FINSEQ_1, SUBSET_1, XBOOLE_0,
VECTSP_1, ORDINAL1, XREAL_0, INT_1, VECTSP_7, RELSET_1;
requirements NUMERALS, BOOLE, ARITHM, SUBSET, REAL;
definitions TARSKI, FUNCT_1, XBOOLE_0, RLVECT_1, STRUCT_0, ALGSTR_0;
equalities FINSEQ_1, VECTSP_1, STRUCT_0, FINSEQ_2, BINOP_1, INT_3, ALGSTR_0,
ORDINAL1;
expansions FUNCT_1, FINSEQ_1, XBOOLE_0, VECTSP_1;
theorems TARSKI, ZFMISC_1, FINSEQ_1, FUNCT_1, VECTSP_7, 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, PARTFUN1, FINSEQ_3, MATRLIN;
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,
i for Element of NAT,
p for FinSequence,
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:11;
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
by A1,STRUCT_0:def 5;
hence thesis by FINSEQ_2:12;
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;
begin :: The two-element field Z_2
definition
func Z_2 -> Field equals
INT.Ring(2);
coherence by INT_2:28,INT_3:12;
end;
theorem
[#]Z_2 = {0,1} by CARD_1:50;
theorem
for a being Element of Z_2 holds a = 0 or a = 1 by CARD_1:50,TARSKI:def 2;
theorem Th5:
0.Z_2 = 0
by NAT_1:44,SUBSET_1:def 8;
theorem Th6:
1.Z_2 = 1 by INT_3:14;
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 4
.= 0 by NAT_D:25;
hence thesis;
end;
theorem
for x being Element of Z_2 holds x = 0.Z_2 iff x <> 1.Z_2 by Th5,Th6,
CARD_1:50,TARSKI:def 2;
begin :: Set-theoretical Preliminaries
definition
let X be set,x be object;
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:50
,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:50,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:50,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 not x in v by A1,XBOOLE_0:1;
then
A4: v@x = 0.Z_2 by Def3;
u@x = 1.Z_2 by A3,Def3;
hence thesis by A2,A4,RLVECT_1:4;
end;
suppose
A5: not x in u;
then x in v by A1,XBOOLE_0:1;
then
A6: v@x = 1.Z_2 by Def3;
u@x = 0.Z_2 by A5,Def3;
hence thesis by A2,A6,RLVECT_1:4;
end;
end;
suppose
A7: not x in u \+\ v;
then
A8: (u \+\ v)@x = 0.Z_2 by Def3;
per cases;
suppose
x in u;
then x in v & u@x = 1.Z_2 by A7,Def3,XBOOLE_0:1;
hence thesis by A8,Def3,Th7;
end;
suppose
A9: not x in u;
then not x in v by A7,XBOOLE_0:1;
then
A10: v@x = 0.Z_2 by Def3;
u@x = 0.Z_2 by A9,Def3;
hence thesis by A8,A10,RLVECT_1:4;
end;
end;
end;
theorem
for X,Y being set holds X = Y iff for x being object holds X@x = Y@x
proof
let X,Y be set;
thus X = Y implies for x being object holds X@x = Y@x;
thus (for x being object holds X@x = Y@x) implies X = Y
proof
assume
A1: for x being object holds X@x = Y@x;
thus X c= Y
proof
let y be object;
assume y in X;
then X@y = 1.Z_2 by Def3;
then Y@y = 1.Z_2 by A1;
hence thesis by Def3;
end;
let y be object;
assume y in Y;
then Y@y = 1.Z_2 by Def3;
then X@y = 1.Z_2 by A1;
hence thesis by Def3;
end;
end;
begin :: The Boolean Bector Space of Subsets of a Set
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;
assume x in bool X & y in bool X;
then reconsider x,y as Subset of X;
set z = x \+\ y;
take z;
thus thesis;
end;
consider f being Function of [:bool X,bool X:],bool X such that
A2: 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 9(A1);
reconsider f as BinOp of bool X;
take f;
for c,d being Subset of X holds f.(c,d) = c \+\ d
proof
let c,d be Subset of X;
ex a,b being Subset of X st c = a & d = b & f.(c,d) = a \+\ b by A2;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let f,g be BinOp of bool X such that
A3: ( for c,d being Subset of X holds f.(c,d) = c \+\ d)& for c,d
being Subset of X holds g.(c,d) = c \+\ d;
A4: for x being object st x in dom f holds f.x = g.x
proof
let x be object;
assume x in dom f;
then consider y,z being object such that
A5: y in bool X and
A6: z in bool X and
A7: x = [y,z] by ZFMISC_1:def 2;
reconsider z as Subset of X by A6;
reconsider y as Subset of X by A5;
f.(y,z) = y \+\ z & g.(y,z) = y \+\ z by A3;
hence thesis by A7;
end;
dom f = [:bool X,bool X:] by FUNCT_2:def 1;
then dom f = dom g by FUNCT_2:def 1;
hence thesis by A4;
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:50,TARSKI:def 2;
suppose
A1: a = 0.Z_2;
then a \*\ (c \+\ d) = {}X & a \*\ c = {}X by Def4;
hence thesis by A1,Def4;
end;
suppose
A2: a = 1.Z_2;
then a \*\ (c \+\ d) = c \+\ d & a \*\ c = c by Def4;
hence thesis by A2,Def4;
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:50,TARSKI:def 2;
suppose
A1: a = 0.Z_2;
then a \*\ c = {}X by Def4;
hence thesis by A1,RLVECT_1:4;
end;
suppose
A2: a = 1.Z_2;
per cases by Th5,Th6,CARD_1:50,TARSKI:def 2;
suppose
A3: b = 0.Z_2;
then b \*\ c = {}X by Def4;
hence thesis by A3,RLVECT_1:4;
end;
suppose
A4: b = 1.Z_2;
A5: c \+\ c = {}X by XBOOLE_1:92;
b \*\ c = c by A4,Def4;
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:50,TARSKI:def 2;
suppose
A1: a = 0.Z_2;
then a \*\ (b \*\ c) = {}X by Def4;
hence thesis by A1,Def4;
end;
suppose
A2: a = 1.Z_2;
then a \*\ (b \*\ c) = b \*\ c by Def4;
hence thesis by A2;
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 y as Subset of X by A3;
reconsider x as Element of Z_2 by A2;
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 9(A1);
take f;
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;
ex a9 being Element of Z_2, c9 being Subset of X st a = a9 & c = c9 &
f.(a,c) = a9 \*\ c9 by A4;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let f,g be Function of [:the carrier of Z_2,bool X:],bool X such that
A5: ( for a being Element of Z_2, c being Subset of X holds f.(a,c) =
a \*\ c)& for a being Element of Z_2, c being Subset of X holds g.(a,c) = a \*\
c;
A6: for x being object st x in dom f holds f.x = g.x
proof
let x be object;
assume x in dom f;
then consider y,z being object such that
A7: y in the carrier of Z_2 and
A8: z in bool X and
A9: x = [y,z] by ZFMISC_1:def 2;
reconsider z as Subset of X by A8;
reconsider y as Element of Z_2 by A7;
f.(y,z) = y \*\ z & g.(y,z) = y \*\ z by A5;
hence thesis by A9;
end;
dom f = [:the carrier of Z_2,bool X:] by FUNCT_2:def 1;
then dom f = dom g by FUNCT_2:def 1;
hence thesis by A6;
end;
end;
definition
let X be set;
func bspace(X) -> non empty ModuleStr over Z_2 equals
ModuleStr (# 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 that
A1: a = A and
A2: b = B and
A3: c = C;
b+c = B \+\ C by A2,A3,Def5;
hence a+(b+c) = A \+\ (B \+\ C) by A1,Def5;
a+b = A \+\ B by A1,A2,Def5;
hence (a+b)+c = (A \+\ B) \+\ C by A3,Def5;
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;
a*x = a \*\ c & b*y = b \*\ d by A1,A2,Def6;
hence (a*x)+(b*y) = (a \*\ c) \+\ (b \*\ d) by Def5;
x+y = c \+\ d by A1,A2,Def5;
hence a*(x+y) = a \*\ (c \+\ d) by Def6;
thus (a+b)*x = (a+b) \*\ c by A1,Def6;
thus (a*b)*x = (a*b) \*\ c by A1,Def6;
b*x = b \*\ c by A1,Def6;
hence a*(b*x) = a \*\ (b \*\ c) by Def6;
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;
take x;
A \+\ A = {}X by XBOOLE_1:92;
hence thesis by 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 vector-distributive scalar-distributive
scalar-associative scalar-unital
by Th25,Th26,Th27,Th28;
registration
let X be set;
cluster bspace(X) -> vector-distributive scalar-distributive
scalar-associative scalar-unital
Abelian right_complementable
add-associative right_zeroed;
coherence by Th21,Th22,Th23,Th24,Th29;
end;
begin :: The Linear Independence and Linear Span of 1-element Subsets
definition
let X be set;
func singletons(X) -> set equals
{ f where f is Subset of X : f is 1-element };
coherence;
end;
definition
let X be set;
redefine func singletons(X) -> Subset of bspace(X); :: redefines singletons (BSPACE, definition)
coherence
proof
set S = singletons(X);
S c= bool(X)
proof
let f be object;
assume f in S;
then ex g being Subset of X st f = g & g is 1-element;
then reconsider f as Subset of X;
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
set x = the 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 1-element
proof
let X be non empty set, f be Subset of X;
assume f is Element of singletons(X);
then f in singletons(X);
then ex g being Subset of X st g = f & g is 1-element;
hence thesis;
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; :: redefines . (FUNCT_1, definition)
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
:Def9:
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
by A1,FINSEQ_3:25,A2;
rng p c= the carrier of Z_2
proof
let y be object;
assume y in rng p;
then consider a being object such that
A4: a in dom p and
A5: p.a = y by FUNCT_1:def 3;
p.a = (s.a)@x by A2,A4;
hence thesis by A5;
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
A6: len f = len s and
A7: for j being Nat st 1 <= j & j <= len s holds f.j = (s.j)@x and
A8: len g = len s and
A9: 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
A10: 1 <= k & k <= len f;
f.k = (s.k)@x by A6,A7,A10;
hence thesis by A6,A9,A10;
end;
hence thesis by A6,A8;
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 Def9
.= 0;
hence thesis;
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 u9 = u, v9 = v as Subset of X;
(u + v)@x = (u9 \+\ v9)@x by Def5
.= (u9@x) + (v9@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 Def9
.= (len s) + (len <*f*>) by FINSEQ_1:22
.= (len s) + 1 by FINSEQ_1:39;
A2: 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;
per cases by A1,A4,NAT_1:8;
suppose
A5: k <= len s;
dom (s@x) = Seg (len (s@x)) by FINSEQ_1:def 3
.= Seg (len s) by Def9;
then k in dom (s@x) by A3,A5;
then
A6: R.k = (s@x).k by FINSEQ_1:def 7
.= (s.k)@x by A3,A5,Def9;
dom s = Seg (len s) by FINSEQ_1:def 3;
then
A7: k in dom s by A3,A5;
k <= len (s ^ <*f*>) by A4,Def9;
then L.k = ((s ^ <*f*>).k)@x by A3,Def9;
hence thesis by A6,A7,FINSEQ_1:def 7;
end;
suppose
A8: k = len L;
dom (<*f@x*>) = {1} by FINSEQ_1:2,def 8;
then
A9: 1 in dom (<*f@x*>) by TARSKI:def 1;
len (s@x) = len s by Def9;
then
A10: R.k = <*f@x*>.1 by A1,A8,A9,FINSEQ_1:def 7
.= f@x;
dom (<*f*>) = {1} by FINSEQ_1:2,def 8;
then 1 in dom (<*f*>) by TARSKI:def 1;
then
A11: (s ^ <*f*>).k = <*f*>.1 by A1,A8,FINSEQ_1:def 7
.= f;
k <= len (s ^ <*f*>) by A4,Def9;
hence thesis by A3,A10,A11,Def9;
end;
end;
len ((s@x) ^ <*f@x*>) = (len (s@x)) + (len <*f@x*>) by FINSEQ_1:22
.= (len s) + (len <*f@x*>) by Def9
.= (len s) + 1 by FINSEQ_1:39;
hence thesis by A1,A2;
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
reconsider z = 0.V as Subset of X;
set e = <*>V;
A2: z@x = 0.Z_2 by Def3;
Sum e = 0.V & e@x = <*>Z_2 by Th31,RLVECT_1:43;
hence thesis by A2,RLVECT_1:43;
end;
A3: 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
A4: Q[p];
(Sum (p ^ <*f*>))@x = ((Sum p) + (Sum <*f*>))@x by RLVECT_1:41
.= ((Sum p) + f)@x by RLVECT_1:44
.= (Sum p)@x + f@x by Th32
.= Sum (p@x) + Sum (<*f@x*>) by A4,RLVECT_1:44
.= Sum (p@x ^ <*f@x*>) by RLVECT_1:41
.= Sum ((p ^ <*f*>)@x) by Th33;
hence thesis;
end;
for p being FinSequence of V holds Q[p] from IndSeqS(A1,A3);
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);
assume x in Carrier l;
then l.x <> 0.Z_2 by VECTSP_6:2;
hence thesis by Th5,Th6,CARD_1:50,TARSKI:def 2;
end;
registration let X be empty set;
cluster singletons X -> empty;
coherence
proof
assume singletons(X) is non empty;
then consider f being object such that
A1: f in singletons(X);
ex g being Subset of X st g = f & g is 1-element by A1;
hence thesis;
end;
end;
theorem Th36:
singletons(X) is linearly-independent
proof
per cases;
suppose
X is empty;
hence thesis;
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
A1: Sum l = 0.V;
reconsider s = Sum l as Subset of X;
set C = Carrier l;
A2: l!(Carrier l) = l by RANKNULL:24;
assume C <> {};
then consider f being Element of V such that
A3: f in C by SUBSET_1:4;
reconsider f as Subset of X;
reconsider g = f as Element of V;
A4: {g} c= Carrier l by A3,ZFMISC_1:31;
reconsider n = l!{g} as Linear_Combination of {g};
reconsider m = l!(C \ {g}) as Linear_Combination of C \ {g};
reconsider l as Linear_Combination of C by A2;
reconsider t = Sum m, u = Sum n as Subset of X;
g in {g} by TARSKI:def 1;
then
A5: Sum n = (n.g)*g & n.g = l.g by RANKNULL:25,VECTSP_6:17;
l.g <> 0.Z_2 by A3,VECTSP_6:2;
then l.g = 1_Z_2 by Th5,Th6,CARD_1:50,TARSKI:def 2;
then
A6: u = f by A5;
C c= S by VECTSP_6:def 4;
then f is 1-element by A3,Th30;
then consider x being Element of X such that
A7: f = {x} by CARD_1:65;
x in f by A7,TARSKI:def 1;
then
A8: f@x = 1.Z_2 by Def3;
A9: 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
A10: g <> f and
A11: g in C;
C c= S by VECTSP_6:def 4;
then g is 1-element by A11,Th30;
then consider y being Element of X such that
A12: g = {y} by CARD_1:65;
now
assume g@x <> 0.Z_2;
then x in {y} by A12,Def3;
hence contradiction by A7,A10,A12,TARSKI:def 1;
end;
hence thesis;
end;
A13: t@x = 0
proof
consider F being FinSequence of V such that
A14: F is one-to-one & rng F = Carrier m and
A15: t = Sum (m (#) F) by VECTSP_6:def 6;
A16: (Sum (m (#) F))@x = Sum ((m (#) F)@x) by Th34;
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
A17: rng F = Carrier m;
set R = (len F) |-> 0.Z_2;
set L = (m (#) F)@x;
A18: len (m (#) F) = len F by VECTSP_6:def 5;
then
A19: len L = len F by Def9;
A20: for k being Nat st 1 <= k & k <= len L holds L.k = R.k
proof
let k be Nat such that
A21: 1 <= k & k <= len L;
A22: k in Seg (len F) by A19,A21;
len (m (#) F) = len F by VECTSP_6:def 5;
then dom (m (#) F) = Seg (len F) by FINSEQ_1:def 3;
then k in dom (m (#) F) by A19,A21;
then
A23: (m (#) F).k = m.(F/.k)*(F/.k) by VECTSP_6:def 5;
reconsider Fk = F/.k as Subset of X;
A24: Carrier m c= C \ {f} by VECTSP_6:def 4;
dom F = Seg (len F) by FINSEQ_1:def 3;
then
A25: k in dom F by A19,A21;
then
A26: F/.k = F.k by PARTFUN1:def 6;
then m.(F/.k) = 1_Z_2 by A17,A25,Th35,FUNCT_1:3;
then
A27: (m (#) F).k = Fk by A23;
A28: F/.k in Carrier m by A17,A25,A26,FUNCT_1:3;
then
A29: Fk in C by A24,XBOOLE_0:def 5;
A30: Fk <> f
proof
assume Fk = f;
then not f in {f} by A28,A24,XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
L.k = ((m (#) F).k)@x by A18,A19,A21,Def9
.= 0.Z_2 by A9,A27,A30,A29;
hence thesis by A22,FUNCOP_1:7;
end;
dom R = Seg (len F) by FUNCOP_1:13;
then len L = len R by A19,FINSEQ_1:def 3;
hence thesis by A20;
end;
then (m (#) F)@x = (len F) |-> 0.Z_2 by A14;
hence thesis by A15,A16,Th5,MATRIX_3:11;
end;
l = n + m by A4,RANKNULL:27;
then Sum l = (Sum m) + (Sum n) by VECTSP_6:44;
then s = t \+\ u by Def5;
then
A31: s@x = t@x + u@x by Th15;
s@x = 0.Z_2 by A1,Def3;
hence thesis by A8,A31,A13,A6,RLVECT_1:4;
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 Th38:
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: P[{}]
proof
reconsider l = ZeroLC(V) as Linear_Combination of S by VECTSP_6:5;
assume {} is Subset of X;
take l;
Sum l = 0.V by VECTSP_6:15;
hence thesis;
end;
A2: 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
A3: P[B];
assume
A4: 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
A5: Sum l = B by A3;
per cases;
suppose
A6: x in B;
take l;
thus thesis by A5,A6,ZFMISC_1:40;
end;
suppose
not x in B;
then
A7: B misses {x} by ZFMISC_1:50;
reconsider z = ZeroLC(V) as Linear_Combination of {}V by VECTSP_6:5;
reconsider f = {x} as Element of V by A4,XBOOLE_1:11;
reconsider g = f as Subset of X;
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:92;
then
A8: m.f = 1_Z_2 by FUNCT_7:31;
f in S;
then {f} c= S by ZFMISC_1:31;
then m is Linear_Combination of S by VECTSP_6:4;
then reconsider n = l + m as Linear_Combination of S by VECTSP_6:24;
take n;
Sum n = (Sum l) + (Sum m) by VECTSP_6:44
.= (Sum l) + (m.f)*f by VECTSP_6:17
.= (Sum l) + f by A8
.= B \+\ g by A5,Def5
.= (B \/ {x}) \ (B /\ {x}) by XBOOLE_1:101
.= (B \/ {x}) \ {} by A7
.= B \/ {x};
hence thesis;
end;
end;
A9: A is finite;
P[A] from FINSET_1:sch 2(A9,A1,A2);
hence thesis;
end;
theorem Th39:
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;
ex l being Linear_Combination of S st Sum l = A by Th38;
hence thesis by A2,VECTSP_7:7;
end;
hence thesis by VECTSP_4:32;
end;
theorem Th40:
for X being finite set holds singletons(X) is Basis of bspace(X)
proof
let X be finite set;
singletons(X) is linearly-independent & Lin(singletons(X)) = bspace(X)
by Th36,Th39;
hence thesis by VECTSP_7:def 3;
end;
registration
let X be finite set;
cluster singletons(X) -> finite;
coherence;
end;
registration
let X be finite set;
cluster bspace(X) -> finite-dimensional;
coherence
proof
set S = singletons(X);
S is Basis of bspace(X) by Th40;
hence thesis by MATRLIN:def 1;
end;
end;
theorem
card (singletons X) = card X
proof
defpred P[object,object] means $1 in X & $2 = {$1};
A1: for x being object st x in X holds ex y being object st P[x,y];
consider f being Function such that
A2: dom f = X and
A3: for x being object st x in X holds P[x,f.x] from CLASSES1:sch 1(A1);
A4: rng f = singletons(X)
proof
thus rng f c= singletons(X)
proof
let y be object;
assume y in rng f;
then consider x being object such that
A5: x in dom f and
A6: y = f.x by FUNCT_1:def 3;
A7: f.x = {x} by A2,A3,A5;
then reconsider fx = f.x as Subset of X by A2,A5,ZFMISC_1:31;
fx is 1-element by A7;
hence thesis by A6;
end;
let y be object such that
A8: y in singletons(X);
reconsider X as non empty set by A8;
ex z being Subset of X st y = z & z is 1-element by A8;
then reconsider y as 1-element Subset of X;
consider x being Element of X such that
A9: y = {x} by CARD_1:65;
y = f.x by A3,A9;
hence thesis by A2,FUNCT_1:3;
end;
f is one-to-one
proof
let x1,x2 be object such that
A10: x1 in dom f & x2 in dom f and
A11: f.x1 = f.x2;
( P[x1,f.x1])& P[x2,f.x2] by A2,A3,A10;
hence thesis by A11,ZFMISC_1:3;
end;
then X,singletons(X) are_equipotent by A2,A4,WELLORD2:def 4;
hence thesis by CARD_1:5;
end;
theorem
card [#](bspace X) = exp(2,card(X)) by CARD_2:31;
theorem
dim bspace {} = 0
proof
card [#]bspace {} = 1 by CARD_2:42,ZFMISC_1:1;
hence thesis by RANKNULL:5;
end;