:: by Chad E. Brown and Karol P\kak

::

:: Received August 29, 2019

:: Copyright (c) 2019-2021 Association of Mizar Users

definition

let X be 1-sorted ;

mode Permutation of X is Permutation of the carrier of X;

let Y be 1-sorted ;

coherence

Funcs ( the carrier of X, the carrier of Y) is set ;

end;
mode Permutation of X is Permutation of the carrier of X;

let Y be 1-sorted ;

coherence

Funcs ( the carrier of X, the carrier of Y) is set ;

:: deftheorem defines Funcs AIMLOOP:def 1 :

for X, Y being 1-sorted holds Funcs (X,Y) = Funcs ( the carrier of X, the carrier of Y);

for X, Y being 1-sorted holds Funcs (X,Y) = Funcs ( the carrier of X, the carrier of Y);

registration
end;

definition

let Q be non empty left_mult-cancelable invertible multLoopStr ;

let x, y be Element of Q;

existence

ex b_{1} being Element of Q st x * b_{1} = y
by ALGSTR_1:def 6;

uniqueness

for b_{1}, b_{2} being Element of Q st x * b_{1} = y & x * b_{2} = y holds

b_{1} = b_{2}
by ALGSTR_0:def 20;

end;
let x, y be Element of Q;

existence

ex b

uniqueness

for b

b

:: deftheorem Def2 defines \ AIMLOOP:def 2 :

for Q being non empty left_mult-cancelable invertible multLoopStr

for x, y, b_{4} being Element of Q holds

( b_{4} = x \ y iff x * b_{4} = y );

for Q being non empty left_mult-cancelable invertible multLoopStr

for x, y, b

