:: {AIM } Loops and the {AIM } Conjecture
:: by Chad E. Brown and Karol P\kak
::
:: 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 ;
func Funcs (X,Y) -> set equals :: AIMLOOP:def 1
Funcs ( the carrier of X, the carrier of Y);
coherence
Funcs ( the carrier of X, the carrier of Y) is set
;
end;

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

registration
let X, Y be 1-sorted ;
cluster Funcs (X,Y) -> functional ;
coherence
Funcs (X,Y) is functional
;
end;

definition
let Q be non empty left_mult-cancelable invertible multLoopStr ;
let x, y be Element of Q;
func x \ y -> Element of Q means :Def2: :: AIMLOOP:def 2
x * it = y;
existence
ex b1 being Element of Q st x * b1 = y
by ALGSTR_1:def 6;
uniqueness
for b1, b2 being Element of Q st x * b1 = y & x * b2 = y holds
b1 = b2
by ALGSTR_0:def 20;
end;

:: deftheorem Def2 defines \ AIMLOOP:def 2 :
for Q being non empty left_mult-cancelable invertible multLoopStr
for x, y, b4 being Element of Q holds
( b4 = x \ y iff x * b4 = y );

definition
let Q be non empty right_mult-cancelable invertible multLoopStr ;
let x, y be Element of Q;
func x / y -> Element of Q means :Def3: :: AIMLOOP:def 3
it * y = x;
existence
ex b1 being Element of Q st b1 * y = x
by ALGSTR_1:def 6;
uniqueness
for b1, b2 being Element of Q st b1 * y = x & b2 * y = x holds
b1 = b2
by ALGSTR_0:def 21;
end;

:: deftheorem Def3 defines / AIMLOOP:def 3 :
for Q being non empty right_mult-cancelable invertible multLoopStr
for x, y, b4 being Element of Q holds
( b4 = x / y iff b4 * y = x );

registration
let Q be multLoop;
let x, y be Element of Q;
reduce x \ (x * y) to y;
reducibility
x \ (x * y) = y
by Def2;
reduce x * (x \ y) to y;
reducibility
x * (x \ y) = y
by Def2;
reduce (x * y) / y to x;
reducibility
(x * y) / y = x
by Def3;
reduce (x / y) * y to x;
reducibility
(x / y) * y = x
by Def3;
end;

definition
let Q be non empty left_mult-cancelable invertible multLoopStr ;
let u, x be Element of Q;
func T_map (u,x) -> Element of Q equals :: AIMLOOP:def 4
x \ (u * x);
coherence
x \ (u * x) is Element of Q
;
end;

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

definition
let Q be non empty left_mult-cancelable invertible multLoopStr ;
let u, x, y be Element of Q;
func L_map (u,x,y) -> Element of Q equals :: AIMLOOP:def 5
(y * x) \ (y * (x * u));
coherence
(y * x) \ (y * (x * u)) is Element of Q
;
end;

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

definition
let Q be non empty right_mult-cancelable invertible multLoopStr ;
let u, x, y be Element of Q;
func R_map (u,x,y) -> Element of Q equals :: AIMLOOP:def 6
((u * x) * y) / (x * y);
coherence
((u * x) * y) / (x * y) is Element of Q
;
end;

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

definition
let Q be multLoop;
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);
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);
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);
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);
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);
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);
end;

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

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

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

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

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

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

definition
let Q be multLoop;
let x, y be Element of Q;
func K_op (x,y) -> Element of Q equals :: AIMLOOP:def 13
(y * x) \ (x * y);
coherence
(y * x) \ (x * y) is Element of Q
;
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);

definition
let Q be multLoop;
let x, y, z be Element of Q;
func a_op (x,y,z) -> Element of Q equals :: AIMLOOP:def 14
(x * (y * z)) \ ((x * y) * z);
coherence
(x * (y * z)) \ ((x * y) * z) is Element of Q
;
end;

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

definition
let Q be multLoop;
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;
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;
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;
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;
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;
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;
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;
end;

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

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

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

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

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

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

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

