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

proof

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

proof

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

proof

assume z in (x * (lp (Ker f))) * (y * (lp (Ker f))) ; :: thesis: z in (x * y) * (lp (Ker f))
then consider v, w being Element of Q such that
A2: ( v in x * (lp (Ker f)) & w in y * (lp (Ker f)) & z = v * w ) by Def42;
A3: f . y = f . w by Th47, A2;
f . z = (f . v) * (f . w) by Def28b, A2
.= (f . x) * (f . y) by Th47, A2, A3
.= f . (x * y) by Def28b ;
hence z in (x * y) * (lp (Ker f)) by Th47; :: thesis: verum

end;

assume z in (x * y) * (lp (Ker f)) ; :: thesis: z in (x * (lp (Ker f))) * (y * (lp (Ker f)))
then A4: f . z = f . (x * y) by Th47;
ex v, w being Element of Q st
( v in x * (lp (Ker f)) & w in y * (lp (Ker f)) & z = v * w )

proof

take z / y ; :: thesis: ex w being Element of Q st
( z / y in x * (lp (Ker f)) & w in y * (lp (Ker f)) & z = (z / y) * w )
take y ; :: thesis: ( z / y in x * (lp (Ker f)) & y in y * (lp (Ker f)) & z = (z / y) * y )
A5: f . (z / y) = (f . z) / (f . y) by Th14
.= ((f . x) * (f . y)) / (f . y) by A4, Def28b
.= f . x ;
f . y = f . y ;
hence ( z / y in x * (lp (Ker f)) & y in y * (lp (Ker f)) & z = (z / y) * y ) by A5, Th47; :: thesis: verum

end;

hence z in (x * (lp (Ker f))) * (y * (lp (Ker f))) by Def42; :: thesis: verum

end;

hence (x * (lp (Ker f))) * (y * (lp (Ker f))) = (x * y) * (lp (Ker f)) by SUBSET_1:3; :: thesis: verum

end;

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

proof

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

proof

assume (x * (lp (Ker f))) * (y * (lp (Ker f))) = (x * (lp (Ker f))) * (z * (lp (Ker f))) ; :: thesis: y * (lp (Ker f)) = z * (lp (Ker f))
then (x * y) * (lp (Ker f)) = (x * (lp (Ker f))) * (z * (lp (Ker f))) by A1;
then A6: (x * y) * (lp (Ker f)) = (x * z) * (lp (Ker f)) by A1;
f . y = (f . x) \ ((f . x) * (f . y))
.= (f . x) \ (f . (x * y)) by Def28b
.= (f . x) \ (f . (x * z)) by A6, Th48
.= (f . x) \ ((f . x) * (f . z)) by Def28b
.= f . z ;
hence y * (lp (Ker f)) = z * (lp (Ker f)) by Th48; :: thesis: verum

end;

assume (y * (lp (Ker f))) * (x * (lp (Ker f))) = (z * (lp (Ker f))) * (x * (lp (Ker f))) ; :: thesis: y * (lp (Ker f)) = z * (lp (Ker f))
then (y * x) * (lp (Ker f)) = (z * (lp (Ker f))) * (x * (lp (Ker f))) by A1;
then A7: (y * x) * (lp (Ker f)) = (z * x) * (lp (Ker f)) by A1;
f . y = ((f . y) * (f . x)) / (f . x)
.= (f . (y * x)) / (f . x) by Def28b
.= (f . (z * x)) / (f . x) by A7, Th48
.= ((f . z) * (f . x)) / (f . x) by Def28b
.= f . z ;
hence y * (lp (Ker f)) = z * (lp (Ker f)) by Th48; :: thesis: verum

end;

hence lp (Ker f) is normal ; :: thesis: verum