( b

definition

let Q be non empty right_mult-cancelable invertible multLoopStr ;

let x, y be Element of Q;

existence

ex b_{1} being Element of Q st b_{1} * y = x
by ALGSTR_1:def 6;

uniqueness

for b_{1}, b_{2} being Element of Q st b_{1} * y = x & b_{2} * y = x holds

b_{1} = b_{2}
by ALGSTR_0:def 21;

end;
let x, y be Element of Q;

existence

ex b

uniqueness

for b

b

:: deftheorem Def3 defines / AIMLOOP:def 3 :

for Q being non empty right_mult-cancelable invertible multLoopStr

for x, y, b_{4} being Element of Q holds

( b_{4} = x / y iff b_{4} * y = x );

for Q being non empty right_mult-cancelable invertible multLoopStr

for x, y, b

( b

registration

let Q be multLoop;

let x, y be Element of Q;

reducibility

x \ (x * y) = y by Def2;

reducibility

x * (x \ y) = y by Def2;

reducibility

(x * y) / y = x by Def3;

reducibility

(x / y) * y = x by Def3;

end;
let x, y be Element of Q;

reducibility

x \ (x * y) = y by Def2;

reducibility

x * (x \ y) = y by Def2;

reducibility

(x * y) / y = x by Def3;

reducibility

(x / y) * y = x by Def3;

definition

let Q be non empty left_mult-cancelable invertible multLoopStr ;

let u, x be Element of Q;

coherence

x \ (u * x) is Element of Q ;

end;
let u, x be Element of Q;

coherence

x \ (u * x) is Element of Q ;

:: deftheorem defines T_map AIMLOOP:def 4 :

for Q being non empty left_mult-cancelable invertible multLoopStr

for u, x being Element of Q holds T_map (u,x) = x \ (u * x);

for Q being non empty left_mult-cancelable invertible multLoopStr

for u, x being Element of Q holds T_map (u,x) = x \ (u * x);

definition

let Q be non empty left_mult-cancelable invertible multLoopStr ;

let u, x, y be Element of Q;

coherence

(y * x) \ (y * (x * u)) is Element of Q ;

end;
let u, x, y be Element of Q;

coherence

(y * x) \ (y * (x * u)) is Element of Q ;

:: deftheorem defines L_map AIMLOOP:def 5 :

for Q being non empty left_mult-cancelable invertible multLoopStr

for u, x, y being Element of Q holds L_map (u,x,y) = (y * x) \ (y * (x * u));

for Q being non empty left_mult-cancelable invertible multLoopStr

for u, x, y being Element of Q holds L_map (u,x,y) = (y * x) \ (y * (x * u));

definition

let Q be non empty right_mult-cancelable invertible multLoopStr ;

let u, x, y be Element of Q;

coherence

((u * x) * y) / (x * y) is Element of Q ;

end;
let u, x, y be Element of Q;

coherence

((u * x) * y) / (x * y) is Element of Q ;

:: deftheorem defines R_map AIMLOOP:def 6 :

for Q being non empty right_mult-cancelable invertible multLoopStr

for u, x, y being Element of Q holds R_map (u,x,y) = ((u * x) * y) / (x * y);

for Q being non empty right_mult-cancelable invertible multLoopStr

for u, x, y being Element of Q holds R_map (u,x,y) = ((u * x) * y) / (x * y);

definition

let Q be multLoop;

end;
attr Q is satisfying_TT means :: AIMLOOP:def 7

for u, x, y being Element of Q holds T_map ((T_map (u,x)),y) = T_map ((T_map (u,y)),x);

for u, x, y being Element of Q holds T_map ((T_map (u,x)),y) = T_map ((T_map (u,y)),x);

attr Q is satisfying_TL means :: AIMLOOP:def 8

for u, x, y, z being Element of Q holds T_map ((L_map (u,x,y)),z) = L_map ((T_map (u,z)),x,y);

for u, x, y, z being Element of Q holds T_map ((L_map (u,x,y)),z) = L_map ((T_map (u,z)),x,y);

attr Q is satisfying_TR means :: AIMLOOP:def 9

for u, x, y, z being Element of Q holds T_map ((R_map (u,x,y)),z) = R_map ((T_map (u,z)),x,y);

for u, x, y, z being Element of Q holds T_map ((R_map (u,x,y)),z) = R_map ((T_map (u,z)),x,y);

attr Q is satisfying_LR means :: AIMLOOP:def 10

for u, x, y, z, w being Element of Q holds L_map ((R_map (u,x,y)),z,w) = R_map ((L_map (u,z,w)),x,y);

for u, x, y, z, w being Element of Q holds L_map ((R_map (u,x,y)),z,w) = R_map ((L_map (u,z,w)),x,y);

attr Q is satisfying_LL means :: AIMLOOP:def 11

for u, x, y, z, w being Element of Q holds L_map ((L_map (u,x,y)),z,w) = L_map ((L_map (u,z,w)),x,y);

for u, x, y, z, w being Element of Q holds L_map ((L_map (u,x,y)),z,w) = L_map ((L_map (u,z,w)),x,y);

attr Q is satisfying_RR means :: AIMLOOP:def 12

for u, x, y, z, w being Element of Q holds R_map ((R_map (u,x,y)),z,w) = R_map ((R_map (u,z,w)),x,y);

for u, x, y, z, w being Element of Q holds R_map ((R_map (u,x,y)),z,w) = R_map ((R_map (u,z,w)),x,y);

:: deftheorem defines satisfying_TT AIMLOOP:def 7 :

for Q being multLoop holds

( Q is satisfying_TT iff for u, x, y being Element of Q holds T_map ((T_map (u,x)),y) = T_map ((T_map (u,y)),x) );

for Q being multLoop holds

( Q is satisfying_TT iff for u, x, y being Element of Q holds T_map ((T_map (u,x)),y) = T_map ((T_map (u,y)),x) );

:: deftheorem defines satisfying_TL AIMLOOP:def 8 :

for Q being multLoop holds

( Q is satisfying_TL iff for u, x, y, z being Element of Q holds T_map ((L_map (u,x,y)),z) = L_map ((T_map (u,z)),x,y) );

for Q being multLoop holds

( Q is satisfying_TL iff for u, x, y, z being Element of Q holds T_map ((L_map (u,x,y)),z) = L_map ((T_map (u,z)),x,y) );

:: deftheorem defines satisfying_TR AIMLOOP:def 9 :

for Q being multLoop holds

( Q is satisfying_TR iff for u, x, y, z being Element of Q holds T_map ((R_map (u,x,y)),z) = R_map ((T_map (u,z)),x,y) );

for Q being multLoop holds

( Q is satisfying_TR iff for u, x, y, z being Element of Q holds T_map ((R_map (u,x,y)),z) = R_map ((T_map (u,z)),x,y) );

:: deftheorem defines satisfying_LR AIMLOOP:def 10 :

for Q being multLoop holds

( Q is satisfying_LR iff for u, x, y, z, w being Element of Q holds L_map ((R_map (u,x,y)),z,w) = R_map ((L_map (u,z,w)),x,y) );

for Q being multLoop holds

( Q is satisfying_LR iff for u, x, y, z, w being Element of Q holds L_map ((R_map (u,x,y)),z,w) = R_map ((L_map (u,z,w)),x,y) );

:: deftheorem defines satisfying_LL AIMLOOP:def 11 :

for Q being multLoop holds

( Q is satisfying_LL iff for u, x, y, z, w being Element of Q holds L_map ((L_map (u,x,y)),z,w) = L_map ((L_map (u,z,w)),x,y) );

for Q being multLoop holds

( Q is satisfying_LL iff for u, x, y, z, w being Element of Q holds L_map ((L_map (u,x,y)),z,w) = L_map ((L_map (u,z,w)),x,y) );

:: deftheorem defines satisfying_RR AIMLOOP:def 12 :

for Q being multLoop holds

( Q is satisfying_RR iff for u, x, y, z, w being Element of Q holds R_map ((R_map (u,x,y)),z,w) = R_map ((R_map (u,z,w)),x,y) );

for Q being multLoop holds

( Q is satisfying_RR iff for u, x, y, z, w being Element of Q holds R_map ((R_map (u,x,y)),z,w) = R_map ((R_map (u,z,w)),x,y) );

definition
end;

:: deftheorem defines K_op AIMLOOP:def 13 :

for Q being multLoop

for x, y being Element of Q holds K_op (x,y) = (y * x) \ (x * y);

for Q being multLoop

for x, y being Element of Q holds K_op (x,y) = (y * x) \ (x * y);

definition

let Q be multLoop;

let x, y, z be Element of Q;

coherence

(x * (y * z)) \ ((x * y) * z) is Element of Q ;

end;
let x, y, z be Element of Q;

coherence

(x * (y * z)) \ ((x * y) * z) is Element of Q ;

:: deftheorem defines a_op AIMLOOP:def 14 :

for Q being multLoop

for x, y, z being Element of Q holds a_op (x,y,z) = (x * (y * z)) \ ((x * y) * z);

for Q being multLoop

for x, y, z being Element of Q holds a_op (x,y,z) = (x * (y * z)) \ ((x * y) * z);

definition

let Q be multLoop;

end;
attr Q is satisfying_aa1 means :Def15: :: AIMLOOP:def 15

for x, y, z, u, w being Element of Q holds a_op ((a_op (x,y,z)),u,w) = 1. Q;

for x, y, z, u, w being Element of Q holds a_op ((a_op (x,y,z)),u,w) = 1. Q;

attr Q is satisfying_aa2 means :Def16: :: AIMLOOP:def 16

for x, y, z, u, w being Element of Q holds a_op (x,(a_op (y,z,u)),w) = 1. Q;

for x, y, z, u, w being Element of Q holds a_op (x,(a_op (y,z,u)),w) = 1. Q;

attr Q is satisfying_aa3 means :Def17: :: AIMLOOP:def 17

for x, y, z, u, w being Element of Q holds a_op (x,y,(a_op (z,u,w))) = 1. Q;

for x, y, z, u, w being Element of Q holds a_op (x,y,(a_op (z,u,w))) = 1. Q;

attr Q is satisfying_Ka means :Def18: :: AIMLOOP:def 18

for x, y, z, u being Element of Q holds K_op ((a_op (x,y,z)),u) = 1. Q;

for x, y, z, u being Element of Q holds K_op ((a_op (x,y,z)),u) = 1. Q;

attr Q is satisfying_aK1 means :Def19: :: AIMLOOP:def 19

for x, y, z, u being Element of Q holds a_op ((K_op (x,y)),z,u) = 1. Q;

for x, y, z, u being Element of Q holds a_op ((K_op (x,y)),z,u) = 1. Q;

attr Q is satisfying_aK2 means :Def20: :: AIMLOOP:def 20

for x, y, z, u being Element of Q holds a_op (x,(K_op (y,z)),u) = 1. Q;

for x, y, z, u being Element of Q holds a_op (x,(K_op (y,z)),u) = 1. Q;

attr Q is satisfying_aK3 means :Def21: :: AIMLOOP:def 21

for x, y, z, u being Element of Q holds a_op (x,y,(K_op (z,u))) = 1. Q;

for x, y, z, u being Element of Q holds a_op (x,y,(K_op (z,u))) = 1. Q;

:: deftheorem Def15 defines satisfying_aa1 AIMLOOP:def 15 :

for Q being multLoop holds

( Q is satisfying_aa1 iff for x, y, z, u, w being Element of Q holds a_op ((a_op (x,y,z)),u,w) = 1. Q );

for Q being multLoop holds

( Q is satisfying_aa1 iff for x, y, z, u, w being Element of Q holds a_op ((a_op (x,y,z)),u,w) = 1. Q );

:: deftheorem Def16 defines satisfying_aa2 AIMLOOP:def 16 :

for Q being multLoop holds

( Q is satisfying_aa2 iff for x, y, z, u, w being Element of Q holds a_op (x,(a_op (y,z,u)),w) = 1. Q );

for Q being multLoop holds

( Q is satisfying_aa2 iff for x, y, z, u, w being Element of Q holds a_op (x,(a_op (y,z,u)),w) = 1. Q );

:: deftheorem Def17 defines satisfying_aa3 AIMLOOP:def 17 :

for Q being multLoop holds

( Q is satisfying_aa3 iff for x, y, z, u, w being Element of Q holds a_op (x,y,(a_op (z,u,w))) = 1. Q );

for Q being multLoop holds

( Q is satisfying_aa3 iff for x, y, z, u, w being Element of Q holds a_op (x,y,(a_op (z,u,w))) = 1. Q );

:: deftheorem Def18 defines satisfying_Ka AIMLOOP:def 18 :

for Q being multLoop holds

( Q is satisfying_Ka iff for x, y, z, u being Element of Q holds K_op ((a_op (x,y,z)),u) = 1. Q );

for Q being multLoop holds

( Q is satisfying_Ka iff for x, y, z, u being Element of Q holds K_op ((a_op (x,y,z)),u) = 1. Q );

:: deftheorem Def19 defines satisfying_aK1 AIMLOOP:def 19 :

for Q being multLoop holds

( Q is satisfying_aK1 iff for x, y, z, u being Element of Q holds a_op ((K_op (x,y)),z,u) = 1. Q );

for Q being multLoop holds

( Q is satisfying_aK1 iff for x, y, z, u being Element of Q holds a_op ((K_op (x,y)),z,u) = 1. Q );

:: deftheorem Def20 defines satisfying_aK2 AIMLOOP:def 20 :

for Q being multLoop holds

( Q is satisfying_aK2 iff for x, y, z, u being Element of Q holds a_op (x,(K_op (y,z)),u) = 1. Q );

for Q being multLoop holds

( Q is satisfying_aK2 iff for x, y, z, u being Element of Q holds a_op (x,(K_op (y,z)),u) = 1. Q );

:: deftheorem Def21 defines satisfying_aK3 AIMLOOP:def 21 :

for Q being multLoop holds

( Q is satisfying_aK3 iff for x, y, z, u being Element of Q holds a_op (x,y,(K_op (z,u))) = 1. Q );

for Q being multLoop holds

( Q is satisfying_aK3 iff for x, y, z, u being Element of Q holds a_op (x,y,(K_op (z,u))) = 1. Q );

registration

ex b_{1} being multLoop st

( b_{1} is strict & b_{1} is satisfying_TT & b_{1} is satisfying_TL & b_{1} is satisfying_TR & b_{1} is satisfying_LR & b_{1} is satisfying_LL & b_{1} is satisfying_RR & b_{1} is satisfying_aa1 & b_{1} is satisfying_aa2 & b_{1} is satisfying_aa3 & b_{1} is satisfying_Ka & b_{1} is satisfying_aK1 & b_{1} is satisfying_aK2 & b_{1} is satisfying_aK3 )
end;

cluster non empty left_mult-cancelable right_mult-cancelable mult-cancelable strict invertible right_unital well-unital left_unital unital satisfying_TT satisfying_TL satisfying_TR satisfying_LR satisfying_LL satisfying_RR satisfying_aa1 satisfying_aa2 satisfying_aa3 satisfying_Ka satisfying_aK1 satisfying_aK2 satisfying_aK3 for multLoopStr ;

existence ex b

( b

proof end;

theorem :: AIMLOOP:3

theorem :: AIMLOOP:4

registration

let Q be multLoop;

let x be Element of Q;

reducibility

(1. Q) \ x = x

x / (1. Q) = x

reducibility

y / (x \ y) = x

(y / x) \ y = x

end;
let x be Element of Q;

reducibility

(1. Q) \ x = x

proof end;

reducibility x / (1. Q) = x

proof end;

let y be Element of Q;reducibility

y / (x \ y) = x

proof end;

reducibility (y / x) \ y = x

proof end;

theorem Th9: :: AIMLOOP:9

for Q being multLoop

for x, y, z being Element of Q st a_op (x,y,z) = 1. Q holds

x * (y * z) = (x * y) * z

for x, y, z being Element of Q st a_op (x,y,z) = 1. Q holds

x * (y * z) = (x * y) * z

proof end;

definition

let Q be multLoop;

defpred S_{1}[ Element of Q] means for y, z being Element of Q holds ($1 * y) * z = $1 * (y * z);

defpred S_{2}[ Element of Q] means for x, z being Element of Q holds (x * $1) * z = x * ($1 * z);

defpred S_{3}[ Element of Q] means for x, y being Element of Q holds (x * y) * $1 = x * (y * $1);

defpred S_{4}[ Element of Q] means for y being Element of Q holds $1 * y = y * $1;

ex b_{1} being Subset of Q st

for x being Element of Q holds

( x in b_{1} iff for y, z being Element of Q holds (x * y) * z = x * (y * z) )

for b_{1}, b_{2} being Subset of Q st ( for x being Element of Q holds

( x in b_{1} iff for y, z being Element of Q holds (x * y) * z = x * (y * z) ) ) & ( for x being Element of Q holds

( x in b_{2} iff for y, z being Element of Q holds (x * y) * z = x * (y * z) ) ) holds

b_{1} = b_{2}

ex b_{1} being Subset of Q st

for y being Element of Q holds

( y in b_{1} iff for x, z being Element of Q holds (x * y) * z = x * (y * z) )

for b_{1}, b_{2} being Subset of Q st ( for y being Element of Q holds

( y in b_{1} iff for x, z being Element of Q holds (x * y) * z = x * (y * z) ) ) & ( for y being Element of Q holds

( y in b_{2} iff for x, z being Element of Q holds (x * y) * z = x * (y * z) ) ) holds

b_{1} = b_{2}

ex b_{1} being Subset of Q st

for z being Element of Q holds

( z in b_{1} iff for x, y being Element of Q holds (x * y) * z = x * (y * z) )

for b_{1}, b_{2} being Subset of Q st ( for z being Element of Q holds

( z in b_{1} iff for x, y being Element of Q holds (x * y) * z = x * (y * z) ) ) & ( for z being Element of Q holds

( z in b_{2} iff for x, y being Element of Q holds (x * y) * z = x * (y * z) ) ) holds

b_{1} = b_{2}

ex b_{1} being Subset of Q st

for x being Element of Q holds

( x in b_{1} iff for y being Element of Q holds x * y = y * x )

for b_{1}, b_{2} being Subset of Q st ( for x being Element of Q holds

( x in b_{1} iff for y being Element of Q holds x * y = y * x ) ) & ( for x being Element of Q holds

( x in b_{2} iff for y being Element of Q holds x * y = y * x ) ) holds

b_{1} = b_{2}

end;
defpred S

defpred S

defpred S

defpred S

func Nucl_l Q -> Subset of Q means :Def22: :: AIMLOOP:def 22

for x being Element of Q holds

( x in it iff for y, z being Element of Q holds (x * y) * z = x * (y * z) );

existence for x being Element of Q holds

( x in it iff for y, z being Element of Q holds (x * y) * z = x * (y * z) );

ex b

for x being Element of Q holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

func Nucl_m Q -> Subset of Q means :Def23: :: AIMLOOP:def 23

for y being Element of Q holds

( y in it iff for x, z being Element of Q holds (x * y) * z = x * (y * z) );

existence for y being Element of Q holds

( y in it iff for x, z being Element of Q holds (x * y) * z = x * (y * z) );

ex b

for y being Element of Q holds

( y in b

proof end;

uniqueness for b

( y in b

( y in b

b

proof end;

func Nucl_r Q -> Subset of Q means :Def24: :: AIMLOOP:def 24

for z being Element of Q holds

( z in it iff for x, y being Element of Q holds (x * y) * z = x * (y * z) );

existence for z being Element of Q holds

( z in it iff for x, y being Element of Q holds (x * y) * z = x * (y * z) );

ex b

for z being Element of Q holds

( z in b

proof end;

uniqueness for b

( z in b

( z in b

b

proof end;

func Comm Q -> Subset of Q means :Def25: :: AIMLOOP:def 25

for x being Element of Q holds

( x in it iff for y being Element of Q holds x * y = y * x );

existence for x being Element of Q holds

( x in it iff for y being Element of Q holds x * y = y * x );

ex b

for x being Element of Q holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def22 defines Nucl_l AIMLOOP:def 22 :

for Q being multLoop

for b_{2} being Subset of Q holds

( b_{2} = Nucl_l Q iff for x being Element of Q holds

( x in b_{2} iff for y, z being Element of Q holds (x * y) * z = x * (y * z) ) );

for Q being multLoop

for b

( b

( x in b

:: deftheorem Def23 defines Nucl_m AIMLOOP:def 23 :

for Q being multLoop

for b_{2} being Subset of Q holds

( b_{2} = Nucl_m Q iff for y being Element of Q holds

( y in b_{2} iff for x, z being Element of Q holds (x * y) * z = x * (y * z) ) );

for Q being multLoop

for b

( b

( y in b

:: deftheorem Def24 defines Nucl_r AIMLOOP:def 24 :

for Q being multLoop

for b_{2} being Subset of Q holds

( b_{2} = Nucl_r Q iff for z being Element of Q holds

( z in b_{2} iff for x, y being Element of Q holds (x * y) * z = x * (y * z) ) );

for Q being multLoop

for b

( b

( z in b

:: deftheorem Def25 defines Comm AIMLOOP:def 25 :

for Q being multLoop

for b_{2} being Subset of Q holds

( b_{2} = Comm Q iff for x being Element of Q holds

( x in b_{2} iff for y being Element of Q holds x * y = y * x ) );

for Q being multLoop

for b

( b

( x in b

definition
end;

:: deftheorem defines Nucl AIMLOOP:def 26 :

for Q being multLoop holds Nucl Q = ((Nucl_l Q) /\ (Nucl_m Q)) /\ (Nucl_r Q);

for Q being multLoop holds Nucl Q = ((Nucl_l Q) /\ (Nucl_m Q)) /\ (Nucl_r Q);

theorem Th12: :: AIMLOOP:12

for Q being multLoop

for x being Element of Q holds

( x in Nucl Q iff ( x in Nucl_l Q & x in Nucl_m Q & x in Nucl_r Q ) )

for x being Element of Q holds

( x in Nucl Q iff ( x in Nucl_l Q & x in Nucl_m Q & x in Nucl_r Q ) )

proof end;

:: deftheorem defines Cent AIMLOOP:def 27 :

for Q being multLoop holds Cent Q = (Comm Q) /\ (Nucl Q);

for Q being multLoop holds Cent Q = (Comm Q) /\ (Nucl Q);

definition

let Q1, Q2 be multLoop;

let f be Function of Q1,Q2;

end;
let f be Function of Q1,Q2;

attr f is quasi-homomorphic means :Def28b: :: AIMLOOP:def 29

for x, y being Element of Q1 holds f . (x * y) = (f . x) * (f . y);

for x, y being Element of Q1 holds f . (x * y) = (f . x) * (f . y);

:: deftheorem Def28a defines unity-preserving AIMLOOP:def 28 :

for Q1, Q2 being multLoop

for f being Function of Q1,Q2 holds

( f is unity-preserving iff f . (1. Q1) = 1. Q2 );

for Q1, Q2 being multLoop

for f being Function of Q1,Q2 holds

( f is unity-preserving iff f . (1. Q1) = 1. Q2 );

:: deftheorem Def28b defines quasi-homomorphic AIMLOOP:def 29 :

for Q1, Q2 being multLoop

for f being Function of Q1,Q2 holds

( f is quasi-homomorphic iff for x, y being Element of Q1 holds f . (x * y) = (f . x) * (f . y) );

for Q1, Q2 being multLoop

for f being Function of Q1,Q2 holds

( f is quasi-homomorphic iff for x, y being Element of Q1 holds f . (x * y) = (f . x) * (f . y) );

:: deftheorem defines homomorphic AIMLOOP:def 30 :

for Q1, Q2 being multLoop

for f being Function of Q1,Q2 holds

( f is homomorphic iff ( f is unity-preserving & f is quasi-homomorphic ) );

for Q1, Q2 being multLoop

for f being Function of Q1,Q2 holds

( f is homomorphic iff ( f is unity-preserving & f is quasi-homomorphic ) );

registration

let Q1, Q2 be multLoop;

for b_{1} being Function of Q1,Q2 st b_{1} is unity-preserving & b_{1} is quasi-homomorphic holds

b_{1} is homomorphic
;

for b_{1} being Function of Q1,Q2 st b_{1} is homomorphic holds

( b_{1} is unity-preserving & b_{1} is quasi-homomorphic )
;

end;
cluster Function-like quasi_total unity-preserving quasi-homomorphic -> homomorphic for Element of bool [: the carrier of Q1, the carrier of Q2:];

coherence for b

b

cluster Function-like quasi_total homomorphic -> unity-preserving quasi-homomorphic for Element of bool [: the carrier of Q1, the carrier of Q2:];

coherence for b

( b

registration

let Q1, Q2 be multLoop;

coherence

for b_{1} being Function of Q1,Q2 st b_{1} = ([#] Q1) --> (1. Q2) holds

b_{1} is homomorphic

end;
coherence

for b

b

proof end;

registration

let Q1, Q2 be multLoop;

ex b_{1} being Function of Q1,Q2 st b_{1} is homomorphic

end;
cluster Relation-like the carrier of Q1 -defined the carrier of Q2 -valued Function-like non empty V14( the carrier of Q1) quasi_total homomorphic for Element of bool [: the carrier of Q1, the carrier of Q2:];

existence ex b

proof end;

definition

let Q, Q2 be multLoop;

let f be homomorphic Function of Q,Q2;

ex b_{1} being Subset of Q st

for x being Element of Q holds

( x in b_{1} iff f . x = 1. Q2 )

for b_{1}, b_{2} being Subset of Q st ( for x being Element of Q holds

( x in b_{1} iff f . x = 1. Q2 ) ) & ( for x being Element of Q holds

( x in b_{2} iff f . x = 1. Q2 ) ) holds

b_{1} = b_{2}

end;
let f be homomorphic Function of Q,Q2;

func Ker f -> Subset of Q means :Def29: :: AIMLOOP:def 31

for x being Element of Q holds

( x in it iff f . x = 1. Q2 );

existence for x being Element of Q holds

( x in it iff f . x = 1. Q2 );

ex b

for x being Element of Q holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def29 defines Ker AIMLOOP:def 31 :

for Q, Q2 being multLoop

for f being homomorphic Function of Q,Q2

for b_{4} being Subset of Q holds

( b_{4} = Ker f iff for x being Element of Q holds

( x in b_{4} iff f . x = 1. Q2 ) );

for Q, Q2 being multLoop

for f being homomorphic Function of Q,Q2

for b

( b

( x in b

theorem Th13: :: AIMLOOP:13

for Q1, Q2 being multLoop

for f being homomorphic Function of Q1,Q2

for x, y being Element of Q1 holds f . (x \ y) = (f . x) \ (f . y)

for f being homomorphic Function of Q1,Q2

for x, y being Element of Q1 holds f . (x \ y) = (f . x) \ (f . y)

proof end;

theorem Th14: :: AIMLOOP:14

for Q1, Q2 being multLoop

for f being homomorphic Function of Q1,Q2

for x, y being Element of Q1 holds f . (x / y) = (f . x) / (f . y)

for f being homomorphic Function of Q1,Q2

for x, y being Element of Q1 holds f . (x / y) = (f . x) / (f . y)

proof end;

theorem Th15: :: AIMLOOP:15

for Q1, Q2 being multLoop

for f being homomorphic Function of Q1,Q2 st ( for y being Element of Q2 ex x being Element of Q1 st f . x = y ) & ( for x, y, z being Element of Q1 holds a_op (x,y,z) in Ker f ) holds

Q2 is associative

for f being homomorphic Function of Q1,Q2 st ( for y being Element of Q2 ex x being Element of Q1 st f . x = y ) & ( for x, y, z being Element of Q1 holds a_op (x,y,z) in Ker f ) holds

Q2 is associative

proof end;

theorem Th16: :: AIMLOOP:16

for Q1 being satisfying_aa1 satisfying_aa2 satisfying_aa3 satisfying_aK1 satisfying_aK2 satisfying_aK3 multLoop

for Q2 being multLoop

for f being homomorphic Function of Q1,Q2 st ( for y being Element of Q2 ex x being Element of Q1 st f . x = y ) & Nucl Q1 c= Ker f holds

Q2 is commutative multGroup

for Q2 being multLoop

for f being homomorphic Function of Q1,Q2 st ( for y being Element of Q2 ex x being Element of Q1 st f . x = y ) & Nucl Q1 c= Ker f holds

Q2 is commutative multGroup

proof end;

theorem Th17: :: AIMLOOP:17

for Q1 being satisfying_aa1 satisfying_aa2 satisfying_aa3 satisfying_Ka multLoop

for Q2 being multLoop

for f being homomorphic Function of Q1,Q2 st ( for y being Element of Q2 ex x being Element of Q1 st f . x = y ) & Cent Q1 c= Ker f holds

Q2 is multGroup

for Q2 being multLoop

for f being homomorphic Function of Q1,Q2 st ( for y being Element of Q2 ex x being Element of Q1 st f . x = y ) & Cent Q1 c= Ker f holds

Q2 is multGroup

proof end;

:: following GROUP_2

definition

let Q be non empty multLoopStr ;

ex b_{1} being non empty multLoopStr st

( the carrier of b_{1} c= the carrier of Q & the multF of b_{1} = the multF of Q || the carrier of b_{1} & the OneF of b_{1} = the OneF of Q )

end;
mode SubLoopStr of Q -> non empty multLoopStr means :Def30: :: AIMLOOP:def 32

( the carrier of it c= the carrier of Q & the multF of it = the multF of Q || the carrier of it & the OneF of it = the OneF of Q );

existence ( the carrier of it c= the carrier of Q & the multF of it = the multF of Q || the carrier of it & the OneF of it = the OneF of Q );

ex b

( the carrier of b

proof end;

:: deftheorem Def30 defines SubLoopStr AIMLOOP:def 32 :

for Q, b_{2} being non empty multLoopStr holds

( b_{2} is SubLoopStr of Q iff ( the carrier of b_{2} c= the carrier of Q & the multF of b_{2} = the multF of Q || the carrier of b_{2} & the OneF of b_{2} = the OneF of Q ) );

for Q, b

( b

registration

let Q be multLoop;

existence

ex b_{1} being SubLoopStr of Q st

( b_{1} is well-unital & b_{1} is invertible & b_{1} is cancelable & not b_{1} is empty & b_{1} is strict )

end;
existence

ex b

( b

proof end;

definition
end;

definition

let Q be non empty multLoopStr ;

let H be SubLoopStr of Q;

let A be Subset of H;

coherence

A is Subset of Q

end;
let H be SubLoopStr of Q;

let A be Subset of H;

coherence

A is Subset of Q

proof end;

:: deftheorem defines @ AIMLOOP:def 33 :

for Q being non empty multLoopStr

for H being SubLoopStr of Q

for A being Subset of H holds @ A = A;

for Q being non empty multLoopStr

for H being SubLoopStr of Q

for A being Subset of H holds @ A = A;

defpred S

( y in $2 & z in $2 & ( $3 = y * z or $3 = y \ z or $3 = y / z ) );

definition

let Q be multLoop;

let H1, H2 be Subset of Q;

ex b_{1} being Subset of Q st

for x being Element of Q holds

( x in b_{1} iff ( x in H1 or x = 1. Q or ex y, z being Element of Q st

( y in H2 & z in H2 & ( x = y * z or x = y \ z or x = y / z ) ) ) )

for b_{1}, b_{2} being Subset of Q st ( for x being Element of Q holds

( x in b_{1} iff ( x in H1 or x = 1. Q or ex y, z being Element of Q st

( y in H2 & z in H2 & ( x = y * z or x = y \ z or x = y / z ) ) ) ) ) & ( for x being Element of Q holds

( x in b_{2} iff ( x in H1 or x = 1. Q or ex y, z being Element of Q st

( y in H2 & z in H2 & ( x = y * z or x = y \ z or x = y / z ) ) ) ) ) holds

b_{1} = b_{2}

end;
let H1, H2 be Subset of Q;

func loopclose1 (H1,H2) -> Subset of Q means :Def32: :: AIMLOOP:def 34

for x being Element of Q holds

( x in it iff ( x in H1 or x = 1. Q or ex y, z being Element of Q st

( y in H2 & z in H2 & ( x = y * z or x = y \ z or x = y / z ) ) ) );

existence for x being Element of Q holds

( x in it iff ( x in H1 or x = 1. Q or ex y, z being Element of Q st

( y in H2 & z in H2 & ( x = y * z or x = y \ z or x = y / z ) ) ) );

ex b

for x being Element of Q holds

( x in b

( y in H2 & z in H2 & ( x = y * z or x = y \ z or x = y / z ) ) ) )

proof end;

uniqueness for b

( x in b

( y in H2 & z in H2 & ( x = y * z or x = y \ z or x = y / z ) ) ) ) ) & ( for x being Element of Q holds

( x in b

( y in H2 & z in H2 & ( x = y * z or x = y \ z or x = y / z ) ) ) ) ) holds

b

proof end;

:: deftheorem Def32 defines loopclose1 AIMLOOP:def 34 :

for Q being multLoop

for H1, H2, b_{4} being Subset of Q holds

( b_{4} = loopclose1 (H1,H2) iff for x being Element of Q holds

( x in b_{4} iff ( x in H1 or x = 1. Q or ex y, z being Element of Q st

( y in H2 & z in H2 & ( x = y * z or x = y \ z or x = y / z ) ) ) ) );

for Q being multLoop

for H1, H2, b

( b

( x in b

( y in H2 & z in H2 & ( x = y * z or x = y \ z or x = y / z ) ) ) ) );

definition

let Q be multLoop;

let H be Subset of Q;

ex b_{1} being strict SubLoop of Q st

( H c= [#] b_{1} & ( for H2 being SubLoop of Q st H c= [#] H2 holds

[#] b_{1} c= [#] H2 ) )

for b_{1}, b_{2} being strict SubLoop of Q st H c= [#] b_{1} & ( for H2 being SubLoop of Q st H c= [#] H2 holds

[#] b_{1} c= [#] H2 ) & H c= [#] b_{2} & ( for H2 being SubLoop of Q st H c= [#] H2 holds

[#] b_{2} c= [#] H2 ) holds

b_{1} = b_{2}

end;
let H be Subset of Q;

func lp H -> strict SubLoop of Q means :Def33: :: AIMLOOP:def 35

( H c= [#] it & ( for H2 being SubLoop of Q st H c= [#] H2 holds

[#] it c= [#] H2 ) );

existence ( H c= [#] it & ( for H2 being SubLoop of Q st H c= [#] H2 holds

[#] it c= [#] H2 ) );

ex b

( H c= [#] b

[#] b

proof end;

uniqueness for b

[#] b

[#] b

b

proof end;

:: deftheorem Def33 defines lp AIMLOOP:def 35 :

for Q being multLoop

for H being Subset of Q

for b_{3} being strict SubLoop of Q holds

( b_{3} = lp H iff ( H c= [#] b_{3} & ( for H2 being SubLoop of Q st H c= [#] H2 holds

[#] b_{3} c= [#] H2 ) ) );

for Q being multLoop

for H being Subset of Q

for b

( b

[#] b

theorem Th18: :: AIMLOOP:18

for Q being multLoop

for H being Subset of Q st 1. Q in H & ( for x, y being Element of Q st x in H & y in H holds

x * y in H ) & ( for x, y being Element of Q st x in H & y in H holds

x \ y in H ) & ( for x, y being Element of Q st x in H & y in H holds

x / y in H ) holds

[#] (lp H) = H

for H being Subset of Q st 1. Q in H & ( for x, y being Element of Q st x in H & y in H holds

x * y in H ) & ( for x, y being Element of Q st x in H & y in H holds

x \ y in H ) & ( for x, y being Element of Q st x in H & y in H holds

x / y in H ) holds

[#] (lp H) = H

proof end;

registration

let Q be multLoop;

coherence

not Nucl_l Q is empty by Th20a;

coherence

not Nucl_m Q is empty by Th20b;

coherence

not Nucl_r Q is empty by Th20c;

coherence

not Nucl Q is empty by Th20;

end;
coherence

not Nucl_l Q is empty by Th20a;

coherence

not Nucl_m Q is empty by Th20b;

coherence

not Nucl_r Q is empty by Th20c;

coherence

not Nucl Q is empty by Th20;

::We now define a set Mlt Q of multiplicative mappings of Q

::and cosets (mostly following Albert 1943 for cosets).

::and cosets (mostly following Albert 1943 for cosets).

definition

let X be functional set ;

end;
attr X is composition-closed means :Def34: :: AIMLOOP:def 36

for f, g being Element of X st f in X & g in X holds

f * g in X;

for f, g being Element of X st f in X & g in X holds

f * g in X;

attr X is inverse-closed means :Def35: :: AIMLOOP:def 37

for f being Element of X st f in X holds

f " in X;

for f being Element of X st f in X holds

f " in X;

:: deftheorem Def34 defines composition-closed AIMLOOP:def 36 :

for X being functional set holds

( X is composition-closed iff for f, g being Element of X st f in X & g in X holds

f * g in X );

for X being functional set holds

( X is composition-closed iff for f, g being Element of X st f in X & g in X holds

f * g in X );

:: deftheorem Def35 defines inverse-closed AIMLOOP:def 37 :

for X being functional set holds

( X is inverse-closed iff for f being Element of X st f in X holds

f " in X );

for X being functional set holds

( X is inverse-closed iff for f being Element of X st f in X holds

f " in X );

registration
end;

registration

existence

ex b_{1} being functional set st

( b_{1} is composition-closed & b_{1} is inverse-closed & not b_{1} is empty )

end;
ex b

( b

proof end;

registration

let Q be multLoopStr ;

existence

ex b_{1} being Subset of (Funcs (Q,Q)) st

( b_{1} is composition-closed & b_{1} is inverse-closed & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

definition
end;

:: deftheorem defines left-right-mult-closed AIMLOOP:def 38 :

for Q being non empty multLoopStr

for H being Subset of Q

for S being Subset of (Funcs (Q,Q)) holds

( H left-right-mult-closed S iff for u being Element of Q st u in H holds

( (curry the multF of Q) . u in S & (curry' the multF of Q) . u in S ) );

for Q being non empty multLoopStr

for H being Subset of Q

for S being Subset of (Funcs (Q,Q)) holds

( H left-right-mult-closed S iff for u being Element of Q st u in H holds

( (curry the multF of Q) . u in S & (curry' the multF of Q) . u in S ) );

defpred S

( u in $2 & $4 = (curry' the multF of $1) . u ) or ex u being Element of $1 st

( u in $2 & $4 = (curry the multF of $1) . u ) or ex g, h being Permutation of $1 st

( g in $3 & h in $3 & $4 = g * h ) or ex g being Permutation of $1 st

( g in $3 & $4 = g " ) );

definition

let Q be non empty multLoopStr ;

let H be Subset of Q;

let S be Subset of (Funcs (Q,Q));

ex b_{1} being Subset of (Funcs (Q,Q)) st

for f being object holds

( f in b_{1} iff ( ex u being Element of Q st

( u in H & f = (curry' the multF of Q) . u ) or ex u being Element of Q st

( u in H & f = (curry the multF of Q) . u ) or ex g, h being Permutation of Q st

( g in S & h in S & f = g * h ) or ex g being Permutation of Q st

( g in S & f = g " ) ) )

for b_{1}, b_{2} being Subset of (Funcs (Q,Q)) st ( for f being object holds

( f in b_{1} iff ( ex u being Element of Q st

( u in H & f = (curry' the multF of Q) . u ) or ex u being Element of Q st

( u in H & f = (curry the multF of Q) . u ) or ex g, h being Permutation of Q st

( g in S & h in S & f = g * h ) or ex g being Permutation of Q st

( g in S & f = g " ) ) ) ) & ( for f being object holds

( f in b_{2} iff ( ex u being Element of Q st

( u in H & f = (curry' the multF of Q) . u ) or ex u being Element of Q st

( u in H & f = (curry the multF of Q) . u ) or ex g, h being Permutation of Q st

( g in S & h in S & f = g * h ) or ex g being Permutation of Q st

( g in S & f = g " ) ) ) ) holds

b_{1} = b_{2}

end;
let H be Subset of Q;

let S be Subset of (Funcs (Q,Q));

func MltClos1 (H,S) -> Subset of (Funcs (Q,Q)) means :Def37: :: AIMLOOP:def 39

for f being object holds

( f in it iff ( ex u being Element of Q st

( u in H & f = (curry' the multF of Q) . u ) or ex u being Element of Q st

( u in H & f = (curry the multF of Q) . u ) or ex g, h being Permutation of Q st

( g in S & h in S & f = g * h ) or ex g being Permutation of Q st

( g in S & f = g " ) ) );

existence for f being object holds

( f in it iff ( ex u being Element of Q st

( u in H & f = (curry' the multF of Q) . u ) or ex u being Element of Q st

( u in H & f = (curry the multF of Q) . u ) or ex g, h being Permutation of Q st

( g in S & h in S & f = g * h ) or ex g being Permutation of Q st

( g in S & f = g " ) ) );

ex b

for f being object holds

( f in b

( u in H & f = (curry' the multF of Q) . u ) or ex u being Element of Q st

( u in H & f = (curry the multF of Q) . u ) or ex g, h being Permutation of Q st

( g in S & h in S & f = g * h ) or ex g being Permutation of Q st

( g in S & f = g " ) ) )

proof end;

uniqueness for b

( f in b

( u in H & f = (curry' the multF of Q) . u ) or ex u being Element of Q st

( u in H & f = (curry the multF of Q) . u ) or ex g, h being Permutation of Q st

( g in S & h in S & f = g * h ) or ex g being Permutation of Q st

( g in S & f = g " ) ) ) ) & ( for f being object holds

( f in b

( u in H & f = (curry' the multF of Q) . u ) or ex u being Element of Q st

( u in H & f = (curry the multF of Q) . u ) or ex g, h being Permutation of Q st

( g in S & h in S & f = g * h ) or ex g being Permutation of Q st

( g in S & f = g " ) ) ) ) holds

b

proof end;

:: deftheorem Def37 defines MltClos1 AIMLOOP:def 39 :

for Q being non empty multLoopStr

for H being Subset of Q

for S, b_{4} being Subset of (Funcs (Q,Q)) holds

( b_{4} = MltClos1 (H,S) iff for f being object holds

( f in b_{4} iff ( ex u being Element of Q st

( u in H & f = (curry' the multF of Q) . u ) or ex u being Element of Q st

( u in H & f = (curry the multF of Q) . u ) or ex g, h being Permutation of Q st

( g in S & h in S & f = g * h ) or ex g being Permutation of Q st

( g in S & f = g " ) ) ) );

for Q being non empty multLoopStr

for H being Subset of Q

for S, b

( b

( f in b

( u in H & f = (curry' the multF of Q) . u ) or ex u being Element of Q st

( u in H & f = (curry the multF of Q) . u ) or ex g, h being Permutation of Q st

( g in S & h in S & f = g * h ) or ex g being Permutation of Q st

( g in S & f = g " ) ) ) );

theorem Th26: :: AIMLOOP:29

for Q being multLoop

for H being Subset of Q

for phi being Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) st ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) holds

phi is V278()

for H being Subset of Q

for phi being Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) st ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) holds

phi is V278()

proof end;

theorem Th27: :: AIMLOOP:30

for Q being multLoop

for H being Subset of Q

for phi being Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) st ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) holds

for Y being Subset of (Funcs (Q,Q)) st phi . Y c= Y holds

( ( for u being Element of Q st u in H holds

(curry the multF of Q) . u in Y ) & ( for u being Element of Q st u in H holds

(curry' the multF of Q) . u in Y ) )

for H being Subset of Q

for phi being Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) st ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) holds

for Y being Subset of (Funcs (Q,Q)) st phi . Y c= Y holds

( ( for u being Element of Q st u in H holds

(curry the multF of Q) . u in Y ) & ( for u being Element of Q st u in H holds

(curry' the multF of Q) . u in Y ) )

proof end;

theorem Th28: :: AIMLOOP:31

for Q being multLoop

for H being Subset of Q

for phi being Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) st ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) holds

for Y being Subset of (Funcs (Q,Q)) st ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds

Y c= S ) holds

for f being Element of Funcs (Q,Q) st f in Y holds

f is Permutation of Q

for H being Subset of Q

for phi being Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) st ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) holds

for Y being Subset of (Funcs (Q,Q)) st ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds

Y c= S ) holds

for f being Element of Funcs (Q,Q) st f in Y holds

f is Permutation of Q

proof end;

theorem Th29: :: AIMLOOP:32

for Q being multLoop

for H being Subset of Q

for phi being Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) st ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) holds

for Y being Subset of (Funcs (Q,Q)) st Y is_a_fixpoint_of phi & ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds

Y c= S ) holds

( Y is composition-closed & Y is inverse-closed )

for H being Subset of Q

for phi being Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) st ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) holds

for Y being Subset of (Funcs (Q,Q)) st Y is_a_fixpoint_of phi & ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds

Y c= S ) holds

( Y is composition-closed & Y is inverse-closed )

proof end;

theorem Th31: :: AIMLOOP:34

for Q being multLoop

for u being Element of Q holds (curry' the multF of Q) . u is Permutation of the carrier of Q

for u being Element of Q holds (curry' the multF of Q) . u is Permutation of the carrier of Q

proof end;

definition

let Q be multLoop;

let H be Subset of Q;

ex b_{1} being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st

( H left-right-mult-closed b_{1} & ( for X being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed X holds

b_{1} c= X ) )

for b_{1}, b_{2} being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed b_{1} & ( for X being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed X holds

b_{1} c= X ) & H left-right-mult-closed b_{2} & ( for X being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed X holds

b_{2} c= X ) holds

b_{1} = b_{2}
;

end;
let H be Subset of Q;

func Mlt H -> composition-closed inverse-closed Subset of (Funcs (Q,Q)) means :Def38: :: AIMLOOP:def 40

( H left-right-mult-closed it & ( for X being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed X holds

it c= X ) );

existence ( H left-right-mult-closed it & ( for X being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed X holds

it c= X ) );

ex b

( H left-right-mult-closed b

b

proof end;

uniqueness for b

b

b

b

:: deftheorem Def38 defines Mlt AIMLOOP:def 40 :

for Q being multLoop

for H being Subset of Q

for b_{3} being composition-closed inverse-closed Subset of (Funcs (Q,Q)) holds

( b_{3} = Mlt H iff ( H left-right-mult-closed b_{3} & ( for X being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed X holds

b_{3} c= X ) ) );

for Q being multLoop

for H being Subset of Q

for b

( b

b

theorem Th32: :: AIMLOOP:35

for Q being multLoop

for H being Subset of Q

for u being Element of Q st u in H holds

(curry the multF of Q) . u in Mlt H

for H being Subset of Q

for u being Element of Q st u in H holds

(curry the multF of Q) . u in Mlt H

proof end;

theorem Th33: :: AIMLOOP:36

for Q being multLoop

for H being Subset of Q

for u being Element of Q st u in H holds

(curry' the multF of Q) . u in Mlt H

for H being Subset of Q

for u being Element of Q st u in H holds

(curry' the multF of Q) . u in Mlt H

proof end;

theorem Th34: :: AIMLOOP:37

for Q being multLoop

for H being Subset of Q

for phi being Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) st ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) holds

( Mlt H is_a_fixpoint_of phi & ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds

Mlt H c= S ) )

for H being Subset of Q

for phi being Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) st ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) holds

( Mlt H is_a_fixpoint_of phi & ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds

Mlt H c= S ) )

proof end;

theorem Th35: :: AIMLOOP:38

for Q being multLoop

for H being Subset of Q

for f being Element of Funcs (Q,Q) st f in Mlt H holds

f is Permutation of Q

for H being Subset of Q

for f being Element of Funcs (Q,Q) st f in Mlt H holds

f is Permutation of Q

proof end;

definition

let Q be multLoop;

let H be Subset of Q;

let x be Element of Q;

ex b_{1} being Subset of Q st

for y being Element of Q holds

( y in b_{1} iff ex h being Permutation of Q st

( h in Mlt H & y = h . x ) )

for b_{1}, b_{2} being Subset of Q st ( for y being Element of Q holds

( y in b_{1} iff ex h being Permutation of Q st

( h in Mlt H & y = h . x ) ) ) & ( for y being Element of Q holds

( y in b_{2} iff ex h being Permutation of Q st

( h in Mlt H & y = h . x ) ) ) holds

b_{1} = b_{2}

end;
let H be Subset of Q;

let x be Element of Q;

func x * H -> Subset of Q means :Def39: :: AIMLOOP:def 41

for y being Element of Q holds

( y in it iff ex h being Permutation of Q st

( h in Mlt H & y = h . x ) );

existence for y being Element of Q holds

( y in it iff ex h being Permutation of Q st

( h in Mlt H & y = h . x ) );

ex b

for y being Element of Q holds

( y in b

( h in Mlt H & y = h . x ) )

proof end;

uniqueness for b

( y in b

( h in Mlt H & y = h . x ) ) ) & ( for y being Element of Q holds

( y in b

( h in Mlt H & y = h . x ) ) ) holds

b

proof end;

:: deftheorem Def39 defines * AIMLOOP:def 41 :

for Q being multLoop

for H being Subset of Q

for x being Element of Q

for b_{4} being Subset of Q holds

( b_{4} = x * H iff for y being Element of Q holds

( y in b_{4} iff ex h being Permutation of Q st

( h in Mlt H & y = h . x ) ) );

for Q being multLoop

for H being Subset of Q

for x being Element of Q

for b

( b

( y in b

( h in Mlt H & y = h . x ) ) );

definition

let Q be multLoop;

let H be SubLoop of Q;

let x be Element of Q;

coherence

x * (@ ([#] H)) is Subset of Q ;

end;
let H be SubLoop of Q;

let x be Element of Q;

coherence

x * (@ ([#] H)) is Subset of Q ;

:: deftheorem defines * AIMLOOP:def 42 :

for Q being multLoop

for H being SubLoop of Q

for x being Element of Q holds x * H = x * (@ ([#] H));

for Q being multLoop

for H being SubLoop of Q

for x being Element of Q holds x * H = x * (@ ([#] H));

definition

let Q be multLoop;

let N be SubLoop of Q;

ex b_{1} being Subset-Family of Q st

for H being Subset of Q holds

( H in b_{1} iff ex x being Element of Q st H = x * N )

for b_{1}, b_{2} being Subset-Family of Q st ( for H being Subset of Q holds

( H in b_{1} iff ex x being Element of Q st H = x * N ) ) & ( for H being Subset of Q holds

( H in b_{2} iff ex x being Element of Q st H = x * N ) ) holds

b_{1} = b_{2}

end;
let N be SubLoop of Q;

func Cosets N -> Subset-Family of Q means :Def41: :: AIMLOOP:def 43

for H being Subset of Q holds

( H in it iff ex x being Element of Q st H = x * N );

existence for H being Subset of Q holds

( H in it iff ex x being Element of Q st H = x * N );

ex b

for H being Subset of Q holds

( H in b

proof end;

uniqueness for b

( H in b

( H in b

b

proof end;

:: deftheorem Def41 defines Cosets AIMLOOP:def 43 :

for Q being multLoop

for N being SubLoop of Q

for b_{3} being Subset-Family of Q holds

( b_{3} = Cosets N iff for H being Subset of Q holds

( H in b_{3} iff ex x being Element of Q st H = x * N ) );

for Q being multLoop

for N being SubLoop of Q

for b

( b

( H in b

registration
end;

::We define the notion of a normal subloop

::and construct quotients by normal subloops.

::and construct quotients by normal subloops.

definition

let Q be multLoopStr ;

let H1, H2 be Subset of Q;

ex b_{1} being Subset of Q st

for x being Element of Q holds

( x in b_{1} iff ex y, z being Element of Q st

( y in H1 & z in H2 & x = y * z ) )

for b_{1}, b_{2} being Subset of Q st ( for x being Element of Q holds

( x in b_{1} iff ex y, z being Element of Q st

( y in H1 & z in H2 & x = y * z ) ) ) & ( for x being Element of Q holds

( x in b_{2} iff ex y, z being Element of Q st

( y in H1 & z in H2 & x = y * z ) ) ) holds

b_{1} = b_{2}

ex b_{1} being Subset of Q st

for x being Element of Q holds

( x in b_{1} iff ex y, z being Element of Q st

( y in H1 & z in H2 & x = y \ z ) )

for b_{1}, b_{2} being Subset of Q st ( for x being Element of Q holds

( x in b_{1} iff ex y, z being Element of Q st

( y in H1 & z in H2 & x = y \ z ) ) ) & ( for x being Element of Q holds

( x in b_{2} iff ex y, z being Element of Q st

( y in H1 & z in H2 & x = y \ z ) ) ) holds

b_{1} = b_{2}

end;
let H1, H2 be Subset of Q;

func H1 * H2 -> Subset of Q means :Def42: :: AIMLOOP:def 44

for x being Element of Q holds

( x in it iff ex y, z being Element of Q st

( y in H1 & z in H2 & x = y * z ) );

existence for x being Element of Q holds

( x in it iff ex y, z being Element of Q st

( y in H1 & z in H2 & x = y * z ) );

ex b

for x being Element of Q holds

( x in b

( y in H1 & z in H2 & x = y * z ) )

proof end;

uniqueness for b

( x in b

( y in H1 & z in H2 & x = y * z ) ) ) & ( for x being Element of Q holds

( x in b

( y in H1 & z in H2 & x = y * z ) ) ) holds

b

proof end;

func H1 \ H2 -> Subset of Q means :: AIMLOOP:def 45

for x being Element of Q holds

( x in it iff ex y, z being Element of Q st

( y in H1 & z in H2 & x = y \ z ) );

existence for x being Element of Q holds

( x in it iff ex y, z being Element of Q st

( y in H1 & z in H2 & x = y \ z ) );

ex b

for x being Element of Q holds

( x in b

( y in H1 & z in H2 & x = y \ z ) )

proof end;

uniqueness for b

( x in b

( y in H1 & z in H2 & x = y \ z ) ) ) & ( for x being Element of Q holds

( x in b

( y in H1 & z in H2 & x = y \ z ) ) ) holds

b

proof end;

:: deftheorem Def42 defines * AIMLOOP:def 44 :

for Q being multLoopStr

for H1, H2, b_{4} being Subset of Q holds

( b_{4} = H1 * H2 iff for x being Element of Q holds

( x in b_{4} iff ex y, z being Element of Q st

( y in H1 & z in H2 & x = y * z ) ) );

for Q being multLoopStr

for H1, H2, b

( b

( x in b

( y in H1 & z in H2 & x = y * z ) ) );

:: deftheorem defines \ AIMLOOP:def 45 :

for Q being multLoopStr

for H1, H2, b_{4} being Subset of Q holds

( b_{4} = H1 \ H2 iff for x being Element of Q holds

( x in b_{4} iff ex y, z being Element of Q st

( y in H1 & z in H2 & x = y \ z ) ) );

for Q being multLoopStr

for H1, H2, b

( b

( x in b

( y in H1 & z in H2 & x = y \ z ) ) );

:: deftheorem Def44 defines normal AIMLOOP:def 46 :

for Q being multLoop

for H being SubLoop of Q holds

( H is normal iff for x, y being Element of Q holds

( (x * H) * (y * H) = (x * y) * H & ( for z being Element of Q holds

( ( (x * H) * (y * H) = (x * H) * (z * H) implies y * H = z * H ) & ( (y * H) * (x * H) = (z * H) * (x * H) implies y * H = z * H ) ) ) ) );

for Q being multLoop

for H being SubLoop of Q holds

( H is normal iff for x, y being Element of Q holds

( (x * H) * (y * H) = (x * y) * H & ( for z being Element of Q holds

( ( (x * H) * (y * H) = (x * H) * (z * H) implies y * H = z * H ) & ( (y * H) * (x * H) = (z * H) * (x * H) implies y * H = z * H ) ) ) ) );

registration

let Q be multLoop;

ex b_{1} being SubLoop of Q st b_{1} is normal

end;
cluster non empty left_mult-cancelable right_mult-cancelable mult-cancelable invertible right_unital well-unital left_unital unital normal for SubLoopStr of Q;

existence ex b

proof end;

definition

let Q be multLoop;

let N be normal SubLoop of Q;

coherence

(1. Q) * N is Element of Cosets N by Def41;

end;
let N be normal SubLoop of Q;

coherence

(1. Q) * N is Element of Cosets N by Def41;

:: deftheorem defines SubLoop_As_Coset AIMLOOP:def 47 :

for Q being multLoop

for N being normal SubLoop of Q holds SubLoop_As_Coset N = (1. Q) * N;

for Q being multLoop

for N being normal SubLoop of Q holds SubLoop_As_Coset N = (1. Q) * N;

definition

let Q be multLoop;

let N be normal SubLoop of Q;

ex b_{1} being BinOp of (Cosets N) st

for H1, H2 being Element of Cosets N holds b_{1} . (H1,H2) = H1 * H2

for b_{1}, b_{2} being BinOp of (Cosets N) st ( for H1, H2 being Element of Cosets N holds b_{1} . (H1,H2) = H1 * H2 ) & ( for H1, H2 being Element of Cosets N holds b_{2} . (H1,H2) = H1 * H2 ) holds

b_{1} = b_{2}

end;
let N be normal SubLoop of Q;

func Coset_Loop_Op N -> BinOp of (Cosets N) means :Def46: :: AIMLOOP:def 48

for H1, H2 being Element of Cosets N holds it . (H1,H2) = H1 * H2;

existence for H1, H2 being Element of Cosets N holds it . (H1,H2) = H1 * H2;

ex b

for H1, H2 being Element of Cosets N holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def46 defines Coset_Loop_Op AIMLOOP:def 48 :

for Q being multLoop

for N being normal SubLoop of Q

for b_{3} being BinOp of (Cosets N) holds

( b_{3} = Coset_Loop_Op N iff for H1, H2 being Element of Cosets N holds b_{3} . (H1,H2) = H1 * H2 );

for Q being multLoop

for N being normal SubLoop of Q

for b

( b

definition

let Q be multLoop;

let N be normal SubLoop of Q;

multLoopStr(# (Cosets N),(Coset_Loop_Op N),(SubLoop_As_Coset N) #) is strict multLoopStr ;

end;
let N be normal SubLoop of Q;

func Q _/_ N -> strict multLoopStr equals :: AIMLOOP:def 49

multLoopStr(# (Cosets N),(Coset_Loop_Op N),(SubLoop_As_Coset N) #);

coherence multLoopStr(# (Cosets N),(Coset_Loop_Op N),(SubLoop_As_Coset N) #);

multLoopStr(# (Cosets N),(Coset_Loop_Op N),(SubLoop_As_Coset N) #) is strict multLoopStr ;

:: deftheorem defines _/_ AIMLOOP:def 49 :

for Q being multLoop

for N being normal SubLoop of Q holds Q _/_ N = multLoopStr(# (Cosets N),(Coset_Loop_Op N),(SubLoop_As_Coset N) #);

for Q being multLoop

for N being normal SubLoop of Q holds Q _/_ N = multLoopStr(# (Cosets N),(Coset_Loop_Op N),(SubLoop_As_Coset N) #);

registration

let Q be multLoop;

let N be normal SubLoop of Q;

coherence

( Q _/_ N is well-unital & Q _/_ N is invertible & Q _/_ N is mult-cancelable )

end;
let N be normal SubLoop of Q;

coherence

( Q _/_ N is well-unital & Q _/_ N is invertible & Q _/_ N is mult-cancelable )

proof end;

definition

let Q be multLoop;

let N be normal SubLoop of Q;

ex b_{1} being Function of Q,(Q _/_ N) st

for x being Element of Q holds b_{1} . x = x * N

for b_{1}, b_{2} being Function of Q,(Q _/_ N) st ( for x being Element of Q holds b_{1} . x = x * N ) & ( for x being Element of Q holds b_{2} . x = x * N ) holds

b_{1} = b_{2}

end;
let N be normal SubLoop of Q;

func QuotientHom (Q,N) -> Function of Q,(Q _/_ N) means :Def48: :: AIMLOOP:def 50

for x being Element of Q holds it . x = x * N;

existence for x being Element of Q holds it . x = x * N;

ex b

for x being Element of Q holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def48 defines QuotientHom AIMLOOP:def 50 :

for Q being multLoop

for N being normal SubLoop of Q

for b_{3} being Function of Q,(Q _/_ N) holds

( b_{3} = QuotientHom (Q,N) iff for x being Element of Q holds b_{3} . x = x * N );

for Q being multLoop

for N being normal SubLoop of Q

for b

( b

registration

let Q be multLoop;

let N be normal SubLoop of Q;

coherence

QuotientHom (Q,N) is homomorphic

end;
let N be normal SubLoop of Q;

coherence

QuotientHom (Q,N) is homomorphic

proof end;

theorem Th36: :: AIMLOOP:39

for Q being multLoop

for H being SubLoop of Q

for x, y being Element of Q

for x1, y1 being Element of H st x = x1 & y = y1 holds

x * y = x1 * y1

for H being SubLoop of Q

for x, y being Element of Q

for x1, y1 being Element of H st x = x1 & y = y1 holds

x * y = x1 * y1

proof end;

theorem Th37: :: AIMLOOP:40

for Q being multLoop

for H being SubLoop of Q

for x, y being Element of Q st x in the carrier of H & y in the carrier of H holds

x * y in the carrier of H

for H being SubLoop of Q

for x, y being Element of Q st x in the carrier of H & y in the carrier of H holds

x * y in the carrier of H

proof end;

theorem Th38: :: AIMLOOP:41

for Q being multLoop

for H being SubLoop of Q

for x, y being Element of Q

for x1, y1 being Element of H st x = x1 & y = y1 holds

x \ y = x1 \ y1

for H being SubLoop of Q

for x, y being Element of Q

for x1, y1 being Element of H st x = x1 & y = y1 holds

x \ y = x1 \ y1

proof end;

theorem Th39: :: AIMLOOP:42

for Q being multLoop

for H being SubLoop of Q

for x, y being Element of Q st x in the carrier of H & y in the carrier of H holds

x \ y in the carrier of H

for H being SubLoop of Q

for x, y being Element of Q st x in the carrier of H & y in the carrier of H holds

x \ y in the carrier of H

proof end;

theorem Th40: :: AIMLOOP:43

for Q being multLoop

for H being SubLoop of Q

for x, y being Element of Q

for x1, y1 being Element of H st x = x1 & y = y1 holds

x / y = x1 / y1

for H being SubLoop of Q

for x, y being Element of Q

for x1, y1 being Element of H st x = x1 & y = y1 holds

x / y = x1 / y1

proof end;

theorem Th41: :: AIMLOOP:44

for Q being multLoop

for H being SubLoop of Q

for x, y being Element of Q st x in the carrier of H & y in the carrier of H holds

x / y in the carrier of H

for H being SubLoop of Q

for x, y being Element of Q st x in the carrier of H & y in the carrier of H holds

x / y in the carrier of H

proof end;

scheme :: AIMLOOP:sch 1

MltInd{ F_{1}() -> multLoop, F_{2}() -> Subset of F_{1}(), P_{1}[ Function of F_{1}(),F_{1}()] } :

provided

MltInd{ F

provided

A1:
for u being Element of F_{1}() st u in F_{2}() holds

for f being Function of F_{1}(),F_{1}() st ( for x being Element of F_{1}() holds f . x = x * u ) holds

P_{1}[f]
and

A2: for u being Element of F_{1}() st u in F_{2}() holds

for f being Function of F_{1}(),F_{1}() st ( for x being Element of F_{1}() holds f . x = u * x ) holds

P_{1}[f]
and

A3: for g, h being Permutation of F_{1}() st P_{1}[g] & P_{1}[h] holds

P_{1}[g * h]
and

A4: for g being Permutation of F_{1}() st P_{1}[g] holds

P_{1}[g " ]

for f being Function of F

P

A2: for u being Element of F

for f being Function of F

P

A3: for g, h being Permutation of F

P

A4: for g being Permutation of F

P

proof end;

theorem Th42: :: AIMLOOP:45

for Q being multLoop

for N being SubLoop of Q

for f being Function of Q,Q st f in Mlt (@ ([#] N)) holds

for x being Element of Q holds

( x in @ ([#] N) iff f . x in @ ([#] N) )

for N being SubLoop of Q

for f being Function of Q,Q st f in Mlt (@ ([#] N)) holds

for x being Element of Q holds

( x in @ ([#] N) iff f . x in @ ([#] N) )

proof end;

theorem Th45: :: AIMLOOP:48

for Q, Q2 being multLoop

for f being homomorphic Function of Q,Q2

for h being Function of Q,Q st h in Mlt (Ker f) holds

f * h = f

for f being homomorphic Function of Q,Q2

for h being Function of Q,Q st h in Mlt (Ker f) holds

f * h = f

proof end;

theorem Th46: :: AIMLOOP:49

for Q, Q2 being multLoop

for f being homomorphic Function of Q,Q2

for x, y being Element of Q holds

( y in x * (Ker f) iff f . x = f . y )

for f being homomorphic Function of Q,Q2

for x, y being Element of Q holds

( y in x * (Ker f) iff f . x = f . y )

proof end;

theorem Th47: :: AIMLOOP:50

for Q, Q2 being multLoop

for f being homomorphic Function of Q,Q2

for x, y being Element of Q holds

( y in x * (lp (Ker f)) iff f . x = f . y )

for f being homomorphic Function of Q,Q2

for x, y being Element of Q holds

( y in x * (lp (Ker f)) iff f . x = f . y )

proof end;

theorem Th48: :: AIMLOOP:51

for Q, Q2 being multLoop

for f being homomorphic Function of Q,Q2

for x, y being Element of Q holds

( x * (lp (Ker f)) = y * (lp (Ker f)) iff f . x = f . y )

for f being homomorphic Function of Q,Q2

for x, y being Element of Q holds

( x * (lp (Ker f)) = y * (lp (Ker f)) iff f . x = f . y )

proof end;

theorem Th51: :: AIMLOOP:54

for Q being multLoop

for f being Function of Q,Q st f in Mlt (Cent Q) holds

ex z being Element of Q st

( z in Cent Q & ( for x being Element of Q holds f . x = x * z ) )

for f being Function of Q,Q st f in Mlt (Cent Q) holds

ex z being Element of Q st

( z in Cent Q & ( for x being Element of Q holds f . x = x * z ) )

proof end;

theorem Th52: :: AIMLOOP:55

for Q being multLoop

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 ) )

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 ) )

proof end;

theorem Th53: :: AIMLOOP:56

for Q being multLoop

for x, y being Element of Q holds

( x * (lp (Cent Q)) = y * (lp (Cent Q)) iff ex z being Element of Q st

( z in Cent Q & y = x * z ) )

for x, y being Element of Q holds

( x * (lp (Cent Q)) = y * (lp (Cent Q)) iff ex z being Element of Q st

( z in Cent Q & y = x * z ) )

proof end;

::We define the set InnAut of inner mappings of Q,

::define the notion of an AIM loop and relate this to

::the conditions on T, L, and R defined by satisfies_TT, etc.

::For AIM loops we will prove the nucleus and the center are normal.

::define the notion of an AIM loop and relate this to

::the conditions on T, L, and R defined by satisfies_TT, etc.

::For AIM loops we will prove the nucleus and the center are normal.

definition

let Q be multLoop;

ex b_{1} being Subset of (Funcs (Q,Q)) st

for f being object holds

( f in b_{1} iff ex g being Function of Q,Q st

( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) )

for b_{1}, b_{2} being Subset of (Funcs (Q,Q)) st ( for f being object holds

( f in b_{1} iff ex g being Function of Q,Q st

( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) ) & ( for f being object holds

( f in b_{2} iff ex g being Function of Q,Q st

( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) ) holds

b_{1} = b_{2}

end;
func InnAut Q -> Subset of (Funcs (Q,Q)) means :Def49: :: AIMLOOP:def 51

for f being object holds

( f in it iff ex g being Function of Q,Q st

( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) );

existence for f being object holds

( f in it iff ex g being Function of Q,Q st

( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) );

ex b

for f being object holds

( f in b

( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) )

proof end;

uniqueness for b

( f in b

( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) ) & ( for f being object holds

( f in b

( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) ) holds

b

proof end;

:: deftheorem Def49 defines InnAut AIMLOOP:def 51 :

for Q being multLoop

for b_{2} being Subset of (Funcs (Q,Q)) holds

( b_{2} = InnAut Q iff for f being object holds

( f in b_{2} iff ex g being Function of Q,Q st

( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) );

for Q being multLoop

for b

( b

( f in b

( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) );

registration

let Q be multLoop;

coherence

( not InnAut Q is empty & InnAut Q is composition-closed & InnAut Q is inverse-closed )

end;
coherence

( not InnAut Q is empty & InnAut Q is composition-closed & InnAut Q is inverse-closed )

proof end;

theorem Th55: :: AIMLOOP:58

for Q being multLoop

for f being Function of Q,Q holds

( f in InnAut Q iff ( f in Mlt ([#] Q) & f . (1. Q) = 1. Q ) )

for f being Function of Q,Q holds

( f in InnAut Q iff ( f in Mlt ([#] Q) & f . (1. Q) = 1. Q ) )

proof end;

:: deftheorem Def50 defines AIM AIMLOOP:def 52 :

for Q being multLoop holds

( Q is AIM iff for f, g being Function of Q,Q st f in InnAut Q & g in InnAut Q holds

f * g = g * f );

for Q being multLoop holds

( Q is AIM iff for f, g being Function of Q,Q st f in InnAut Q & g in InnAut Q holds

f * g = g * f );

definition

let Q be multLoop;

let x be Element of Q;

deffunc H_{1}( Element of Q) -> Element of Q = T_map ($1,x);

ex b_{1} being Function of Q,Q st

for u being Element of Q holds b_{1} . u = T_map (u,x)

for b_{1}, b_{2} being Function of Q,Q st ( for u being Element of Q holds b_{1} . u = T_map (u,x) ) & ( for u being Element of Q holds b_{2} . u = T_map (u,x) ) holds

b_{1} = b_{2}

end;
let x be Element of Q;

deffunc H

func T_MAP x -> Function of Q,Q means :TM1: :: AIMLOOP:def 53

for u being Element of Q holds it . u = T_map (u,x);

existence for u being Element of Q holds it . u = T_map (u,x);

ex b

for u being Element of Q holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem TM1 defines T_MAP AIMLOOP:def 53 :

for Q being multLoop

for x being Element of Q

for b_{3} being Function of Q,Q holds

( b_{3} = T_MAP x iff for u being Element of Q holds b_{3} . u = T_map (u,x) );

for Q being multLoop

for x being Element of Q

for b

( b

definition

let Q be multLoop;

let x, y be Element of Q;

deffunc H_{1}( Element of Q) -> Element of Q = L_map ($1,x,y);

ex b_{1} being Function of Q,Q st

for u being Element of Q holds b_{1} . u = L_map (u,x,y)

for b_{1}, b_{2} being Function of Q,Q st ( for u being Element of Q holds b_{1} . u = L_map (u,x,y) ) & ( for u being Element of Q holds b_{2} . u = L_map (u,x,y) ) holds

b_{1} = b_{2}

end;
let x, y be Element of Q;

deffunc H

func L_MAP (x,y) -> Function of Q,Q means :LM1: :: AIMLOOP:def 54

for u being Element of Q holds it . u = L_map (u,x,y);

existence for u being Element of Q holds it . u = L_map (u,x,y);

ex b

for u being Element of Q holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem LM1 defines L_MAP AIMLOOP:def 54 :

for Q being multLoop

for x, y being Element of Q

for b_{4} being Function of Q,Q holds

( b_{4} = L_MAP (x,y) iff for u being Element of Q holds b_{4} . u = L_map (u,x,y) );

for Q being multLoop

for x, y being Element of Q

for b

( b

definition

let Q be multLoop;

let x, y be Element of Q;

deffunc H_{1}( Element of Q) -> Element of Q = R_map ($1,x,y);

ex b_{1} being Function of Q,Q st

for u being Element of Q holds b_{1} . u = R_map (u,x,y)

for b_{1}, b_{2} being Function of Q,Q st ( for u being Element of Q holds b_{1} . u = R_map (u,x,y) ) & ( for u being Element of Q holds b_{2} . u = R_map (u,x,y) ) holds

b_{1} = b_{2}

end;
let x, y be Element of Q;

deffunc H

func R_MAP (x,y) -> Function of Q,Q means :RM1: :: AIMLOOP:def 55

for u being Element of Q holds it . u = R_map (u,x,y);

existence for u being Element of Q holds it . u = R_map (u,x,y);

ex b

for u being Element of Q holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem RM1 defines R_MAP AIMLOOP:def 55 :

for Q being multLoop

for x, y being Element of Q

for b_{4} being Function of Q,Q holds

( b_{4} = R_MAP (x,y) iff for u being Element of Q holds b_{4} . u = R_map (u,x,y) );

for Q being multLoop

for x, y being Element of Q

for b

( b

registration
end;

registration

ex b_{1} being multLoop st

( not b_{1} is empty & b_{1} is strict & b_{1} is AIM )
end;

cluster non empty left_mult-cancelable right_mult-cancelable mult-cancelable strict invertible right_unital well-unital left_unital unital AIM for multLoopStr ;

existence ex b

( not b

proof end;

registration

for b_{1} being AIM multLoop holds

( b_{1} is satisfying_TT & b_{1} is satisfying_TL & b_{1} is satisfying_TR & b_{1} is satisfying_LR & b_{1} is satisfying_LL & b_{1} is satisfying_RR )
end;

cluster non empty mult-cancelable invertible well-unital AIM -> satisfying_TT satisfying_TL satisfying_TR satisfying_LR satisfying_LL satisfying_RR AIM for multLoopStr ;

coherence for b

( b

proof end;

theorem Th59: :: AIMLOOP:62

for Q being multLoop

for f being Function of Q,Q st f in Mlt (Nucl Q) holds

ex u, v being Element of Q st

( u in Nucl Q & v in Nucl Q & ( for x being Element of Q holds f . x = u * (x * v) ) )

for f being Function of Q,Q st f in Mlt (Nucl Q) holds

ex u, v being Element of Q st

( u in Nucl Q & v in Nucl Q & ( for x being Element of Q holds f . x = u * (x * v) ) )

proof end;

theorem Th60: :: AIMLOOP:63

for Q being multLoop

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) ) )

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) ) )

proof end;

theorem Th61: :: AIMLOOP:64

for Q being multLoop

for x, y being Element of Q holds

( 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) ) )

for x, y being Element of Q holds

( 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) ) )

proof end;

:: Suggested result and proof by Kinyon Sep 10 2018

:: as crucial part of proving the nucleus of an AIM loop

:: is normal.

:: as crucial part of proving the nucleus of an AIM loop

:: is normal.

:: This proof was difficult and required a hint from Kinyon.

:: Kinyon's hint was essentially the proof of NuclT above.

:: Kinyon's hint was essentially the proof of NuclT above.

registration
end;

:: Main Theorem The AIM Conjecture follows

::from knowing every AIM loop satisfies

::aa1, aa2, aa3, Ka, aK1, aK2 and aK3.

::This theorem justifies using first-order theorem provers

::to try to prove the AIM Conjecture.

::from knowing every AIM loop satisfies

::aa1, aa2, aa3, Ka, aK1, aK2 and aK3.

::This theorem justifies using first-order theorem provers

::to try to prove the AIM Conjecture.

theorem :: AIMLOOP:68

( ( 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 ) ) implies for Q being AIM multLoop holds

( Q _/_ (lp (Nucl Q)) is commutative multGroup & Q _/_ (lp (Cent Q)) is multGroup ) )

( 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 ) ) implies for Q being AIM multLoop holds

( Q _/_ (lp (Nucl Q)) is commutative multGroup & Q _/_ (lp (Cent Q)) is multGroup ) )

proof end;