registration
existence
ex b1 being multLoop st
( b1 is strict & b1 is satisfying_TT & b1 is satisfying_TL & b1 is satisfying_TR & b1 is satisfying_LR & b1 is satisfying_LL & b1 is satisfying_RR & b1 is satisfying_aa1 & b1 is satisfying_aa2 & b1 is satisfying_aa3 & b1 is satisfying_Ka & b1 is satisfying_aK1 & b1 is satisfying_aK2 & b1 is satisfying_aK3 )
proof end;
end;

theorem Th1: :: AIMLOOP:1
for Q being multLoop
for x, y, z, u being Element of Q st x * y = u & x * z = u holds
y = z
proof end;

theorem Th2: :: AIMLOOP:2
for Q being multLoop
for x, y, z, u being Element of Q st y * x = u & z * x = u holds
y = z
proof end;

theorem :: AIMLOOP:3
for Q being multLoop
for x, y, z being Element of Q st x * y = x * z holds
y = z by Th1;

theorem :: AIMLOOP:4
for Q being multLoop
for x, y, z being Element of Q st y * x = z * x holds
y = z by Th2;

registration
let Q be multLoop;
let x be Element of Q;
reduce (1. Q) \ x to x;
reducibility
(1. Q) \ x = x
proof end;
reduce x / (1. Q) to x;
reducibility
x / (1. Q) = x
proof end;
let y be Element of Q;
reduce y / (x \ y) to x;
reducibility
y / (x \ y) = x
proof end;
reduce (y / x) \ y to x;
reducibility
(y / x) \ y = x
proof end;
end;

theorem Th5: :: AIMLOOP:5
for Q being multLoop
for x being Element of Q holds x \ x = 1. Q
proof end;

theorem Th6: :: AIMLOOP:6
for Q being multLoop
for x being Element of Q holds x / x = 1. Q
proof end;

theorem :: AIMLOOP:7
for Q being multLoop
for x, y being Element of Q st x \ y = 1. Q holds
x = y
proof end;

theorem :: AIMLOOP:8
for Q being multLoop
for x, y being Element of Q st x / y = 1. Q holds
x = y
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
proof end;

theorem Th10: :: AIMLOOP:10
for Q being multLoop
for x, y being Element of Q st K_op (x,y) = 1. Q holds
x * y = y * x
proof end;

theorem :: AIMLOOP:11
for Q being multLoop
for x, y, z being Element of Q st a_op (x,y,z) = 1. Q holds
L_map (z,y,x) = z
proof end;

definition
let Q be multLoop;
defpred S1[ Element of Q] means for y, z being Element of Q holds ($1 * y) * z =$1 * (y * z);
defpred S2[ Element of Q] means for x, z being Element of Q holds (x * $1) * z = x * ($1 * z);
defpred S3[ Element of Q] means for x, y being Element of Q holds (x * y) * $1 = x * (y *$1);
defpred S4[ Element of Q] means for y being Element of Q holds $1 * y = y *$1;
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
ex b1 being Subset of Q st
for x being Element of Q holds
( x in b1 iff for y, z being Element of Q holds (x * y) * z = x * (y * z) )
proof end;
uniqueness
for b1, b2 being Subset of Q st ( for x being Element of Q holds
( x in b1 iff for y, z being Element of Q holds (x * y) * z = x * (y * z) ) ) & ( for x being Element of Q holds
( x in b2 iff for y, z being Element of Q holds (x * y) * z = x * (y * z) ) ) holds
b1 = b2
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
ex b1 being Subset of Q st
for y being Element of Q holds
( y in b1 iff for x, z being Element of Q holds (x * y) * z = x * (y * z) )
proof end;
uniqueness
for b1, b2 being Subset of Q st ( for y being Element of Q holds
( y in b1 iff for x, z being Element of Q holds (x * y) * z = x * (y * z) ) ) & ( for y being Element of Q holds
( y in b2 iff for x, z being Element of Q holds (x * y) * z = x * (y * z) ) ) holds
b1 = b2
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
ex b1 being Subset of Q st
for z being Element of Q holds
( z in b1 iff for x, y being Element of Q holds (x * y) * z = x * (y * z) )
proof end;
uniqueness
for b1, b2 being Subset of Q st ( for z being Element of Q holds
( z in b1 iff for x, y being Element of Q holds (x * y) * z = x * (y * z) ) ) & ( for z being Element of Q holds
( z in b2 iff for x, y being Element of Q holds (x * y) * z = x * (y * z) ) ) holds
b1 = b2
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
ex b1 being Subset of Q st
for x being Element of Q holds
( x in b1 iff for y being Element of Q holds x * y = y * x )
proof end;
uniqueness
for b1, b2 being Subset of Q st ( for x being Element of Q holds
( x in b1 iff for y being Element of Q holds x * y = y * x ) ) & ( for x being Element of Q holds
( x in b2 iff for y being Element of Q holds x * y = y * x ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines Nucl_l AIMLOOP:def 22 :
for Q being multLoop
for b2 being Subset of Q holds
( b2 = Nucl_l Q iff for x being Element of Q holds
( x in b2 iff for y, z being Element of Q holds (x * y) * z = x * (y * z) ) );

:: deftheorem Def23 defines Nucl_m AIMLOOP:def 23 :
for Q being multLoop
for b2 being Subset of Q holds
( b2 = Nucl_m Q iff for y being Element of Q holds
( y in b2 iff for x, z being Element of Q holds (x * y) * z = x * (y * z) ) );

:: deftheorem Def24 defines Nucl_r AIMLOOP:def 24 :
for Q being multLoop
for b2 being Subset of Q holds
( b2 = Nucl_r Q iff for z being Element of Q holds
( z in b2 iff for x, y being Element of Q holds (x * y) * z = x * (y * z) ) );

:: deftheorem Def25 defines Comm AIMLOOP:def 25 :
for Q being multLoop
for b2 being Subset of Q holds
( b2 = Comm Q iff for x being Element of Q holds
( x in b2 iff for y being Element of Q holds x * y = y * x ) );

definition
let Q be multLoop;
func Nucl Q -> Subset of Q equals :: AIMLOOP:def 26
(() /\ ()) /\ ();
coherence
(() /\ ()) /\ () is Subset of Q
;
end;

:: deftheorem defines Nucl AIMLOOP:def 26 :
for Q being multLoop holds Nucl 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 ) )
proof end;

