:: Ring Ideals
:: by Jonathan Backer , Piotr Rudnicki and Christoph Schwarzweller
::
:: Received November 20, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users


registration
cluster non empty add-associative right_zeroed left_zeroed for addLoopStr ;
existence
ex b1 being non empty addLoopStr st
( b1 is add-associative & b1 is left_zeroed & b1 is right_zeroed )
proof end;
end;

registration
cluster non empty non trivial add-cancelable Abelian add-associative right_zeroed well-unital distributive associative commutative left_zeroed for doubleLoopStr ;
existence
ex b1 being non trivial doubleLoopStr st
( b1 is Abelian & b1 is left_zeroed & b1 is right_zeroed & b1 is add-cancelable & b1 is well-unital & b1 is add-associative & b1 is associative & b1 is commutative & b1 is distributive )
proof end;
end;

theorem Th1: :: IDEAL_1:1
for V being non empty add-associative right_zeroed left_zeroed addLoopStr
for v, u being Element of V holds Sum <*v,u*> = v + u
proof end;

definition
let L be non empty addLoopStr ;
let F be Subset of L;
attr F is add-closed means :Def1: :: IDEAL_1:def 1
 for x, y being Element of L st x in F & y in F holds
x + y in F;
end;

:: deftheorem Def1 defines add-closed IDEAL_1:def 1 :
for L being non empty addLoopStr
for F being Subset of L holds
( F is add-closed iff for x, y being Element of L st x in F & y in F holds
x + y in F );

definition
let L be non empty multMagma ;
let F be Subset of L;
attr F is left-ideal means :Def2: :: IDEAL_1:def 2
 for p, x being Element of L st x in F holds
p * x in F;
attr F is right-ideal means :Def3: :: IDEAL_1:def 3
 for p, x being Element of L st x in F holds
x * p in F;
end;

:: deftheorem Def2 defines left-ideal IDEAL_1:def 2 :
for L being non empty multMagma
for F being Subset of L holds
( F is left-ideal iff for p, x being Element of L st x in F holds
p * x in F );

:: deftheorem Def3 defines right-ideal IDEAL_1:def 3 :
for L being non empty multMagma
for F being Subset of L holds
( F is right-ideal iff for p, x being Element of L st x in F holds
x * p in F );

registration
let L be non empty addLoopStr ;
cluster non empty add-closed for Element of bool the carrier of L;
existence
ex b1 being non empty Subset of L st b1 is add-closed
proof end;
end;

registration
let L be non empty multMagma ;
cluster non empty left-ideal for Element of bool the carrier of L;
existence
ex b1 being non empty Subset of L st b1 is left-ideal
proof end;
cluster non empty right-ideal for Element of bool the carrier of L;
existence
ex b1 being non empty Subset of L st b1 is right-ideal
proof end;
end;

registration
let L be non empty doubleLoopStr ;
cluster non empty add-closed left-ideal right-ideal for Element of bool the carrier of L;
existence
ex b1 being non empty Subset of L st
( b1 is add-closed & b1 is left-ideal & b1 is right-ideal )
proof end;
cluster non empty add-closed right-ideal for Element of bool the carrier of L;
existence
ex b1 being non empty Subset of L st
( b1 is add-closed & b1 is right-ideal )
proof end;
cluster non empty add-closed left-ideal for Element of bool the carrier of L;
existence
ex b1 being non empty Subset of L st
( b1 is add-closed & b1 is left-ideal )
proof end;
end;

registration
let R be non empty commutative multMagma ;
cluster non empty left-ideal -> non empty right-ideal for Element of bool the carrier of R;
coherence
for b1 being non empty Subset of R st b1 is left-ideal holds
b1 is right-ideal
proof end;
cluster non empty right-ideal -> non empty left-ideal for Element of bool the carrier of R;
coherence
for b1 being non empty Subset of R st b1 is right-ideal holds
b1 is left-ideal
proof end;
end;

definition
let L be non empty doubleLoopStr ;
mode Ideal of L is non empty add-closed left-ideal right-ideal Subset of L;
end;

definition
let L be non empty doubleLoopStr ;
mode RightIdeal of L is non empty add-closed right-ideal Subset of L;
end;

definition
let L be non empty doubleLoopStr ;
mode LeftIdeal of L is non empty add-closed left-ideal Subset of L;
end;

theorem Th2: :: IDEAL_1:2
for R being non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr
for I being non empty left-ideal Subset of R holds 0. R in I
proof end;

theorem Th3: :: IDEAL_1:3
for R being non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr
for I being non empty right-ideal Subset of R holds 0. R in I
proof end;

theorem Th4: :: IDEAL_1:4
for L being non empty right_zeroed addLoopStr holds {(0. L)} is add-closed
proof end;

theorem Th5: :: IDEAL_1:5
for L being non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr holds {(0. L)} is left-ideal
proof end;

theorem Th6: :: IDEAL_1:6
for L being non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr holds {(0. L)} is right-ideal
proof end;

registration
let L be non empty right_zeroed addLoopStr ;
cluster {(0. L)} -> add-closed for Subset of L;
coherence
for b1 being Subset of L st b1 = {(0. L)} holds
b1 is add-closed by Th4;
end;

registration
let L be non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr ;
cluster {(0. L)} -> left-ideal for Subset of L;
coherence
for b1 being Subset of L st b1 = {(0. L)} holds
b1 is left-ideal by Th5;
end;

registration
let L be non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr ;
cluster {(0. L)} -> right-ideal for Subset of L;
coherence
for b1 being Subset of L st b1 = {(0. L)} holds
b1 is right-ideal by Th6;
end;

theorem :: IDEAL_1:7
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr holds {(0. L)} is Ideal of L ;

theorem :: IDEAL_1:8
for L being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr holds {(0. L)} is LeftIdeal of L ;

theorem :: IDEAL_1:9
for L being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr holds {(0. L)} is RightIdeal of L ;

theorem Th10: :: IDEAL_1:10
for L being non empty doubleLoopStr holds the carrier of L is Ideal of L
proof end;

theorem Th11: :: IDEAL_1:11
for L being non empty doubleLoopStr holds the carrier of L is LeftIdeal of L
proof end;

theorem Th12: :: IDEAL_1:12
for L being non empty doubleLoopStr holds the carrier of L is RightIdeal of L
proof end;

