let Q be multLoop; :: thesis: for x, y being Element of Q holds
( y in x * (lp (Cent Q)) iff ex z being Element of Q st
( z in Cent Q & y = x * z ) )
let x, y be Element of Q; :: thesis: ( y in x * (lp (Cent Q)) iff ex z being Element of Q st
( z in Cent Q & y = x * z ) )
thus ( y in x * (lp (Cent Q)) implies ex z being Element of Q st
( z in Cent Q & y = x * z ) ) :: thesis: ( ex z being Element of Q st
( z in Cent Q & y = x * z ) implies y in x * (lp (Cent Q)) )
proof
assume y in x * (lp (Cent Q)) ; :: thesis: ex z being Element of Q st
( z in Cent Q & y = x * z )
then y in x * (Cent Q) by Th25;
then consider h being Permutation of Q such that
A1: ( h in Mlt (Cent Q) & h . x = y ) by Def39;
consider z being Element of Q such that
A2: ( z in Cent Q & ( for v being Element of Q holds h . v = v * z ) ) by Th51, A1;
take z ; :: thesis: ( z in Cent Q & y = x * z )
thus ( z in Cent Q & y = x * z ) by A2, A1; :: thesis: verum
end;
given z being Element of Q such that A3: ( z in Cent Q & y = x * z ) ; :: thesis: y in x * (lp (Cent Q))
reconsider h = (curry' the multF of Q) . z as Permutation of Q by Th31;
ex h being Permutation of Q st
( h in Mlt (Cent Q) & h . x = y )
proof
reconsider h = (curry' the multF of Q) . z as Permutation of Q by Th31;
take h ; :: thesis: ( h in Mlt (Cent Q) & h . x = y )
thus ( h in Mlt (Cent Q) & h . x = y ) by FUNCT_5:70, Th33, A3; :: thesis: verum
end;
then y in x * (Cent Q) by Def39;
hence y in x * (lp (Cent Q)) by Th25; :: thesis: verum