:: Ring Ideals
::  by Jonathan Backer , Piotr Rudnicki and Christoph Schwarzweller
::
:: Received November 20, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, RLVECT_1, ALGSTR_1, XBOOLE_0, ALGSTR_0, STRUCT_0,
      VECTSP_2, VECTSP_1, BINOP_1, LATTICES, ZFMISC_1, SUBSET_1, CARD_3,
      FINSEQ_1, ARYTM_3, ORDINAL4, RELAT_1, CARD_FIL, SUPINF_2, TARSKI,
      ARYTM_1, MESFUNC1, CARD_1, NEWTON, NAT_1, XXREAL_0, REALSET1, FUNCT_1,
      FUNCT_7, GROUP_1, PARTFUN1, PRELAMB, MCART_1, SETFAM_1, RLVECT_3, GCD_1,
      LATTICE3, SQUARE_1, FINSET_1, INT_3, XCMPLX_0, IDEAL_1, RECDEF_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, FUNCT_1,
      FINSEQ_1, ORDINAL1, REALSET1, INT_3, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0,
      NAT_1, RELSET_1, PARTFUN1, FUNCT_2, ALGSTR_1, XXREAL_2, XTUPLE_0,
      MCART_1, POLYNOM1, SETFAM_1, DOMAIN_1, FINSEQ_4, NEWTON, STRUCT_0,
      ALGSTR_0, RLVECT_1, VECTSP_1, GROUP_1, BINOP_1, VECTSP_2, FUNCT_7, GCD_1,
      BINOM;
 constructors SETFAM_1, BINOP_1, REALSET2, ALGSTR_1, GCD_1, INT_3, POLYNOM1,
      BINOM, XXREAL_2, RELSET_1, FUNCT_7, FVSUM_1, FINSEQ_4, XTUPLE_0, NEWTON;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_2, FINSET_1, XXREAL_0,
      XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, REALSET1, STRUCT_0, VECTSP_1,
      ALGSTR_1, INT_3, VALUED_0, ALGSTR_0, XXREAL_2, CARD_1, RELSET_1,
      XTUPLE_0, ORDINAL1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

registration
  cluster add-associative left_zeroed right_zeroed for non empty addLoopStr;
end;

registration
  cluster Abelian left_zeroed right_zeroed add-cancelable well-unital
    add-associative associative commutative distributive for non trivial
    doubleLoopStr;
end;

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

begin :: Ideals

definition
  let L be non empty addLoopStr, F being Subset of L;
  attr F is add-closed means
:: IDEAL_1:def 1

  for x, y being Element of L st x in F & y in F holds x+y in F;
end;

definition
  let L be non empty multMagma, F be Subset of L;
  attr F is left-ideal means
:: 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
:: IDEAL_1:def 3

  for p, x being Element of L st x in F holds x*p in F;
end;

registration
  let L be non empty addLoopStr;
  cluster add-closed for non empty Subset of L;
end;

registration
  let L be non empty multMagma;
  cluster left-ideal for non empty Subset of L;
  cluster right-ideal for non empty Subset of L;
end;

registration
  let L be non empty doubleLoopStr;
  cluster add-closed left-ideal right-ideal for non empty Subset of L;
  cluster add-closed right-ideal for non empty Subset of L;
  cluster add-closed left-ideal for non empty Subset of L;
end;

registration
  let R be commutative non empty multMagma;
  cluster left-ideal -> right-ideal for non empty Subset of R;
  cluster right-ideal -> left-ideal for non empty Subset of R;
end;

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

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

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

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

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

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

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

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

registration
  let L be right_zeroed non empty addLoopStr;
  cluster {0.L} -> add-closed for Subset of L;
end;

registration
  let L be left_zeroed right_add-cancelable right-distributive non empty
  doubleLoopStr;
  cluster {0.L} -> left-ideal for Subset of L;
end;

registration
  let L be right_zeroed left_add-cancelable left-distributive non empty
  doubleLoopStr;
  cluster {0.L} -> right-ideal for Subset of L;
end;

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

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

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

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

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

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

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