definition
let R be non empty add-cancelable right_zeroed distributive left_zeroed doubleLoopStr ;
let I be Ideal of R;
:: original: trivial
redefine attr I is trivial means :: IDEAL_1:def 4
I = {(0. R)};
compatibility
( I is trivial iff I = {(0. R)} )
proof end;
end;

:: deftheorem defines trivial IDEAL_1:def 4 :
for R being non empty add-cancelable right_zeroed distributive left_zeroed doubleLoopStr
for I being Ideal of R holds
( I is trivial iff I = {(0. R)} );

registration
let R be non empty non trivial add-cancelable right_zeroed distributive left_zeroed doubleLoopStr ;
cluster non empty proper add-closed left-ideal right-ideal for Element of bool the carrier of R;
existence
ex b1 being Ideal of R st b1 is proper
proof end;
end;

theorem Th13: :: IDEAL_1:13
for L being non empty right_complementable add-associative right_zeroed left-distributive left_unital doubleLoopStr
for I being non empty left-ideal Subset of L
for x being Element of L st x in I holds
- x in I
proof end;

theorem Th14: :: IDEAL_1:14
for L being non empty right_complementable add-associative right_zeroed right-distributive right_unital doubleLoopStr
for I being non empty right-ideal Subset of L
for x being Element of L st x in I holds
- x in I
proof end;

theorem :: IDEAL_1:15
for L being non empty right_complementable add-associative right_zeroed left-distributive left_unital doubleLoopStr
for I being LeftIdeal of L
for x, y being Element of L st x in I & y in I holds
x - y in I
proof end;

theorem :: IDEAL_1:16
for L being non empty right_complementable add-associative right_zeroed right-distributive right_unital doubleLoopStr
for I being RightIdeal of L
for x, y being Element of L st x in I & y in I holds
x - y in I
proof end;

theorem Th17: :: IDEAL_1:17
for R being non empty add-cancelable add-associative right_zeroed distributive left_zeroed doubleLoopStr
for I being non empty add-closed right-ideal Subset of R
for a being Element of I
for n being Element of NAT holds n * a in I
proof end;

theorem :: IDEAL_1:18
for R being non empty add-cancelable right_zeroed well-unital distributive associative left_zeroed doubleLoopStr
for I being non empty right-ideal Subset of R
for a being Element of I
for n being Element of NAT st n <> 0 holds
a |^ n in I
proof end;

definition
let R be non empty addLoopStr ;
let I be non empty add-closed Subset of R;
func add| (I,R) -> BinOp of I equals :: IDEAL_1:def 5
 the addF of R || I;
coherence
the addF of R || I is BinOp of I
proof end;
end;

:: deftheorem defines add| IDEAL_1:def 5 :
for R being non empty addLoopStr
for I being non empty add-closed Subset of R holds add| (I,R) = the addF of R || I;

definition
let R be non empty multMagma ;
let I be non empty right-ideal Subset of R;
func mult| (I,R) -> BinOp of I equals :: IDEAL_1:def 6
 the multF of R || I;
coherence
the multF of R || I is BinOp of I
proof end;
end;

:: deftheorem defines mult| IDEAL_1:def 6 :
for R being non empty multMagma
for I being non empty right-ideal Subset of R holds mult| (I,R) = the multF of R || I;

