:: by Jonathan Backer , Piotr Rudnicki and Christoph Schwarzweller

::

:: Received November 20, 2000

:: Copyright (c) 2000-2012 Association of Mizar Users

begin

registration

existence

ex b_{1} being non empty addLoopStr st

( b_{1} is add-associative & b_{1} is left_zeroed & b_{1} is right_zeroed )

end;
ex b

( b

proof end;

registration

ex b_{1} being non trivial doubleLoopStr st

( b_{1} is Abelian & b_{1} is left_zeroed & b_{1} is right_zeroed & b_{1} is add-cancelable & b_{1} is well-unital & b_{1} is add-associative & b_{1} is associative & b_{1} is commutative & b_{1} is distributive )
end;

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

existence ex b

( b

proof 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

for v, u being Element of V holds Sum <*v,u*> = v + u

proof end;

begin

definition

let L be non empty addLoopStr ;

let F be Subset of L;

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

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

x + y in F;

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

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;

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

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;

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

x * p in F;

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

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

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 ;

existence

ex b_{1} being non empty Subset of L st b_{1} is add-closed

end;
existence

ex b

proof end;

registration

let L be non empty multMagma ;

existence

ex b_{1} being non empty Subset of L st b_{1} is left-ideal

ex b_{1} being non empty Subset of L st b_{1} is right-ideal

end;
existence

ex b

proof end;

existence ex b

proof end;

registration

let L be non empty doubleLoopStr ;

existence

ex b_{1} being non empty Subset of L st

( b_{1} is add-closed & b_{1} is left-ideal & b_{1} is right-ideal )

ex b_{1} being non empty Subset of L st

( b_{1} is add-closed & b_{1} is right-ideal )

ex b_{1} being non empty Subset of L st

( b_{1} is add-closed & b_{1} is left-ideal )

end;
existence

ex b

( b

proof end;

existence ex b

( b

proof end;

existence ex b

( b

proof end;

registration

let R be non empty commutative multMagma ;

coherence

for b_{1} being non empty Subset of R st b_{1} is left-ideal holds

b_{1} is right-ideal

for b_{1} being non empty Subset of R st b_{1} is right-ideal holds

b_{1} is left-ideal

end;
coherence

for b

b

proof end;

coherence for b

b

proof 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;
mode Ideal of L is non empty add-closed left-ideal right-ideal Subset of L;

definition

let L be non empty doubleLoopStr ;

mode RightIdeal of L is non empty add-closed right-ideal Subset of L;

end;
mode RightIdeal of L is non empty add-closed right-ideal Subset of L;

definition

let L be non empty doubleLoopStr ;

mode LeftIdeal of L is non empty add-closed left-ideal Subset of L;

end;
mode LeftIdeal of L is non empty add-closed left-ideal Subset of L;

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

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

for I being non empty right-ideal Subset of R holds 0. R in I

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 ;

coherence

for b_{1} being Subset of L st b_{1} = {(0. L)} holds

b_{1} is add-closed
by Th4;

end;
coherence

for b

b

registration

let L be non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr ;

coherence

for b_{1} being Subset of L st b_{1} = {(0. L)} holds

b_{1} is left-ideal
by Th5;

end;
coherence

for b

b

registration

let L be non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr ;

coherence

for b_{1} being Subset of L st b_{1} = {(0. L)} holds

b_{1} is right-ideal
by Th6;

end;
coherence

for b

b

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 ;

definition

let R be non empty add-cancelable right_zeroed distributive left_zeroed doubleLoopStr ;

let I be Ideal of R;

compatibility

( I is trivial iff I = {(0. R)} )

end;
let I be Ideal of R;

compatibility

( I is trivial iff I = {(0. R)} )

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

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 ;

existence

ex b_{1} being Ideal of R st b_{1} is proper

end;
existence

ex b

proof 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

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

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

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

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

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

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;

coherence

the addF of R || I is BinOp of I

end;
let I be non empty add-closed Subset of R;

coherence

the addF of R || I is BinOp of I

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

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;

coherence

the multF of R || I is BinOp of I

end;
let I be non empty right-ideal Subset of R;

coherence

the multF of R || I is BinOp of I

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

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;

addLoopStr(# I,(add| (I,R)),(In ((0. R),I)) #) is non empty addLoopStr ;

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

addLoopStr(# I,(add| (I,R)),(In ((0. R),I)) #) is non empty addLoopStr ;

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

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;

coherence

Gr (I,R) is add-associative

end;
let I be non empty add-closed Subset of R;

coherence

Gr (I,R) is add-associative

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

coherence

Gr (I,R) is right_zeroed

end;
let I be non empty add-closed right-ideal Subset of R;

coherence

Gr (I,R) is right_zeroed

proof end;

registration

let R be non empty Abelian doubleLoopStr ;

let I be non empty add-closed Subset of R;

coherence

Gr (I,R) is Abelian

end;
let I be non empty add-closed Subset of R;

coherence

Gr (I,R) is Abelian

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

coherence

Gr (I,R) is right_complementable

end;
let I be non empty add-closed right-ideal Subset of R;

coherence

Gr (I,R) is right_complementable

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

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 )

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 )

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

( R is Field iff for I being Ideal of R holds

( I = {(0. R)} or I = the carrier of R ) )

proof end;

begin

definition

let R be non empty multLoopStr ;

let A be non empty Subset of R;

ex b_{1} being FinSequence of the carrier of R st

for i being set st i in dom b_{1} holds

ex u, v being Element of R ex a being Element of A st b_{1} /. i = (u * a) * v

ex b_{1} being FinSequence of the carrier of R st

for i being set st i in dom b_{1} holds

ex u being Element of R ex a being Element of A st b_{1} /. i = u * a

ex b_{1} being FinSequence of the carrier of R st

for i being set st i in dom b_{1} holds

ex u being Element of R ex a being Element of A st b_{1} /. i = a * u

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

ex b

for i being set st i in dom b

ex u, v being Element of R ex a being Element of A st b

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

ex b

for i being set st i in dom b

ex u being Element of R ex a being Element of A st b

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

ex b

for i being set st i in dom b

ex u being Element of R ex a being Element of A st b

proof end;

:: deftheorem Def8 defines LinearCombination IDEAL_1:def 8 :

for R being non empty multLoopStr

for A being non empty Subset of R

for b_{3} being FinSequence of the carrier of R holds

( b_{3} is LinearCombination of A iff for i being set st i in dom b_{3} holds

ex u, v being Element of R ex a being Element of A st b_{3} /. i = (u * a) * v );

for R being non empty multLoopStr

for A being non empty Subset of R

for b

( b

ex u, v being Element of R ex a being Element of A st b

:: deftheorem Def9 defines LeftLinearCombination IDEAL_1:def 9 :

for R being non empty multLoopStr

for A being non empty Subset of R

for b_{3} being FinSequence of the carrier of R holds

( b_{3} is LeftLinearCombination of A iff for i being set st i in dom b_{3} holds

ex u being Element of R ex a being Element of A st b_{3} /. i = u * a );

for R being non empty multLoopStr

for A being non empty Subset of R

for b

( b

ex u being Element of R ex a being Element of A st b

:: deftheorem Def10 defines RightLinearCombination IDEAL_1:def 10 :

for R being non empty multLoopStr

for A being non empty Subset of R

for b_{3} being FinSequence of the carrier of R holds

( b_{3} is RightLinearCombination of A iff for i being set st i in dom b_{3} holds

ex u being Element of R ex a being Element of A st b_{3} /. i = a * u );

for R being non empty multLoopStr

for A being non empty Subset of R

for b

( b

ex u being Element of R ex a being Element of A st b

registration

let R be non empty multLoopStr ;

let A be non empty Subset of R;

not for b_{1} being LinearCombination of A holds b_{1} is empty

not for b_{1} being LeftLinearCombination of A holds b_{1} is empty

not for b_{1} being RightLinearCombination of A holds b_{1} is empty

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

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 b

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 b

proof 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 )

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 )

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 )

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 )

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

end;
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:];

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

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

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

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

end;
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:];

:: 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 & ( for i being set st i in dom L holds

( L . i = ((E /. i) `1) * ((E /. i) `2) & (E /. i) `2 in A ) ) ) );

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

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

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

end;
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:];

:: 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 & ( for i being set st i in dom L holds

( L . i = ((E /. i) `1) * ((E /. i) `2) & (E /. i) `1 in A ) ) ) );

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

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

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

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

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

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

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

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

