:: The Vector Space of Subsets of a Set Based on Symmetric Difference
:: by Jesse Alama
::
:: Received October 9, 2007
:: Copyright (c) 2007-2011 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);

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;

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{ F₁() -> 1-sorted , P₁[ set ] } :

for p being FinSequence of F₁() holds P₁[p]

provided

A1: P₁[ <*> F₁()] and
A2: for p being FinSequence of F₁()
for x being Element of F₁() st P₁[p] holds
P₁[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:44, INT_3:22;

end;

:: deftheorem defines Z_2 BSPACE:def 2 :
Z_2 = INT.Ring 2;

theorem :: BSPACE:3

[#] Z_2 = {0,1} by CARD_1:88;

theorem :: BSPACE:4

for a being Element of Z_2 holds
( a = 0 or a = 1 ) by CARD_1:88, TARSKI:def 2;

theorem Th5: :: BSPACE:5

0. Z_2 = 0

proof end;

theorem Th6: :: BSPACE:6

1. Z_2 = 1 by INT_3:24;

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:88, 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 b₁ 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:88, 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 b₁ being Subset of X st a = 1. Z_2 & a = 0. Z_2 holds
( b₁ = c iff b₁ = {} 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 b₁ being BinOp of (bool X) st
for c, d being Subset of X holds b₁ . (c,d) = c \+\ d

proof end;

uniqueness
for b₁, b₂ being BinOp of (bool X) st ( for c, d being Subset of X holds b₁ . (c,d) = c \+\ d ) & ( for c, d being Subset of X holds b₂ . (c,d) = c \+\ d ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines bspace-sum BSPACE:def 5 :
for X being set
for b₂ being BinOp of (bool X) holds
( b₂ = bspace-sum X iff for c, d being Subset of X holds b₂ . (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 b₁ 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 b₁ . (a,c) = a \*\ c

proof end;

uniqueness
for b₁, b₂ 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 b₁ . (a,c) = a \*\ c ) & ( for a being Element of Z_2
for c being Subset of X holds b₂ . (a,c) = a \*\ c ) holds
b₁ = b₂

proof end;

end;

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

definition

let X be set ;
func bspace X -> non empty VectSpStr of 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 of 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 ;
attr X is Singleton means :Def8: :: BSPACE:def 8
( not X is empty & X is trivial );

end;

:: deftheorem Def8 defines Singleton BSPACE:def 8 :
for X being set holds
( X is Singleton iff ( not X is empty & X is trivial ) );

registration

cluster Singleton -> non empty trivial set ;
coherence
for b₁ being set st b₁ is Singleton holds
( not b₁ is empty & b₁ is trivial ) by Def8;
cluster non empty trivial -> Singleton set ;
coherence
for b₁ being set st not b₁ is empty & b₁ is trivial holds
b₁ is Singleton by Def8;

end;

definition

let X be set ;
let f be Subset of X;
:: original: Singleton
redefine attr f is Singleton means :Def9: :: BSPACE:def 9
ex x being set st
( x in X & f = {x} );
compatibility
( f is Singleton iff ex x being set st
( x in X & f = {x} ) )

proof end;

end;

:: deftheorem Def9 defines Singleton BSPACE:def 9 :
for X being set
for f being Subset of X holds
( f is Singleton iff ex x being set st
( x in X & f = {x} ) );

definition

let X be set ;
func singletons X -> set equals :: BSPACE:def 10
{ f where f is Subset of X : f is Singleton } ;
coherence
{ f where f is Subset of X : f is Singleton } is set ;

end;

:: deftheorem defines singletons BSPACE:def 10 :
for X being set holds singletons X = { f where f is Subset of X : f is Singleton } ;

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 Singleton

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 :Def11: :: BSPACE:def 11
( len it = len s & ( for j being Nat st 1 <= j & j <= len s holds
it . j = (s . j) @ x ) );
existence
ex b₁ being FinSequence of Z_2 st
( len b₁ = len s & ( for j being Nat st 1 <= j & j <= len s holds
b₁ . j = (s . j) @ x ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of Z_2 st len b₁ = len s & ( for j being Nat st 1 <= j & j <= len s holds
b₁ . j = (s . j) @ x ) & len b₂ = len s & ( for j being Nat st 1 <= j & j <= len s holds
b₂ . j = (s . j) @ x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines @ BSPACE:def 11 :
for X being non empty set
for s being FinSequence of (bspace X)
for x being Element of X
for b₄ being FinSequence of Z_2 holds
( b₄ = s @ x iff ( len b₄ = len s & ( for j being Nat st 1 <= j & j <= len s holds
b₄ . 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;

theorem Th36: :: BSPACE:36

singletons {} = {}

proof end;

theorem Th37: :: BSPACE:37

for X being set holds singletons X is linearly-independent

proof end;

theorem :: BSPACE:38

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 Th39: :: BSPACE:39

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 Th40: :: BSPACE:40

for X being finite set holds Lin (singletons X) = bspace X

proof end;

theorem Th41: :: BSPACE:41

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:42

for X being set holds card (singletons X) = card X

proof end;

theorem :: BSPACE:43

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

theorem :: BSPACE:44

dim (bspace {}) = 0

proof end;