:: The Vector Space of Subsets of a Set Based on Symmetric Difference
:: by Jesse Alama
::
:: Received October 9, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

definition
let S be 1-sorted ;
func <*> S ->  FinSequence of S equals :: BSPACE:def 1
 <*> ([#] S);
coherence
 <*> ([#] S) is FinSequence of S ;
end;

:: deftheorem  defines <*> BSPACE:def_1_:_
 for S being 1-sorted holds <*> S = <*> ([#] S);

:: copied from FINSEQ_2:13
theorem :: BSPACE:1
for S being 1-sorted
for i being Element of NAT
for p being FinSequence of S st i in dom p holds
p . i in S
proofend;

:: copied from FINSEQ_2:14
theorem :: BSPACE:2
for S being 1-sorted
for p being FinSequence st ( for i being Nat st i in dom p holds
p . i in S ) holds
p is FinSequence of S
proofend;

scheme :: BSPACE:sch 1
IndSeqS{ F1() ->  1-sorted , P1[ set ] } :
 for p being FinSequence of F1() holds P1[p]
provided
A1: P1[ <*> F1()] and
A2: for p being FinSequence of F1()
for x being Element of F1() st P1[p] holds
P1[p ^ <*x*>]
proofend;

begin

definition
func Z_2  ->  Field equals :: BSPACE:def 2
 INT.Ring 2;
coherence
 INT.Ring 2 is Field by INT_2:28, INT_3:12;
end;

:: deftheorem  defines Z_2 BSPACE:def_2_:_
 Z_2 = INT.Ring 2;

theorem :: BSPACE:3
[#] Z_2 = {0,1} by CARD_1:50;

theorem :: BSPACE:4
for a being Element of Z_2 holds
( a = 0 or a = 1 ) by CARD_1:50, TARSKI:def_2;

theorem Th5: :: BSPACE:5
0. Z_2 = 0
proofend;

theorem Th6: :: BSPACE:6
1. Z_2 = 1 by INT_3:14;

theorem Th7: :: BSPACE:7
(1. Z_2) + (1. Z_2) = 0. Z_2
proofend;

theorem :: BSPACE:8
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

definition
let X, x be set ;
funcX @ x ->  Element of Z_2 equals :Def3: :: BSPACE:def 3
 1. Z_2 if x in X
otherwise  0. Z_2;
coherence
 ( ( x in X implies 1. Z_2 is Element of Z_2 ) &amp; ( not x in X implies 0. Z_2 is Element of Z_2 ) ) ;
consistency
 for b1 being Element of Z_2 holds verum ;
end;

:: deftheorem Def3 defines @ BSPACE:def_3_:_
 for X, x being set holds
( ( x in X implies X @ x = 1. Z_2 ) &amp; ( not x in X implies X @ x = 0. Z_2 ) );

theorem :: BSPACE:9
for X, x being set holds
( X @ x = 1. Z_2 iff x in X ) by Def3;

theorem :: BSPACE:10
for X, x being set holds
( X @ x = 0. Z_2 iff not x in X ) by Def3;

theorem :: BSPACE:11
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 :: BSPACE:12
for X, x, y being set holds
( X @ x = X @ y iff ( x in X iff y in X ) )
proofend;

theorem :: BSPACE:13
for X, Y, x being set holds
( X @ x = Y @ x iff ( x in X iff x in Y ) )
proofend;

theorem :: BSPACE:14
for x being set holds {} @ x = 0. Z_2 by Def3;

theorem Th15: :: BSPACE:15
for X being set
for u, v being Subset of X
for x being Element of X holds (u \+\ v) @ x = (u @ x) + (v @ x)
proofend;

theorem :: BSPACE:16
for X, Y being set holds
( X = Y iff for x being set holds X @ x = Y @ x )
proofend;

begin

definition
let X be set ;
let a be Element of Z_2;
let c be Subset of X;
funca \*\ c ->  Subset of X equals :Def4: :: BSPACE:def 4
c if a = 1. Z_2
{} X if a = 0. Z_2
;
consistency
 for b1 being Subset of X st a = 1. Z_2 &amp; a = 0. Z_2 holds
( b1 = c iff b1 = {} X ) ;
coherence
 ( ( a = 1. Z_2 implies c is Subset of X ) &amp; ( a = 0. Z_2 implies {} X is Subset of X ) ) ;
end;

:: deftheorem Def4 defines \*\ BSPACE:def_4_:_
 for X being set
for a being Element of Z_2
for c being Subset of X holds
( ( a = 1. Z_2 implies a \*\ c = c ) &amp; ( a = 0. Z_2 implies a \*\ c = {} X ) );

definition
let X be set ;
func bspace-sum X ->  BinOp of (bool X) means :Def5: :: BSPACE:def 5
 for c, d being Subset of X holds it . (c,d) = c \+\ d;
existence
 ex b1 being BinOp of (bool X) st
for c, d being Subset of X holds b1 . (c,d) = c \+\ d
proofend;
uniqueness
 for b1, b2 being BinOp of (bool X) st ( for c, d being Subset of X holds b1 . (c,d) = c \+\ d ) &amp; ( for c, d being Subset of X holds b2 . (c,d) = c \+\ d ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines bspace-sum BSPACE:def_5_:_
 for X being set
for b2 being BinOp of (bool X) holds
( b2 = bspace-sum X iff for c, d being Subset of X holds b2 . (c,d) = c \+\ d );

theorem Th17: :: BSPACE:17
for X being set
for a being Element of Z_2
for c, d being Subset of X holds a \*\ (c \+\ d) = (a \*\ c) \+\ (a \*\ d)
proofend;

theorem Th18: :: BSPACE:18
for X being set
for a, b being Element of Z_2
for c being Subset of X holds (a + b) \*\ c = (a \*\ c) \+\ (b \*\ c)
proofend;

theorem :: BSPACE:19
for X being set
for c being Subset of X holds (1. Z_2) \*\ c = c by Def4;

theorem Th20: :: BSPACE:20
for X being set
for a, b being Element of Z_2
for c being Subset of X holds a \*\ (b \*\ c) = (a * b) \*\ c
proofend;

definition
let X be set ;
func bspace-scalar-mult X ->  Function of [: the carrier of Z_2,(bool X):],(bool X) means :Def6: :: BSPACE:def 6
 for a being Element of Z_2
for c being Subset of X holds it . (a,c) = a \*\ c;
existence
 ex b1 being Function of [: the carrier of Z_2,(bool X):],(bool X) st
for a being Element of Z_2
for c being Subset of X holds b1 . (a,c) = a \*\ c
proofend;
uniqueness
 for b1, b2 being Function of [: the carrier of Z_2,(bool X):],(bool X) st ( for a being Element of Z_2
for c being Subset of X holds b1 . (a,c) = a \*\ c ) &amp; ( for a being Element of Z_2
for c being Subset of X holds b2 . (a,c) = a \*\ c ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines bspace-scalar-mult BSPACE:def_6_:_
 for X being set
for b2 being Function of [: the carrier of Z_2,(bool X):],(bool X) holds
( b2 = bspace-scalar-mult X iff for a being Element of Z_2
for c being Subset of X holds b2 . (a,c) = a \*\ c );

definition
let X be set ;
func bspace X ->  non empty VectSpStr over Z_2  equals :: BSPACE:def 7
 VectSpStr(# (bool X),(bspace-sum X),({} X),(bspace-scalar-mult X) #);
coherence
 VectSpStr(# (bool X),(bspace-sum X),({} X),(bspace-scalar-mult X) #) is non empty VectSpStr over Z_2 ;
end;

:: deftheorem  defines bspace BSPACE:def_7_:_
 for X being set holds bspace X = VectSpStr(# (bool X),(bspace-sum X),({} X),(bspace-scalar-mult X) #);

Lm1:  for X being set
for a, b, c being Element of (bspace X)
for A, B, C being Subset of X st a = A &amp; b = B &amp; c = C holds
( a + (b + c) = A \+\ (B \+\ C) &amp; (a + b) + c = (A \+\ B) \+\ C )
proofend;

Lm2:  for X being set
for a, b being Element of Z_2
for x, y being Element of (bspace X)
for c, d being Subset of X st x = c &amp; y = d holds
( (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) &amp; a * (x + y) = a \*\ (c \+\ d) &amp; (a + b) * x = (a + b) \*\ c &amp; (a * b) * x = (a * b) \*\ c &amp; a * (b * x) = a \*\ (b \*\ c) )
proofend;

theorem Th21: :: BSPACE:21
for X being set holds bspace X is Abelian
proofend;

theorem Th22: :: BSPACE:22
for X being set holds bspace X is add-associative
proofend;

theorem Th23: :: BSPACE:23
for X being set holds bspace X is right_zeroed
proofend;

theorem Th24: :: BSPACE:24
for X being set holds bspace X is right_complementable
proofend;

theorem Th25: :: BSPACE:25
for X being set
for a being Element of Z_2
for x, y being Element of (bspace X) holds a * (x + y) = (a * x) + (a * y)
proofend;

theorem Th26: :: BSPACE:26
for X being set
for a, b being Element of Z_2
for x being Element of (bspace X) holds (a + b) * x = (a * x) + (b * x)
proofend;

theorem Th27: :: BSPACE:27
for X being set
for a, b being Element of Z_2
for x being Element of (bspace X) holds (a * b) * x = a * (b * x)
proofend;

theorem Th28: :: BSPACE:28
for X being set
for x being Element of (bspace X) holds (1_ Z_2) * x = x
proofend;

theorem Th29: :: BSPACE:29
for X being set holds
( bspace X is vector-distributive &amp; bspace X is scalar-distributive &amp; bspace X is scalar-associative &amp; bspace X is scalar-unital )
proofend;

registration
let X be set ;
cluster bspace X ->  non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ;
coherence
 ( bspace X is vector-distributive &amp; bspace X is scalar-distributive &amp; bspace X is scalar-associative &amp; bspace X is scalar-unital &amp; bspace X is Abelian &amp; bspace X is right_complementable &amp; bspace X is add-associative &amp; bspace X is right_zeroed ) by Th21, Th22, Th23, Th24, Th29;
end;

begin

definition
let X be set ;
func singletons X ->  set  equals :: BSPACE:def 8
 {  f where f is Subset of X : f is 1 -element  }  ;
coherence
  {  f where f is Subset of X : f is 1 -element  }  is set ;
end;

:: deftheorem  defines singletons BSPACE:def_8_:_
 for X being set holds singletons X =  {  f where f is Subset of X : f is 1 -element  }  ;

definition
let X be set ;
:: original:singletons
redefine func singletons X ->  Subset of (bspace X);
coherence
 singletons X is Subset of (bspace X)
proofend;
end;

registration
let X be non empty set ;
cluster singletons X ->  non empty ;
coherence
 not singletons X is empty
proofend;
end;

theorem Th30: :: BSPACE:30
for X being non empty set
for f being Subset of X st f is Element of singletons X holds
f is 1 -element
proofend;

definition
let F be Field;
let V be VectSp of F;
let l be Linear_Combination of V;
let x be Element of V;
:: original:.
redefine funcl . x ->  Element of F;
coherence
 l . x is Element of F
proofend;
end;

definition
let X be non empty set ;
let s be FinSequence of (bspace X);
let x be Element of X;
funcs @ x ->  FinSequence of Z_2 means :Def9: :: BSPACE:def 9
( len it = len s &amp; ( for j being Nat st 1 <= j &amp; j <= len s holds
it . j = (s . j) @ x ) );
existence
 ex b1 being FinSequence of Z_2 st
( len b1 = len s &amp; ( for j being Nat st 1 <= j &amp; j <= len s holds
b1 . j = (s . j) @ x ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of Z_2 st len b1 = len s &amp; ( for j being Nat st 1 <= j &amp; j <= len s holds
b1 . j = (s . j) @ x ) &amp; len b2 = len s &amp; ( for j being Nat st 1 <= j &amp; j <= len s holds
b2 . j = (s . j) @ x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines @ BSPACE:def_9_:_
 for X being non empty set
for s being FinSequence of (bspace X)
for x being Element of X
for b4 being FinSequence of Z_2 holds
( b4 = s @ x iff ( len b4 = len s &amp; ( for j being Nat st 1 <= j &amp; j <= len s holds
b4 . j = (s . j) @ x ) ) );

theorem Th31: :: BSPACE:31
for X being non empty set
for x being Element of X holds (<*> (bspace X)) @ x = <*> Z_2
proofend;

theorem Th32: :: BSPACE:32
for X being set
for u, v being Element of (bspace X)
for x being Element of X holds (u + v) @ x = (u @ x) + (v @ x)
proofend;

theorem Th33: :: BSPACE:33
for X being non empty set
for s being FinSequence of (bspace X)
for f being Element of (bspace X)
for x being Element of X holds (s ^ <*f*>) @ x = (s @ x) ^ <*(f @ x)*>
proofend;

theorem Th34: :: BSPACE:34
for X being non empty set
for s being FinSequence of (bspace X)
for x being Element of X holds (Sum s) @ x = Sum (s @ x)
proofend;

theorem Th35: :: BSPACE:35
for X being non empty set
for l being Linear_Combination of bspace X
for x being Element of (bspace X) st x in Carrier l holds
l . x = 1_ Z_2
proofend;

registration
let X be empty set ;
cluster singletons X ->  empty ;
coherence
 singletons X is empty
proofend;
end;

theorem Th36: :: BSPACE:36
for X being set holds singletons X is linearly-independent
proofend;

theorem :: BSPACE:37
for X being set
for f being Element of (bspace X) st ex x being set st
( x in X &amp; f = {x} ) holds
f in singletons X ;

theorem Th38: :: BSPACE:38
for X being finite set
for A being Subset of X ex l being Linear_Combination of singletons X st Sum l = A
proofend;

theorem Th39: :: BSPACE:39
for X being finite set holds Lin (singletons X) = bspace X
proofend;

theorem Th40: :: BSPACE:40
for X being finite set holds singletons X is Basis of bspace X
proofend;

registration
let X be finite set ;
cluster singletons X ->  finite ;
coherence
 singletons X is finite ;
end;

registration
let X be finite set ;
cluster bspace X ->  non empty finite-dimensional ;
coherence
 bspace X is finite-dimensional
proofend;
end;

theorem :: BSPACE:41
for X being set holds card (singletons X) = card X
proofend;

theorem :: BSPACE:42
for X being set holds card ([#] (bspace X)) = exp (2,(card X)) by CARD_2:31;

theorem :: BSPACE:43
dim (bspace {}) = 0
proofend;