definition
let R be non empty addLoopStr ;
let I be non empty add-closed Subset of R;
func Gr (I,R) -> non empty addLoopStr equals :: IDEAL_1:def 7
 addLoopStr(# I,(add| (I,R)),(In ((0. R),I)) #);
coherence
addLoopStr(# I,(add| (I,R)),(In ((0. R),I)) #) is non empty addLoopStr ;
end;

:: deftheorem defines Gr IDEAL_1:def 7 :
for R being non empty addLoopStr
for I being non empty add-closed Subset of R holds Gr (I,R) = addLoopStr(# I,(add| (I,R)),(In ((0. R),I)) #);

registration
let R be non empty add-cancelable add-associative right_zeroed distributive left_zeroed doubleLoopStr ;
let I be non empty add-closed Subset of R;
cluster Gr (I,R) -> non empty add-associative ;
coherence
Gr (I,R) is add-associative
proof end;
end;

registration
let R be non empty add-cancelable add-associative right_zeroed distributive left_zeroed doubleLoopStr ;
let I be non empty add-closed right-ideal Subset of R;
cluster Gr (I,R) -> non empty right_zeroed ;
coherence
Gr (I,R) is right_zeroed
proof end;
end;

registration
let R be non empty Abelian doubleLoopStr ;
let I be non empty add-closed Subset of R;
cluster Gr (I,R) -> non empty Abelian ;
coherence
Gr (I,R) is Abelian
proof end;
end;

registration
let R be non empty right_complementable Abelian add-associative right_zeroed right_unital distributive left_zeroed doubleLoopStr ;
let I be non empty add-closed right-ideal Subset of R;
cluster Gr (I,R) -> non empty right_complementable ;
coherence
Gr (I,R) is right_complementable
proof end;
end;

Lm1: for R being comRing
for a being Element of R holds { (a * r) where r is Element of R : verum } is Ideal of R
proof end;

theorem Th19: :: IDEAL_1:19
for R being non empty right_unital doubleLoopStr
for I being non empty left-ideal Subset of R holds
( I is proper iff not 1. R in I )
proof end;

theorem :: IDEAL_1:20
for R being non empty right_unital left_unital doubleLoopStr
for I being non empty right-ideal Subset of R holds
( I is proper iff for u being Element of R st u is unital holds
not u in I )
proof end;

theorem :: IDEAL_1:21
for R being non empty right_unital doubleLoopStr
for I being non empty left-ideal right-ideal Subset of R holds
( I is proper iff for u being Element of R st u is unital holds
not u in I )
proof end;

theorem :: IDEAL_1:22
for R being non degenerated comRing holds
( R is Field iff for I being Ideal of R holds
( I = {(0. R)} or I = the carrier of R ) )
proof end;

definition
let R be non empty multLoopStr ;
let A be non empty Subset of R;
mode LinearCombination of A -> FinSequence of the carrier of R means :Def8: :: IDEAL_1:def 8
 for i being set st i in dom it holds
ex u, v being Element of R ex a being Element of A st it /. i = (u * a) * v;
existence
ex b1 being FinSequence of the carrier of R st
for i being set st i in dom b1 holds
ex u, v being Element of R ex a being Element of A st b1 /. i = (u * a) * v
proof end;
mode LeftLinearCombination of A -> FinSequence of the carrier of R means :Def9: :: IDEAL_1:def 9
 for i being set st i in dom it holds
ex u being Element of R ex a being Element of A st it /. i = u * a;
existence
ex b1 being FinSequence of the carrier of R st
for i being set st i in dom b1 holds
ex u being Element of R ex a being Element of A st b1 /. i = u * a
proof end;
mode RightLinearCombination of A -> FinSequence of the carrier of R means :Def10: :: IDEAL_1:def 10
 for i being set st i in dom it holds
ex u being Element of R ex a being Element of A st it /. i = a * u;
existence
ex b1 being FinSequence of the carrier of R st
for i being set st i in dom b1 holds
ex u being Element of R ex a being Element of A st b1 /. i = a * u
proof end;
end;

:: deftheorem Def8 defines LinearCombination IDEAL_1:def 8 :
for R being non empty multLoopStr
for A being non empty Subset of R
for b3 being FinSequence of the carrier of R holds
( b3 is LinearCombination of A iff for i being set st i in dom b3 holds
ex u, v being Element of R ex a being Element of A st b3 /. i = (u * a) * v );

:: deftheorem Def9 defines LeftLinearCombination IDEAL_1:def 9 :
for R being non empty multLoopStr
for A being non empty Subset of R
for b3 being FinSequence of the carrier of R holds
( b3 is LeftLinearCombination of A iff for i being set st i in dom b3 holds
ex u being Element of R ex a being Element of A st b3 /. i = u * a );

:: deftheorem Def10 defines RightLinearCombination IDEAL_1:def 10 :
for R being non empty multLoopStr
for A being non empty Subset of R
for b3 being FinSequence of the carrier of R holds
( b3 is RightLinearCombination of A iff for i being set st i in dom b3 holds
ex u being Element of R ex a being Element of A st b3 /. i = a * u );

registration
let R be non empty multLoopStr ;
let A be non empty Subset of R;
cluster non empty Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like for LinearCombination of A;
existence
not for b1 being LinearCombination of A holds b1 is empty
proof end;
cluster non empty Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like for LeftLinearCombination of A;
existence
not for b1 being LeftLinearCombination of A holds b1 is empty
proof end;
cluster non empty Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like for RightLinearCombination of A;
existence
not for b1 being RightLinearCombination of A holds b1 is empty
proof end;
end;

definition
let R be non empty multLoopStr ;
let A, B be non empty Subset of R;
let F be LinearCombination of A;
let G be LinearCombination of B;
:: original: ^
redefine func F ^ G -> LinearCombination of A \/ B;
coherence
F ^ G is LinearCombination of A \/ B
proof end;
end;

theorem Th23: :: IDEAL_1:23
for R being non empty associative multLoopStr
for A being non empty Subset of R
for a being Element of R
for F being LinearCombination of A holds a * F is LinearCombination of A
proof end;

theorem Th24: :: IDEAL_1:24
for R being non empty associative multLoopStr
for A being non empty Subset of R
for a being Element of R
for F being LinearCombination of A holds F * a is LinearCombination of A
proof end;

theorem Th25: :: IDEAL_1:25
for R being non empty right_unital multLoopStr
for A being non empty Subset of R
for f being LeftLinearCombination of A holds f is LinearCombination of A
proof end;

definition
let R be non empty multLoopStr ;
let A, B be non empty Subset of R;
let F be LeftLinearCombination of A;
let G be LeftLinearCombination of B;
:: original: ^
redefine func F ^ G -> LeftLinearCombination of A \/ B;
coherence
F ^ G is LeftLinearCombination of A \/ B
proof end;
end;

theorem Th26: :: IDEAL_1:26
for R being non empty associative multLoopStr
for A being non empty Subset of R
for a being Element of R
for F being LeftLinearCombination of A holds a * F is LeftLinearCombination of A
proof end;

theorem :: IDEAL_1:27
for R being non empty multLoopStr
for A being non empty Subset of R
for a being Element of R
for F being LeftLinearCombination of A holds F * a is LinearCombination of A
proof end;

theorem Th28: :: IDEAL_1:28
for R being non empty left_unital multLoopStr
for A being non empty Subset of R
for f being RightLinearCombination of A holds f is LinearCombination of A
proof end;

definition
let R be non empty multLoopStr ;
let A, B be non empty Subset of R;
let F be RightLinearCombination of A;
let G be RightLinearCombination of B;
:: original: ^
redefine func F ^ G -> RightLinearCombination of A \/ B;
coherence
F ^ G is RightLinearCombination of A \/ B
proof end;
end;

theorem Th29: :: IDEAL_1:29
for R being non empty associative multLoopStr
for A being non empty Subset of R
for a being Element of R
for F being RightLinearCombination of A holds F * a is RightLinearCombination of A
proof end;

theorem :: IDEAL_1:30
for R being non empty associative multLoopStr
for A being non empty Subset of R
for a being Element of R
for F being RightLinearCombination of A holds a * F is LinearCombination of A
proof end;

theorem Th31: :: IDEAL_1:31
for R being non empty associative commutative multLoopStr
for A being non empty Subset of R
for f being LinearCombination of A holds
( f is LeftLinearCombination of A & f is RightLinearCombination of A )
proof end;

theorem Th32: :: IDEAL_1:32
for S being non empty doubleLoopStr
for F being non empty Subset of S
for lc being non empty LinearCombination of F ex p being LinearCombination of F ex e being Element of S st
( lc = p ^ <*e*> & <*e*> is LinearCombination of F )
proof end;

theorem Th33: :: IDEAL_1:33
for S being non empty doubleLoopStr
for F being non empty Subset of S
for lc being non empty LeftLinearCombination of F ex p being LeftLinearCombination of F ex e being Element of S st
( lc = p ^ <*e*> & <*e*> is LeftLinearCombination of F )
proof end;

theorem Th34: :: IDEAL_1:34
for S being non empty doubleLoopStr
for F being non empty Subset of S
for lc being non empty RightLinearCombination of F ex p being RightLinearCombination of F ex e being Element of S st
( lc = p ^ <*e*> & <*e*> is RightLinearCombination of F )
proof end;

definition
let R be non empty multLoopStr ;
let A be non empty Subset of R;
let L be LinearCombination of A;
let E be FinSequence of [: the carrier of R, the carrier of R, the carrier of R:];
pred E represents L means :: IDEAL_1:def 11
( len E = len L & ( for i being set st i in dom L holds
( L . i = (((E /. i) `1_3) * ((E /. i) `2_3)) * ((E /. i) `3_3) & (E /. i) `2_3 in A ) ) );
end;

:: deftheorem defines represents IDEAL_1:def 11 :
for R being non empty multLoopStr
for A being non empty Subset of R
for L being LinearCombination of A
for E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] holds
( E represents L iff ( len E = len L & ( for i being set st i in dom L holds
( L . i = (((E /. i) `1_3) * ((E /. i) `2_3)) * ((E /. i) `3_3) & (E /. i) `2_3 in A ) ) ) );

theorem :: IDEAL_1:35
for R being non empty multLoopStr
for A being non empty Subset of R
for L being LinearCombination of A ex E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] st E represents L
proof end;

theorem :: IDEAL_1:36
for R, S being non empty multLoopStr
for F being non empty Subset of R
for lc being LinearCombination of F
for G being non empty Subset of S
for P being Function of the carrier of R, the carrier of S
for E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] st P .: F c= G & E represents lc holds
ex LC being LinearCombination of G st
( len lc = len LC & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) )
proof end;

definition
let R be non empty multLoopStr ;
let A be non empty Subset of R;
let L be LeftLinearCombination of A;
let E be FinSequence of [: the carrier of R, the carrier of R:];
pred E represents L means :: IDEAL_1:def 12
( len E = len L & ( for i being set st i in dom L holds
( L . i = ((E /. i) `1) * ((E /. i) `2) & (E /. i) `2 in A ) ) );
end;

:: deftheorem defines represents IDEAL_1:def 12 :
for R being non empty multLoopStr
for A being non empty Subset of R
for L being LeftLinearCombination of A
for E being FinSequence of [: the carrier of R, the carrier of R:] holds
( E represents L iff ( len E = len L & ( for i being set st i in dom L holds
( L . i = ((E /. i) `1) * ((E /. i) `2) & (E /. i) `2 in A ) ) ) );

