:: The Vector Space of Subsets of a Set Based on Disjoint Union
:: by Jesse Alama
::
:: Received October 9, 2007
:: Copyright (c) 2007 Association of Mizar Users
:: deftheorem defines <*> BSPACE:def 1 :
theorem :: BSPACE:1
theorem :: BSPACE:2
:: deftheorem defines Z_2 BSPACE:def 2 :
theorem :: BSPACE:3
theorem :: BSPACE:4
theorem Th5: :: BSPACE:5
theorem Th6: :: BSPACE:6
theorem Th7: :: BSPACE:7
theorem :: BSPACE:8
:: deftheorem Def3 defines @ BSPACE:def 3 :
theorem :: BSPACE:9
theorem :: BSPACE:10
theorem :: BSPACE:11
theorem :: BSPACE:12
for
X,
x,
y being
set holds
(
X @ x = X @ y iff (
x in X iff
y in X ) )
theorem :: BSPACE:13
for
X,
Y,
x being
set holds
(
X @ x = Y @ x iff (
x in X iff
x in Y ) )
theorem :: BSPACE:14
theorem Th15: :: BSPACE:15
theorem :: BSPACE:16
for
X,
Y being
set holds
(
X = Y iff for
x being
set holds
X @ x = Y @ x )
:: deftheorem Def4 defines \*\ BSPACE:def 4 :
:: deftheorem Def5 defines bspace-sum BSPACE:def 5 :
theorem Th17: :: BSPACE:17
theorem Th18: :: BSPACE:18
theorem :: BSPACE:19
theorem Th20: :: BSPACE:20
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
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
end;
:: deftheorem Def6 defines bspace-scalar-mult BSPACE:def 6 :
:: deftheorem defines bspace BSPACE:def 7 :
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 )
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) )
theorem Th21: :: BSPACE:21
theorem Th22: :: BSPACE:22
theorem Th23: :: BSPACE:23
theorem Th24: :: BSPACE:24
theorem Th25: :: BSPACE:25
theorem Th26: :: BSPACE:26
theorem Th27: :: BSPACE:27
theorem Th28: :: BSPACE:28
theorem Th29: :: BSPACE:29
:: deftheorem Def8 defines Singleton BSPACE:def 8 :
:: deftheorem Def9 defines Singleton BSPACE:def 9 :
:: deftheorem defines singletons BSPACE:def 10 :
theorem Th30: :: BSPACE:30
:: deftheorem Def11 defines @ BSPACE:def 11 :
theorem Th31: :: BSPACE:31
theorem Th32: :: BSPACE:32
theorem Th33: :: BSPACE:33
theorem Th34: :: BSPACE:34
theorem Th35: :: BSPACE:35
theorem Th36: :: BSPACE:36
theorem Th37: :: BSPACE:37
theorem :: BSPACE:38
theorem Th39: :: BSPACE:39
theorem Th40: :: BSPACE:40
theorem Th41: :: BSPACE:41
theorem :: BSPACE:42
theorem :: BSPACE:43
theorem :: BSPACE:44