proof end;

begin

definition

let L be non empty doubleLoopStr ;

let F be Subset of L;

assume A1: not F is empty ;

ex b_{1} being Ideal of L st

( F c= b_{1} & ( for I being Ideal of L st F c= I holds

b_{1} c= I ) )

for b_{1}, b_{2} being Ideal of L st F c= b_{1} & ( for I being Ideal of L st F c= I holds

b_{1} c= I ) & F c= b_{2} & ( for I being Ideal of L st F c= I holds

b_{2} c= I ) holds

b_{1} = b_{2}

ex b_{1} being LeftIdeal of L st

( F c= b_{1} & ( for I being LeftIdeal of L st F c= I holds

b_{1} c= I ) )

for b_{1}, b_{2} being LeftIdeal of L st F c= b_{1} & ( for I being LeftIdeal of L st F c= I holds

b_{1} c= I ) & F c= b_{2} & ( for I being LeftIdeal of L st F c= I holds

b_{2} c= I ) holds

b_{1} = b_{2}

ex b_{1} being RightIdeal of L st

( F c= b_{1} & ( for I being RightIdeal of L st F c= I holds

b_{1} c= I ) )

for b_{1}, b_{2} being RightIdeal of L st F c= b_{1} & ( for I being RightIdeal of L st F c= I holds

b_{1} c= I ) & F c= b_{2} & ( for I being RightIdeal of L st F c= I holds

b_{2} c= I ) holds