theorem :: IDEAL_1:37
for R being non empty multLoopStr
for A being non empty Subset of R
for L being LeftLinearCombination of A ex E being FinSequence of [: the carrier of R, the carrier of R:] st E represents L
proof end;

theorem :: IDEAL_1:38
for R, S being non empty multLoopStr
for F being non empty Subset of R
for lc being LeftLinearCombination of F
for G being non empty Subset of S
for P being Function of the carrier of R, the carrier of S
for E being FinSequence of [: the carrier of R, the carrier of R:] st P .: F c= G & E represents lc holds
ex LC being LeftLinearCombination of G st
( len lc = len LC & ( for i being set st i in dom LC holds
LC . i = (P . ((E /. i) `1)) * (P . ((E /. i) `2)) ) )
proof end;

definition
let R be non empty multLoopStr ;
let A be non empty Subset of R;
let L be RightLinearCombination of A;
let E be FinSequence of [: the carrier of R, the carrier of R:];
pred E represents L means :: IDEAL_1:def 13
( len E = len L & ( for i being set st i in dom L holds
( L . i = ((E /. i) `1) * ((E /. i) `2) & (E /. i) `1 in A ) ) );
end;

:: deftheorem defines represents IDEAL_1:def 13 :
for R being non empty multLoopStr
for A being non empty Subset of R
for L being RightLinearCombination of A
for E being FinSequence of [: the carrier of R, the carrier of R:] holds
( E represents L iff ( len E = len L & ( for i being set st i in dom L holds
( L . i = ((E /. i) `1) * ((E /. i) `2) & (E /. i) `1 in A ) ) ) );

theorem :: IDEAL_1:39
for R being non empty multLoopStr
for A being non empty Subset of R
for L being RightLinearCombination of A ex E being FinSequence of [: the carrier of R, the carrier of R:] st E represents L
proof end;

theorem :: IDEAL_1:40
for R, S being non empty multLoopStr
for F being non empty Subset of R
for lc being RightLinearCombination of F
for G being non empty Subset of S
for P being Function of the carrier of R, the carrier of S
for E being FinSequence of [: the carrier of R, the carrier of R:] st P .: F c= G & E represents lc holds
ex LC being RightLinearCombination of G st
( len lc = len LC & ( for i being set st i in dom LC holds
LC . i = (P . ((E /. i) `1)) * (P . ((E /. i) `2)) ) )
proof end;

theorem :: IDEAL_1:41
for R being non empty multLoopStr
for A being non empty Subset of R
for l being LinearCombination of A
for n being Nat holds l | (Seg n) is LinearCombination of A
proof end;

theorem :: IDEAL_1:42
for R being non empty multLoopStr
for A being non empty Subset of R
for l being LeftLinearCombination of A
for n being Nat holds l | (Seg n) is LeftLinearCombination of A
proof end;

theorem :: IDEAL_1:43
for R being non empty multLoopStr
for A being non empty Subset of R
for l being RightLinearCombination of A
for n being Nat holds l | (Seg n) is RightLinearCombination of A
proof end;

definition
let L be non empty doubleLoopStr ;
let F be Subset of L;
assume A1: not F is empty ;
func F -Ideal -> Ideal of L means :Def14: :: IDEAL_1:def 14
( F c= it & ( for I being Ideal of L st F c= I holds
it c= I ) );
existence
ex b1 being Ideal of L st
( F c= b1 & ( for I being Ideal of L st F c= I holds
b1 c= I ) )
proof end;
uniqueness
for b1, b2 being Ideal of L st F c= b1 & ( for I being Ideal of L st F c= I holds
b1 c= I ) & F c= b2 & ( for I being Ideal of L st F c= I holds
b2 c= I ) holds
b1 = b2 ;
func F -LeftIdeal -> LeftIdeal of L means :Def15: :: IDEAL_1:def 15
( F c= it & ( for I being LeftIdeal of L st F c= I holds
it c= I ) );
existence
ex b1 being LeftIdeal of L st
( F c= b1 & ( for I being LeftIdeal of L st F c= I holds
b1 c= I ) )
proof end;
uniqueness
for b1, b2 being LeftIdeal of L st F c= b1 & ( for I being LeftIdeal of L st F c= I holds
b1 c= I ) & F c= b2 & ( for I being LeftIdeal of L st F c= I holds
b2 c= I ) holds
b1 = b2 ;
func F -RightIdeal -> RightIdeal of L means :Def16: :: IDEAL_1:def 16
( F c= it & ( for I being RightIdeal of L st F c= I holds
it c= I ) );
existence
ex b1 being RightIdeal of L st
( F c= b1 & ( for I being RightIdeal of L st F c= I holds
b1 c= I ) )
proof end;
uniqueness
for b1, b2 being RightIdeal of L st F c= b1 & ( for I being RightIdeal of L st F c= I holds
b1 c= I ) & F c= b2 & ( for I being RightIdeal of L st F c= I holds
b2 c= I ) holds
b1 = b2 ;
end;