definition
let Q be multLoop;
func Cent Q -> Subset of Q equals :: AIMLOOP:def 27
(Comm Q) /\ (Nucl Q);
coherence
(Comm Q) /\ (Nucl Q) is Subset of Q
;
end;

:: deftheorem defines Cent AIMLOOP:def 27 :
for Q being multLoop holds Cent Q = (Comm Q) /\ (Nucl Q);

definition
let Q1, Q2 be multLoop;
let f be Function of Q1,Q2;
attr f is unity-preserving means :Def28a: :: AIMLOOP:def 28
f . (1. Q1) = 1. 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);
end;

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

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

definition
let Q1, Q2 be multLoop;
let f be Function of Q1,Q2;
attr f is homomorphic means :: AIMLOOP:def 30
( f is unity-preserving & f is quasi-homomorphic );
end;

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

registration
let Q1, Q2 be multLoop;
cluster Function-like quasi_total unity-preserving quasi-homomorphic -> homomorphic for Element of bool [: the carrier of Q1, the carrier of Q2:];
coherence
for b1 being Function of Q1,Q2 st b1 is unity-preserving & b1 is quasi-homomorphic holds
b1 is homomorphic
;
cluster Function-like quasi_total homomorphic -> unity-preserving quasi-homomorphic for Element of bool [: the carrier of Q1, the carrier of Q2:];
coherence
for b1 being Function of Q1,Q2 st b1 is homomorphic holds
( b1 is unity-preserving & b1 is quasi-homomorphic )
;
end;

