set X = Z_2 ;
set X0 = n -tuples_on BOOLEAN;
set Z0 = ZeroB n;
set ADD = XORB n;
set LMLT = MLTB n;
set XP = ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #);
reconsider 1X = TRUE as Element of Z_2 by BSPACE:6;
A1:
( ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is scalar-distributive & ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is vector-distributive & ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is scalar-associative & ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is scalar-unital )
proof
thus
ModuleStr(#
(n -tuples_on BOOLEAN),
(XORB n),
(ZeroB n),
(MLTB n) #) is
scalar-distributive
( ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is vector-distributive & ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is scalar-associative & ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is scalar-unital )proof
let x,
y be
Element of
Z_2;
VECTSP_1:def 14 for b1 being Element of the carrier of ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) holds (x + y) * b1 = (x * b1) + (y * b1)let v be
Element of
ModuleStr(#
(n -tuples_on BOOLEAN),
(XORB n),
(ZeroB n),
(MLTB n) #);
(x + y) * v = (x * v) + (y * v)
reconsider v1 =
v as
Element of
n -tuples_on BOOLEAN ;
reconsider xyv1 =
(x + y) * v as
Element of
n -tuples_on BOOLEAN ;
reconsider xv =
x * v as
Element of
n -tuples_on BOOLEAN ;
reconsider yv =
y * v as
Element of
n -tuples_on BOOLEAN ;
reconsider xyv2 =
(x * v) + (y * v) as
Element of
n -tuples_on BOOLEAN ;
A2:
len xyv1 = n
by CARD_1:def 7;
A3:
len xyv2 = n
by CARD_1:def 7;
now for i being Nat st 1 <= i & i <= len xyv1 holds
xyv1 . i = xyv2 . ilet i be
Nat;
( 1 <= i & i <= len xyv1 implies xyv1 . i = xyv2 . i )assume
( 1
<= i &
i <= len xyv1 )
;
xyv1 . i = xyv2 . ithen A4:
i in Seg n
by A2;
A5:
xv . i = x '&' (v1 . i)
by Def4, A4, BSPACE:3;
A6:
yv . i = y '&' (v1 . i)
by Def4, A4, BSPACE:3;
thus xyv1 . i =
(x 'xor' y) '&' (v1 . i)
by Def4, A4, BSPACE:3
.=
(xv . i) 'xor' (yv . i)
by XBOOLEAN:75, A5, A6
.=
(Op-XOR (xv,yv)) . i
by DESCIP_1:def 4, A4
.=
xyv2 . i
by Def1
;
verum end;
hence
(x + y) * v = (x * v) + (y * v)
by FINSEQ_1:14, CARD_1:def 7, A3;
verum
end;
thus
ModuleStr(#
(n -tuples_on BOOLEAN),
(XORB n),
(ZeroB n),
(MLTB n) #) is
vector-distributive
( ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is scalar-associative & ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is scalar-unital )proof
let x be
Element of
Z_2;
VECTSP_1:def 13 for b1, b2 being Element of the carrier of ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) holds x * (b1 + b2) = (x * b1) + (x * b2)let v,
w be
Element of
ModuleStr(#
(n -tuples_on BOOLEAN),
(XORB n),
(ZeroB n),
(MLTB n) #);
x * (v + w) = (x * v) + (x * w)
reconsider v1 =
v as
Element of
n -tuples_on BOOLEAN ;
reconsider w1 =
w as
Element of
n -tuples_on BOOLEAN ;
reconsider xvw1 =
x * (v + w) as
Element of
n -tuples_on BOOLEAN ;
reconsider vw =
v + w as
Element of
n -tuples_on BOOLEAN ;
reconsider xv =
x * v as
Element of
n -tuples_on BOOLEAN ;
reconsider xw =
x * w as
Element of
n -tuples_on BOOLEAN ;
reconsider xvw2 =
(x * v) + (x * w) as
Element of
n -tuples_on BOOLEAN ;
A7:
len xvw1 = n
by CARD_1:def 7;
A8:
len xvw2 = n
by CARD_1:def 7;
now for i being Nat st 1 <= i & i <= len xvw1 holds
xvw2 . i = xvw1 . ilet i be
Nat;
( 1 <= i & i <= len xvw1 implies xvw2 . i = xvw1 . i )assume
( 1
<= i &
i <= len xvw1 )
;
xvw2 . i = xvw1 . ithen A9:
i in Seg n
by A7;
A10:
xv . i = x '&' (v1 . i)
by Def4, A9, BSPACE:3;
A11:
xw . i = x '&' (w1 . i)
by Def4, A9, BSPACE:3;
A12:
vw . i =
(Op-XOR (v1,w1)) . i
by Def1
.=
(v1 . i) 'xor' (w1 . i)
by DESCIP_1:def 4, A9
;
thus xvw2 . i =
(Op-XOR (xv,xw)) . i
by Def1
.=
(x '&' (v1 . i)) 'xor' (x '&' (w1 . i))
by DESCIP_1:def 4, A9, A10, A11
.=
x '&' (vw . i)
by XBOOLEAN:75, A12
.=
xvw1 . i
by Def4, A9, BSPACE:3
;
verum end;
hence
x * (v + w) = (x * v) + (x * w)
by FINSEQ_1:14, CARD_1:def 7, A8;
verum
end;
thus
ModuleStr(#
(n -tuples_on BOOLEAN),
(XORB n),
(ZeroB n),
(MLTB n) #) is
scalar-associative
ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is scalar-unital
thus
ModuleStr(#
(n -tuples_on BOOLEAN),
(XORB n),
(ZeroB n),
(MLTB n) #) is
scalar-unital
verum
end;
A19:
ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is add-associative
proof
for
u,
v,
w being
Element of
ModuleStr(#
(n -tuples_on BOOLEAN),
(XORB n),
(ZeroB n),
(MLTB n) #) holds
(u + v) + w = u + (v + w)
proof
let u,
v,
w be
Element of
ModuleStr(#
(n -tuples_on BOOLEAN),
(XORB n),
(ZeroB n),
(MLTB n) #);
(u + v) + w = u + (v + w)
reconsider u1 =
u,
v1 =
v,
w1 =
w as
Element of
n -tuples_on BOOLEAN ;
A20:
u + v = Op-XOR (
u1,
v1)
by Def1;
A21:
v + w = Op-XOR (
v1,
w1)
by Def1;
thus (u + v) + w =
Op-XOR (
(Op-XOR (u1,v1)),
w1)
by A20, Def1
.=
Op-XOR (
u1,
(Op-XOR (v1,w1)))
by Th1
.=
u + (v + w)
by A21, Def1
;
verum
end;
hence
ModuleStr(#
(n -tuples_on BOOLEAN),
(XORB n),
(ZeroB n),
(MLTB n) #) is
add-associative
by RLVECT_1:def 3;
verum
end;
A22:
ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is right_zeroed
proof
for
v being
Element of
ModuleStr(#
(n -tuples_on BOOLEAN),
(XORB n),
(ZeroB n),
(MLTB n) #) holds
v + (0. ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #)) = v
proof
let v be
Element of
ModuleStr(#
(n -tuples_on BOOLEAN),
(XORB n),
(ZeroB n),
(MLTB n) #);
v + (0. ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #)) = v
reconsider v1 =
v as
Element of
n -tuples_on BOOLEAN ;
thus v + (0. ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #)) =
Op-XOR (
v1,
(ZeroB n))
by Def1
.=
v
by Th2
;
verum
end;
hence
ModuleStr(#
(n -tuples_on BOOLEAN),
(XORB n),
(ZeroB n),
(MLTB n) #) is
right_zeroed
by RLVECT_1:def 4;
verum
end;
A23:
ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is right_complementable
ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is Abelian
hence
ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is VectSp of Z_2
by A1, A19, A22, A23; verum