:: deftheorem Def14 defines -Ideal IDEAL_1:def 14 :
for L being non empty doubleLoopStr
for F being Subset of L st not F is empty holds
for b3 being Ideal of L holds
( b3 = F -Ideal iff ( F c= b3 & ( for I being Ideal of L st F c= I holds
b3 c= I ) ) );

:: deftheorem Def15 defines -LeftIdeal IDEAL_1:def 15 :
for L being non empty doubleLoopStr
for F being Subset of L st not F is empty holds
for b3 being LeftIdeal of L holds
( b3 = F -LeftIdeal iff ( F c= b3 & ( for I being LeftIdeal of L st F c= I holds
b3 c= I ) ) );

:: deftheorem Def16 defines -RightIdeal IDEAL_1:def 16 :
for L being non empty doubleLoopStr
for F being Subset of L st not F is empty holds
for b3 being RightIdeal of L holds
( b3 = F -RightIdeal iff ( F c= b3 & ( for I being RightIdeal of L st F c= I holds
b3 c= I ) ) );

theorem Th44: :: IDEAL_1:44
for L being non empty doubleLoopStr
for I being Ideal of L holds I -Ideal = I by Def14;

theorem Th45: :: IDEAL_1:45
for L being non empty doubleLoopStr
for I being LeftIdeal of L holds I -LeftIdeal = I by Def15;

theorem Th46: :: IDEAL_1:46
for L being non empty doubleLoopStr
for I being RightIdeal of L holds I -RightIdeal = I by Def16;

definition
let L be non empty doubleLoopStr ;
let I be Ideal of L;
mode Basis of I -> non empty Subset of L means :: IDEAL_1:def 17
it -Ideal = I;
existence
ex b1 being non empty Subset of L st b1 -Ideal = I
proof end;
end;

:: deftheorem defines Basis IDEAL_1:def 17 :
for L being non empty doubleLoopStr
for I being Ideal of L
for b3 being non empty Subset of L holds
( b3 is Basis of I iff b3 -Ideal = I );

theorem :: IDEAL_1:47
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr holds {(0. L)} -Ideal = {(0. L)} by Th44;

theorem :: IDEAL_1:48
for L being non empty add-cancelable right_zeroed distributive left_zeroed doubleLoopStr holds {(0. L)} -Ideal = {(0. L)} by Th44;

theorem :: IDEAL_1:49
for L being non empty right_add-cancelable right_zeroed right-distributive left_zeroed doubleLoopStr holds {(0. L)} -LeftIdeal = {(0. L)} by Th45;

theorem :: IDEAL_1:50
for L being non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr holds {(0. L)} -RightIdeal = {(0. L)} by Th46;

theorem :: IDEAL_1:51
for L being non empty well-unital doubleLoopStr holds {(1. L)} -Ideal = the carrier of L
proof end;

theorem :: IDEAL_1:52
for L being non empty right_unital doubleLoopStr holds {(1. L)} -LeftIdeal = the carrier of L
proof end;

theorem :: IDEAL_1:53
for L being non empty left_unital doubleLoopStr holds {(1. L)} -RightIdeal = the carrier of L
proof end;

