let Q be multLoop; :: thesis: lp (Cent Q) is normal
set H = lp (Cent Q);
A1: for x, y being Element of Q holds (x * (lp (Cent Q))) * (y * (lp (Cent Q))) = (x * y) * (lp (Cent Q))

proof

let x, y be Element of Q; :: thesis: (x * (lp (Cent Q))) * (y * (lp (Cent Q))) = (x * y) * (lp (Cent Q))
for z being Element of Q holds
( z in (x * (lp (Cent Q))) * (y * (lp (Cent Q))) iff z in (x * y) * (lp (Cent Q)) )

proof

let z be Element of Q; :: thesis: ( z in (x * (lp (Cent Q))) * (y * (lp (Cent Q))) iff z in (x * y) * (lp (Cent Q)) )
thus ( z in (x * (lp (Cent Q))) * (y * (lp (Cent Q))) implies z in (x * y) * (lp (Cent Q)) ) :: thesis: ( z in (x * y) * (lp (Cent Q)) implies z in (x * (lp (Cent Q))) * (y * (lp (Cent Q))) )

proof

assume z in (x * (lp (Cent Q))) * (y * (lp (Cent Q))) ; :: thesis: z in (x * y) * (lp (Cent Q))
then consider v, w being Element of Q such that
A2: ( v in x * (lp (Cent Q)) & w in y * (lp (Cent Q)) & z = v * w ) by Def42;
consider v1 being Element of Q such that
A3: ( v1 in Cent Q & v = x * v1 ) by Th52, A2;
consider w1 being Element of Q such that
A4: ( w1 in Cent Q & w = y * w1 ) by Th52, A2;
( v1 in [#] (lp (Cent Q)) & w1 in [#] (lp (Cent Q)) ) by A3, A4, Th25;
then v1 * w1 in [#] (lp (Cent Q)) by Th37;
then A5: v1 * w1 in Cent Q by Th25;
A6: v1 in Comm Q by A3, XBOOLE_0:def 4;
A7: v1 in Nucl Q by A3, XBOOLE_0:def 4;
A8: ( v1 in Nucl_m Q & v1 in Nucl_r Q ) by A7, Th12;
w1 in Nucl Q by A4, XBOOLE_0:def 4;
then A9: w1 in Nucl_r Q by Th12;
z = ((x * v1) * y) * w1 by Def24, A9, A4, A3, A2
.= (x * (v1 * y)) * w1 by Def23, A8
.= (x * (y * v1)) * w1 by Def25, A6
.= ((x * y) * v1) * w1 by Def24, A8
.= (x * y) * (v1 * w1) by Def24, A9 ;
hence z in (x * y) * (lp (Cent Q)) by Th52, A5; :: thesis: verum

end;

assume z in (x * y) * (lp (Cent Q)) ; :: thesis: z in (x * (lp (Cent Q))) * (y * (lp (Cent Q)))
then consider w being Element of Q such that
A10: ( w in Cent Q & z = (x * y) * w ) by Th52;
w in Nucl Q by A10, XBOOLE_0:def 4;
then A11: w in Nucl_r Q by Th12;
ex u, v being Element of Q st
( u in x * (lp (Cent Q)) & v in y * (lp (Cent Q)) & z = u * v )

proof

take x * (1. Q) ; :: thesis: ex v being Element of Q st
( x * (1. Q) in x * (lp (Cent Q)) & v in y * (lp (Cent Q)) & z = (x * (1. Q)) * v )
take y * w ; :: thesis: ( x * (1. Q) in x * (lp (Cent Q)) & y * w in y * (lp (Cent Q)) & z = (x * (1. Q)) * (y * w) )
thus ( x * (1. Q) in x * (lp (Cent Q)) & y * w in y * (lp (Cent Q)) & z = (x * (1. Q)) * (y * w) ) by Def24, A11, Th52, Th50, A10; :: thesis: verum

end;

hence z in (x * (lp (Cent Q))) * (y * (lp (Cent Q))) by Def42; :: thesis: verum

end;

hence (x * (lp (Cent Q))) * (y * (lp (Cent Q))) = (x * y) * (lp (Cent Q)) by SUBSET_1:3; :: thesis: verum

end;

for x, y being Element of Q holds
( (x * (lp (Cent Q))) * (y * (lp (Cent Q))) = (x * y) * (lp (Cent Q)) & ( for z being Element of Q holds
( ( (x * (lp (Cent Q))) * (y * (lp (Cent Q))) = (x * (lp (Cent Q))) * (z * (lp (Cent Q))) implies y * (lp (Cent Q)) = z * (lp (Cent Q)) ) & ( (y * (lp (Cent Q))) * (x * (lp (Cent Q))) = (z * (lp (Cent Q))) * (x * (lp (Cent Q))) implies y * (lp (Cent Q)) = z * (lp (Cent Q)) ) ) ) )

proof

let x, y be Element of Q; :: thesis: ( (x * (lp (Cent Q))) * (y * (lp (Cent Q))) = (x * y) * (lp (Cent Q)) & ( for z being Element of Q holds
( ( (x * (lp (Cent Q))) * (y * (lp (Cent Q))) = (x * (lp (Cent Q))) * (z * (lp (Cent Q))) implies y * (lp (Cent Q)) = z * (lp (Cent Q)) ) & ( (y * (lp (Cent Q))) * (x * (lp (Cent Q))) = (z * (lp (Cent Q))) * (x * (lp (Cent Q))) implies y * (lp (Cent Q)) = z * (lp (Cent Q)) ) ) ) )
thus (x * (lp (Cent Q))) * (y * (lp (Cent Q))) = (x * y) * (lp (Cent Q)) by A1; :: thesis: for z being Element of Q holds
( ( (x * (lp (Cent Q))) * (y * (lp (Cent Q))) = (x * (lp (Cent Q))) * (z * (lp (Cent Q))) implies y * (lp (Cent Q)) = z * (lp (Cent Q)) ) & ( (y * (lp (Cent Q))) * (x * (lp (Cent Q))) = (z * (lp (Cent Q))) * (x * (lp (Cent Q))) implies y * (lp (Cent Q)) = z * (lp (Cent Q)) ) )
let z be Element of Q; :: thesis: ( ( (x * (lp (Cent Q))) * (y * (lp (Cent Q))) = (x * (lp (Cent Q))) * (z * (lp (Cent Q))) implies y * (lp (Cent Q)) = z * (lp (Cent Q)) ) & ( (y * (lp (Cent Q))) * (x * (lp (Cent Q))) = (z * (lp (Cent Q))) * (x * (lp (Cent Q))) implies y * (lp (Cent Q)) = z * (lp (Cent Q)) ) )
thus ( (x * (lp (Cent Q))) * (y * (lp (Cent Q))) = (x * (lp (Cent Q))) * (z * (lp (Cent Q))) implies y * (lp (Cent Q)) = z * (lp (Cent Q)) ) :: thesis: ( (y * (lp (Cent Q))) * (x * (lp (Cent Q))) = (z * (lp (Cent Q))) * (x * (lp (Cent Q))) implies y * (lp (Cent Q)) = z * (lp (Cent Q)) )

proof

assume (x * (lp (Cent Q))) * (y * (lp (Cent Q))) = (x * (lp (Cent Q))) * (z * (lp (Cent Q))) ; :: thesis: y * (lp (Cent Q)) = z * (lp (Cent Q))
then (x * y) * (lp (Cent Q)) = (x * (lp (Cent Q))) * (z * (lp (Cent Q))) by A1;
then (x * y) * (lp (Cent Q)) = (x * z) * (lp (Cent Q)) by A1;
then consider w being Element of Q such that
A12: ( w in Cent Q & x * z = (x * y) * w ) by Th53;
w in Nucl Q by A12, XBOOLE_0:def 4;
then A13: w in Nucl_r Q by Th12;
x * z = x * (y * w) by A12, Def24, A13;
hence y * (lp (Cent Q)) = z * (lp (Cent Q)) by Th1, Th53, A12; :: thesis: verum

end;

assume (y * (lp (Cent Q))) * (x * (lp (Cent Q))) = (z * (lp (Cent Q))) * (x * (lp (Cent Q))) ; :: thesis: y * (lp (Cent Q)) = z * (lp (Cent Q))
then (y * x) * (lp (Cent Q)) = (z * (lp (Cent Q))) * (x * (lp (Cent Q))) by A1;
then (y * x) * (lp (Cent Q)) = (z * x) * (lp (Cent Q)) by A1;
then consider w being Element of Q such that
A14: ( w in Cent Q & z * x = (y * x) * w ) by Th53;
A15: w in Comm Q by A14, XBOOLE_0:def 4;
w in Nucl Q by A14, XBOOLE_0:def 4;
then A16: w in Nucl_l Q by Th12;
z * x = w * (y * x) by A14, Def25, A15
.= (w * y) * x by Def22, A16 ;
then z = w * y by Th2;
then z = y * w by Def25, A15;
hence y * (lp (Cent Q)) = z * (lp (Cent Q)) by Th53, A14; :: thesis: verum

end;

hence lp (Cent Q) is normal ; :: thesis: verum