let Q be multLoop; 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;
(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;
( 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)) )
( 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)))
;
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;
verum
end;
assume
z in (x * y) * (lp (Cent Q))
;
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 )
hence
z in (x * (lp (Cent Q))) * (y * (lp (Cent Q)))
by Def42;
verum
end;
hence
(x * (lp (Cent Q))) * (y * (lp (Cent Q))) = (x * y) * (lp (Cent Q))
by SUBSET_1:3;
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)) ) ) ) )
hence
lp (Cent Q) is normal
; verum