b_{1} = b_{2}

end;
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 ( F c= it & ( for I being Ideal of L st F c= I holds

it c= I ) );

ex b

( F c= b

b

proof end;

uniqueness for b

b

b

b

proof end;

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 ( F c= it & ( for I being LeftIdeal of L st F c= I holds

it c= I ) );

ex b

( F c= b

b

proof end;

uniqueness for b

b

b

b

proof end;

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 ( F c= it & ( for I being RightIdeal of L st F c= I holds

it c= I ) );

ex b

( F c= b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being Ideal of L holds

( b_{3} = F -Ideal iff ( F c= b_{3} & ( for I being Ideal of L st F c= I holds

b_{3} c= I ) ) );

for L being non empty doubleLoopStr

for F being Subset of L st not F is empty holds

for b

( b

b

:: 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 b_{3} being LeftIdeal of L holds

( b_{3} = F -LeftIdeal iff ( F c= b_{3} & ( for I being LeftIdeal of L st F c= I holds

b_{3} c= I ) ) );

for L being non empty doubleLoopStr

for F being Subset of L st not F is empty holds

for b

( b

b

:: 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 b_{3} being RightIdeal of L holds

( b_{3} = F -RightIdeal iff ( F c= b_{3} & ( for I being RightIdeal of L st F c= I holds

b_{3} c= I ) ) );

for L being non empty doubleLoopStr

for F being Subset of L st not F is empty holds

for b

( b

b

definition

let L be non empty doubleLoopStr ;

let I be Ideal of L;

existence

ex b_{1} being non empty Subset of L st b_{1} -Ideal = I

end;
let I be Ideal of L;

existence

ex b

proof end;

:: deftheorem defines Basis IDEAL_1:def 17 :

for L being non empty doubleLoopStr

for I being Ideal of L

for b_{3} being non empty Subset of L holds

( b_{3} is Basis of I iff b_{3} -Ideal = I );

for L being non empty doubleLoopStr

for I being Ideal of L

for b

( b

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

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

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

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

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

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

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 associative commutative well-unital distributive left_zeroed doubleLoopStr

for F being non empty Subset of R holds

( F -Ideal = F -LeftIdeal & F -Ideal = F -RightIdeal )

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 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 }

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 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 }

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

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 )

for a, b being Element of R holds

( a in {a,b} -Ideal & b in {a,b} -Ideal )

proof end;

theorem :: IDEAL_1:69

begin

definition

let R be non empty multMagma ;

let I be Subset of R;

let a be Element of R;

coherence

{ (a * i) where i is Element of R : i in I } is Subset of R

end;
let I be Subset of R;

let a be Element of R;

coherence

{ (a * i) where i is Element of R : i in I } is Subset of R

proof 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 } ;

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;

coherence

not a * I is empty

end;
let I be non empty Subset of R;

let a be Element of R;

coherence

not a * I is empty

proof end;

registration

let R be non empty distributive doubleLoopStr ;

let I be add-closed Subset of R;

let a be Element of R;

coherence

a * I is add-closed

end;
let I be add-closed Subset of R;

let a be Element of R;

coherence

a * I is add-closed

proof end;

registration

let R be non empty associative doubleLoopStr ;

let I be right-ideal Subset of R;

let a be Element of R;

coherence

a * I is right-ideal

end;
let I be right-ideal Subset of R;

let a be Element of R;

coherence

a * I is right-ideal

proof 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)}

for I being non empty Subset of R holds (0. R) * I = {(0. R)}

proof end;

definition

let R be non empty addLoopStr ;

let I, J be Subset of R;

{ (a + b) where a, b is Element of R : ( a in I & b in J ) } is Subset of R

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

{ (a + b) where a, b is Element of R : ( a in I & b in J ) } is Subset of R

proof 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 & b in J ) } ;

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 & b in J ) } ;

