set cR = center R;

set ccR = the carrier of (center R);

set cs = centralizer s;

set ccs = the carrier of (centralizer s);

set lm = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):];

A1: the carrier of (center R) c= the carrier of R by Th16;

A2: the carrier of (centralizer s) 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 (center R), the carrier of (centralizer s):] c= [: the carrier of R, the carrier of R:]

set Vos = ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #);

set cV = the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #);

set aV = the addF of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #);

A9: ( ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is vector-distributive & ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-distributive & ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-associative & ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-unital )_{1} being strict VectSp of center R st

( addLoopStr(# the carrier of b_{1}, the addF of b_{1}, the ZeroF of b_{1} #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b_{1} = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] )
by A9, A28, A29, A30; :: thesis: verum

set ccR = the carrier of (center R);

set cs = centralizer s;

set ccs = the carrier of (centralizer s);

set lm = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):];

A1: the carrier of (center R) c= the carrier of R by Th16;

A2: the carrier of (centralizer s) 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 (center R), the carrier of (centralizer s):] c= [: the carrier of R, the carrier of R:]

proof

then A4:
dom ( the multF of R | [: the carrier of (center R), the carrier of (centralizer s):]) = [: the carrier of (center R), the carrier of (centralizer s):]
by A3, RELAT_1:62;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [: the carrier of (center R), the carrier of (centralizer s):] or x in [: the carrier of R, the carrier of R:] )

assume x in [: the carrier of (center R), the carrier of (centralizer s):] ; :: thesis: x in [: the carrier of R, the carrier of R:]

then ex x1, x2 being object st

( x1 in the carrier of (center R) & x2 in the carrier of (centralizer s) & x = [x1,x2] ) by ZFMISC_1:def 2;

hence x in [: the carrier of R, the carrier of R:] by A1, A2, ZFMISC_1:def 2; :: thesis: verum

end;assume x in [: the carrier of (center R), the carrier of (centralizer s):] ; :: thesis: x in [: the carrier of R, the carrier of R:]

then ex x1, x2 being object st

( x1 in the carrier of (center R) & x2 in the carrier of (centralizer s) & x = [x1,x2] ) by ZFMISC_1:def 2;

hence x in [: the carrier of R, the carrier of R:] by A1, A2, ZFMISC_1:def 2; :: thesis: verum

now :: thesis: for x being object st x in [: the carrier of (center R), the carrier of (centralizer s):] holds

( the multF of R | [: the carrier of (center R), the carrier of (centralizer s):]) . x in the carrier of (centralizer s)

then reconsider lm = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] as Function of [: the carrier of (center R), the carrier of (centralizer s):], the carrier of (centralizer s) by A4, FUNCT_2:3;( the multF of R | [: the carrier of (center R), the carrier of (centralizer s):]) . x in the carrier of (centralizer s)

let x be object ; :: thesis: ( x in [: the carrier of (center R), the carrier of (centralizer s):] implies ( the multF of R | [: the carrier of (center R), the carrier of (centralizer s):]) . x in the carrier of (centralizer s) )

assume A5: x in [: the carrier of (center R), the carrier of (centralizer s):] ; :: thesis: ( the multF of R | [: the carrier of (center R), the carrier of (centralizer s):]) . x in the carrier of (centralizer s)

then consider x1, x2 being object such that

A6: x1 in the carrier of (center R) and

A7: x2 in the carrier of (centralizer s) 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 (center R), the carrier of (centralizer s):]) . x = x1 * x2 by A5, A8, FUNCT_1:49;

hence ( the multF of R | [: the carrier of (center R), the carrier of (centralizer s):]) . x in the carrier of (centralizer s) by A6, A7, Th26; :: thesis: verum

end;assume A5: x in [: the carrier of (center R), the carrier of (centralizer s):] ; :: thesis: ( the multF of R | [: the carrier of (center R), the carrier of (centralizer s):]) . x in the carrier of (centralizer s)

then consider x1, x2 being object such that

A6: x1 in the carrier of (center R) and

A7: x2 in the carrier of (centralizer s) 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 (center R), the carrier of (centralizer s):]) . x = x1 * x2 by A5, A8, FUNCT_1:49;

hence ( the multF of R | [: the carrier of (center R), the carrier of (centralizer s):]) . x in the carrier of (centralizer s) by A6, A7, Th26; :: thesis: verum

set Vos = ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #);

set cV = the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #);

set aV = the addF of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #);

A9: ( ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is vector-distributive & ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-distributive & ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-associative & ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-unital )

proof

A28:
ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is add-associative
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;

