let Q be multLoop; :: thesis: ( Q is AIM implies lp (Nucl Q) is normal )
assume A1: Q is AIM ; :: thesis: lp (Nucl Q) is normal
set H = lp (Nucl Q);
A2: for x, y being Element of Q holds
( ex v being Element of Q st
( v in Nucl Q & y = x * v ) iff ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) )

proof

let x, y be Element of Q; :: thesis: ( ex v being Element of Q st
( v in Nucl Q & y = x * v ) iff ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) )
thus ( ex v being Element of Q st
( v in Nucl Q & y = x * v ) 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 ex v being Element of Q st
( v in Nucl Q & y = x * v ) )

proof

given v being Element of Q such that A3: ( v in Nucl Q & y = x * v ) ; :: thesis: ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) )
take 1. Q ; :: thesis: ex v being Element of Q st
( 1. Q in Nucl Q & v in Nucl Q & y = (1. Q) * (x * v) )
take v ; :: thesis: ( 1. Q in Nucl Q & v in Nucl Q & y = (1. Q) * (x * v) )
thus ( 1. Q in Nucl Q & v in Nucl Q & y = (1. Q) * (x * v) ) by A3, Th20; :: thesis: verum

end;

thus ( ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) implies ex v being Element of Q st
( v in Nucl Q & y = x * v ) ) :: thesis: verum

proof

given u, v being Element of Q such that A4: ( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) ; :: thesis: ex v being Element of Q st
( v in Nucl Q & y = x * v )
take (T_map (u,x)) * v ; :: thesis: ( (T_map (u,x)) * v in Nucl Q & y = x * ((T_map (u,x)) * v) )
T_map (u,x) in Nucl Q by A1, Th62, A4;
then ( T_map (u,x) in [#] (lp (Nucl Q)) & v in [#] (lp (Nucl Q)) ) by A4, Th24;
then (T_map (u,x)) * v in [#] (lp (Nucl Q)) by Th37;
hence (T_map (u,x)) * v in Nucl Q by Th24; :: thesis: y = x * ((T_map (u,x)) * v)
A5: v in Nucl_r Q by Th12, A4;
y = (x * (x \ (u * x))) * v by Def24, A5, A4
.= x * ((T_map (u,x)) * v) by Def24, A5 ;
hence y = x * ((T_map (u,x)) * v) ; :: thesis: verum

end;

end;

A6: for x, y being Element of Q holds
( y in x * (lp (Nucl Q)) iff ex v being Element of Q st
( v in Nucl Q & y = x * v ) )

proof

let x, y be Element of Q; :: thesis: ( y in x * (lp (Nucl Q)) iff ex v being Element of Q st
( v in Nucl Q & y = x * v ) )
( 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) ) ) by Th60;
hence ( y in x * (lp (Nucl Q)) iff ex v being Element of Q st
( v in Nucl Q & y = x * v ) ) by A2; :: thesis: verum

end;

A7: for x, y being Element of Q holds
( x * (lp (Nucl Q)) = y * (lp (Nucl Q)) iff ex v being Element of Q st
( v in Nucl Q & y = x * v ) )

proof

let x, y be Element of Q; :: thesis: ( x * (lp (Nucl Q)) = y * (lp (Nucl Q)) iff ex v being Element of Q st
( v in Nucl Q & y = x * v ) )
( x * (lp (Nucl Q)) = y * (lp (Nucl Q)) iff ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) ) by Th61;
hence ( x * (lp (Nucl Q)) = y * (lp (Nucl Q)) iff ex v being Element of Q st
( v in Nucl Q & y = x * v ) ) by A2; :: thesis: verum

end;

A8: for x, y being Element of Q holds (x * (lp (Nucl Q))) * (y * (lp (Nucl Q))) = (x * y) * (lp (Nucl Q))

proof

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

proof

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

proof

assume z in (x * (lp (Nucl Q))) * (y * (lp (Nucl Q))) ; :: thesis: z in (x * y) * (lp (Nucl Q))
then consider x2, y2 being Element of Q such that
A9: ( x2 in x * (lp (Nucl Q)) & y2 in y * (lp (Nucl Q)) & z = x2 * y2 ) by Def42;
ex v being Element of Q st
( v in Nucl Q & z = (x * y) * v )

proof

