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 ex x1, x2 being set st
( x1 in the carrier of (center R) & x2 in the carrier of R & x = [x1,x2] ) by ZFMISC_1:def 2;
hence x in [:the carrier of R,the carrier of R:] by A1, ZFMISC_1:def 2; :: thesis: verum
end;
then A3: 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 A4: 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 R
then consider x1, x2 being set such that
A5: x1 in the carrier of (center R) and
A6: x2 in the carrier of R and
A7: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1 = x1 as Element of R by A1, A5;
reconsider x2 = x2 as Element of R by A6;
(the multF of R | [:the carrier of (center R),the carrier of R:]) . x = x1 * x2 by A4, A7, 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 A3, 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 #);
A8: ( VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is vector-distributive & VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is scalar-distributive & VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is scalar-associative & VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is scalar-unital )
proof
A10: the multF of (center R) = the multF of R || the carrier of (center R) by Def4;
A11: the addF of (center R) = the addF of R || the carrier of (center R) by Def4;
thus VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is vector-distributive :: thesis: ( VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is scalar-distributive & VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is scalar-associative & VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is scalar-unital )
proof
let x 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)
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 in the carrier of (center R) ;
then reconsider xx = x as Element of R by A1;
reconsider vv = v, ww = w as Element of R ;
A12: [x,w] in [:the carrier of (center R),the carrier of R:] by ZFMISC_1:def 2;
A13: [x,(v + w)] in [:the carrier of (center R),the carrier of R:] by ZFMISC_1:def 2;
A15: [x,v] in [:the carrier of (center R),the carrier of R:] by ZFMISC_1:def 2;
thus x * (v + w) = xx * (vv + ww) by A13, 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 A15, FUNCT_1:72
.= (x * v) + (x * w) by A12, FUNCT_1:72 ; :: thesis: verum
end;
thus VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is scalar-distributive :: thesis: ( VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is scalar-associative & VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is scalar-unital )
proof
let x, y be Element of the carrier of (center R); :: according to VECTSP_1:def 27 :: thesis: for b1 being Element of the carrier of VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) holds (x + y) * b1 = (x * b1) + (y * b1)
let v be Element of the carrier of VectSpStr(# the carrier of R,the addF of R,(0. R),lm #); :: thesis: (x + y) * v = (x * v) + (y * v)
A9: 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, A9;
reconsider vv = v as Element of R ;
A14: [y,v] in [:the carrier of (center R),the carrier of R:] by ZFMISC_1:def 2;
A15: [x,v] in [:the carrier of (center R),the carrier of R:] by ZFMISC_1:def 2;
A16: [(x + y),v] in [:the carrier of (center R),the carrier of R:] by ZFMISC_1:def 2;
A20: [x,y] in [:the carrier of (center R),the carrier of (center R):] by ZFMISC_1:def 2;
thus (x + y) * v = the multF of R . [(the addF of (center R) . [x,y]),vv] by A16, FUNCT_1:72
.= (xx + yy) * vv by A11, A20, 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 A15, FUNCT_1:72
.= (x * v) + (y * v) by A14, FUNCT_1:72 ; :: thesis: verum
end;
thus VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is scalar-associative :: thesis: VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is scalar-unital
proof
let x, y be Element of the carrier of (center R); :: according to VECTSP_1:def 28 :: thesis: for b1 being Element of the carrier of VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) holds (x * y) * b1 = x * (y * b1)
let v be Element of the carrier of VectSpStr(# the carrier of R,the addF of R,(0. R),lm #); :: thesis: (x * y) * v = x * (y * v)
A9: 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, A9;
reconsider vv = v as Element of R ;
A17: [x,(y * v)] in [:the carrier of (center R),the carrier of R:] by ZFMISC_1:def 2;
A18: [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: [x,y] in [:the carrier of (center R),the carrier of (center R):] by ZFMISC_1:def 2;
thus (x * y) * v = the multF of R . [(the multF of (center R) . x,y),vv] by A19, FUNCT_1:72
.= (xx * yy) * vv by A10, A20, FUNCT_1:72
.= xx * (yy * vv) by GROUP_1:def 4
.= the multF of R . [xx,(lm . y,v)] by A18, FUNCT_1:72
.= x * (y * v) by A17, FUNCT_1:72 ; :: thesis: verum
end;
let v be Element of the carrier of VectSpStr(# the carrier of R,the addF of R,(0. R),lm #); :: according to VECTSP_1:def 29 :: thesis: (1. (center R)) * v = v
reconsider vv = v as Element of R ;
1_ R in center R by Th20;
then 1_ R in the carrier of (center R) by STRUCT_0:def 5;
then A21: [(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 A21, FUNCT_1:72
.= v by VECTSP_1:def 19 ; :: thesis: verum
end;
A22: VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is add-associative
proof
let u, v, w be Element of the carrier of VectSpStr(# the carrier of R,the addF of R,(0. R),lm #); :: according to RLVECT_1:def 6 :: thesis: (u + v) + w = u + (v + w)
reconsider uu = u, vv = v, ww = w as Element of the carrier of R ;
thus (u + v) + w = (uu + vv) + ww
.= uu + (vv + ww) by RLVECT_1:def 6
.= u + (v + w) ; :: thesis: verum
end;
A23: VectSpStr(# the carrier of R,the addF of R,(0. R),lm #) is right_zeroed
proof
let v be Element of the carrier of VectSpStr(# the carrier of R,the addF of R,(0. R),lm #); :: according to RLVECT_1:def 7 :: thesis: v + (0. VectSpStr(# the carrier of R,the addF of R,(0. R),lm #)) = v
reconsider vv = v as Element of the carrier of R ;
thus v + (0. VectSpStr(# the carrier of R,the addF of R,(0. R),lm #)) = vv + (0. R)
.= v by RLVECT_1:def 7 ; :: thesis: verum
end;
A24: 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
A25: 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 A25;
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
proof
let v, w be Element of the carrier of VectSpStr(# the carrier of R,the addF of R,(0. R),lm #); :: according to RLVECT_1:def 5 :: thesis: v + w = w + v
reconsider vv = v, ww = w as Element of the carrier of R ;
thus v + w = ww + vv by RLVECT_1:5
.= w + v ; :: thesis: verum
end;
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 A8, A22, A23, A24; :: thesis: verum