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


begin

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

registration
cluster non empty non trivial add-cancelable Abelian add-associative right_zeroed associative commutative well-unital distributive 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 )
proofend;
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
proofend;

begin

definition
let L be non empty addLoopStr ;
let F be Subset of L;
attrF is add-closed  means :Def1: :: IDEAL_1:def 1
 for x, y being Element of L st x in F &amp; 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 &amp; y in F holds
x + y in F );

definition
let L be non empty multMagma ;
let F be Subset of L;
attrF 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;
attrF 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
proofend;
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
proofend;
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
proofend;
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 &amp; b1 is left-ideal &amp; b1 is right-ideal )
proofend;
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 &amp; b1 is right-ideal )
proofend;
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 &amp; b1 is left-ideal )
proofend;
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
proofend;
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
proofend;
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
proofend;

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
proofend;

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

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

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

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
proofend;

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

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

definition
let R be non empty add-cancelable right_zeroed distributive left_zeroed doubleLoopStr ;
let I be Ideal of R;
:: original:trivial
redefine attrI is trivial  means :: IDEAL_1:def 4
I = {(0. R)};
compatibility
 ( I is trivial iff I = {(0. R)} )
proofend;
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
proofend;
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
proofend;

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
proofend;

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 &amp; y in I holds
x - y in I
proofend;

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 &amp; y in I holds
x - y in I
proofend;

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
proofend;

theorem :: IDEAL_1:18
for R being non empty add-cancelable right_zeroed associative well-unital distributive 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
proofend;

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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;

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

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

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

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

begin

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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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 funcF ^ G ->  LinearCombination of A \/ B;
coherence
 F ^ G is LinearCombination of A \/ B
proofend;
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
proofend;

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
proofend;

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
proofend;

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 funcF ^ G ->  LeftLinearCombination of A \/ B;
coherence
 F ^ G is LeftLinearCombination of A \/ B
proofend;
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
proofend;

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
proofend;

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
proofend;

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 funcF ^ G ->  RightLinearCombination of A \/ B;
coherence
 F ^ G is RightLinearCombination of A \/ B