registration
  let R be non trivial left_zeroed right_zeroed add-cancelable distributive
  non empty doubleLoopStr;
  cluster proper for Ideal of R;
end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

begin  :: Linear combinations

definition
  let R be non empty multLoopStr, A be non empty Subset of R;
  mode LinearCombination of A -> FinSequence of the carrier of R means
:: IDEAL_1:def 8

  for i being set st i in dom it
   ex u,v being Element of R, a being Element of A st it/.i = u*a*v;
  mode LeftLinearCombination of A -> FinSequence of the carrier of R means
:: IDEAL_1:def 9

  for i being set st i in dom it
  ex u being Element of R, a being Element of A st it/.i = u*a;
  mode RightLinearCombination of A -> FinSequence of the carrier of R means
:: IDEAL_1:def 10

  for i being set st i in dom it
  ex u being Element of R, a being Element of A st it/.i = a*u;
end;

registration
  let R be non empty multLoopStr, A be non empty Subset of R;
  cluster non empty for LinearCombination of A;
  cluster non empty for LeftLinearCombination of A;
  cluster non empty for RightLinearCombination of A;
end;

definition
  let R be non empty multLoopStr, A,B be non empty Subset of R, F be
  LinearCombination of A, G be LinearCombination of B;
  redefine func F^G -> LinearCombination of (A \/ B);
end;

theorem :: IDEAL_1:23
  for R be associative non empty multLoopStr, A be non empty
  Subset of R, a be Element of R, F be LinearCombination of A holds a*F is
  LinearCombination of A;

theorem :: IDEAL_1:24
  for R be associative non empty multLoopStr, A be non empty
  Subset of R, a be Element of R, F be LinearCombination of A holds F*a is
  LinearCombination of A;

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

definition
  let R be non empty multLoopStr, A,B be non empty Subset of R, F be
  LeftLinearCombination of A, G be LeftLinearCombination of B;
  redefine func F^G -> LeftLinearCombination of (A \/ B);
end;

theorem :: IDEAL_1:26
  for R be associative non empty multLoopStr, A be non empty
  Subset of R, a be Element of R, F be LeftLinearCombination of A holds
  a*F is LeftLinearCombination of A;

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

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

definition
  let R be non empty multLoopStr, A,B be non empty Subset of R, F be
  RightLinearCombination of A, G be RightLinearCombination of B;
  redefine func F^G -> RightLinearCombination of (A \/ B);
end;

theorem :: IDEAL_1:29
  for R be associative non empty multLoopStr, A be non empty
  Subset of R, a be Element of R, F be RightLinearCombination of A holds
  F*a is RightLinearCombination of A;

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

theorem :: IDEAL_1:31
  for R being commutative associative non empty multLoopStr, A
  being non empty Subset of R, f being LinearCombination of A holds
  f is LeftLinearCombination of A & f is RightLinearCombination of A;

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

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

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

definition
  let R be non empty multLoopStr, A be non empty Subset of R,
  L be LinearCombination of A,
  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;

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

theorem :: IDEAL_1:36
  for R, S being non empty multLoopStr, F being non empty Subset of R,
  lc being LinearCombination of F, G being non empty Subset of S, P being
  Function of the carrier of R, the carrier of S, 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));

definition
  let R be non empty multLoopStr, A be non empty Subset of R,
  L be LeftLinearCombination of A,
  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;

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

theorem :: IDEAL_1:38
  for R, S being non empty multLoopStr, F being non empty Subset of R,
  lc being LeftLinearCombination of F, G being non empty Subset of S, P being
  Function of the carrier of R, the carrier of S, 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);

definition
  let R be non empty multLoopStr, A be non empty Subset of R, L be
  RightLinearCombination of A, 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;

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

theorem :: IDEAL_1:40
  for R, S being non empty multLoopStr, F being non empty Subset of R,
  lc being RightLinearCombination of F, G being non empty Subset of S, P being
  Function of the carrier of R, the carrier of S, 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);

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

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

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

begin :: Generated ideals

definition
  let L be non empty doubleLoopStr, F be Subset of L;
  assume
 F is non empty;
  func F-Ideal -> Ideal of L means
