:: IDEAL_1 semantic presentation

registration

cluster non empty add-associative right_zeroed left_zeroed LoopStr ;
existence

proof end;

end;

registration

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

proof end;

end;

theorem Th1: :: IDEAL_1:1

for V being non empty add-associative right_zeroed left_zeroed LoopStr
for v, u being Element of V holds Sum <*v,u*> = v + u

proof end;

definition

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

end;

:: deftheorem Def1 defines add-closed IDEAL_1:def 1 :

definition

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

end;

:: deftheorem Def2 defines left-ideal IDEAL_1:def 2 :

:: deftheorem Def3 defines right-ideal IDEAL_1:def 3 :

registration

let L be non empty LoopStr ;
cluster non empty add-closed Element of bool the carrier of L;
existence

proof end;

end;

registration

let L be non empty HGrStr ;
cluster non empty left-ideal Element of bool the carrier of L;
existence

proof end;

cluster non empty right-ideal Element of bool the carrier of L;
existence

proof end;

end;

registration

let L be non empty doubleLoopStr ;
cluster non empty add-closed left-ideal right-ideal Element of bool the carrier of L;
existence

proof end;

cluster non empty add-closed right-ideal Element of bool the carrier of L;
existence

proof end;

cluster non empty add-closed left-ideal Element of bool the carrier of L;
existence

proof end;

end;

registration

let R be non empty commutative HGrStr ;
cluster non empty left-ideal -> non empty right-ideal Element of bool the carrier of R;
coherence

proof end;

cluster non empty right-ideal -> non empty left-ideal Element of bool the carrier of R;
coherence

proof end;

end;

definition

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

end;

definition

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

end;

definition

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

end;

theorem Th2: :: IDEAL_1:2

for R being non empty right_zeroed left-distributive add-left-cancelable doubleLoopStr
for I being non empty left-ideal Subset of R holds 0. R in I

proof end;

theorem Th3: :: IDEAL_1:3

for R being non empty right-distributive left_zeroed add-right-cancelable doubleLoopStr
for I being non empty right-ideal Subset of R holds 0. R in I

proof end;

theorem Th4: :: IDEAL_1:4

for L being non empty right_zeroed LoopStr holds {(0. L)} is add-closed

proof end;

theorem Th5: :: IDEAL_1:5

for L being non empty right-distributive left_zeroed add-right-cancelable doubleLoopStr holds {(0. L)} is left-ideal

proof end;

theorem Th6: :: IDEAL_1:6

for L being non empty right_zeroed left-distributive add-left-cancelable doubleLoopStr holds {(0. L)} is right-ideal

proof end;

registration

let L be non empty right_zeroed LoopStr ;
cluster {(0. L)} -> add-closed Subset of L;
coherence by Th4;

end;

registration

let L be non empty right-distributive left_zeroed add-right-cancelable doubleLoopStr ;
cluster {(0. L)} -> left-ideal Subset of L;
coherence by Th5;

end;

registration

let L be non empty right_zeroed left-distributive add-left-cancelable doubleLoopStr ;
cluster {(0. L)} -> right-ideal Subset of L;
coherence by Th6;

end;

theorem Th7: :: IDEAL_1:7

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

proof end;

theorem :: IDEAL_1:8

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

proof end;

theorem :: IDEAL_1:9

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

proof end;

theorem Th10: :: IDEAL_1:10

for L being non empty doubleLoopStr holds the carrier of L is Ideal of L

proof end;

theorem Th11: :: IDEAL_1:11

for L being non empty doubleLoopStr holds the carrier of L is LeftIdeal of L

proof end;

theorem Th12: :: IDEAL_1:12

for L being non empty doubleLoopStr holds the carrier of L is RightIdeal of L

proof end;

definition

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

proof end;

end;

:: deftheorem defines trivial IDEAL_1:def 4 :

definition