registration

let R be non empty addLoopStr ;

let I, J be non empty Subset of R;

coherence

not I + J is empty

end;
let I, J be non empty Subset of R;

coherence

not I + J is empty

proof 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

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

registration

let R be non empty Abelian add-associative addLoopStr ;

let I, J be add-closed Subset of R;

coherence

I + J is add-closed

end;
let I, J be add-closed Subset of R;

coherence

I + J is add-closed

proof end;

registration

let R be non empty left-distributive doubleLoopStr ;

let I, J be right-ideal Subset of R;

coherence

I + J is right-ideal

end;
let I, J be right-ideal Subset of R;

coherence

I + J is right-ideal

proof end;

registration

let R be non empty right-distributive doubleLoopStr ;

let I, J be left-ideal Subset of R;

coherence

I + J is left-ideal

end;
let I, J be left-ideal Subset of R;

coherence

I + J is left-ideal

proof 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

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

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

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

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 associative commutative well-unital distributive left_zeroed doubleLoopStr

for a, b being Element of R holds {a,b} -Ideal = ({a} -Ideal) + ({b} -Ideal)

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;

I /\ J is Subset of R

for b_{1} being Subset of R holds

( b_{1} = I /\ J iff b_{1} = { x where x is Element of R : ( x in I & x in J ) } )

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

I /\ J is Subset of R

proof end;

compatibility for b

( b

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

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;

coherence

not I /\ J is empty

end;
let I, J be non empty left-ideal Subset of R;

coherence

not I /\ J is empty

proof end;

registration

let R be non empty addLoopStr ;

let I, J be add-closed Subset of R;

coherence

for b_{1} being Subset of R st b_{1} = I /\ J holds

b_{1} is add-closed

end;
let I, J be add-closed Subset of R;

coherence

for b

b

proof end;

registration

let R be non empty multLoopStr ;

let I, J be left-ideal Subset of R;

coherence

for b_{1} being Subset of R st b_{1} = I /\ J holds

b_{1} is left-ideal

end;
let I, J be left-ideal Subset of R;

coherence

for b

b

proof end;

registration

let R be non empty multLoopStr ;

let I, J be right-ideal Subset of R;

coherence

for b_{1} being Subset of R st b_{1} = I /\ J holds

b_{1} is right-ideal

end;
let I, J be right-ideal Subset of R;

coherence

for b

b

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

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;

{ (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

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

{ (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;

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

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

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

registration

let R be non empty add-associative right_zeroed doubleLoopStr ;

let I, J be Subset of R;

coherence

I *' J is add-closed

end;
let I, J be Subset of R;

coherence

I *' J is add-closed

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

coherence

I *' J is right-ideal

end;
let I, J be right-ideal Subset of R;

coherence

I *' J is right-ideal

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

coherence

I *' J is left-ideal

end;
let I, J be left-ideal Subset of R;

coherence

I *' J is left-ideal

proof 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)}

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

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

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

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

for I, J being non empty add-closed left-ideal Subset of R holds (I + J) *' (I /\ J) c= I /\ J

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

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)

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

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;

coherence

{ a where a is Element of R : a * J c= I } is Subset of R

end;
let I, J be Subset of R;

coherence

{ a where a is Element of R : a * J c= I } is Subset of R

proof 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 } ;

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;

coherence

not I % J is empty

end;
let I, J be non empty left-ideal Subset of R;

coherence

not I % J is empty

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

coherence

I % J is add-closed

end;
let I, J be non empty add-closed left-ideal Subset of R;

coherence

I % J is add-closed

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

coherence

I % J is left-ideal

I % J is right-ideal ;

end;
let I, J be non empty left-ideal Subset of R;

coherence

I % J is left-ideal

proof end;

coherence I % J is right-ideal ;

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

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

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

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

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)

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)

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;

