:: 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
proof end;

:: 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
proof end;

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*>]
proof end;

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
proof end;

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
proof end;

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 ;
func X @ 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 ) & ( 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 ) & ( 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 ) )
proof end;

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

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)
proof end;

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

begin

definition
let X be set ;
let a be Element of Z_2;
let c be Subset of X;
func a \*\ 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 & a = 0. Z_2 holds
( b1 = c iff b1 = {} X )
;
coherence
( ( a = 1. Z_2 implies c is Subset of X ) & ( 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 ) & ( 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
proof end;
uniqueness
for b1, b2 being BinOp of (bool X) st ( for c, d being Subset of X holds b1 . (c,d) = c \+\ d ) & ( for c, d being Subset of X holds b2 . (c,d) = c \+\ d ) holds
b1 = b2
proof end;
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)
proof end;

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)
proof end;

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
proof end;

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
proof end;
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 ) & ( for a being Element of Z_2
for c being Subset of X holds b2 . (a,c) = a \*\ c ) holds
b1 = b2
proof end;
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 & b = B & c = C holds
( a + (b + c) = A \+\ (B \+\ C) & (a + b) + c = (A \+\ B) \+\ C )

proof end;

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 & 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 end;

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

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

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

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

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)
proof end;

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)
proof end;

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)
proof end;

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

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

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 & bspace X is scalar-distributive & bspace X is scalar-associative & bspace X is scalar-unital & bspace X is Abelian & bspace X is right_complementable & bspace X is add-associative & 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)
proof end;
end;

registration
let X be non empty set ;
cluster singletons X -> non empty ;
coherence
not singletons X is empty
proof end;
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
proof end;

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 func l . x -> Element of F;
coherence
l . x is Element of F
proof end;
end;

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

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)
proof end;

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)*>
proof end;

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)
proof end;

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
proof end;

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

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

theorem :: BSPACE:37
for X being set
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: :: 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
proof end;

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

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

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
proof end;
end;

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

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
proof end;