A12: the addF of (centralizer s) = the addF of R || the carrier of (centralizer s) by Def5;

thus ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is vector-distributive :: thesis: ( ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-distributive & ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-associative & ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-unital )

reconsider vv = v as Element of R by A2;

1_ R in center R by Th19;

then 1_ R in the carrier of (center R) ;

then A27: [(1_ R),vv] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

thus (1. (center R)) * v = lm . ((1. R),vv) by Def4

.= (1. R) * vv by A27, FUNCT_1:49

.= v ; :: thesis: verum

end;A11: the addF of (center R) = the addF of R || the carrier of (center R) by Def4;

A12: the addF of (centralizer s) = the addF of R || the carrier of (centralizer s) by Def5;

thus ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is vector-distributive :: thesis: ( ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-distributive & ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-associative & ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-unital )

proof

thus
ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-distributive
:: thesis: ( ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-associative & ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-unital )
let x be Element of the carrier of (center R); :: according to VECTSP_1:def 13 :: thesis: for b_{1}, b_{2} being Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) holds x * (b_{1} + b_{2}) = (x * b_{1}) + (x * b_{2})

let v, w be Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),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 (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A14: [x,(v + w)] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A15: [v,w] in [: the carrier of (centralizer s), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A16: [x,v] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A17: [(x * v),(x * w)] in [: the carrier of (centralizer s), the carrier of (centralizer s):] by ZFMISC_1:def 2;

thus x * (v + w) = the multF of R . [x,( the addF of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) . [v,w])] by A14, FUNCT_1:49

.= xx * (vv + ww) by A12, A15, FUNCT_1:49

.= (xx * vv) + (xx * ww) by VECTSP_1:def 2

.= the addF of R . [(x * v),( the multF of R . [xx,ww])] by A16, FUNCT_1:49

.= the addF of R . [(x * v),(x * w)] by A13, FUNCT_1:49

.= (x * v) + (x * w) by A12, A17, FUNCT_1:49 ; :: thesis: verum

end;let v, w be Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),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 (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A14: [x,(v + w)] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A15: [v,w] in [: the carrier of (centralizer s), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A16: [x,v] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A17: [(x * v),(x * w)] in [: the carrier of (centralizer s), the carrier of (centralizer s):] by ZFMISC_1:def 2;

thus x * (v + w) = the multF of R . [x,( the addF of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) . [v,w])] by A14, FUNCT_1:49

.= xx * (vv + ww) by A12, A15, FUNCT_1:49

.= (xx * vv) + (xx * ww) by VECTSP_1:def 2

.= the addF of R . [(x * v),( the multF of R . [xx,ww])] by A16, FUNCT_1:49

.= the addF of R . [(x * v),(x * w)] by A13, FUNCT_1:49

.= (x * v) + (x * w) by A12, A17, FUNCT_1:49 ; :: thesis: verum

proof

thus
ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-associative
:: thesis: ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is scalar-unital
let x, y be Element of the carrier of (center R); :: according to VECTSP_1:def 14 :: thesis: for b_{1} being Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) holds (x + y) * b_{1} = (x * b_{1}) + (y * b_{1})

let v be Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),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 (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A19: [x,v] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A20: [(x + y),v] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A21: [x,y] in [: the carrier of (center R), the carrier of (center R):] by ZFMISC_1:def 2;

A22: [(x * v),(y * v)] in [: the carrier of (centralizer s), the carrier of (centralizer s):] by ZFMISC_1:def 2;

thus (x + y) * v = the multF of R . [( the addF of (center R) . [x,y]),vv] by A20, FUNCT_1:49

.= (xx + yy) * vv by A11, A21, FUNCT_1:49

.= (xx * vv) + (yy * vv) by VECTSP_1:def 3

.= the addF of R . [(x * v),( the multF of R . [yy,vv])] by A19, FUNCT_1:49

.= the addF of R . [(x * v),(lm . (y,v))] by A18, FUNCT_1:49

.= (x * v) + (y * v) by A12, A22, FUNCT_1:49 ; :: thesis: verum

end;let v be Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),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 (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A19: [x,v] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A20: [(x + y),v] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A21: [x,y] in [: the carrier of (center R), the carrier of (center R):] by ZFMISC_1:def 2;

A22: [(x * v),(y * v)] in [: the carrier of (centralizer s), the carrier of (centralizer s):] by ZFMISC_1:def 2;

thus (x + y) * v = the multF of R . [( the addF of (center R) . [x,y]),vv] by A20, FUNCT_1:49

.= (xx + yy) * vv by A11, A21, FUNCT_1:49

.= (xx * vv) + (yy * vv) by VECTSP_1:def 3

.= the addF of R . [(x * v),( the multF of R . [yy,vv])] by A19, FUNCT_1:49

.= the addF of R . [(x * v),(lm . (y,v))] by A18, FUNCT_1:49

.= (x * v) + (y * v) by A12, A22, FUNCT_1:49 ; :: thesis: verum

proof

let v be Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #); :: according to VECTSP_1:def 16 :: thesis: (1. (center R)) * v = v
let x, y be Element of the carrier of (center R); :: according to VECTSP_1:def 15 :: thesis: for b_{1} being Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) holds (x * y) * b_{1} = x * (y * b_{1})

