let Q be multLoop; :: thesis: for x, y being Element of Q holds
( y in x * (lp (Nucl Q)) iff ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) )
let x, y be Element of Q; :: thesis: ( y in x * (lp (Nucl Q)) iff ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) )
thus ( y in x * (lp (Nucl Q)) implies ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) ) :: thesis: ( ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) implies y in x * (lp (Nucl Q)) )
proof
assume y in x * (lp (Nucl Q)) ; :: thesis: ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) )
then y in x * (Nucl Q) by Th24;
then consider h being Permutation of the carrier of Q such that
A1: ( h in Mlt (Nucl Q) & h . x = y ) by Def39;
consider u, v being Element of Q such that
A2: ( u in Nucl Q & v in Nucl Q & ( for z being Element of Q holds h . z = u * (z * v) ) ) by Th59, A1;
take u ; :: thesis: ex v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) )
take v ; :: thesis: ( u in Nucl Q & v in Nucl Q & y = u * (x * v) )
thus ( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) by A1, A2; :: thesis: verum
end;
given u, v being Element of Q such that A3: ( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) ; :: thesis: y in x * (lp (Nucl Q))
ex h being Permutation of the carrier of Q st
( h in Mlt (Nucl Q) & h . x = y )
proof
reconsider h = (curry' the multF of Q) . v, k = (curry the multF of Q) . u as Permutation of the carrier of Q by Th31, Th30;
take k * h ; :: thesis: ( k * h in Mlt (Nucl Q) & (k * h) . x = y )
( h in Mlt (Nucl Q) & k in Mlt (Nucl Q) ) by Th33, Th32, A3;
hence k * h in Mlt (Nucl Q) by Def34; :: thesis: (k * h) . x = y
(k * h) . x = k . (h . x) by FUNCT_2:15
.= k . (x * v) by FUNCT_5:70
.= y by A3, FUNCT_5:69 ;
hence (k * h) . x = y ; :: thesis: verum
end;
then y in x * (Nucl Q) by Def39;
hence y in x * (lp (Nucl Q)) by Th24; :: thesis: verum