theorem :: IDEAL_1:54
for L being non empty doubleLoopStr holds ([#] L) -Ideal = the carrier of L by Def14;

theorem :: IDEAL_1:55
for L being non empty doubleLoopStr holds ([#] L) -LeftIdeal = the carrier of L by Def15;

theorem :: IDEAL_1:56
for L being non empty doubleLoopStr holds ([#] L) -RightIdeal = the carrier of L by Def16;

theorem Th57: :: IDEAL_1:57
for L being non empty doubleLoopStr
for A, B being non empty Subset of L st A c= B holds
A -Ideal c= B -Ideal
proof end;

theorem :: IDEAL_1:58
for L being non empty doubleLoopStr
for A, B being non empty Subset of L st A c= B holds
A -LeftIdeal c= B -LeftIdeal
proof end;

theorem :: IDEAL_1:59
for L being non empty doubleLoopStr
for A, B being non empty Subset of L st A c= B holds
A -RightIdeal c= B -RightIdeal
proof end;

theorem Th60: :: IDEAL_1:60
for L being non empty add-cancelable add-associative right_zeroed well-unital distributive associative left_zeroed doubleLoopStr
for F being non empty Subset of L
for x being set holds
( x in F -Ideal iff ex f being LinearCombination of F st x = Sum f )
proof end;

theorem Th61: :: IDEAL_1:61
for L being non empty add-cancelable add-associative right_zeroed well-unital distributive associative left_zeroed doubleLoopStr
for F being non empty Subset of L
for x being set holds
( x in F -LeftIdeal iff ex f being LeftLinearCombination of F st x = Sum f )
proof end;

theorem Th62: :: IDEAL_1:62
for L being non empty add-cancelable add-associative right_zeroed well-unital distributive associative left_zeroed doubleLoopStr
for F being non empty Subset of L
for x being set holds
( x in F -RightIdeal iff ex f being RightLinearCombination of F st x = Sum f )
proof end;

theorem Th63: :: IDEAL_1:63
for R being non empty add-cancelable add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr
for F being non empty Subset of R holds
( F -Ideal = F -LeftIdeal & F -Ideal = F -RightIdeal )
proof end;

theorem Th64: :: IDEAL_1:64
for R being non empty add-cancelable add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr
for a being Element of R holds {a} -Ideal = { (a * r) where r is Element of R : verum }
proof end;

theorem Th65: :: IDEAL_1:65
for R being non empty add-cancelable Abelian add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr
for a, b being Element of R holds {a,b} -Ideal = { ((a * r) + (b * s)) where r, s is Element of R : verum }
proof end;

theorem Th66: :: IDEAL_1:66
for R being non empty doubleLoopStr
for a being Element of R holds a in {a} -Ideal
proof end;

theorem :: IDEAL_1:67
for R being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr
for A being non empty Subset of R
for a being Element of R st a in A -Ideal holds
{a} -Ideal c= A -Ideal
proof end;

Lm2: for a, b being set holds {a} c= {a,b}
proof end;

theorem :: IDEAL_1:68
for R being non empty doubleLoopStr
for a, b being Element of R holds
( a in {a,b} -Ideal & b in {a,b} -Ideal )
proof end;

theorem :: IDEAL_1:69
for R being non empty doubleLoopStr
for a, b being Element of R holds
( {a} -Ideal c= {a,b} -Ideal & {b} -Ideal c= {a,b} -Ideal ) by Lm2, Th57;

definition
let R be non empty multMagma ;
let I be Subset of R;
let a be Element of R;
func a * I -> Subset of R equals :: IDEAL_1:def 18
 { (a * i) where i is Element of R : i in I } ;
coherence
{ (a * i) where i is Element of R : i in I } is Subset of R
proof end;
end;

:: deftheorem defines * IDEAL_1:def 18 :
for R being non empty multMagma
for I being Subset of R
for a being Element of R holds a * I = { (a * i) where i is Element of R : i in I } ;

registration
let R be non empty multLoopStr ;
let I be non empty Subset of R;
let a be Element of R;
cluster a * I -> non empty ;
coherence
not a * I is empty
proof end;
end;

registration
let R be non empty distributive doubleLoopStr ;
let I be add-closed Subset of R;
let a be Element of R;
cluster a * I -> add-closed ;
coherence
a * I is add-closed
proof end;
end;

registration
let R be non empty associative doubleLoopStr ;
let I be right-ideal Subset of R;
let a be Element of R;
cluster a * I -> right-ideal ;
coherence
a * I is right-ideal
proof end;
end;

theorem Th70: :: IDEAL_1:70
for R being non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr
for I being non empty Subset of R holds (0. R) * I = {(0. R)}
proof end;

theorem :: IDEAL_1:71
for R being non empty left_unital doubleLoopStr
for I being Subset of R holds (1. R) * I = I
proof end;

definition
let R be addMagma ;
let I, J be Subset of R;
func I + J -> Subset of R equals :: IDEAL_1:def 19
 { (a + b) where a, b is Element of R : ( a in I & b in J ) } ;
coherence
{ (a + b) where a, b is Element of R : ( a in I & b in J ) } is Subset of R
proof end;
end;

:: deftheorem defines + IDEAL_1:def 19 :
for R being addMagma
for I, J being Subset of R holds I + J = { (a + b) where a, b is Element of R : ( a in I & b in J ) } ;

registration
let R be non empty addLoopStr ;
let I, J be non empty Subset of R;
cluster I + J -> non empty ;
coherence
not I + J is empty
proof end;
end;

definition
let R be non empty Abelian addLoopStr ;
let I, J be Subset of R;
:: original: +
redefine func I + J -> Subset of R;
commutativity
for I, J being Subset of R holds I + J = J + I
proof end;
end;

registration
let R be non empty Abelian add-associative addLoopStr ;
let I, J be add-closed Subset of R;
cluster I + J -> add-closed ;
coherence
I + J is add-closed
proof end;
end;

registration
let R be non empty left-distributive doubleLoopStr ;
let I, J be right-ideal Subset of R;
cluster I + J -> right-ideal ;
coherence
I + J is right-ideal
proof end;
end;

registration
let R be non empty right-distributive doubleLoopStr ;
let I, J be left-ideal Subset of R;
cluster I + J -> left-ideal ;
coherence
I + J is left-ideal
proof end;
end;

theorem :: IDEAL_1:72
for R being non empty add-associative addLoopStr
for I, J, K being Subset of R holds I + (J + K) = (I + J) + K
proof end;

theorem Th73: :: IDEAL_1:73
for R being non empty right_add-cancelable right_zeroed right-distributive left_zeroed doubleLoopStr
for I, J being non empty right-ideal Subset of R holds I c= I + J
proof end;

theorem Th74: :: IDEAL_1:74
for R being non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr
for I, J being non empty right-ideal Subset of R holds J c= I + J
proof end;

theorem :: IDEAL_1:75
for R being non empty addLoopStr
for I, J being Subset of R
for K being add-closed Subset of R st I c= K & J c= K holds
I + J c= K
proof end;

theorem :: IDEAL_1:76
for R being non empty add-cancelable Abelian add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr
for a, b being Element of R holds {a,b} -Ideal = ({a} -Ideal) + ({b} -Ideal)
proof end;

definition
let R be non empty 1-sorted ;
let I, J be Subset of R;
:: original: /\
redefine func I /\ J -> Subset of R equals :: IDEAL_1:def 20
 { x where x is Element of R : ( x in I & x in J ) } ;
coherence
I /\ J is Subset of R
proof end;
compatibility
for b1 being Subset of R holds
( b1 = I /\ J iff b1 = { x where x is Element of R : ( x in I & x in J ) } )
proof end;
end;

:: deftheorem defines /\ IDEAL_1:def 20 :
for R being non empty 1-sorted
for I, J being Subset of R holds I /\ J = { x where x is Element of R : ( x in I & x in J ) } ;

registration
let R be non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr ;
let I, J be non empty left-ideal Subset of R;
cluster I /\ J -> non empty ;
coherence
not I /\ J is empty
proof end;
end;

registration
let R be non empty addLoopStr ;
let I, J be add-closed Subset of R;
cluster I /\ J -> add-closed for Subset of R;
coherence
for b1 being Subset of R st b1 = I /\ J holds
b1 is add-closed
proof end;
end;

registration
let R be non empty multLoopStr ;
let I, J be left-ideal Subset of R;
cluster I /\ J -> left-ideal for Subset of R;
coherence
for b1 being Subset of R st b1 = I /\ J holds
b1 is left-ideal
proof end;
end;

registration
let R be non empty multLoopStr ;
let I, J be right-ideal Subset of R;
cluster I /\ J -> right-ideal for Subset of R;
coherence
for b1 being Subset of R st b1 = I /\ J holds
b1 is right-ideal
proof end;
end;

theorem :: IDEAL_1:77
for R being non empty right_complementable Abelian add-associative right_zeroed left-distributive left_unital left_zeroed doubleLoopStr
for I being non empty add-closed left-ideal Subset of R
for J being Subset of R
for K being non empty Subset of R st J c= I holds
I /\ (J + K) = J + (I /\ K)
proof end;

definition
let R be non empty doubleLoopStr ;
let I, J be Subset of R;
func I *' J -> Subset of R equals :: IDEAL_1:def 21
 { (Sum s) where s is FinSequence of the carrier of R : for i being Element of NAT st 1 <= i & i <= len s holds
ex a, b being Element of R st
( s . i = a * b & a in I & b in J ) } ;
coherence
{ (Sum s) where s is FinSequence of the carrier of R : for i being Element of NAT st 1 <= i & i <= len s holds
ex a, b being Element of R st
( s . i = a * b & a in I & b in J ) } is Subset of R
proof end;
end;

:: deftheorem defines *' IDEAL_1:def 21 :
for R being non empty doubleLoopStr
for I, J being Subset of R holds I *' J = { (Sum s) where s is FinSequence of the carrier of R : for i being Element of NAT st 1 <= i & i <= len s holds
ex a, b being Element of R st
( s . i = a * b & a in I & b in J ) } ;

registration
let R be non empty doubleLoopStr ;
let I, J be Subset of R;
cluster I *' J -> non empty ;
coherence
not I *' J is empty
proof end;
end;

definition
let R be non empty commutative doubleLoopStr ;
let I, J be Subset of R;
:: original: *'
redefine func I *' J -> Subset of R;
commutativity
for I, J being Subset of R holds I *' J = J *' I
proof end;
end;

registration
let R be non empty add-associative right_zeroed doubleLoopStr ;
let I, J be Subset of R;
cluster I *' J -> add-closed ;
coherence
I *' J is add-closed
proof end;
end;

registration
let R be non empty left_add-cancelable right_zeroed left-distributive associative doubleLoopStr ;
let I, J be right-ideal Subset of R;
cluster I *' J -> right-ideal ;
coherence
I *' J is right-ideal
proof end;
end;

registration
let R be non empty right_add-cancelable right-distributive associative left_zeroed doubleLoopStr ;
let I, J be left-ideal Subset of R;
cluster I *' J -> left-ideal ;
coherence
I *' J is left-ideal
proof end;
end;

theorem :: IDEAL_1:78
for R being non empty left_add-cancelable right_zeroed left-distributive left_zeroed doubleLoopStr
for I being non empty Subset of R holds {(0. R)} *' I = {(0. R)}
proof end;

theorem Th79: :: IDEAL_1:79
for R being non empty add-cancelable right_zeroed distributive left_zeroed doubleLoopStr
for I being non empty add-closed right-ideal Subset of R
for J being non empty add-closed left-ideal Subset of R holds I *' J c= I /\ J
proof end;

theorem Th80: :: IDEAL_1:80
for R being non empty add-cancelable Abelian add-associative right_zeroed distributive associative left_zeroed doubleLoopStr
for I, J, K being non empty right-ideal Subset of R holds I *' (J + K) = (I *' J) + (I *' K)
proof end;

theorem Th81: :: IDEAL_1:81
for R being non empty add-cancelable Abelian add-associative right_zeroed distributive associative commutative left_zeroed doubleLoopStr
for I, J being non empty right-ideal Subset of R holds (I + J) *' (I /\ J) c= I *' J
proof end;

theorem :: IDEAL_1:82
for R being non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr
for I, J being non empty add-closed left-ideal Subset of R holds (I + J) *' (I /\ J) c= I /\ J
proof end;

definition
let R be addMagma ;
let I, J be Subset of R;
pred I,J are_co-prime means :: IDEAL_1:def 22
I + J = the carrier of R;
end;

:: deftheorem defines are_co-prime IDEAL_1:def 22 :
for R being addMagma
for I, J being Subset of R holds
( I,J are_co-prime iff I + J = the carrier of R );

theorem Th83: :: IDEAL_1:83
for R being non empty left_unital left_zeroed doubleLoopStr
for I, J being non empty Subset of R st I,J are_co-prime holds
I /\ J c= (I + J) *' (I /\ J)
proof end;

theorem :: IDEAL_1:84
for R being non empty add-cancelable Abelian add-associative right_zeroed distributive left_unital associative commutative left_zeroed doubleLoopStr
for I being non empty add-closed left-ideal right-ideal Subset of R
for J being non empty add-closed left-ideal Subset of R st I,J are_co-prime holds
I *' J = I /\ J
proof end;

definition
let R be non empty multMagma ;
let I, J be Subset of R;
func I % J -> Subset of R equals :: IDEAL_1:def 23
 { a where a is Element of R : a * J c= I } ;
coherence
{ a where a is Element of R : a * J c= I } is Subset of R
proof end;
end;

:: deftheorem defines % IDEAL_1:def 23 :
for R being non empty multMagma
for I, J being Subset of R holds I % J = { a where a is Element of R : a * J c= I } ;

registration
let R be non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr ;
let I, J be non empty left-ideal Subset of R;
cluster I % J -> non empty ;
coherence
not I % J is empty
proof end;
end;

registration
let R be non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr ;
let I, J be non empty add-closed left-ideal Subset of R;
cluster I % J -> add-closed ;
coherence
I % J is add-closed
proof end;
end;

registration
let R be non empty left_add-cancelable right_zeroed left-distributive associative commutative doubleLoopStr ;
let I, J be non empty left-ideal Subset of R;
cluster I % J -> left-ideal ;
coherence
I % J is left-ideal
proof end;
cluster I % J -> right-ideal ;
coherence
I % J is right-ideal ;
end;

theorem :: IDEAL_1:85
for R being non empty multLoopStr
for I being non empty right-ideal Subset of R
for J being Subset of R holds I c= I % J
proof end;

theorem :: IDEAL_1:86
for R being non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr
for I being non empty add-closed left-ideal Subset of R
for J being Subset of R holds (I % J) *' J c= I
proof end;

theorem Th87: :: IDEAL_1:87
for R being non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr
for I being non empty add-closed right-ideal Subset of R
for J being Subset of R holds (I % J) *' J c= I
proof end;

theorem :: IDEAL_1:88
for R being non empty right_add-cancelable right-distributive associative commutative left_zeroed doubleLoopStr
for I being non empty add-closed right-ideal Subset of R
for J, K being Subset of R holds (I % J) % K = I % (J *' K)
proof end;

theorem :: IDEAL_1:89
for R being non empty multLoopStr
for I, J, K being Subset of R holds (J /\ K) % I = (J % I) /\ (K % I)
proof end;

theorem :: IDEAL_1:90
for R being non empty right_add-cancelable right_zeroed right-distributive left_zeroed doubleLoopStr
for I being add-closed Subset of R
for J, K being non empty right-ideal Subset of R holds I % (J + K) = (I % J) /\ (I % K)
proof end;

definition
let R be non empty well-unital doubleLoopStr ;
let I be Subset of R;
func sqrt I -> Subset of R equals :: IDEAL_1:def 24
 { a where a is Element of R : ex n being Element of NAT st a |^ n in I } ;
coherence
{ a where a is Element of R : ex n being Element of NAT st a |^ n in I } is Subset of R
proof end;
end;

:: deftheorem defines sqrt IDEAL_1:def 24 :
for R being non empty well-unital doubleLoopStr
for I being Subset of R holds sqrt I = { a where a is Element of R : ex n being Element of NAT st a |^ n in I } ;

registration
let R be non empty well-unital doubleLoopStr ;
let I be non empty Subset of R;
cluster sqrt I -> non empty ;
coherence
not sqrt I is empty
proof end;
end;

registration
let R be non empty add-cancelable Abelian add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr ;
let I be non empty add-closed right-ideal Subset of R;
cluster sqrt I -> add-closed ;
coherence
sqrt I is add-closed
proof end;
end;

registration
let R be non empty well-unital associative commutative doubleLoopStr ;
let I be non empty left-ideal Subset of R;
cluster sqrt I -> left-ideal ;
coherence
sqrt I is left-ideal
proof end;
cluster sqrt I -> right-ideal ;
coherence
sqrt I is right-ideal ;
end;

theorem :: IDEAL_1:91
for R being non empty well-unital associative doubleLoopStr
for I being non empty Subset of R
for a being Element of R holds
( a in sqrt I iff ex n being Element of NAT st a |^ n in sqrt I )
proof end;

theorem :: IDEAL_1:92
for R being non empty add-cancelable right_zeroed well-unital distributive associative left_zeroed doubleLoopStr
for I being non empty add-closed right-ideal Subset of R
for J being non empty add-closed left-ideal Subset of R holds sqrt (I *' J) = sqrt (I /\ J)
proof end;

definition
let L be non empty doubleLoopStr ;
let I be Ideal of L;
attr I is finitely_generated means :: IDEAL_1:def 25
 ex F being non empty finite Subset of L st I = F -Ideal ;
end;

:: deftheorem defines finitely_generated IDEAL_1:def 25 :
for L being non empty doubleLoopStr
for I being Ideal of L holds
( I is finitely_generated iff ex F being non empty finite Subset of L st I = F -Ideal );

registration
let L be non empty doubleLoopStr ;
cluster non empty add-closed left-ideal right-ideal finitely_generated for Element of bool the carrier of L;
existence
ex b1 being Ideal of L st b1 is finitely_generated
proof end;
end;

registration
let L be non empty doubleLoopStr ;
let F be non empty finite Subset of L;
cluster F -Ideal -> finitely_generated ;
coherence
F -Ideal is finitely_generated ;
end;

definition
let L be non empty doubleLoopStr ;
attr L is Noetherian means :Def26: :: IDEAL_1:def 26
 for I being Ideal of L holds I is finitely_generated ;
end;

:: deftheorem Def26 defines Noetherian IDEAL_1:def 26 :
for L being non empty doubleLoopStr holds
( L is Noetherian iff for I being Ideal of L holds I is finitely_generated );

registration
cluster non empty non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative Euclidian for doubleLoopStr ;
existence
ex b1 being non empty doubleLoopStr st
( b1 is Euclidian & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is well-unital & b1 is distributive & b1 is commutative & b1 is associative & not b1 is degenerated )
proof end;
end;

definition
let L be non empty doubleLoopStr ;
let I be Ideal of L;
attr I is principal means :: IDEAL_1:def 27
 ex e being Element of L st I = {e} -Ideal ;
end;

:: deftheorem defines principal IDEAL_1:def 27 :
for L being non empty doubleLoopStr
for I being Ideal of L holds
( I is principal iff ex e being Element of L st I = {e} -Ideal );

definition
let L be non empty doubleLoopStr ;
attr L is PID means :: IDEAL_1:def 28
 for I being Ideal of L holds I is principal ;
end;

:: deftheorem defines PID IDEAL_1:def 28 :
for L being non empty doubleLoopStr holds
( L is PID iff for I being Ideal of L holds I is principal );

theorem Th93: :: IDEAL_1:93
for L being non empty doubleLoopStr
for F being non empty Subset of L st F <> {(0. L)} holds
ex x being Element of L st
( x <> 0. L & x in F )
proof end;

theorem Th94: :: IDEAL_1:94
for R being non empty right_complementable add-associative right_zeroed well-unital distributive left_zeroed Euclidian doubleLoopStr holds R is PID
proof end;

theorem Th95: :: IDEAL_1:95
for L being non empty doubleLoopStr st L is PID holds
L is Noetherian
proof end;

registration
cluster INT.Ring -> Noetherian ;
coherence
INT.Ring is Noetherian
proof end;
end;

registration
cluster non empty non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative Noetherian for doubleLoopStr ;
existence
ex b1 being non empty doubleLoopStr st
( b1 is Noetherian & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is well-unital & b1 is distributive & b1 is commutative & b1 is associative & not b1 is degenerated )
proof end;
end;

theorem :: IDEAL_1:96
for R being non empty add-cancelable add-associative right_zeroed well-unital distributive associative left_zeroed Noetherian doubleLoopStr
for B being non empty Subset of R ex C being non empty finite Subset of R st
( C c= B & C -Ideal = B -Ideal )
proof end;

theorem :: IDEAL_1:97
for R being non empty doubleLoopStr st ( for B being non empty Subset of R ex C being non empty finite Subset of R st
( C c= B & C -Ideal = B -Ideal ) ) holds
for a being sequence of R ex m being Element of NAT st a . (m + 1) in (rng (a | (m + 1))) -Ideal
proof end;

registration
let X, Y be non empty set ;
let f be Function of X,Y;
let A be non empty Subset of X;
cluster f | A -> non empty ;
coherence
not f | A is empty
proof end;
end;

theorem :: IDEAL_1:98
for R being non empty doubleLoopStr st ( for a being sequence of R ex m being Element of NAT st a . (m + 1) in (rng (a | (m + 1))) -Ideal ) holds
for F being sequence of (bool the carrier of R) holds
( ex i being Nat st F . i is not Ideal of R or ex j, k being Nat st
( j < k & not F . j c< F . k ) )
proof end;

theorem :: IDEAL_1:99
for R being non empty doubleLoopStr st ( for F being sequence of (bool the carrier of R) holds
( ex i being Element of NAT st F . i is not Ideal of R or ex j, k being Element of NAT st
( j < k & not F . j c< F . k ) ) ) holds
R is Noetherian
proof end;