registration
let Q1, Q2 be multLoop;
cluster ([#] Q1) --> (1. Q2) -> homomorphic for Function of Q1,Q2;
coherence
for b1 being Function of Q1,Q2 st b1 = ([#] Q1) --> (1. Q2) holds
b1 is homomorphic
proof end;
end;

registration
let Q1, Q2 be multLoop;
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 b1 being Function of Q1,Q2 st b1 is homomorphic
proof end;
end;

definition
let Q, Q2 be multLoop;
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
ex b1 being Subset of Q st
for x being Element of Q holds
( x in b1 iff f . x = 1. Q2 )
proof end;
uniqueness
for b1, b2 being Subset of Q st ( for x being Element of Q holds
( x in b1 iff f . x = 1. Q2 ) ) & ( for x being Element of Q holds
( x in b2 iff f . x = 1. Q2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def29 defines Ker AIMLOOP:def 31 :
for Q, Q2 being multLoop
for f being homomorphic Function of Q,Q2
for b4 being Subset of Q holds
( b4 = Ker f iff for x being Element of Q holds
( x in b4 iff f . x = 1. Q2 ) );

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)
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)
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
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
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
proof end;

:: following GROUP_2
definition
let Q be non empty multLoopStr ;
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
ex b1 being non empty multLoopStr st
( the carrier of b1 c= the carrier of Q & the multF of b1 = the multF of Q || the carrier of b1 & the OneF of b1 = the OneF of Q )
proof end;
end;

:: deftheorem Def30 defines SubLoopStr AIMLOOP:def 32 :
for Q, b2 being non empty multLoopStr holds
( b2 is SubLoopStr of Q iff ( the carrier of b2 c= the carrier of Q & the multF of b2 = the multF of Q || the carrier of b2 & the OneF of b2 = the OneF of Q ) );

registration
let Q be multLoop;
existence
ex b1 being SubLoopStr of Q st
( b1 is well-unital & b1 is invertible & b1 is cancelable & not b1 is empty & b1 is strict )
proof end;
end;

definition end;

definition
let Q be non empty multLoopStr ;
let H be SubLoopStr of Q;
let A be Subset of H;
func @ A -> Subset of Q equals :: AIMLOOP:def 33
A;
coherence
A is Subset of Q
proof end;
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;

defpred S1[ multLoop, Subset of $1, object ] means ex y, z being Element of$1 st
( 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; 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 ex b1 being Subset of Q st for x being Element of Q holds ( x in b1 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 ) ) ) ) proof end; uniqueness for b1, b2 being Subset of Q st ( for x being Element of Q holds ( x in b1 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 b2 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 b1 = b2 proof end; end; :: deftheorem Def32 defines loopclose1 AIMLOOP:def 34 : for Q being multLoop for H1, H2, b4 being Subset of Q holds ( b4 = loopclose1 (H1,H2) iff for x being Element of Q holds ( x in b4 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 ) ) ) ) ); definition let Q be multLoop; 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 ex b1 being strict SubLoop of Q st ( H c= [#] b1 & ( for H2 being SubLoop of Q st H c= [#] H2 holds [#] b1 c= [#] H2 ) ) proof end; uniqueness for b1, b2 being strict SubLoop of Q st H c= [#] b1 & ( for H2 being SubLoop of Q st H c= [#] H2 holds [#] b1 c= [#] H2 ) & H c= [#] b2 & ( for H2 being SubLoop of Q st H c= [#] H2 holds [#] b2 c= [#] H2 ) holds b1 = b2 proof end; end; :: deftheorem Def33 defines lp AIMLOOP:def 35 : for Q being multLoop for H being Subset of Q for b3 being strict SubLoop of Q holds ( b3 = lp H iff ( H c= [#] b3 & ( for H2 being SubLoop of Q st H c= [#] H2 holds [#] b3 c= [#] H2 ) ) ); 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 proof end; theorem Th19: :: AIMLOOP:19 for Q, Q2 being multLoop for f being homomorphic Function of Q,Q2 holds [#] (lp (Ker f)) = Ker f proof end; theorem Th20a: :: AIMLOOP:20 for Q being multLoop holds 1. Q in Nucl_l Q proof end; theorem Th20b: :: AIMLOOP:21 for Q being multLoop holds 1. Q in Nucl_m Q proof end; theorem Th20c: :: AIMLOOP:22 for Q being multLoop holds 1. Q in Nucl_r Q proof end; theorem Th20: :: AIMLOOP:23 for Q being multLoop holds 1. Q in Nucl Q proof end; registration let Q be multLoop; cluster Nucl_l Q -> non empty ; coherence not Nucl_l Q is empty by Th20a; cluster Nucl_m Q -> non empty ; coherence not Nucl_m Q is empty by Th20b; cluster Nucl_r Q -> non empty ; coherence not Nucl_r Q is empty by Th20c; cluster Nucl Q -> non empty ; coherence not Nucl Q is empty by Th20; end; theorem Th21: :: AIMLOOP:24 for Q being multLoop for x, y being Element of Q st x in Nucl Q & y in Nucl Q holds x * y in Nucl Q proof end; theorem Th22: :: AIMLOOP:25 for Q being multLoop for x, y being Element of Q st x in Nucl Q & y in Nucl Q holds x \ y in Nucl Q proof end; theorem Th23: :: AIMLOOP:26 for Q being multLoop for x, y being Element of Q st x in Nucl Q & y in Nucl Q holds x / y in Nucl Q proof end; theorem Th24: :: AIMLOOP:27 for Q being multLoop holds [#] (lp (Nucl Q)) = Nucl Q proof end; theorem Th25: :: AIMLOOP:28 for Q being multLoop holds [#] (lp (Cent Q)) = Cent Q proof end; ::We now define a set Mlt Q of multiplicative mappings of Q ::and cosets (mostly following Albert 1943 for cosets). definition let X be functional set ; 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; attr X is inverse-closed means :Def35: :: AIMLOOP:def 37 for f being Element of X st f in X holds f " in X; end; :: 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 ); :: 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 ); registration let A be set ; coherence ( {(id A)} is composition-closed & {(id A)} is inverse-closed ) proof end; end; registration existence ex b1 being functional set st ( b1 is composition-closed & b1 is inverse-closed & not b1 is empty ) proof end; end; registration let Q be multLoopStr ; existence ex b1 being Subset of (Funcs (Q,Q)) st ( b1 is composition-closed & b1 is inverse-closed & not b1 is empty ) proof end; end; definition let Q be non empty multLoopStr ; let H be Subset of Q; let S be Subset of (Funcs (Q,Q)); pred H left-right-mult-closed S means :: AIMLOOP:def 38 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 ); 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 ) ); defpred S2[ multLoopStr , Subset of$1, Subset of (Funcs ($1,$1)), object ] means ( ex u being Element of $1 st ( 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)); 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 ex b1 being Subset of (Funcs (Q,Q)) st for f being object holds ( f in b1 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 " ) ) ) proof end; uniqueness for b1, b2 being Subset of (Funcs (Q,Q)) st ( for f being object holds ( f in b1 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 b2 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 b1 = b2 proof end; end; :: deftheorem Def37 defines MltClos1 AIMLOOP:def 39 : for Q being non empty multLoopStr for H being Subset of Q for S, b4 being Subset of (Funcs (Q,Q)) holds ( b4 = MltClos1 (H,S) iff for f being object holds ( f in b4 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 " ) ) ) ); 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() 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 ) ) 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 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 ) proof end; theorem Th30: :: AIMLOOP:33 for Q being multLoop for u being Element of Q holds (curry the multF of Q) . u is Permutation of Q 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 proof end; definition let Q be multLoop; 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 ex b1 being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st ( H left-right-mult-closed b1 & ( for X being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed X holds b1 c= X ) ) proof end; uniqueness for b1, b2 being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed b1 & ( for X being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed X holds b1 c= X ) & H left-right-mult-closed b2 & ( for X being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed X holds b2 c= X ) holds b1 = b2 ; end; :: deftheorem Def38 defines Mlt AIMLOOP:def 40 : for Q being multLoop for H being Subset of Q for b3 being composition-closed inverse-closed Subset of (Funcs (Q,Q)) holds ( b3 = Mlt H iff ( H left-right-mult-closed b3 & ( for X being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed X holds b3 c= X ) ) ); 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 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 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 ) ) 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 proof end; definition let Q be multLoop; 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 ex b1 being Subset of Q st for y being Element of Q holds ( y in b1 iff ex h being Permutation of Q st ( h in Mlt H & y = h . x ) ) proof end; uniqueness for b1, b2 being Subset of Q st ( for y being Element of Q holds ( y in b1 iff ex h being Permutation of Q st ( h in Mlt H & y = h . x ) ) ) & ( for y being Element of Q holds ( y in b2 iff ex h being Permutation of Q st ( h in Mlt H & y = h . x ) ) ) holds b1 = b2 proof end; end; :: deftheorem Def39 defines * AIMLOOP:def 41 : for Q being multLoop for H being Subset of Q for x being Element of Q for b4 being Subset of Q holds ( b4 = x * H iff for y being Element of Q holds ( y in b4 iff ex h being Permutation of Q st ( h in Mlt H & y = h . x ) ) ); definition let Q be multLoop; let H be SubLoop of Q; let x be Element of Q; func x * H -> Subset of Q equals :: AIMLOOP:def 42 x * (@ ([#] H)); coherence x * (@ ([#] H)) is Subset of Q ; end; :: 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)); definition let Q be multLoop; 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 ex b1 being Subset-Family of Q st for H being Subset of Q holds ( H in b1 iff ex x being Element of Q st H = x * N ) proof end; uniqueness for b1, b2 being Subset-Family of Q st ( for H being Subset of Q holds ( H in b1 iff ex x being Element of Q st H = x * N ) ) & ( for H being Subset of Q holds ( H in b2 iff ex x being Element of Q st H = x * N ) ) holds b1 = b2 proof end; end; :: deftheorem Def41 defines Cosets AIMLOOP:def 43 : for Q being multLoop for N being SubLoop of Q for b3 being Subset-Family of Q holds ( b3 = Cosets N iff for H being Subset of Q holds ( H in b3 iff ex x being Element of Q st H = x * N ) ); registration let Q be multLoop; let N be SubLoop of Q; cluster Cosets N -> non empty ; coherence not Cosets N is empty proof end; end; ::We define the notion of a normal subloop ::and construct quotients by normal subloops. definition let Q be multLoopStr ; 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 ex b1 being Subset of Q st for x being Element of Q holds ( x in b1 iff ex y, z being Element of Q st ( y in H1 & z in H2 & x = y * z ) ) proof end; uniqueness for b1, b2 being Subset of Q st ( for x being Element of Q holds ( x in b1 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 b2 iff ex y, z being Element of Q st ( y in H1 & z in H2 & x = y * z ) ) ) holds b1 = b2 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 ex b1 being Subset of Q st for x being Element of Q holds ( x in b1 iff ex y, z being Element of Q st ( y in H1 & z in H2 & x = y \ z ) ) proof end; uniqueness for b1, b2 being Subset of Q st ( for x being Element of Q holds ( x in b1 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 b2 iff ex y, z being Element of Q st ( y in H1 & z in H2 & x = y \ z ) ) ) holds b1 = b2 proof end; end; :: deftheorem Def42 defines * AIMLOOP:def 44 : for Q being multLoopStr for H1, H2, b4 being Subset of Q holds ( b4 = H1 * H2 iff for x being Element of Q holds ( x in b4 iff ex y, z being Element of Q st ( y in H1 & z in H2 & x = y * z ) ) ); :: deftheorem defines \ AIMLOOP:def 45 : for Q being multLoopStr for H1, H2, b4 being Subset of Q holds ( b4 = H1 \ H2 iff for x being Element of Q holds ( x in b4 iff ex y, z being Element of Q st ( y in H1 & z in H2 & x = y \ z ) ) ); definition let Q be multLoop; let H be SubLoop of Q; attr H is normal means :Def44: :: AIMLOOP:def 46 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 ) ) ) ); end; :: 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 ) ) ) ) ); registration let Q be multLoop; existence ex b1 being SubLoop of Q st b1 is normal proof end; end; definition let Q be multLoop; let N be normal SubLoop of Q; func SubLoop_As_Coset N -> Element of Cosets N equals :: AIMLOOP:def 47 (1. Q) * N; coherence (1. Q) * N is Element of Cosets N by Def41; end; :: 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; definition let Q be multLoop; let N be normal SubLoop of Q; func Coset_Loop_Op N -> BinOp of () means :Def46: :: AIMLOOP:def 48 for H1, H2 being Element of Cosets N holds it . (H1,H2) = H1 * H2; existence ex b1 being BinOp of () st for H1, H2 being Element of Cosets N holds b1 . (H1,H2) = H1 * H2 proof end; uniqueness for b1, b2 being BinOp of () st ( for H1, H2 being Element of Cosets N holds b1 . (H1,H2) = H1 * H2 ) & ( for H1, H2 being Element of Cosets N holds b2 . (H1,H2) = H1 * H2 ) holds b1 = b2 proof end; end; :: deftheorem Def46 defines Coset_Loop_Op AIMLOOP:def 48 : for Q being multLoop for N being normal SubLoop of Q for b3 being BinOp of () holds ( b3 = Coset_Loop_Op N iff for H1, H2 being Element of Cosets N holds b3 . (H1,H2) = H1 * H2 ); definition let Q be multLoop; let N be normal SubLoop of Q; func Q _/_ N -> strict multLoopStr equals :: AIMLOOP:def 49 multLoopStr(# (),(),() #); coherence multLoopStr(# (),(),() #) is strict multLoopStr ; end; :: deftheorem defines _/_ AIMLOOP:def 49 : for Q being multLoop for N being normal SubLoop of Q holds Q _/_ N = multLoopStr(# (),(),() #); registration let Q be multLoop; let N be normal SubLoop of Q; cluster Q _/_ N -> non empty strict ; coherence not Q _/_ N is empty ; end; 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 ) proof end; end; definition let Q be multLoop; 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 ex b1 being Function of Q,(Q _/_ N) st for x being Element of Q holds b1 . x = x * N proof end; uniqueness for b1, b2 being Function of Q,(Q _/_ N) st ( for x being Element of Q holds b1 . x = x * N ) & ( for x being Element of Q holds b2 . x = x * N ) holds b1 = b2 proof end; end; :: deftheorem Def48 defines QuotientHom AIMLOOP:def 50 : for Q being multLoop for N being normal SubLoop of Q for b3 being Function of Q,(Q _/_ N) holds ( b3 = QuotientHom (Q,N) iff for x being Element of Q holds b3 . x = x * N ); registration let Q be multLoop; let N be normal SubLoop of Q; cluster QuotientHom (Q,N) -> homomorphic ; coherence QuotientHom (Q,N) is homomorphic proof end; 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 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 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 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 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 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 proof end; scheme :: AIMLOOP:sch 1 MltInd{ F1() -> multLoop, F2() -> Subset of F1(), P1[ Function of F1(),F1()] } : for f being Function of F1(),F1() st f in Mlt F2() holds P1[f] provided A1: for u being Element of F1() st u in F2() holds for f being Function of F1(),F1() st ( for x being Element of F1() holds f . x = x * u ) holds P1[f] and A2: for u being Element of F1() st u in F2() holds for f being Function of F1(),F1() st ( for x being Element of F1() holds f . x = u * x ) holds P1[f] and A3: for g, h being Permutation of F1() st P1[g] & P1[h] holds P1[g * h] and A4: for g being Permutation of F1() st P1[g] holds P1[g " ] 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) ) proof end; theorem Th43: :: AIMLOOP:46 for Q being multLoop for N being normal SubLoop of Q holds the carrier of N = (1. Q) * N proof end; theorem Th44: :: AIMLOOP:47 for Q being multLoop for N being normal SubLoop of Q holds Ker (QuotientHom (Q,N)) = @ ([#] 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 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 ) 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 ) 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 ) proof end; theorem :: AIMLOOP:52 for Q, Q2 being multLoop for f being homomorphic Function of Q,Q2 holds lp (Ker f) is normal proof end; theorem Th50: :: AIMLOOP:53 for Q being multLoop holds ( 1. Q in [#] (lp (Cent Q)) & 1. Q in Cent Q ) 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 ) ) 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 ) ) 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 ) ) proof end; theorem Th54: :: AIMLOOP:57 for Q being multLoop holds lp (Cent Q) is normal 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. definition let Q be multLoop; 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 ex b1 being Subset of (Funcs (Q,Q)) st for f being object holds ( f in b1 iff ex g being Function of Q,Q st ( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) proof end; uniqueness for b1, b2 being Subset of (Funcs (Q,Q)) st ( for f being object holds ( f in b1 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 b2 iff ex g being Function of Q,Q st ( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) ) holds b1 = b2 proof end; end; :: deftheorem Def49 defines InnAut AIMLOOP:def 51 : for Q being multLoop for b2 being Subset of (Funcs (Q,Q)) holds ( b2 = InnAut Q iff for f being object holds ( f in b2 iff ex g being Function of Q,Q st ( 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 ) proof end; 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 ) ) proof end; definition let Q be multLoop; attr Q is AIM means :Def50: :: AIMLOOP:def 52 for f, g being Function of Q,Q st f in InnAut Q & g in InnAut Q holds f * g = g * f; 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 ); definition let Q be multLoop; let x be Element of Q; deffunc H1( Element of Q) -> Element of Q = T_map ($1,x);
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
ex b1 being Function of Q,Q st
for u being Element of Q holds b1 . u = T_map (u,x)
proof end;
uniqueness
for b1, b2 being Function of Q,Q st ( for u being Element of Q holds b1 . u = T_map (u,x) ) & ( for u being Element of Q holds b2 . u = T_map (u,x) ) holds
b1 = b2
proof end;
end;

:: deftheorem TM1 defines T_MAP AIMLOOP:def 53 :
for Q being multLoop
for x being Element of Q
for b3 being Function of Q,Q holds
( b3 = T_MAP x iff for u being Element of Q holds b3 . u = T_map (u,x) );

theorem Th56: :: AIMLOOP:59
for Q being multLoop
for x being Element of Q holds T_MAP x in InnAut Q
proof end;

definition
let Q be multLoop;
let x, y be Element of Q;
deffunc H1( Element of Q) -> Element of Q = L_map ($1,x,y); 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 ex b1 being Function of Q,Q st for u being Element of Q holds b1 . u = L_map (u,x,y) proof end; uniqueness for b1, b2 being Function of Q,Q st ( for u being Element of Q holds b1 . u = L_map (u,x,y) ) & ( for u being Element of Q holds b2 . u = L_map (u,x,y) ) holds b1 = b2 proof end; end; :: deftheorem LM1 defines L_MAP AIMLOOP:def 54 : for Q being multLoop for x, y being Element of Q for b4 being Function of Q,Q holds ( b4 = L_MAP (x,y) iff for u being Element of Q holds b4 . u = L_map (u,x,y) ); theorem Th57: :: AIMLOOP:60 for Q being multLoop for x, y being Element of Q holds L_MAP (x,y) in InnAut Q proof end; definition let Q be multLoop; let x, y be Element of Q; deffunc H1( Element of Q) -> Element of Q = R_map ($1,x,y);
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
ex b1 being Function of Q,Q st
for u being Element of Q holds b1 . u = R_map (u,x,y)
proof end;
uniqueness
for b1, b2 being Function of Q,Q st ( for u being Element of Q holds b1 . u = R_map (u,x,y) ) & ( for u being Element of Q holds b2 . u = R_map (u,x,y) ) holds
b1 = b2
proof end;
end;

:: deftheorem RM1 defines R_MAP AIMLOOP:def 55 :
for Q being multLoop
for x, y being Element of Q
for b4 being Function of Q,Q holds
( b4 = R_MAP (x,y) iff for u being Element of Q holds b4 . u = R_map (u,x,y) );

theorem Th58: :: AIMLOOP:61
for Q being multLoop
for x, y being Element of Q holds R_MAP (x,y) in InnAut Q
proof end;

registration
coherence
proof end;
end;

registration
existence
ex b1 being multLoop st
( not b1 is empty & b1 is strict & b1 is AIM )
proof end;
end;

registration
coherence
for b1 being AIM multLoop holds
( b1 is satisfying_TT & b1 is satisfying_TL & b1 is satisfying_TR & b1 is satisfying_LR & b1 is satisfying_LL & b1 is satisfying_RR )
proof end;
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) ) )
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) ) )
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) ) )
proof end;

:: Suggested result and proof by Kinyon Sep 10 2018
:: as crucial part of proving the nucleus of an AIM loop
:: is normal.
theorem Th62: :: AIMLOOP:65
for Q being AIM multLoop
for x, u being Element of Q st u in Nucl Q holds
T_map (u,x) in Nucl Q
proof end;

theorem Th63: :: AIMLOOP:66
for Q being AIM multLoop
for x, u being Element of Q st u in Nucl Q holds
(x * u) / x in Nucl Q
proof end;

:: This proof was difficult and required a hint from Kinyon.
:: Kinyon's hint was essentially the proof of NuclT above.
theorem Th64: :: AIMLOOP:67
for Q being multLoop st Q is AIM holds
lp (Nucl Q) is normal
proof end;

registration
let Q be AIM multLoop;
cluster lp (Nucl Q) -> strict normal ;
coherence
lp (Nucl Q) is normal
by Th64;
end;

registration
let Q be multLoop;
cluster lp (Cent Q) -> strict normal ;
coherence
lp (Cent Q) is normal
by Th54;
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.
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 ) )
proof end;