proofend;
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
proofend;

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
proofend;

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 &amp; f is RightLinearCombination of A )
proofend;

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*> &amp; <*e*> is LinearCombination of F )
proofend;

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*> &amp; <*e*> is LeftLinearCombination of F )
proofend;

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*> &amp; <*e*> is RightLinearCombination of F )
proofend;

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:];
predE represents L means :Def11: :: IDEAL_1:def 11
( len E = len L &amp; ( for i being set st i in dom L holds
( L . i = (((E /. i) `1_3) * ((E /. i) `2_3)) * ((E /. i) `3_3) &amp; (E /. i) `2_3 in A ) ) );
end;

:: deftheorem Def11 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 &amp; ( for i being set st i in dom L holds
( L . i = (((E /. i) `1_3) * ((E /. i) `2_3)) * ((E /. i) `3_3) &amp; (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
proofend;

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 &amp; E represents lc holds
ex LC being LinearCombination of G st
( len lc = len LC &amp; ( 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)) ) )
proofend;

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:];
predE represents L means :Def12: :: IDEAL_1:def 12
( len E = len L &amp; ( for i being set st i in dom L holds
( L . i = ((E /. i) `1) * ((E /. i) `2) &amp; (E /. i) `2 in A ) ) );
end;

:: deftheorem Def12 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 &amp; ( for i being set st i in dom L holds
( L . i = ((E /. i) `1) * ((E /. i) `2) &amp; (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
proofend;

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 &amp; E represents lc holds
ex LC being LeftLinearCombination of G st
( len lc = len LC &amp; ( for i being set st i in dom LC holds
LC . i = (P . ((E /. i) `1)) * (P . ((E /. i) `2)) ) )
proofend;

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:];
predE represents L means :Def13: :: IDEAL_1:def 13
( len E = len L &amp; ( for i being set st i in dom L holds
( L . i = ((E /. i) `1) * ((E /. i) `2) &amp; (E /. i) `1 in A ) ) );
end;

:: deftheorem Def13 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 &amp; ( for i being set st i in dom L holds
( L . i = ((E /. i) `1) * ((E /. i) `2) &amp; (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
proofend;

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 &amp; E represents lc holds
ex LC being RightLinearCombination of G st
( len lc = len LC &amp; ( for i being set st i in dom LC holds
LC . i = (P . ((E /. i) `1)) * (P . ((E /. i) `2)) ) )
proofend;

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 Element of NAT holds l | (Seg n) is LinearCombination of A
proofend;

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 Element of NAT holds l | (Seg n) is LeftLinearCombination of A
proofend;

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 Element of NAT holds l | (Seg n) is RightLinearCombination of A
proofend;

begin

definition
let L be non empty doubleLoopStr ;
let F be Subset of L;
assume A1: not F is empty ;
funcF -Ideal  ->  Ideal of L means :Def14: :: IDEAL_1:def 14
( F c= it &amp; ( 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 &amp; ( for I being Ideal of L st F c= I holds
b1 c= I ) )
proofend;
uniqueness
 for b1, b2 being Ideal of L st F c= b1 &amp; ( for I being Ideal of L st F c= I holds
b1 c= I ) &amp; F c= b2 &amp; ( for I being Ideal of L st F c= I holds
b2 c= I ) holds
b1 = b2
proofend;
funcF -LeftIdeal  ->  LeftIdeal of L means :Def15: :: IDEAL_1:def 15
( F c= it &amp; ( 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 &amp; ( for I being LeftIdeal of L st F c= I holds
b1 c= I ) )
proofend;
uniqueness
 for b1, b2 being LeftIdeal of L st F c= b1 &amp; ( for I being LeftIdeal of L st F c= I holds
b1 c= I ) &amp; F c= b2 &amp; ( for I being LeftIdeal of L st F c= I holds
b2 c= I ) holds
b1 = b2
proofend;
funcF -RightIdeal  ->  RightIdeal of L means :Def16: :: IDEAL_1:def 16
( F c= it &amp; ( 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 &amp; ( for I being RightIdeal of L st F c= I holds
b1 c= I ) )
proofend;
uniqueness
 for b1, b2 being RightIdeal of L st F c= b1 &amp; ( for I being RightIdeal of L st F c= I holds
b1 c= I ) &amp; F c= b2 &amp; ( for I being RightIdeal of L st F c= I holds
b2 c= I ) holds
b1 = b2
proofend;
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 &amp; ( 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 &amp; ( 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 &amp; ( 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
proofend;

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

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

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
proofend;
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
proofend;

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

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

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

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

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

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
proofend;

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
proofend;

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
proofend;

theorem Th60: :: IDEAL_1:60
for L being non empty add-cancelable add-associative right_zeroed associative well-unital distributive 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 )
proofend;

theorem Th61: :: IDEAL_1:61
for L being non empty add-cancelable add-associative right_zeroed associative well-unital distributive 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 )
proofend;

theorem Th62: :: IDEAL_1:62
for L being non empty add-cancelable add-associative right_zeroed associative well-unital distributive 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 )
proofend;

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

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

theorem Th65: :: IDEAL_1:65
for R being non empty add-cancelable Abelian add-associative right_zeroed associative commutative well-unital distributive 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  }
proofend;

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

theorem :: IDEAL_1:67
for R being non empty right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive 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
proofend;

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

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

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

begin

definition
let R be non empty multMagma ;
let I be Subset of R;
let a be Element of R;
funca * 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
proofend;
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;
clustera * I ->  non empty ;
coherence
 not a * I is empty
proofend;
end;

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

registration
let R be non empty associative doubleLoopStr ;
let I be right-ideal Subset of R;
let a be Element of R;
clustera * I ->  right-ideal ;
coherence
 a * I is right-ideal
proofend;
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)}
proofend;

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

definition
let R be non empty addLoopStr ;
let I, J be Subset of R;
funcI + J ->  Subset of R equals :: IDEAL_1:def 19
 {  (a + b) where a, b is Element of R : ( a in I &amp; b in J )  }  ;
coherence
  {  (a + b) where a, b is Element of R : ( a in I &amp; b in J )  }  is Subset of R
proofend;
end;

:: deftheorem  defines + IDEAL_1:def_19_:_
 for R being non empty addLoopStr
for I, J being Subset of R holds I + J =  {  (a + b) where a, b is Element of R : ( a in I &amp; b in J )  }  ;

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

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

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

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

registration
let R be non empty right-distributive doubleLoopStr ;
let I, J be left-ideal Subset of R;
clusterI + J ->  left-ideal ;
coherence
 I + J is left-ideal
proofend;
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
proofend;

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
proofend;

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
proofend;

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 &amp; J c= K holds
I + J c= K
proofend;

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

definition
let R be non empty 1-sorted ;
let I, J be Subset of R;
:: original:/\
redefine funcI /\ J ->  Subset of R equals :: IDEAL_1:def 20
 {  x where x is Element of R : ( x in I &amp; x in J )  }  ;
coherence
 I /\ J is Subset of R
proofend;
compatibility
 for b1 being Subset of R holds
( b1 = I /\ J iff b1 =  {  x where x is Element of R : ( x in I &amp; x in J )  }  )
proofend;
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 &amp; 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;
clusterI /\ J ->  non empty ;
coherence
 not I /\ J is empty
proofend;
end;

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

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

registration
let R be non empty multLoopStr ;
let I, J be right-ideal Subset of R;
clusterI /\ J ->  right-ideal for Subset of R;
coherence
 for b1 being Subset of R st b1 = I /\ J holds
b1 is right-ideal
proofend;
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)
proofend;

definition
let R be non empty doubleLoopStr ;
let I, J be Subset of R;
funcI *' 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 &amp; i <= len s holds
ex a, b being Element of R st
( s . i = a * b &amp; a in I &amp; b in J )  }  ;
coherence
  {  (Sum s) where s is FinSequence of the carrier of R : for i being Element of NAT st 1 <= i &amp; i <= len s holds
ex a, b being Element of R st
( s . i = a * b &amp; a in I &amp; b in J )  }  is Subset of R
proofend;
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 &amp; i <= len s holds
ex a, b being Element of R st
( s . i = a * b &amp; a in I &amp; b in J )  }  ;

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

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

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

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

registration
let R be non empty right_add-cancelable associative right-distributive left_zeroed doubleLoopStr ;
let I, J be left-ideal Subset of R;
clusterI *' J ->  left-ideal ;
coherence
 I *' J is left-ideal
proofend;
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)}
proofend;

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
proofend;

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

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

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
proofend;

definition
let R be non empty addLoopStr ;
let I, J be Subset of R;
predI,J are_co-prime  means :Def22: :: IDEAL_1:def 22
I + J = the carrier of R;
end;

:: deftheorem Def22 defines are_co-prime IDEAL_1:def_22_:_
 for R being non empty addLoopStr
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)
proofend;

theorem :: IDEAL_1:84
for R being non empty add-cancelable Abelian add-associative right_zeroed associative commutative distributive left_unital 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
proofend;

definition
let R be non empty multMagma ;
let I, J be Subset of R;
funcI % 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
proofend;
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;
clusterI % J ->  non empty ;
coherence
 not I % J is empty
proofend;
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;
clusterI % J ->  add-closed ;
coherence
 I % J is add-closed
proofend;
end;

registration
let R be non empty left_add-cancelable right_zeroed associative commutative left-distributive doubleLoopStr ;
let I, J be non empty left-ideal Subset of R;
clusterI % J ->  left-ideal ;
coherence
 I % J is left-ideal
proofend;
clusterI % 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
proofend;

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
proofend;

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
proofend;

theorem :: IDEAL_1:88
for R being non empty right_add-cancelable associative commutative right-distributive 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)
proofend;

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

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

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
proofend;
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
proofend;
end;

registration
let R be non empty add-cancelable Abelian add-associative right_zeroed associative commutative well-unital distributive 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
proofend;
end;

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

theorem :: IDEAL_1:91
for R being non empty associative well-unital 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 )
proofend;

theorem :: IDEAL_1:92
for R being non empty add-cancelable right_zeroed associative well-unital 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 sqrt (I *' J) = sqrt (I /\ J)
proofend;

begin

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

:: deftheorem Def25 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
proofend;
end;

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

definition
let L be non empty doubleLoopStr ;
attrL 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 associative commutative well-unital distributive Euclidian for doubleLoopStr ;
existence
 ex b1 being non empty doubleLoopStr st
( b1 is Euclidian &amp; b1 is Abelian &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable &amp; b1 is well-unital &amp; b1 is distributive &amp; b1 is commutative &amp; b1 is associative &amp; not b1 is degenerated )
proofend;
end;

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

:: deftheorem Def27 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 ;
attrL is PID  means :Def28: :: IDEAL_1:def 28
 for I being Ideal of L holds I is principal ;
end;

:: deftheorem Def28 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 &amp; x in F )
proofend;

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
proofend;

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

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

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

theorem :: IDEAL_1:96
for R being non empty add-cancelable add-associative right_zeroed associative well-unital distributive 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 &amp; C -Ideal = B -Ideal )
proofend;

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 &amp; 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
proofend;

registration
let X, Y be non empty set ;
let f be Function of X,Y;
let A be non empty Subset of X;
clusterf | A ->  non empty ;
coherence
 not f | A is empty
proofend;
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 Function of NAT,(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 &amp; not F . j c< F . k ) )
proofend;

theorem :: IDEAL_1:99
for R being non empty doubleLoopStr st ( for F being Function of NAT,(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 &amp; not F . j c< F . k ) ) ) holds
R is Noetherian
proofend;