let S be 1-sorted ;
let T be Subset of S;
attr T is proper means :Def5: :: IDEAL_1:def 5
T <> the carrier of S;

end;

:: deftheorem Def5 defines proper IDEAL_1:def 5 :

registration

let S be non empty 1-sorted ;
cluster proper Element of bool the carrier of S;
existence

proof end;

end;

registration

let R be non empty right_zeroed distributive add-cancelable left_zeroed non trivial doubleLoopStr ;
cluster proper Element of bool the carrier of R;
existence

proof end;

end;

theorem Th13: :: IDEAL_1:13

for L being non empty add-associative right_zeroed right_complementable left-distributive left_unital doubleLoopStr
for I being non empty left-ideal Subset of L
for x being Element of L st x in I holds
- x in I

proof end;

theorem Th14: :: IDEAL_1:14

for L being non empty add-associative right_zeroed right_complementable right-distributive right_unital doubleLoopStr
for I being non empty right-ideal Subset of L
for x being Element of L st x in I holds
- x in I

proof end;

theorem :: IDEAL_1:15

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

proof end;

theorem :: IDEAL_1:16

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

proof end;

theorem Th17: :: IDEAL_1:17

for R being non empty add-associative right_zeroed distributive add-cancelable left_zeroed doubleLoopStr
for I being non empty add-closed right-ideal Subset of R
for a being Element of I
for n being Nat holds n * a in I

proof end;

theorem :: IDEAL_1:18

for R being non empty unital associative right_zeroed distributive add-cancelable left_zeroed doubleLoopStr
for I being non empty right-ideal Subset of R
for a being Element of I
for n being Nat st n <> 0 holds
a |^ n in I

proof end;

definition

let R be non empty LoopStr ;
let I be non empty add-closed Subset of R;
func add| I,R -> BinOp of I equals :: IDEAL_1:def 6
the add of R || I;
coherence

proof end;

end;

:: deftheorem defines add| IDEAL_1:def 6 :

definition

let R be non empty HGrStr ;
let I be non empty right-ideal Subset of R;
func mult| I,R -> BinOp of I equals :: IDEAL_1:def 7
the mult of R || I;
coherence

proof end;

end;

:: deftheorem defines mult| IDEAL_1:def 7 :

definition

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

end;

:: deftheorem defines Gr IDEAL_1:def 8 :

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

let R be non empty Abelian doubleLoopStr ;
let I be non empty add-closed Subset of R;
cluster Gr I,R -> non empty Abelian ;
coherence

proof end;

end;

registration

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

proof end;

end;

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

proof end;

theorem Th19: :: IDEAL_1:19

for R being non empty right_unital doubleLoopStr
for I being non empty left-ideal Subset of R holds
( I is proper iff not 1. R in I )

proof end;

theorem :: IDEAL_1:20

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

proof end;

theorem :: IDEAL_1:21

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

proof end;

theorem :: IDEAL_1:22

for R being non degenerated comRing holds
( R is Field iff for I being Ideal of R holds
( I = {(0. R)} or I = the carrier of R ) )

proof end;

definition

let R be non empty multLoopStr ;
let A be non empty Subset of R;
mode LinearCombination of A -> FinSequence of the carrier of R means :Def9: :: IDEAL_1:def 9
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

proof end;

mode LeftLinearCombination 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 = u * a;
existence

proof end;

mode RightLinearCombination of A -> FinSequence of the carrier of R means :Def11: :: IDEAL_1:def 11
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

proof end;

end;

:: deftheorem Def9 defines LinearCombination IDEAL_1:def 9 :

:: deftheorem Def10 defines LeftLinearCombination IDEAL_1:def 10 :

:: deftheorem Def11 defines RightLinearCombination IDEAL_1:def 11 :

registration

let R be non empty multLoopStr ;
let A be non empty Subset of R;
cluster non empty LinearCombination of A;
existence

proof end;

