set cR = center R;
set ccR = the carrier of (center R);
set ccs = the carrier of R;
set lm = the multF of R | [:the carrier of (center R),the carrier of R:];
A1:
the carrier of (center R) c= the carrier of R
by Th17;
A2:
dom the multF of R = [:the carrier of R,the carrier of R:]
by FUNCT_2:def 1;
[:the carrier of (center R),the carrier of R:] c= [:the carrier of R,the carrier of R:]
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in [:the carrier of (center R),the carrier of R:] or x in [:the carrier of R,the carrier of R:] )
assume
x in [:the carrier of (center R),the carrier of R:]
;
:: thesis: x in [:the carrier of R,the carrier of R:]
then consider x1,
x2 being
set such that A3:
x1 in the
carrier of
(center R)
and A4:
x2 in the
carrier of
R
and A5:
x = [x1,x2]
by ZFMISC_1:def 2;
thus
x in [:the carrier of R,the carrier of R:]
by A1, A3, A4, A5, ZFMISC_1:def 2;
:: thesis: verum
end;
then A6:
dom (the multF of R | [:the carrier of (center R),the carrier of R:]) = [:the carrier of (center R),the carrier of R:]
by A2, RELAT_1:91;
now let x be
set ;
:: thesis: ( x in [:the carrier of (center R),the carrier of R:] implies (the multF of R | [:the carrier of (center R),the carrier of R:]) . x in the carrier of R )assume A7:
x in [:the carrier of (center R),the carrier of R:]
;
:: thesis: (the multF of R | [:the carrier of (center R),the carrier of R:]) . x in the carrier of Rthen consider x1,
x2 being
set such that A8:
x1 in the
carrier of
(center R)
and A9:
x2 in the
carrier of
R
and A10:
x = [x1,x2]
by ZFMISC_1:def 2;
reconsider x1 =
x1 as
Element of
R by A1, A8;
reconsider x2 =
x2 as
Element of
R by A9;
(the multF of R | [:the carrier of (center R),the carrier of R:]) . x = x1 * x2
by A7, A10, FUNCT_1:72;
hence
(the multF of R | [:the carrier of (center R),the carrier of R:]) . x in the
carrier of
R
;
:: thesis: verum end;
then reconsider lm = the multF of R | [:the carrier of (center R),the carrier of R:] as Function of [:the carrier of (center R),the carrier of R:],the carrier of R by A6, FUNCT_2:5;
set Vos = VectSpStr(# the carrier of R,the addF of R,(0. R),lm #);
set cV = the carrier of VectSpStr(# the carrier of R,the addF of R,(0. R),lm #);
A11:
VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is VectSp-like
proof
let x,
y be
Element of the
carrier of
(center R);
:: according to VECTSP_1:def 26 :: thesis: for b1, b2 being Element of the carrier of VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) holds
( x * (b1 + b2) = (x * b1) + (x * b2) & (x + y) * b1 = (x * b1) + (y * b1) & (x * y) * b1 = x * (y * b1) & (1. (center R)) * b1 = b1 )let v,
w be
Element of the
carrier of
VectSpStr(# the
carrier of
R,the
addF of
R,
(0. R),
lm #);
:: thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. (center R)) * v = v )
(
x in the
carrier of
(center R) &
y in the
carrier of
(center R) )
;
then reconsider xx =
x,
yy =
y as
Element of
R by A1;
reconsider vv =
v,
ww =
w as
Element of
R ;
A12:
the
multF of
(center R) = the
multF of
R || the
carrier of
(center R)
by Def4;
A13:
the
addF of
(center R) = the
addF of
R || the
carrier of
(center R)
by Def4;
A14:
[x,w] in [:the carrier of (center R),the carrier of R:]
by ZFMISC_1:def 2;
A15:
[x,(v + w)] in [:the carrier of (center R),the carrier of R:]
by ZFMISC_1:def 2;
A16:
[y,v] in [:the carrier of (center R),the carrier of R:]
by ZFMISC_1:def 2;
A17:
[x,v] in [:the carrier of (center R),the carrier of R:]
by ZFMISC_1:def 2;
A18:
[(x + y),v] in [:the carrier of (center R),the carrier of R:]
by ZFMISC_1:def 2;
A19:
[x,(y * v)] in [:the carrier of (center R),the carrier of R:]
by ZFMISC_1:def 2;
A20:
[y,v] in [:the carrier of (center R),the carrier of R:]
by ZFMISC_1:def 2;
A21:
[(x * y),v] in [:the carrier of (center R),the carrier of R:]
by ZFMISC_1:def 2;
A22:
[x,y] in [:the carrier of (center R),the carrier of (center R):]
by ZFMISC_1:def 2;
thus x * (v + w) =
xx * (vv + ww)
by A15, FUNCT_1:72
.=
(xx * vv) + (xx * ww)
by VECTSP_1:def 11
.=
the
addF of
R . [(x * v),(the multF of R . [xx,ww])]
by A17, FUNCT_1:72
.=
(x * v) + (x * w)
by A14, FUNCT_1:72
;
:: thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. (center R)) * v = v )
thus (x + y) * v =
the
multF of
R . [(the addF of (center R) . [x,y]),vv]
by A18, FUNCT_1:72
.=
(xx + yy) * vv
by A13, A22, FUNCT_1:72
.=
(xx * vv) + (yy * vv)
by VECTSP_1:def 12
.=
the
addF of
R . [(x * v),(the multF of R . [yy,vv])]
by A17, FUNCT_1:72
.=
(x * v) + (y * v)
by A16, FUNCT_1:72
;
:: thesis: ( (x * y) * v = x * (y * v) & (1. (center R)) * v = v )
thus (x * y) * v =
the
multF of
R . [(the multF of (center R) . x,y),vv]
by A21, FUNCT_1:72
.=
(xx * yy) * vv
by A12, A22, FUNCT_1:72
.=
xx * (yy * vv)
by GROUP_1:def 4
.=
the
multF of
R . [xx,(lm . y,v)]
by A20, FUNCT_1:72
.=
x * (y * v)
by A19, FUNCT_1:72
;
:: thesis: (1. (center R)) * v = v
1_ R in center R
by Th20;
then
1_ R in the
carrier of
(center R)
by STRUCT_0:def 5;
then A23:
[(1_ R),vv] in [:the carrier of (center R),the carrier of R:]
by ZFMISC_1:def 2;
thus (1. (center R)) * v =
lm . (1. R),
vv
by Def4
.=
(1. R) * vv
by A23, FUNCT_1:72
.=
v
by VECTSP_1:def 19
;
:: thesis: verum
end;
A24:
VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is add-associative
A25:
VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is right_zeroed
A26:
VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is right_complementable
proof
let v be
Element of the
carrier of
VectSpStr(# the
carrier of
R,the
addF of
R,
(0. R),
lm #);
:: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider vv =
v as
Element of the
carrier of
R ;
consider ww being
Element of the
carrier of
R such that A27:
vv + ww = 0. R
by ALGSTR_0:def 11;
reconsider w =
ww as
Element of the
carrier of
VectSpStr(# the
carrier of
R,the
addF of
R,
(0. R),
lm #) ;
v + w = 0. VectSpStr(# the
carrier of
R,the
addF of
R,
(0. R),
lm #)
by A27;
hence
ex
w being
Element of the
carrier of
VectSpStr(# the
carrier of
R,the
addF of
R,
(0. R),
lm #) st
v + w = 0. VectSpStr(# the
carrier of
R,the
addF of
R,
(0. R),
lm #)
;
:: according to ALGSTR_0:def 11 :: thesis: verum
end;
VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is Abelian
hence
ex b1 being strict VectSp of center R st
( addLoopStr(# the carrier of b1,the addF of b1,the ZeroF of b1 #) = addLoopStr(# the carrier of R,the addF of R,the ZeroF of R #) & the lmult of b1 = the multF of R | [:the carrier of (center R),the carrier of R:] )
by A11, A24, A25, A26; :: thesis: verum