set cR = center R;
set ccR = the carrier of ();
set cs = centralizer s;
set ccs = the carrier of ();
set lm = the multF of R | [: the carrier of (), the carrier of ():];
A1: the carrier of () c= the carrier of R by Th16;
A2: the carrier of () c= the carrier of R by Th23;
A3: dom the multF of R = [: the carrier of R, the carrier of R:] by FUNCT_2:def 1;
[: the carrier of (), the carrier of ():] c= [: the carrier of R, the carrier of R:]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [: the carrier of (), the carrier of ():] or x in [: the carrier of R, the carrier of R:] )
assume x in [: the carrier of (), the carrier of ():] ; :: thesis: x in [: the carrier of R, the carrier of R:]
then ex x1, x2 being object st
( x1 in the carrier of () & x2 in the carrier of () & x = [x1,x2] ) by ZFMISC_1:def 2;
hence x in [: the carrier of R, the carrier of R:] by ; :: thesis: verum
end;
then A4: dom ( the multF of R | [: the carrier of (), the carrier of ():]) = [: the carrier of (), the carrier of ():] by ;
now :: thesis: for x being object st x in [: the carrier of (), the carrier of ():] holds
( the multF of R | [: the carrier of (), the carrier of ():]) . x in the carrier of ()
let x be object ; :: thesis: ( x in [: the carrier of (), the carrier of ():] implies ( the multF of R | [: the carrier of (), the carrier of ():]) . x in the carrier of () )
assume A5: x in [: the carrier of (), the carrier of ():] ; :: thesis: ( the multF of R | [: the carrier of (), the carrier of ():]) . x in the carrier of ()
then consider x1, x2 being object such that
A6: x1 in the carrier of () and
A7: x2 in the carrier of () and
A8: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1 = x1 as Element of R by A1, A6;
reconsider x2 = x2 as Element of R by A2, A7;
( the multF of R | [: the carrier of (), the carrier of ():]) . x = x1 * x2 by ;
hence ( the multF of R | [: the carrier of (), the carrier of ():]) . x in the carrier of () by A6, A7, Th26; :: thesis: verum
end;
then reconsider lm = the multF of R | [: the carrier of (), the carrier of ():] as Function of [: the carrier of (), the carrier of ():], the carrier of () by ;
set Vos = ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #);
set cV = the carrier of ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #);
set aV = the addF of ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #);
A9: ( ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) is vector-distributive & ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) is scalar-distributive & ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) is scalar-associative & ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) is scalar-unital )
proof
A10: the multF of () = the multF of R || the carrier of () by Def4;
A11: the addF of () = the addF of R || the carrier of () by Def4;
A12: the addF of () = the addF of R || the carrier of () by Def5;
thus ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) is vector-distributive :: thesis: ( ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) is scalar-distributive & ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) is scalar-associative & ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) is scalar-unital )
proof
let x be Element of the carrier of (); :: according to VECTSP_1:def 13 :: thesis: for b1, b2 being Element of the carrier of ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) holds x * (b1 + b2) = (x * b1) + (x * b2)
let v, w be Element of the carrier of ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #); :: thesis: x * (v + w) = (x * v) + (x * w)
reconsider xx = x as Element of R by A1;
reconsider vv = v, ww = w as Element of R by A2;
A13: [x,w] in [: the carrier of (), the carrier of ():] by ZFMISC_1:def 2;
A14: [x,(v + w)] in [: the carrier of (), the carrier of ():] by ZFMISC_1:def 2;
A15: [v,w] in [: the carrier of (), the carrier of ():] by ZFMISC_1:def 2;
A16: [x,v] in [: the carrier of (), the carrier of ():] by ZFMISC_1:def 2;
A17: [(x * v),(x * w)] in [: the carrier of (), the carrier of ():] by ZFMISC_1:def 2;
thus x * (v + w) = the multF of R . [x,( the addF of ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) . [v,w])] by
.= xx * (vv + ww) by
.= (xx * vv) + (xx * ww) by VECTSP_1:def 2
.= the addF of R . [(x * v),( the multF of R . [xx,ww])] by
.= the addF of R . [(x * v),(x * w)] by
.= (x * v) + (x * w) by ; :: thesis: verum
end;
thus ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) is scalar-distributive :: thesis: ( ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) is scalar-associative & ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) is scalar-unital )
proof
let x, y be Element of the carrier of (); :: according to VECTSP_1:def 14 :: thesis: for b1 being Element of the carrier of ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) holds (x + y) * b1 = (x * b1) + (y * b1)
let v be Element of the carrier of ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #); :: thesis: (x + y) * v = (x * v) + (y * v)
reconsider xx = x, yy = y as Element of R by A1;
reconsider vv = v as Element of R by A2;
A18: [y,v] in [: the carrier of (), the carrier of ():] by ZFMISC_1:def 2;
A19: [x,v] in [: the carrier of (), the carrier of ():] by ZFMISC_1:def 2;
A20: [(x + y),v] in [: the carrier of (), the carrier of ():] by ZFMISC_1:def 2;
A21: [x,y] in [: the carrier of (), the carrier of ():] by ZFMISC_1:def 2;
A22: [(x * v),(y * v)] in [: the carrier of (), the carrier of ():] by ZFMISC_1:def 2;
thus (x + y) * v = the multF of R . [( the addF of () . [x,y]),vv] by
.= (xx + yy) * vv by
.= (xx * vv) + (yy * vv) by VECTSP_1:def 3
.= the addF of R . [(x * v),( the multF of R . [yy,vv])] by
.= the addF of R . [(x * v),(lm . (y,v))] by
.= (x * v) + (y * v) by ; :: thesis: verum
end;
thus ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) is scalar-associative :: thesis: ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) is scalar-unital
proof
let x, y be Element of the carrier of (); :: according to VECTSP_1:def 15 :: thesis: for b1 being Element of the carrier of ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) holds (x * y) * b1 = x * (y * b1)
let v be Element of the carrier of ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #); :: thesis: (x * y) * v = x * (y * v)
reconsider xx = x, yy = y as Element of R by A1;
reconsider vv = v as Element of R by A2;
A23: [x,(y * v)] in [: the carrier of (), the carrier of ():] by ZFMISC_1:def 2;
A24: [y,v] in [: the carrier of (), the carrier of ():] by ZFMISC_1:def 2;
A25: [(x * y),v] in [: the carrier of (), the carrier of ():] by ZFMISC_1:def 2;
A26: [x,y] in [: the carrier of (), the carrier of ():] by ZFMISC_1:def 2;
thus (x * y) * v = the multF of R . [( the multF of () . (x,y)),vv] by
.= (xx * yy) * vv by
.= xx * (yy * vv) by GROUP_1:def 3
.= the multF of R . [xx,(lm . (y,v))] by
.= x * (y * v) by ; :: thesis: verum
end;
let v be Element of the carrier of ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #); :: according to VECTSP_1:def 16 :: thesis: (1. ()) * v = v
reconsider vv = v as Element of R by A2;
1_ R in center R by Th19;
then 1_ R in the carrier of () ;
then A27: [(1_ R),vv] in [: the carrier of (), the carrier of ():] by ZFMISC_1:def 2;
thus (1. ()) * v = lm . ((1. R),vv) by Def4
.= (1. R) * vv by
.= v ; :: thesis: verum
end;
A28: ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) is add-associative
proof
let u, v, w be Element of the carrier of ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #); :: according to RLVECT_1:def 3 :: thesis: (u + v) + w = u + (v + w)
reconsider uu = u, vv = v, ww = w as Element of the carrier of () ;
thus (u + v) + w = (uu + vv) + ww
.= uu + (vv + ww) by RLVECT_1:def 3
.= u + (v + w) ; :: thesis: verum
end;
A29: ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) is right_zeroed
proof
let v be Element of the carrier of ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #); :: according to RLVECT_1:def 4 :: thesis: v + (0. ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #)) = v
reconsider vv = v as Element of the carrier of () ;
thus v + (0. ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #)) = vv + (0. ())
.= v by RLVECT_1:def 4 ; :: thesis: verum
end;
A30: ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) is right_complementable
proof
let v be Element of the carrier of ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #); :: according to ALGSTR_0:def 16 :: thesis:
reconsider vv = v as Element of the carrier of () ;
consider ww being Element of the carrier of () such that
A31: vv + ww = 0. () by ALGSTR_0:def 11;
reconsider w = ww as Element of the carrier of ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) ;
v + w = 0. ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) by A31;
hence ex w being Element of the carrier of ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) st v + w = 0. ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) ; :: according to ALGSTR_0:def 11 :: thesis: verum
end;
ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #) is Abelian
proof
let v, w be Element of the carrier of ModuleStr(# the carrier of (), the addF of (),(0. ()),lm #); :: according to RLVECT_1:def 2 :: thesis: v + w = w + v
reconsider vv = v, ww = w as Element of the carrier of () ;
thus v + w = ww + vv by RLVECT_1:2
.= 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 (), the addF of (), the ZeroF of () #) & the lmult of b1 = the multF of R | [: the carrier of (), the carrier of ():] ) by A9, A28, A29, A30; :: thesis: verum