cluster non empty LeftLinearCombination of A;
existence

proof end;

cluster non empty RightLinearCombination of A;
existence

proof end;

end;

definition

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

proof end;

end;

theorem Th23: :: IDEAL_1:23

for R being non empty associative multLoopStr
for A being non empty Subset of R
for a being Element of R
for F being LinearCombination of A holds a * F is LinearCombination of A

proof end;

theorem Th24: :: IDEAL_1:24

for R being non empty associative multLoopStr
for A being non empty Subset of R
for a being Element of R
for F being LinearCombination of A holds F * a is LinearCombination of A

proof end;

theorem Th25: :: IDEAL_1:25

for R being non empty right_unital multLoopStr
for A being non empty Subset of R
for f being LeftLinearCombination of A holds f is LinearCombination of A

proof end;

definition

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

proof end;

end;

theorem Th26: :: IDEAL_1:26

for R being non empty associative multLoopStr
for A being non empty Subset of R
for a being Element of R
for F being LeftLinearCombination of A holds a * F is LeftLinearCombination of A

proof end;

theorem :: IDEAL_1:27

for R being non empty multLoopStr
for A being non empty Subset of R
for a being Element of R
for F being LeftLinearCombination of A holds F * a is LinearCombination of A

proof end;

theorem Th28: :: IDEAL_1:28

for R being non empty left_unital multLoopStr
for A being non empty Subset of R
for f being RightLinearCombination of A holds f is LinearCombination of A

proof end;

definition

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

proof end;

end;

theorem Th29: :: IDEAL_1:29

for R being non empty associative multLoopStr
for A being non empty Subset of R
for a being Element of R
for F being RightLinearCombination of A holds F * a is RightLinearCombination of A

proof end;

theorem :: IDEAL_1:30

for R being non empty associative multLoopStr
for A being non empty Subset of R
for a being Element of R
for F being RightLinearCombination of A holds a * F is LinearCombination of A

proof end;

theorem Th31: :: IDEAL_1:31

for R being non empty associative commutative multLoopStr
for A being non empty Subset of R
for f being LinearCombination of A holds
( f is LeftLinearCombination of A & f is RightLinearCombination of A )

proof end;

theorem Th32: :: IDEAL_1:32

for S being non empty doubleLoopStr
for F being non empty Subset of S
for lc being non empty LinearCombination of F ex p being LinearCombination of F ex e being Element of S st
( lc = p ^ <*e*> & <*e*> is LinearCombination of F )

proof end;

theorem Th33: :: IDEAL_1:33

for S being non empty doubleLoopStr
for F being non empty Subset of S
for lc being non empty LeftLinearCombination of F ex p being LeftLinearCombination of F ex e being Element of S st
( lc = p ^ <*e*> & <*e*> is LeftLinearCombination of F )

proof end;

theorem Th34: :: IDEAL_1:34

for S being non empty doubleLoopStr
for F being non empty Subset of S
for lc being non empty RightLinearCombination of F ex p being RightLinearCombination of F ex e being Element of S st
( lc = p ^ <*e*> & <*e*> is RightLinearCombination of F )

proof end;

definition

let R be non empty multLoopStr ;
let A be non empty Subset of R;
let L be LinearCombination of A;
let E be FinSequence of [:the carrier of R,the carrier of R,the carrier of R:];
pred E represents L means :Def12: :: 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) `3 ) & (E /. i) `2 in A ) ) );

end;

:: deftheorem Def12 defines represents IDEAL_1:def 12 :

theorem :: IDEAL_1:35

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

proof end;

theorem :: IDEAL_1:36

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

proof end;

definition