consider u being Element of Q such that
A10: ( u in Nucl Q & x2 = x * u ) by A6, A9;
consider v being Element of Q such that
A11: ( v in Nucl Q & y2 = y * v ) by A6, A9;
take (T_map (u,y)) * v ; :: thesis: ( (T_map (u,y)) * v in Nucl Q & z = (x * y) * ((T_map (u,y)) * v) )
T_map (u,y) in Nucl Q by A1, Th62, A10;
then ( T_map (u,y) in [#] (lp (Nucl Q)) & v in [#] (lp (Nucl Q)) ) by A11, Th24;
then (T_map (u,y)) * v in [#] (lp (Nucl Q)) by Th37;
hence A12: (T_map (u,y)) * v in Nucl Q by Th24; :: thesis: z = (x * y) * ((T_map (u,y)) * v)
A13: u in Nucl_m Q by Th12, A10;
A14: v in Nucl_r Q by Th12, A11;
A15: (T_map (u,y)) * v in Nucl_r Q by Th12, A12;
z = x * (u * (y * v)) by Def23, A13, A11, A10, A9
.= x * ((y * (T_map (u,y))) * v) by Def24, A14
.= x * (y * ((T_map (u,y)) * v)) by Def24, A14
.= (x * y) * ((T_map (u,y)) * v) by Def24, A15 ;
hence z = (x * y) * ((T_map (u,y)) * v) ; :: thesis: verum

end;

hence z in (x * y) * (lp (Nucl Q)) by A6; :: thesis: verum

end;

assume z in (x * y) * (lp (Nucl Q)) ; :: thesis: z in (x * (lp (Nucl Q))) * (y * (lp (Nucl Q)))
then consider v being Element of Q such that
A16: ( v in Nucl Q & z = (x * y) * v ) by A6;
ex x1, y1 being Element of Q st
( x1 in x * (lp (Nucl Q)) & y1 in y * (lp (Nucl Q)) & z = x1 * y1 )

proof

take x ; :: thesis: ex y1 being Element of Q st
( x in x * (lp (Nucl Q)) & y1 in y * (lp (Nucl Q)) & z = x * y1 )
take y * v ; :: thesis: ( x in x * (lp (Nucl Q)) & y * v in y * (lp (Nucl Q)) & z = x * (y * v) )
A17: ( 1. Q in Nucl Q & x = x * (1. Q) ) by Th20;
v in Nucl_r Q by Th12, A16;
hence ( x in x * (lp (Nucl Q)) & y * v in y * (lp (Nucl Q)) & z = x * (y * v) ) by A17, A16, Def24, A6; :: thesis: verum

end;

hence z in (x * (lp (Nucl Q))) * (y * (lp (Nucl Q))) by Def42; :: thesis: verum

end;

hence (x * (lp (Nucl Q))) * (y * (lp (Nucl Q))) = (x * y) * (lp (Nucl Q)) by SUBSET_1:3; :: thesis: verum

end;

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

proof

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

proof

assume (x * (lp (Nucl Q))) * (y * (lp (Nucl Q))) = (x * (lp (Nucl Q))) * (z * (lp (Nucl Q))) ; :: thesis: y * (lp (Nucl Q)) = z * (lp (Nucl Q))
then (x * y) * (lp (Nucl Q)) = (x * (lp (Nucl Q))) * (z * (lp (Nucl Q))) by A8;
then (x * y) * (lp (Nucl Q)) = (x * z) * (lp (Nucl Q)) by A8;
then consider w being Element of Q such that
A18: ( w in Nucl Q & x * z = (x * y) * w ) by A7;
A19: w in Nucl_r Q by Th12, A18;
x * z = x * (y * w) by A18, Def24, A19;
hence y * (lp (Nucl Q)) = z * (lp (Nucl Q)) by Th1, A7, A18; :: thesis: verum

end;

assume (y * (lp (Nucl Q))) * (x * (lp (Nucl Q))) = (z * (lp (Nucl Q))) * (x * (lp (Nucl Q))) ; :: thesis: y * (lp (Nucl Q)) = z * (lp (Nucl Q))
then (y * x) * (lp (Nucl Q)) = (z * (lp (Nucl Q))) * (x * (lp (Nucl Q))) by A8;
then (y * x) * (lp (Nucl Q)) = (z * x) * (lp (Nucl Q)) by A8;
then consider w being Element of Q such that
A20: ( w in Nucl Q & z * x = (y * x) * w ) by A7;
A21: ( w in Nucl_l Q & w in Nucl_r Q ) by Th12, A20;
set v = (x * w) / x;
A22: (x * w) / x in Nucl Q by A1, Th63, A20;
then A23: (x * w) / x in Nucl_m Q by Th12;
z * x = y * (((x * w) / x) * x) by A20, Def24, A21
.= (y * ((x * w) / x)) * x by Def23, A23 ;
hence y * (lp (Nucl Q)) = z * (lp (Nucl Q)) by Th2, A7, A22; :: thesis: verum

end;

hence lp (Nucl Q) is normal ; :: thesis: verum