:: IDEAL_1:def 14

  F c= it & for I being Ideal of L st F c= I holds it c= I;
  func F-LeftIdeal -> LeftIdeal of L means
:: IDEAL_1:def 15

  F c= it & for I being LeftIdeal of L st F c= I holds it c= I;
  func F-RightIdeal -> RightIdeal of L means
:: IDEAL_1:def 16

  F c= it & for I being RightIdeal of L st F c= I holds it c= I;
end;

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

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

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

definition
  let L be non empty doubleLoopStr, I be Ideal of L;
  mode Basis of I -> non empty Subset of L means
:: IDEAL_1:def 17
    it-Ideal = I;
end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem :: IDEAL_1:64
  for R being add-associative left_zeroed right_zeroed
  add-cancelable well-unital associative commutative distributive non empty
doubleLoopStr, a being Element of R holds {a}-Ideal = the set of all
a*r where r is Element
  of R;

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

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

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

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

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

begin :: Some Operations on Ideals

definition
  let R be non empty multMagma, I be Subset of R, 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};
end;

registration
  let R be non empty multLoopStr, I be non empty Subset of R,
  a be Element of R;
  cluster a*I -> non empty;
end;

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

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

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

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

definition
  let R be addMagma, 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};
end;

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

definition
  let R be Abelian non empty addLoopStr, I,J be Subset of R;
  redefine func I + J;
  commutativity;
end;

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

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

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

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

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

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

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

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

definition
  let R be non empty 1-sorted, I,J be Subset of R;
  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 };
end;

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

registration
  let R be non empty addLoopStr, I,J be add-closed Subset of R;
  cluster I /\ J -> add-closed for Subset of R;
end;

registration
  let R be non empty multLoopStr, I,J be left-ideal Subset of R;
  cluster I /\ J -> left-ideal for Subset of R;
end;

registration
  let R be non empty multLoopStr, I,J be right-ideal Subset of R;
  cluster I /\ J -> right-ideal for Subset of R;
end;

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

definition
  let R be non empty doubleLoopStr, 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 ex a,b being
  Element of R st s.i = a*b & a in I & b in J};
end;

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

definition
  let R be commutative non empty doubleLoopStr, I,J be Subset of R;
  redefine func I *' J;
  commutativity;
end;

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

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

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

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

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

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

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

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

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

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

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

definition
  let R be non empty multMagma, 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};
end;

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

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

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

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

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

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

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

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

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

definition
  let R be well-unital non empty doubleLoopStr, 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};
end;

registration
  let R be well-unital non empty doubleLoopStr, I be non empty Subset of R;
  cluster sqrt I -> non empty;
end;

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

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

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

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

begin :: Noetherian ideals

definition
  let L be non empty doubleLoopStr, 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;

registration
  let L be non empty doubleLoopStr;
  cluster finitely_generated for Ideal of L;
end;

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

definition
  let L be non empty doubleLoopStr;
  attr L is Noetherian means
:: IDEAL_1:def 26

  for I being Ideal of L holds I is finitely_generated;
end;

registration
  cluster Euclidian Abelian add-associative right_zeroed right_complementable
    well-unital distributive commutative associative non degenerated for
non empty
    doubleLoopStr;
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;

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;

theorem :: IDEAL_1:93
  for L being non empty doubleLoopStr, F being non empty Subset of
  L st F <> {0.L} ex x being Element of L st x <> 0.L & x in F;

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

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

registration
  cluster INT.Ring -> Noetherian;
end;

registration
  cluster Noetherian Abelian add-associative right_zeroed right_complementable
    well-unital distributive commutative associative non degenerated for
non empty
    doubleLoopStr;
end;

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

theorem :: IDEAL_1:97 :: Lemma_4_5_ii_iii:
  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 for
  a being sequence of R ex m being Element of NAT st a.(m+1) in (rng (a|(m+1)))
  -Ideal;

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

theorem :: IDEAL_1:98 :: Lemma_4_5_iii_iv:
  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 not ex F being
sequence of  bool (the carrier of R) st (for i being Nat holds F
  .i is Ideal of R) & (for j,k being Nat st j < k holds F.j c< F.k);

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