let R be non empty multLoopStr ;
let A be non empty Subset of R;
let L be LeftLinearCombination of A;
let E be FinSequence of [:the carrier of R,the carrier of R:];
pred E represents L means :Def13: :: 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) `2 in A ) ) );

end;

:: deftheorem Def13 defines represents IDEAL_1:def 13 :

theorem :: IDEAL_1:37

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

proof end;

theorem :: IDEAL_1:38

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

proof end;

definition

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

end;

:: deftheorem Def14 defines represents IDEAL_1:def 14 :

theorem :: IDEAL_1:39

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

proof end;

theorem :: IDEAL_1:40

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

proof end;

theorem :: IDEAL_1:41

for R being non empty multLoopStr
for A being non empty Subset of R
for l being LinearCombination of A
for n being Nat holds l | (Seg n) is LinearCombination of A

proof end;

theorem :: IDEAL_1:42

for R being non empty multLoopStr
for A being non empty Subset of R
for l being LeftLinearCombination of A
for n being Nat holds l | (Seg n) is LeftLinearCombination of A

proof end;

theorem :: IDEAL_1:43

for R being non empty multLoopStr
for A being non empty Subset of R
for l being RightLinearCombination of A
for n being Nat holds l | (Seg n) is RightLinearCombination of A

proof end;

definition

let L be non empty doubleLoopStr ;
let F be Subset of L;
assume A1: not F is empty ;
func F -Ideal -> Ideal of L means :Def15: :: IDEAL_1:def 15
( F c= it & ( for I being Ideal of L st F c= I holds
it c= I ) );
existence

proof end;

uniqueness

proof end;

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

proof end;

uniqueness

proof end;

func F -RightIdeal -> RightIdeal of L means :Def17: :: IDEAL_1:def 17
( F c= it & ( for I being RightIdeal of L st F c= I holds
it c= I ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines -Ideal IDEAL_1:def 15 :

:: deftheorem Def16 defines -LeftIdeal IDEAL_1:def 16 :

:: deftheorem Def17 defines -RightIdeal IDEAL_1:def 17 :

theorem Th44: :: IDEAL_1:44

for L being non empty doubleLoopStr
for I being Ideal of L holds I -Ideal = I

proof end;

theorem Th45: :: IDEAL_1:45

for L being non empty doubleLoopStr
for I being LeftIdeal of L holds I -LeftIdeal = I

proof end;

theorem Th46: :: IDEAL_1:46

for L being non empty doubleLoopStr
for I being RightIdeal of L holds I -RightIdeal = I

proof end;

definition

let L be non empty doubleLoopStr ;
let I be Ideal of L;
mode Basis of I -> non empty Subset of L means :: IDEAL_1:def 18
it -Ideal = I;
existence

proof end;

end;

:: deftheorem defines Basis IDEAL_1:def 18 :

theorem Th47: :: IDEAL_1:47

for L being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr holds {(0. L)} -Ideal = {(0. L)}

proof end;

theorem :: IDEAL_1:48

for L being non empty right_zeroed distributive add-cancelable left_zeroed doubleLoopStr holds {(0. L)} -Ideal = {(0. L)}

proof end;

theorem :: IDEAL_1:49

for L being non empty right_zeroed right-distributive left_zeroed add-right-cancelable doubleLoopStr holds {(0. L)} -LeftIdeal = {(0. L)}

proof end;

theorem :: IDEAL_1:50

for L being non empty right_zeroed left-distributive add-left-cancelable doubleLoopStr holds {(0. L)} -RightIdeal = {(0. L)}

proof end;

theorem :: IDEAL_1:51

for L being non empty unital doubleLoopStr holds {(1. L)} -Ideal = the carrier of L

proof end;

theorem :: IDEAL_1:52

for L being non empty right_unital doubleLoopStr holds {(1. L)} -LeftIdeal = the carrier of L

proof end;

theorem :: IDEAL_1:53

for L being non empty left_unital doubleLoopStr holds {(1. L)} -RightIdeal = the carrier of L

proof end;

theorem :: IDEAL_1:54

for L being non empty doubleLoopStr holds ([#] L) -Ideal = the carrier of L

proof end;

theorem :: IDEAL_1:55

for L being non empty doubleLoopStr holds ([#] L) -LeftIdeal = the carrier of L

proof end;

theorem :: IDEAL_1:56

for L being non empty doubleLoopStr holds ([#] L) -RightIdeal = the carrier of L

proof end;

theorem Th57: :: IDEAL_1:57

for L being non empty doubleLoopStr
for A, B being non empty Subset of L st A c= B holds
A -Ideal c= B -Ideal

proof end;

theorem :: IDEAL_1:58

for L being non empty doubleLoopStr
for A, B being non empty Subset of L st A c= B holds
A -LeftIdeal c= B -LeftIdeal

proof end;

theorem :: IDEAL_1:59

for L being non empty doubleLoopStr
for A, B being non empty Subset of L st A c= B holds
A -RightIdeal c= B -RightIdeal

proof end;

theorem Th60: :: IDEAL_1:60

for L being non empty unital associative add-associative right_zeroed distributive add-cancelable left_zeroed doubleLoopStr
for F being non empty Subset of L
for x being set holds
( x in F -Ideal iff ex f being LinearCombination of F st x = Sum f )

proof end;

theorem Th61: :: IDEAL_1:61

for L being non empty unital associative add-associative right_zeroed distributive add-cancelable left_zeroed doubleLoopStr
for F being non empty Subset of L
for x being set holds
( x in F -LeftIdeal iff ex f being LeftLinearCombination of F st x = Sum f )

proof end;

theorem Th62: :: IDEAL_1:62

for L being non empty unital associative add-associative right_zeroed distributive add-cancelable left_zeroed doubleLoopStr
for F being non empty Subset of L
for x being set holds
( x in F -RightIdeal iff ex f being RightLinearCombination of F st x = Sum f )

proof end;

theorem Th63: :: IDEAL_1:63

for R being non empty unital associative commutative add-associative right_zeroed distributive add-cancelable left_zeroed doubleLoopStr
for F being non empty Subset of R holds
( F -Ideal = F -LeftIdeal & F -Ideal = F -RightIdeal )

proof end;

theorem Th64: :: IDEAL_1:64

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

proof end;

theorem Th65: :: IDEAL_1:65

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

proof end;

theorem Th66: :: IDEAL_1:66

for R being non empty doubleLoopStr
for a being Element of R holds a in {a} -Ideal

proof end;

theorem :: IDEAL_1:67

for R being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable 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

proof end;

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

proof end;

theorem :: IDEAL_1:68

for R being non empty doubleLoopStr
for a, b being Element of R holds
( a in {a,b} -Ideal & b in {a,b} -Ideal )

proof end;

theorem :: IDEAL_1:69

for R being non empty doubleLoopStr
for a, b being Element of R holds
( {a} -Ideal c= {a,b} -Ideal & {b} -Ideal c= {a,b} -Ideal )

proof end;

definition

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

proof end;

end;

:: deftheorem defines * IDEAL_1:def 19 :

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

theorem Th70: :: IDEAL_1:70

for R being non empty right_zeroed left-distributive add-left-cancelable doubleLoopStr
for I being non empty Subset of R holds (0. R) * I = {(0. R)}

proof end;

theorem :: IDEAL_1:71

for R being non empty left_unital doubleLoopStr
for I being Subset of R holds (1. R) * I = I

proof end;

definition

let R be non empty LoopStr ;
let I, J be Subset of R;
func I + J -> Subset of R equals :: IDEAL_1:def 20
{ (a + b) where a, b is Element of R : ( a in I & b in J ) } ;
coherence

proof end;

end;

:: deftheorem defines + IDEAL_1:def 20 :

registration

let R be non empty LoopStr ;
let I, J be non empty Subset of R;
cluster I + J -> non empty ;
coherence

proof end;

end;

definition

let R be non empty Abelian LoopStr ;
let I, J be Subset of R;
:: original: +
redefine func I + J -> Subset of R;
commutativity

proof end;

end;

registration

let R be non empty Abelian add-associative LoopStr ;
let I, J be add-closed Subset of R;
cluster I + J -> add-closed ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

theorem :: IDEAL_1:72

for R being non empty add-associative LoopStr
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_zeroed right-distributive left_zeroed add-right-cancelable doubleLoopStr
for I, J being non empty right-ideal Subset of R holds I c= I + J

proof end;

theorem Th74: :: IDEAL_1:74

for R being non empty right-distributive left_zeroed add-right-cancelable doubleLoopStr
for I, J being non empty right-ideal Subset of R holds J c= I + J

proof end;

theorem :: IDEAL_1:75

for R being non empty LoopStr
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

proof end;

definition

let R be non empty 1-sorted ;
let I, J be Subset of R;
:: original: /\
redefine func I /\ J -> Subset of R equals :: IDEAL_1:def 21
{ x where x is Element of R : ( x in I & x in J ) } ;
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem defines /\ IDEAL_1:def 21 :

registration

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

proof end;

end;

registration

let R be non empty LoopStr ;
let I, J be add-closed Subset of R;
cluster I /\ J -> add-closed Subset of R;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

theorem :: IDEAL_1:77

for R being non empty 1-sorted
for I, J being Subset of R holds
( I /\ J c= I & I /\ J c= J ) by XBOOLE_1:17;

theorem :: IDEAL_1:78

for R being non empty 1-sorted
for I, J, K being Subset of R holds I /\ (J /\ K) = (I /\ J) /\ K by XBOOLE_1:16;

theorem :: IDEAL_1:79

for R being non empty 1-sorted
for I, J, K being Subset of R st K c= I & K c= J holds
K c= I /\ J by XBOOLE_1:19;

theorem :: IDEAL_1:80

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

proof end;

definition

let R be non empty doubleLoopStr ;
let I, J be Subset of R;
func I *' J -> Subset of R equals :: IDEAL_1:def 22
{ (Sum s) where s is FinSequence of the carrier of R : for i being 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

proof end;

end;

:: deftheorem defines *' IDEAL_1:def 22 :

registration

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

proof end;

end;

definition

let R be non empty commutative doubleLoopStr ;
let I, J be Subset of R;
:: original: *'
redefine func I *' J -> Subset of R;
commutativity

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

theorem :: IDEAL_1:81

for R being non empty right_zeroed left-distributive left_zeroed add-left-cancelable doubleLoopStr
for I being non empty Subset of R holds {(0. R)} *' I = {(0. R)}

proof end;

theorem Th82: :: IDEAL_1:82

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

proof end;

theorem Th83: :: IDEAL_1:83

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

proof end;

theorem Th84: :: IDEAL_1:84

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

proof end;

theorem :: IDEAL_1:85

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

proof end;

definition

let R be non empty LoopStr ;
let I, J be Subset of R;
pred I,J are_co-prime means :Def23: :: IDEAL_1:def 23
I + J = the carrier of R;

end;

:: deftheorem Def23 defines are_co-prime IDEAL_1:def 23 :

theorem Th86: :: IDEAL_1:86

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

proof end;

theorem :: IDEAL_1:87

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

proof end;

definition

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

proof end;

end;

:: deftheorem defines % IDEAL_1:def 24 :

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

cluster I % J -> non empty left-ideal right-ideal ;
coherence ;

end;

theorem :: IDEAL_1:88

for R being non empty multLoopStr
for I being non empty right-ideal Subset of R
for J being Subset of R holds I c= I % J

proof end;

theorem :: IDEAL_1:89

for R being non empty right_zeroed left-distributive add-left-cancelable doubleLoopStr
for I being non empty add-closed left-ideal Subset of R
for J being Subset of R holds (I % J) *' J c= I

proof end;

theorem Th90: :: IDEAL_1:90

for R being non empty right-distributive left_zeroed add-right-cancelable doubleLoopStr
for I being non empty add-closed right-ideal Subset of R
for J being Subset of R holds (I % J) *' J c= I

proof end;

theorem :: IDEAL_1:91

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

proof end;

theorem :: IDEAL_1:92

for R being non empty multLoopStr
for I, J, K being Subset of R holds (J /\ K) % I = (J % I) /\ (K % I)

proof end;

theorem :: IDEAL_1:93

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

proof end;

definition

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

proof end;

end;

:: deftheorem defines sqrt IDEAL_1:def 25 :

registration

let R be non empty unital doubleLoopStr ;
let I be non empty Subset of R;
cluster sqrt I -> non empty ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

cluster sqrt I -> non empty left-ideal right-ideal ;
coherence ;

end;

theorem :: IDEAL_1:94

for R being non empty unital associative doubleLoopStr
for I being non empty Subset of R
for a being Element of R holds
( a in sqrt I iff ex n being Nat st a |^ n in sqrt I )

proof end;

theorem :: IDEAL_1:95

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

proof end;

definition

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

end;

:: deftheorem Def26 defines finitely_generated IDEAL_1:def 26 :

registration

let L be non empty doubleLoopStr ;
cluster finitely_generated Element of bool the carrier of L;
existence

proof end;

end;

registration

let L be non empty doubleLoopStr ;
let F be non empty finite Subset of L;
cluster F -Ideal -> finitely_generated ;
coherence by Def26;

end;

definition

let L be non empty doubleLoopStr ;
attr L is Noetherian means :Def27: :: IDEAL_1:def 27
for I being Ideal of L holds I is finitely_generated;

end;

:: deftheorem Def27 defines Noetherian IDEAL_1:def 27 :

registration

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

proof end;

end;

definition

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

end;

:: deftheorem Def28 defines principal IDEAL_1:def 28 :

definition

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

end;

:: deftheorem Def29 defines PID IDEAL_1:def 29 :

theorem Th96: :: IDEAL_1:96

for L being non empty doubleLoopStr
for F being non empty Subset of L st F <> {(0. L)} holds
ex x being Element of L st
( x <> 0. L & x in F )

proof end;

theorem Th97: :: IDEAL_1:97

for R being non empty add-associative right_zeroed right_complementable distributive left_unital Euclidian left_zeroed doubleLoopStr holds R is PID

proof end;

theorem Th98: :: IDEAL_1:98

for L being non empty doubleLoopStr st L is PID holds
L is Noetherian

proof end;

registration

cluster INT.Ring -> Noetherian ;
coherence

proof end;

end;

registration

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

proof end;

end;

theorem :: IDEAL_1:99

for R being non empty unital associative add-associative right_zeroed distributive add-cancelable left_zeroed Noetherian doubleLoopStr
for B being non empty Subset of R ex C being non empty finite Subset of R st
( C c= B & C -Ideal = B -Ideal )

proof end;

theorem :: IDEAL_1:100

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 Nat st a . (m + 1) in (rng (a | (Segm (m + 1)))) -Ideal

proof end;

registration

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

proof end;

end;

theorem :: IDEAL_1:101

for R being non empty doubleLoopStr st ( for a being sequence of R ex m being Nat st a . (m + 1) in (rng (a | (Segm (m + 1)))) -Ideal ) holds
for F being Function of NAT , bool the carrier of R holds
( ex i being Nat st F . i is not Ideal of R or ex j, k being Nat st
( j < k & not F . j c< F . k ) )

proof end;

theorem :: IDEAL_1:102

for R being non empty doubleLoopStr st ( for F being Function of NAT , bool the carrier of R holds
( ex i being Nat st F . i is not Ideal of R or ex j, k being Nat st
( j < k & not F . j c< F . k ) ) ) holds
R is Noetherian

proof end;