let Q1 be satisfying_aa1 satisfying_aa2 satisfying_aa3 satisfying_Ka multLoop; for Q2 being multLoop
for f being homomorphic Function of Q1,Q2 st ( for y being Element of Q2 ex x being Element of Q1 st f . x = y ) & Cent Q1 c= Ker f holds
Q2 is multGroup
let Q2 be multLoop; for f being homomorphic Function of Q1,Q2 st ( for y being Element of Q2 ex x being Element of Q1 st f . x = y ) & Cent Q1 c= Ker f holds
Q2 is multGroup
let f be homomorphic Function of Q1,Q2; ( ( for y being Element of Q2 ex x being Element of Q1 st f . x = y ) & Cent Q1 c= Ker f implies Q2 is multGroup )
assume that
A1:
for y being Element of Q2 ex x being Element of Q1 st f . x = y
and
A2:
Cent Q1 c= Ker f
; Q2 is multGroup
now for x1, y1, z1 being Element of Q1 holds a_op (x1,y1,z1) in Ker flet x1,
y1,
z1 be
Element of
Q1;
a_op (x1,y1,z1) in Ker f
a_op (
x1,
y1,
z1)
in Cent Q1
proof
now for u being Element of Q1 holds (a_op (x1,y1,z1)) * u = u * (a_op (x1,y1,z1))let u be
Element of
Q1;
(a_op (x1,y1,z1)) * u = u * (a_op (x1,y1,z1))
K_op (
(a_op (x1,y1,z1)),
u)
= 1. Q1
by Def18;
hence
(a_op (x1,y1,z1)) * u = u * (a_op (x1,y1,z1))
by Th10;
verum end;
then A3:
a_op (
x1,
y1,
z1)
in Comm Q1
by Def25;
now for u, w being Element of Q1 holds ((a_op (x1,y1,z1)) * u) * w = (a_op (x1,y1,z1)) * (u * w)let u,
w be
Element of
Q1;
((a_op (x1,y1,z1)) * u) * w = (a_op (x1,y1,z1)) * (u * w)
a_op (
(a_op (x1,y1,z1)),
u,
w)
= 1. Q1
by Def15;
hence
((a_op (x1,y1,z1)) * u) * w = (a_op (x1,y1,z1)) * (u * w)
by Th9;
verum end;
then A4:
a_op (
x1,
y1,
z1)
in Nucl_l Q1
by Def22;
now for u, w being Element of Q1 holds (u * (a_op (x1,y1,z1))) * w = u * ((a_op (x1,y1,z1)) * w)let u,
w be
Element of
Q1;
(u * (a_op (x1,y1,z1))) * w = u * ((a_op (x1,y1,z1)) * w)
a_op (
u,
(a_op (x1,y1,z1)),
w)
= 1. Q1
by Def16;
hence
(u * (a_op (x1,y1,z1))) * w = u * ((a_op (x1,y1,z1)) * w)
by Th9;
verum end;
then A5:
a_op (
x1,
y1,
z1)
in Nucl_m Q1
by Def23;
now for u, w being Element of Q1 holds (u * w) * (a_op (x1,y1,z1)) = u * (w * (a_op (x1,y1,z1)))let u,
w be
Element of
Q1;
(u * w) * (a_op (x1,y1,z1)) = u * (w * (a_op (x1,y1,z1)))
a_op (
u,
w,
(a_op (x1,y1,z1)))
= 1. Q1
by Def17;
hence
(u * w) * (a_op (x1,y1,z1)) = u * (w * (a_op (x1,y1,z1)))
by Th9;
verum end;
then
a_op (
x1,
y1,
z1)
in Nucl_r Q1
by Def24;
then
a_op (
x1,
y1,
z1)
in Nucl Q1
by A4, A5, Th12;
hence
a_op (
x1,
y1,
z1)
in Cent Q1
by A3, XBOOLE_0:def 4;
verum
end; hence
a_op (
x1,
y1,
z1)
in Ker f
by A2;
verum end;
hence
Q2 is multGroup
by Th15, A1; verum