let v be Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),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 (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A24: [y,v] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A25: [(x * y),v] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A26: [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 A25, FUNCT_1:49

.= (xx * yy) * vv by A10, A26, FUNCT_1:49

.= xx * (yy * vv) by GROUP_1:def 3

.= the multF of R . [xx,(lm . (y,v))] by A24, FUNCT_1:49

.= x * (y * v) by A23, FUNCT_1:49 ; :: thesis: verum

end;let v be Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),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 (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A24: [y,v] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A25: [(x * y),v] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

A26: [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 A25, FUNCT_1:49

.= (xx * yy) * vv by A10, A26, FUNCT_1:49

.= xx * (yy * vv) by GROUP_1:def 3

.= the multF of R . [xx,(lm . (y,v))] by A24, FUNCT_1:49

.= x * (y * v) by A23, FUNCT_1:49 ; :: thesis: verum

reconsider vv = v as Element of R by A2;

1_ R in center R by Th19;

then 1_ R in the carrier of (center R) ;

then A27: [(1_ R),vv] in [: the carrier of (center R), the carrier of (centralizer s):] by ZFMISC_1:def 2;

thus (1. (center R)) * v = lm . ((1. R),vv) by Def4

.= (1. R) * vv by A27, FUNCT_1:49

.= v ; :: thesis: verum

proof

A29:
ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is right_zeroed
let u, v, w be Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),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 (centralizer s) ;

thus (u + v) + w = (uu + vv) + ww

.= uu + (vv + ww) by RLVECT_1:def 3

.= u + (v + w) ; :: thesis: verum

end;reconsider uu = u, vv = v, ww = w as Element of the carrier of (centralizer s) ;

thus (u + v) + w = (uu + vv) + ww

.= uu + (vv + ww) by RLVECT_1:def 3

.= u + (v + w) ; :: thesis: verum

proof

A30:
ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is right_complementable
let v be Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #); :: according to RLVECT_1:def 4 :: thesis: v + (0. ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #)) = v

reconsider vv = v as Element of the carrier of (centralizer s) ;

thus v + (0. ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #)) = vv + (0. (centralizer s))

.= v by RLVECT_1:def 4 ; :: thesis: verum

end;reconsider vv = v as Element of the carrier of (centralizer s) ;

thus v + (0. ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #)) = vv + (0. (centralizer s))

.= v by RLVECT_1:def 4 ; :: thesis: verum

proof

ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) is Abelian
let v be Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable

reconsider vv = v as Element of the carrier of (centralizer s) ;

consider ww being Element of the carrier of (centralizer s) such that

A31: vv + ww = 0. (centralizer s) by ALGSTR_0:def 11;

reconsider w = ww as Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) ;

v + w = 0. ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) by A31;

hence ex w being Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) st v + w = 0. ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) ; :: according to ALGSTR_0:def 11 :: thesis: verum

end;reconsider vv = v as Element of the carrier of (centralizer s) ;

consider ww being Element of the carrier of (centralizer s) such that

A31: vv + ww = 0. (centralizer s) by ALGSTR_0:def 11;

reconsider w = ww as Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) ;

v + w = 0. ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) by A31;

hence ex w being Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) st v + w = 0. ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #) ; :: according to ALGSTR_0:def 11 :: thesis: verum

proof

hence
ex b
let v, w be Element of the carrier of ModuleStr(# the carrier of (centralizer s), the addF of (centralizer s),(0. (centralizer s)),lm #); :: according to RLVECT_1:def 2 :: thesis: v + w = w + v

reconsider vv = v, ww = w as Element of the carrier of (centralizer s) ;

thus v + w = ww + vv by RLVECT_1:2

.= w + v ; :: thesis: verum

end;reconsider vv = v, ww = w as Element of the carrier of (centralizer s) ;

thus v + w = ww + vv by RLVECT_1:2

.= w + v ; :: thesis: verum

( addLoopStr(# the carrier of b