let Q be multLoop; :: thesis: [#] (lp (Cent Q)) = Cent Q
A1: 1. Q in Cent Q

proof

A2: 1. Q in Nucl Q by Th20;
for y being Element of Q holds (1. Q) * y = y * (1. Q) ;
then 1. Q in Comm Q by Def25;
hence 1. Q in Cent Q by XBOOLE_0:def 4, A2; :: thesis: verum

end;

A3: for x, y being Element of Q st x in Cent Q & y in Cent Q holds
x * y in Cent Q

proof

let x, y be Element of Q; :: thesis: ( x in Cent Q & y in Cent Q implies x * y in Cent Q )
assume that
A4: x in Cent Q and
A5: y in Cent Q ; :: thesis: x * y in Cent Q
A6: ( x in Comm Q & x in Nucl Q ) by XBOOLE_0:def 4, A4;
A7: ( y in Comm Q & y in Nucl Q ) by XBOOLE_0:def 4, A5;
A8: x in Nucl_l Q by Th12, A6;
A9: ( y in Nucl_m Q & y in Nucl_r Q ) by Th12, A7;
for z being Element of Q holds (x * y) * z = z * (x * y)

proof

let z be Element of Q; :: thesis: (x * y) * z = z * (x * y)
(x * y) * z = x * (y * z) by A9, Def23
.= x * (z * y) by A7, Def25
.= (x * z) * y by A8, Def22
.= (z * x) * y by A6, Def25
.= z * (x * y) by A9, Def24 ;
hence (x * y) * z = z * (x * y) ; :: thesis: verum

end;

then A10: x * y in Comm Q by Def25;
x * y in Nucl Q by Th21, A6, A7;
hence x * y in Cent Q by XBOOLE_0:def 4, A10; :: thesis: verum

end;

A11: for x, y being Element of Q st x in Cent Q & y in Cent Q holds
x \ y in Cent Q

proof

let x, y be Element of Q; :: thesis: ( x in Cent Q & y in Cent Q implies x \ y in Cent Q )
assume that
A12: x in Cent Q and
A13: y in Cent Q ; :: thesis: x \ y in Cent Q
A14: ( x in Comm Q & x in Nucl Q ) by XBOOLE_0:def 4, A12;
A15: ( y in Comm Q & y in Nucl Q ) by XBOOLE_0:def 4, A13;
A16: x in Nucl_m Q by Th12, A14;
for z being Element of Q holds (x \ y) * z = z * (x \ y)

proof

let z be Element of Q; :: thesis: (x \ y) * z = z * (x \ y)
(x \ y) * z = (x \ y) * ((z / x) * x)
.= (x \ y) * (x * (z / x)) by A14, Def25
.= ((x \ y) * x) * (z / x) by A16, Def23
.= (x * (x \ y)) * (z / x) by A14, Def25
.= (z / x) * (x * (x \ y)) by A15, Def25
.= ((z / x) * x) * (x \ y) by A16, Def23
.= z * (x \ y) ;
hence (x \ y) * z = z * (x \ y) ; :: thesis: verum

end;

then A17: x \ y in Comm Q by Def25;
x \ y in Nucl Q by Th22, A14, A15;
hence x \ y in Cent Q by XBOOLE_0:def 4, A17; :: thesis: verum

end;

for x, y being Element of Q st x in Cent Q & y in Cent Q holds
x / y in Cent Q

proof

let x, y be Element of Q; :: thesis: ( x in Cent Q & y in Cent Q implies x / y in Cent Q )
assume that
A18: x in Cent Q and
A19: y in Cent Q ; :: thesis: x / y in Cent Q
A20: ( x in Comm Q & x in Nucl Q ) by XBOOLE_0:def 4, A18;
A21: ( y in Comm Q & y in Nucl Q ) by XBOOLE_0:def 4, A19;
A22: y in Nucl_m Q by Th12, A21;
for z being Element of Q holds (x / y) * z = z * (x / y)

proof

let z be Element of Q; :: thesis: (x / y) * z = z * (x / y)
thus (x / y) * z = (x / y) * ((z / y) * y)
.= (x / y) * (y * (z / y)) by A21, Def25
.= ((x / y) * y) * (z / y) by A22, Def23
.= (z / y) * ((x / y) * y) by A20, Def25
.= (z / y) * (y * (x / y)) by A21, Def25
.= ((z / y) * y) * (x / y) by A22, Def23
.= z * (x / y) ; :: thesis: verum

end;

then A23: x / y in Comm Q by Def25;
x / y in Nucl Q by Th23, A20, A21;
hence x / y in Cent Q by XBOOLE_0:def 4, A23; :: thesis: verum

end;

hence [#] (lp (Cent Q)) = Cent Q by Th18, A1, A3, A11; :: thesis: verum