:: by Jesse Alama

::

:: Received October 9, 2007

:: Copyright (c) 2007-2021 Association of Mizar Users

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

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

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

provided

IndSeqS{ F

provided

A1:
P_{1}[ <*> F_{1}()]
and

A2: for p being FinSequence of F_{1}()

for x being Element of F_{1}() st P_{1}[p] holds

P_{1}[p ^ <*x*>]

A2: for p being FinSequence of F

for x being Element of F

P

proof end;

theorem :: BSPACE:8

definition

let X be set ;

let x be object ;

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_{1} being Element of Z_2 holds verum
;

end;
let x be object ;

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

:: deftheorem Def3 defines @ BSPACE:def 3 :

for X being set

for x being object holds

( ( x in X implies X @ x = 1. Z_2 ) & ( not x in X implies X @ x = 0. Z_2 ) );

for X being set

for x being object holds

( ( x in X implies X @ x = 1. Z_2 ) & ( not x in X implies X @ x = 0. Z_2 ) );

theorem :: BSPACE:11

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)

for u, v being Subset of X

for x being Element of X holds (u \+\ v) @ x = (u @ x) + (v @ x)

proof end;

definition

let X be set ;

let a be Element of Z_2;

let c be Subset of X;

consistency

for b_{1} being Subset of X st a = 1. Z_2 & a = 0. Z_2 holds

( b_{1} = c iff b_{1} = {} X )
;

coherence

( ( a = 1. Z_2 implies c is Subset of X ) & ( a = 0. Z_2 implies {} X is Subset of X ) ) ;

end;
let a be Element of Z_2;

let c be Subset of X;

consistency

for b

( b

coherence

( ( a = 1. Z_2 implies c is Subset of X ) & ( a = 0. Z_2 implies {} X is Subset of X ) ) ;

:: 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 ) );

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 ;

ex b_{1} being BinOp of (bool X) st

for c, d being Subset of X holds b_{1} . (c,d) = c \+\ d

for b_{1}, b_{2} being BinOp of (bool X) st ( for c, d being Subset of X holds b_{1} . (c,d) = c \+\ d ) & ( for c, d being Subset of X holds b_{2} . (c,d) = c \+\ d ) holds

b_{1} = b_{2}

end;
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 for c, d being Subset of X holds it . (c,d) = c \+\ d;

ex b

for c, d being Subset of X holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines bspace-sum BSPACE:def 5 :

for X being set

for b_{2} being BinOp of (bool X) holds

( b_{2} = bspace-sum X iff for c, d being Subset of X holds b_{2} . (c,d) = c \+\ d );

for X being set

for b

( b

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)

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)

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

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 ;

ex b_{1} 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_{1} . (a,c) = a \*\ c

for b_{1}, b_{2} 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_{1} . (a,c) = a \*\ c ) & ( for a being Element of Z_2

for c being Subset of X holds b_{2} . (a,c) = a \*\ c ) holds

b_{1} = b_{2}

end;
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 for a being Element of Z_2

for c being Subset of X holds it . (a,c) = a \*\ c;

ex b

for a being Element of Z_2

for c being Subset of X holds b

proof end;

uniqueness for b

for c being Subset of X holds b

for c being Subset of X holds b

b

proof end;

:: deftheorem Def6 defines bspace-scalar-mult BSPACE:def 6 :

for X being set

for b_{2} being Function of [: the carrier of Z_2,(bool X):],(bool X) holds

( b_{2} = bspace-scalar-mult X iff for a being Element of Z_2

for c being Subset of X holds b_{2} . (a,c) = a \*\ c );

for X being set

for b

( b

for c being Subset of X holds b

definition

let X be set ;

ModuleStr(# (bool X),(bspace-sum X),({} X),(bspace-scalar-mult X) #) is non empty ModuleStr over Z_2 ;

end;
func bspace X -> non empty ModuleStr over Z_2 equals :: BSPACE:def 7

ModuleStr(# (bool X),(bspace-sum X),({} X),(bspace-scalar-mult X) #);

coherence ModuleStr(# (bool X),(bspace-sum X),({} X),(bspace-scalar-mult X) #);

ModuleStr(# (bool X),(bspace-sum X),({} X),(bspace-scalar-mult X) #) is non empty ModuleStr over Z_2 ;

:: deftheorem defines bspace BSPACE:def 7 :

for X being set holds bspace X = ModuleStr(# (bool X),(bspace-sum X),({} X),(bspace-scalar-mult X) #);

for X being set holds bspace X = ModuleStr(# (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 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)

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)

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)

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 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 ) by Th25, Th26, Th27, Th28;

( bspace X is vector-distributive & bspace X is scalar-distributive & bspace X is scalar-associative & bspace X is scalar-unital ) by Th25, Th26, Th27, Th28;

registration

let X be set ;

( 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;
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;

:: deftheorem defines singletons BSPACE:def 8 :

for X being set holds singletons X = { f where f is Subset of X : f is 1 -element } ;

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)

end;
:: original: singletons

redefine func singletons X -> Subset of (bspace X);

coherence

singletons X is Subset of (bspace X)

proof 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

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

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

definition

let X be non empty set ;

let s be FinSequence of (bspace X);

let x be Element of X;

ex b_{1} being FinSequence of Z_2 st

( len b_{1} = len s & ( for j being Nat st 1 <= j & j <= len s holds

b_{1} . j = (s . j) @ x ) )

for b_{1}, b_{2} being FinSequence of Z_2 st len b_{1} = len s & ( for j being Nat st 1 <= j & j <= len s holds

b_{1} . j = (s . j) @ x ) & len b_{2} = len s & ( for j being Nat st 1 <= j & j <= len s holds

b_{2} . j = (s . j) @ x ) holds

b_{1} = b_{2}

end;
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 ( len it = len s & ( for j being Nat st 1 <= j & j <= len s holds

it . j = (s . j) @ x ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{4} being FinSequence of Z_2 holds

( b_{4} = s @ x iff ( len b_{4} = len s & ( for j being Nat st 1 <= j & j <= len s holds

b_{4} . j = (s . j) @ x ) ) );

for X being non empty set

for s being FinSequence of (bspace X)

for x being Element of X

for b

( b

b

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)

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)*>

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)

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

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

theorem :: BSPACE:37

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

for A being Subset of X ex l being Linear_Combination of singletons X st Sum l = A

proof end;

registration
end;