:: {AIM } Loops and the {AIM } Conjecture
:: 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 ;

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 b₁ being Element of Q st x * b₁ = y by ALGSTR_1:def 6;
uniqueness
for b₁, b₂ being Element of Q st x * b₁ = y & x * b₂ = y holds
b₁ = b₂ 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, b₄ being Element of Q holds
( b₄ = x \ y iff x * b₄ = 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 b₁ being Element of Q st b₁ * y = x by ALGSTR_1:def 6;
uniqueness
for b₁, b₂ being Element of Q st b₁ * y = x & b₂ * y = x holds
b₁ = b₂ 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, b₄ being Element of Q holds
( b₄ = x / y iff b₄ * 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

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₁ being multLoop st
( b₁ is strict & b₁ is satisfying_TT & b₁ is satisfying_TL & b₁ is satisfying_TR & b₁ is satisfying_LR & b₁ is satisfying_LL & b₁ is satisfying_RR & b₁ is satisfying_aa1 & b₁ is satisfying_aa2 & b₁ is satisfying_aa3 & b₁ is satisfying_Ka & b₁ is satisfying_aK1 & b₁ is satisfying_aK2 & b₁ 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 S₁[ Element of Q] means for y, z being Element of Q holds ($1 * y) * z = $1 * (y * z);
defpred S₂[ Element of Q] means for x, z being Element of Q holds (x * $1) * z = x * ($1 * z);
defpred S₃[ Element of Q] means for x, y being Element of Q holds (x * y) * $1 = x * (y * $1);
defpred S₄[ 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 b₁ being Subset of Q st
for x being Element of Q holds
( x in b₁ iff for y, z being Element of Q holds (x * y) * z = x * (y * z) )

proof end;

uniqueness
for b₁, b₂ being Subset of Q st ( for x being Element of Q holds
( x in b₁ 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₂ iff for y, z being Element of Q holds (x * y) * z = x * (y * z) ) ) holds
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
ex b₁ being Subset of Q st
for y being Element of Q holds
( y in b₁ iff for x, z being Element of Q holds (x * y) * z = x * (y * z) )

proof end;

uniqueness
for b₁, b₂ being Subset of Q st ( for y being Element of Q holds
( y in b₁ 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₂ iff for x, z being Element of Q holds (x * y) * z = x * (y * z) ) ) holds
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
ex b₁ being Subset of Q st
for z being Element of Q holds
( z in b₁ iff for x, y being Element of Q holds (x * y) * z = x * (y * z) )

proof end;

uniqueness
for b₁, b₂ being Subset of Q st ( for z being Element of Q holds
( z in b₁ 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₂ iff for x, y being Element of Q holds (x * y) * z = x * (y * z) ) ) holds
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
ex b₁ being Subset of Q st
for x being Element of Q holds
( x in b₁ iff for y being Element of Q holds x * y = y * x )

proof end;

uniqueness
for b₁, b₂ being Subset of Q st ( for x being Element of Q holds
( x in b₁ iff for y being Element of Q holds x * y = y * x ) ) & ( for x being Element of Q holds
( x in b₂ iff for y being Element of Q holds x * y = y * x ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def22 defines Nucl_l AIMLOOP:def 22 :
for Q being multLoop
for b₂ being Subset of Q holds
( b₂ = Nucl_l Q iff for x being Element of Q holds
( x in b₂ 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 b₂ being Subset of Q holds
( b₂ = Nucl_m Q iff for y being Element of Q holds
( y in b₂ 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 b₂ being Subset of Q holds
( b₂ = Nucl_r Q iff for z being Element of Q holds
( z in b₂ 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 b₂ being Subset of Q holds
( b₂ = Comm Q iff for x being Element of Q holds
( x in b₂ 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
((Nucl_l Q) /\ (Nucl_m Q)) /\ (Nucl_r Q);

coherence
((Nucl_l Q) /\ (Nucl_m Q)) /\ (Nucl_r Q) is Subset of Q ;

end;

:: deftheorem defines Nucl AIMLOOP:def 26 :
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 ) )

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 b₁ being Function of Q1,Q2 st b₁ is unity-preserving & b₁ is quasi-homomorphic holds
b₁ 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 b₁ being Function of Q1,Q2 st b₁ is homomorphic holds
( b₁ is unity-preserving & b₁ is quasi-homomorphic ) ;

end;

registration

let Q1, Q2 be multLoop;

cluster ([#] Q1) --> (1. Q2) -> homomorphic for Function of Q1,Q2;

coherence
for b₁ being Function of Q1,Q2 st b₁ = ([#] Q1) --> (1. Q2) holds
b₁ 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 b₁ being Function of Q1,Q2 st b₁ 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 b₁ being Subset of Q st
for x being Element of Q holds
( x in b₁ iff f . x = 1. Q2 )

proof end;

uniqueness
for b₁, b₂ being Subset of Q st ( for x being Element of Q holds
( x in b₁ iff f . x = 1. Q2 ) ) & ( for x being Element of Q holds
( x in b₂ iff f . x = 1. Q2 ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def29 defines Ker AIMLOOP:def 31 :
for Q, Q2 being multLoop
for f being homomorphic Function of Q,Q2
for b₄ being Subset of Q holds
( b₄ = Ker f iff for x being Element of Q holds
( x in b₄ 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 b₁ being non empty multLoopStr st
( the carrier of b₁ c= the carrier of Q & the multF of b₁ = the multF of Q || the carrier of b₁ & the OneF of b₁ = the OneF of Q )

proof end;

end;

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

registration

let Q be multLoop;

cluster non empty cancelable strict invertible well-unital for SubLoopStr of Q;

existence
ex b₁ being SubLoopStr of Q st
( b₁ is well-unital & b₁ is invertible & b₁ is cancelable & not b₁ is empty & b₁ is strict )

proof end;

end;

definition

let Q be multLoop;
mode SubLoop of Q is cancelable invertible well-unital SubLoopStr of Q;

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 S₁[ 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 b₁ being Subset of Q st
for x being Element of Q holds
( x in b₁ 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 b₁, b₂ being Subset of Q st ( for x being Element of Q holds
( x in b₁ 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₂ 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₁ = b₂

proof end;

end;

:: deftheorem Def32 defines loopclose1 AIMLOOP:def 34 :
for Q being multLoop
for H1, H2, b₄ being Subset of Q holds
( b₄ = loopclose1 (H1,H2) iff for x being Element of Q holds
( x in b₄ 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 b₁ being strict SubLoop of Q st
( H c= [#] b₁ & ( for H2 being SubLoop of Q st H c= [#] H2 holds
[#] b₁ c= [#] H2 ) )

proof end;

uniqueness
for b₁, b₂ being strict SubLoop of Q st H c= [#] b₁ & ( for H2 being SubLoop of Q st H c= [#] H2 holds
[#] b₁ c= [#] H2 ) & H c= [#] b₂ & ( for H2 being SubLoop of Q st H c= [#] H2 holds
[#] b₂ c= [#] H2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def33 defines lp AIMLOOP:def 35 :
for Q being multLoop
for H being Subset of Q
for b₃ being strict SubLoop of Q holds
( b₃ = lp H iff ( H c= [#] b₃ & ( for H2 being SubLoop of Q st H c= [#] H2 holds
[#] b₃ 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 ;

cluster {(id A)} -> composition-closed inverse-closed ;

coherence
( {(id A)} is composition-closed & {(id A)} is inverse-closed )

proof end;

end;

registration

cluster functional non empty composition-closed inverse-closed for set ;

existence
ex b₁ being functional set st
( b₁ is composition-closed & b₁ is inverse-closed & not b₁ is empty )

proof end;

end;

registration

let Q be multLoopStr ;

cluster functional non empty composition-closed inverse-closed for Element of bool (Funcs (Q,Q));

existence
ex b₁ being Subset of (Funcs (Q,Q)) st
( b₁ is composition-closed & b₁ is inverse-closed & not b₁ 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 S₂[ 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 b₁ being Subset of (Funcs (Q,Q)) st
for f being object holds
( f in b₁ 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 b₁, b₂ being Subset of (Funcs (Q,Q)) st ( for f being object holds
( f in b₁ 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₂ 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₁ = b₂

proof end;

end;

:: deftheorem Def37 defines MltClos1 AIMLOOP:def 39 :
for Q being non empty multLoopStr
for H being Subset of Q
for S, b₄ being Subset of (Funcs (Q,Q)) holds
( b₄ = MltClos1 (H,S) iff for f being object holds
( f in b₄ 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 b₁ being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st
( H left-right-mult-closed b₁ & ( for X being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed X holds
b₁ c= X ) )

proof end;

uniqueness
for b₁, b₂ being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed b₁ & ( for X being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed X holds
b₁ c= X ) & H left-right-mult-closed b₂ & ( for X being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed X holds
b₂ c= X ) holds
b₁ = b₂ ;

end;

:: deftheorem Def38 defines Mlt AIMLOOP:def 40 :
for Q being multLoop
for H being Subset of Q
for b₃ being composition-closed inverse-closed Subset of (Funcs (Q,Q)) holds
( b₃ = Mlt H iff ( H left-right-mult-closed b₃ & ( for X being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed X holds
b₃ 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 b₁ being Subset of Q st
for y being Element of Q holds
( y in b₁ iff ex h being Permutation of Q st
( h in Mlt H & y = h . x ) )

proof end;

uniqueness
for b₁, b₂ being Subset of Q st ( for y being Element of Q holds
( y in b₁ 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₂ iff ex h being Permutation of Q st
( h in Mlt H & y = h . x ) ) ) holds
b₁ = b₂

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 b₄ being Subset of Q holds
( b₄ = x * H iff for y being Element of Q holds
( y in b₄ 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 b₁ being Subset-Family of Q st
for H being Subset of Q holds
( H in b₁ iff ex x being Element of Q st H = x * N )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of Q st ( for H being Subset of Q holds
( H in b₁ iff ex x being Element of Q st H = x * N ) ) & ( for H being Subset of Q holds
( H in b₂ iff ex x being Element of Q st H = x * N ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def41 defines Cosets AIMLOOP:def 43 :
for Q being multLoop
for N being SubLoop of Q
for b₃ being Subset-Family of Q holds
( b₃ = Cosets N iff for H being Subset of Q holds
( H in b₃ 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 b₁ being Subset of Q st
for x being Element of Q holds
( x in b₁ iff ex y, z being Element of Q st
( y in H1 & z in H2 & x = y * z ) )

proof end;

uniqueness
for b₁, b₂ being Subset of Q st ( for x being Element of Q holds
( x in b₁ 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₂ iff ex y, z being Element of Q st
( y in H1 & z in H2 & x = y * z ) ) ) holds
b₁ = 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
ex b₁ being Subset of Q st
for x being Element of Q holds
( x in b₁ iff ex y, z being Element of Q st
( y in H1 & z in H2 & x = y \ z ) )

proof end;

uniqueness
for b₁, b₂ being Subset of Q st ( for x being Element of Q holds
( x in b₁ 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₂ iff ex y, z being Element of Q st
( y in H1 & z in H2 & x = y \ z ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def42 defines * AIMLOOP:def 44 :
for Q being multLoopStr
for H1, H2, b₄ being Subset of Q holds
( b₄ = H1 * H2 iff for x being Element of Q holds
( x in b₄ 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, b₄ being Subset of Q holds
( b₄ = H1 \ H2 iff for x being Element of Q holds
( x in b₄ 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;

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₁ being SubLoop of Q st b₁ 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 (Cosets N) means :Def46: :: AIMLOOP:def 48
for H1, H2 being Element of Cosets N holds it . (H1,H2) = H1 * H2;

existence
ex b₁ being BinOp of (Cosets N) st
for H1, H2 being Element of Cosets N holds b₁ . (H1,H2) = H1 * H2

proof end;

uniqueness
for b₁, b₂ being BinOp of (Cosets N) st ( for H1, H2 being Element of Cosets N holds b₁ . (H1,H2) = H1 * H2 ) & ( for H1, H2 being Element of Cosets N holds b₂ . (H1,H2) = H1 * H2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def46 defines Coset_Loop_Op AIMLOOP:def 48 :
for Q being multLoop
for N being normal SubLoop of Q
for b₃ being BinOp of (Cosets N) holds
( b₃ = Coset_Loop_Op N iff for H1, H2 being Element of Cosets N holds b₃ . (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(# (Cosets N),(Coset_Loop_Op N),(SubLoop_As_Coset N) #);

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

end;

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

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;

cluster Q _/_ N -> cancelable strict invertible well-unital ;

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 b₁ being Function of Q,(Q _/_ N) st
for x being Element of Q holds b₁ . x = x * N

proof end;

uniqueness
for b₁, b₂ being Function of Q,(Q _/_ N) st ( for x being Element of Q holds b₁ . x = x * N ) & ( for x being Element of Q holds b₂ . x = x * N ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def48 defines QuotientHom AIMLOOP:def 50 :
for Q being multLoop
for N being normal SubLoop of Q
for b₃ being Function of Q,(Q _/_ N) holds
( b₃ = QuotientHom (Q,N) iff for x being Element of Q holds b₃ . 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{ F₁() -> multLoop, F₂() -> Subset of F₁(), P₁[ Function of F₁(),F₁()] } :

for f being Function of F₁(),F₁() st f in Mlt F₂() holds
P₁[f]

provided

A1: for u being Element of F₁() st u in F₂() holds
for f being Function of F₁(),F₁() st ( for x being Element of F₁() holds f . x = x * u ) holds
P₁[f] and
A2: for u being Element of F₁() st u in F₂() holds
for f being Function of F₁(),F₁() st ( for x being Element of F₁() holds f . x = u * x ) holds
P₁[f] and
A3: for g, h being Permutation of F₁() st P₁[g] & P₁[h] holds
P₁[g * h] and
A4: for g being Permutation of F₁() st P₁[g] holds
P₁[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 b₁ being Subset of (Funcs (Q,Q)) st
for f being object holds
( f in b₁ iff ex g being Function of Q,Q st
( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) )

proof end;

uniqueness
for b₁, b₂ being Subset of (Funcs (Q,Q)) st ( for f being object holds
( f in b₁ 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₂ iff ex g being Function of Q,Q st
( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def49 defines InnAut AIMLOOP:def 51 :
for Q being multLoop
for b₂ being Subset of (Funcs (Q,Q)) holds
( b₂ = InnAut Q iff for f being object holds
( f in b₂ 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;

cluster InnAut Q -> non empty composition-closed inverse-closed ;

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 H₁( 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 b₁ being Function of Q,Q st
for u being Element of Q holds b₁ . u = T_map (u,x)

proof end;

uniqueness
for b₁, b₂ being Function of Q,Q st ( for u being Element of Q holds b₁ . u = T_map (u,x) ) & ( for u being Element of Q holds b₂ . u = T_map (u,x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem TM1 defines T_MAP AIMLOOP:def 53 :
for Q being multLoop
for x being Element of Q
for b₃ being Function of Q,Q holds
( b₃ = T_MAP x iff for u being Element of Q holds b₃ . 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 H₁( 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 b₁ being Function of Q,Q st
for u being Element of Q holds b₁ . u = L_map (u,x,y)

proof end;

uniqueness
for b₁, b₂ being Function of Q,Q st ( for u being Element of Q holds b₁ . u = L_map (u,x,y) ) & ( for u being Element of Q holds b₂ . u = L_map (u,x,y) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem LM1 defines L_MAP AIMLOOP:def 54 :
for Q being multLoop
for x, y being Element of Q
for b₄ being Function of Q,Q holds
( b₄ = L_MAP (x,y) iff for u being Element of Q holds b₄ . 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 H₁( 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 b₁ being Function of Q,Q st
for u being Element of Q holds b₁ . u = R_map (u,x,y)

proof end;

uniqueness
for b₁, b₂ being Function of Q,Q st ( for u being Element of Q holds b₁ . u = R_map (u,x,y) ) & ( for u being Element of Q holds b₂ . u = R_map (u,x,y) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem RM1 defines R_MAP AIMLOOP:def 55 :
for Q being multLoop
for x, y being Element of Q
for b₄ being Function of Q,Q holds
( b₄ = R_MAP (x,y) iff for u being Element of Q holds b₄ . 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

cluster Trivial-multLoopStr -> AIM ;

coherence
Trivial-multLoopStr is AIM

proof end;

end;

registration

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₁ being multLoop st
( not b₁ is empty & b₁ is strict & b₁ is AIM )

proof end;

end;

registration

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₁ being AIM multLoop holds
( b₁ is satisfying_TT & b₁ is satisfying_TL & b₁ is satisfying_TR & b₁ is satisfying_LR & b₁ is satisfying_LL & b₁ 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;