{ a where a is Element of R : ex n being Element of NAT st a |^ n in I } is Subset of R

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

{ a where a is Element of R : ex n being Element of NAT st a |^ n in I } is Subset of R

proof 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 } ;

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;

coherence

not sqrt I is empty

end;
let I be non empty Subset of R;

coherence

not sqrt I is empty

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

coherence

sqrt I is add-closed

end;
let I be non empty add-closed right-ideal Subset of R;

coherence

sqrt I is add-closed

proof end;

registration

let R be non empty associative commutative well-unital doubleLoopStr ;

let I be non empty left-ideal Subset of R;

coherence

sqrt I is left-ideal

sqrt I is right-ideal ;

end;
let I be non empty left-ideal Subset of R;

coherence

sqrt I is left-ideal

proof end;

coherence sqrt I is right-ideal ;

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 )

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

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;

begin

definition

let L be non empty doubleLoopStr ;

let I be Ideal of L;

end;
let I be Ideal of L;

attr I is finitely_generated means :Def25: :: IDEAL_1:def 25

ex F being non empty finite Subset of L st I = F -Ideal ;

ex F being non empty finite Subset of L st I = F -Ideal ;

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

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 ;

ex b_{1} being Ideal of L st b_{1} is finitely_generated

end;
cluster non empty add-closed left-ideal right-ideal finitely_generated for Element of bool the carrier of L;

existence ex b

proof end;

registration

let L be non empty doubleLoopStr ;

let F be non empty finite Subset of L;

coherence

F -Ideal is finitely_generated by Def25;

end;
let F be non empty finite Subset of L;

coherence

F -Ideal is finitely_generated by Def25;

definition

let L be non empty doubleLoopStr ;

end;
attr L is Noetherian means :Def26: :: IDEAL_1:def 26

for I being Ideal of L holds I is finitely_generated ;

for I being Ideal of L holds I is finitely_generated ;

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

for L being non empty doubleLoopStr holds

( L is Noetherian iff for I being Ideal of L holds I is finitely_generated );

registration

ex b_{1} being non empty doubleLoopStr st

( b_{1} is Euclidian & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is well-unital & b_{1} is distributive & b_{1} is commutative & b_{1} is associative & not b_{1} is degenerated )
end;

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

existence ex b

( b

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

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

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

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 )

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;

registration

ex b_{1} being non empty doubleLoopStr st

( b_{1} is Noetherian & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is well-unital & b_{1} is distributive & b_{1} is commutative & b_{1} is associative & not b_{1} is degenerated )
end;

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

existence ex b

( b

proof 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 & C -Ideal = B -Ideal )

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

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

coherence

not f | A is empty

end;
let f be Function of X,Y;

let A be non empty Subset of X;

coherence

not f | A is empty

proof 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 & not F . j c< F . k ) )

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 & not F . j c< F . k ) )

proof end;

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 & not F . j c< F . k ) ) ) holds

R is Noetherian

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