assume A1: for Q being multLoop st Q is satisfying_TT & Q is satisfying_TL & Q is satisfying_TR & Q is satisfying_LR & Q is satisfying_LL & Q is satisfying_RR holds
( Q is satisfying_aa1 & Q is satisfying_aa2 & Q is satisfying_aa3 & Q is satisfying_Ka & Q is satisfying_aK1 & Q is satisfying_aK2 & Q is satisfying_aK3 ) ; :: thesis: for Q being AIM multLoop holds
( Q _/_ (lp (Nucl Q)) is commutative multGroup & Q _/_ (lp (Cent Q)) is multGroup )
let Q be AIM multLoop; :: thesis: ( Q _/_ (lp (Nucl Q)) is commutative multGroup & Q _/_ (lp (Cent Q)) is multGroup )
reconsider Q1 = Q as satisfying_aa1 satisfying_aa2 satisfying_aa3 satisfying_Ka satisfying_aK1 satisfying_aK2 satisfying_aK3 multLoop by A1;
set NN = lp (Nucl Q);
set fN = QuotientHom (Q,(lp (Nucl Q)));
A2: for y being Element of (Q _/_ (lp (Nucl Q))) ex x being Element of Q st (QuotientHom (Q,(lp (Nucl Q)))) . x = y
proof
let y be Element of (Q _/_ (lp (Nucl Q))); :: thesis: ex x being Element of Q st (QuotientHom (Q,(lp (Nucl Q)))) . x = y
y in Cosets (lp (Nucl Q)) ;
then consider x being Element of Q such that
A3: y = x * (lp (Nucl Q)) by Def41;
take x ; :: thesis: (QuotientHom (Q,(lp (Nucl Q)))) . x = y
thus (QuotientHom (Q,(lp (Nucl Q)))) . x = y by A3, Def48; :: thesis: verum
end;
Ker (QuotientHom (Q,(lp (Nucl Q)))) = @ ([#] (lp (Nucl Q))) by Th44;
then Nucl Q1 c= Ker (QuotientHom (Q,(lp (Nucl Q)))) by Th24;
hence Q _/_ (lp (Nucl Q)) is commutative multGroup by Th16, A2; :: thesis: Q _/_ (lp (Cent Q)) is multGroup
set NC = lp (Cent Q);
set fC = QuotientHom (Q,(lp (Cent Q)));
A4: for y being Element of (Q _/_ (lp (Cent Q))) ex x being Element of Q st (QuotientHom (Q,(lp (Cent Q)))) . x = y
proof
let y be Element of (Q _/_ (lp (Cent Q))); :: thesis: ex x being Element of Q st (QuotientHom (Q,(lp (Cent Q)))) . x = y
y in Cosets (lp (Cent Q)) ;
then consider x being Element of Q such that
A5: y = x * (lp (Cent Q)) by Def41;
(QuotientHom (Q,(lp (Cent Q)))) . x = y by A5, Def48;
hence ex x being Element of Q st (QuotientHom (Q,(lp (Cent Q)))) . x = y ; :: thesis: verum
end;
Ker (QuotientHom (Q,(lp (Cent Q)))) = @ ([#] (lp (Cent Q))) by Th44;
then Cent Q1 c= Ker (QuotientHom (Q,(lp (Cent Q)))) by Th25;
hence Q _/_ (lp (Cent Q)) is multGroup by Th17, A4; :: thesis: verum