:: 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 b₁ being non empty add-associative right_zeroed left_zeroed LoopStr
for b₂, b₃ being Element of b₁ holds Sum <*b₂,b₃*> = b₂ + b₃

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂ be Subset of c₁;
attr a₂ is add-closed means :Def1: :: IDEAL_1:def 1
for b₁, b₂ being Element of a₁ st b₁ in a₂ & b₂ in a₂ holds
b₁ + b₂ in a₂;

end;

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

definition

let c₁ be non empty HGrStr ;
let c₂ be Subset of c₁;
attr a₂ is left-ideal means :Def2: :: IDEAL_1:def 2
for b₁, b₂ being Element of a₁ st b₂ in a₂ holds
b₁ * b₂ in a₂;
attr a₂ is right-ideal means :Def3: :: IDEAL_1:def 3
for b₁, b₂ being Element of a₁ st b₂ in a₂ holds
b₂ * b₁ in a₂;

end;

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

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

registration

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

proof end;

end;

registration

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

proof end;

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

proof end;

end;

registration

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

proof end;

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

proof end;

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

proof end;

end;

registration

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

proof end;

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

proof end;

end;

definition

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

end;

definition

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

end;

definition

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

end;

theorem Th2: :: IDEAL_1:2

for b₁ being non empty right_zeroed left-distributive add-left-cancelable doubleLoopStr
for b₂ being non empty left-ideal Subset of b₁ holds 0. b₁ in b₂

proof end;

theorem Th3: :: IDEAL_1:3

for b₁ being non empty right-distributive left_zeroed add-right-cancelable doubleLoopStr
for b₂ being non empty right-ideal Subset of b₁ holds 0. b₁ in b₂

proof end;

theorem Th4: :: IDEAL_1:4

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

proof end;

theorem Th5: :: IDEAL_1:5

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

proof end;

theorem Th6: :: IDEAL_1:6

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

proof end;

registration

let c₁ be non empty right_zeroed LoopStr ;
cluster {(0. a₁)} -> add-closed ;
coherence by Th4;

end;

registration

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

end;

registration

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

end;

theorem Th7: :: IDEAL_1:7

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

proof end;

theorem Th8: :: IDEAL_1:8

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

proof end;

theorem Th9: :: IDEAL_1:9

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

proof end;

theorem Th10: :: IDEAL_1:10

for b₁ being non empty doubleLoopStr holds the carrier of b₁ is Ideal of b₁

proof end;

theorem Th11: :: IDEAL_1:11

for b₁ being non empty doubleLoopStr holds the carrier of b₁ is LeftIdeal of b₁

proof end;

theorem Th12: :: IDEAL_1:12

for b₁ being non empty doubleLoopStr holds the carrier of b₁ is RightIdeal of b₁

proof end;

definition

let c₁ be non empty right_zeroed distributive add-cancelable left_zeroed doubleLoopStr ;
let c₂ be Ideal of c₁;
redefine attr trivial as a₂ is trivial means :: IDEAL_1:def 4
a₂ = {(0. a₁)};
compatibility

proof end;

end;

:: deftheorem Def4 defines trivial IDEAL_1:def 4 :

definition

let c₁ be 1-sorted ;
let c₂ be Subset of c₁;
attr a₂ is proper means :Def5: :: IDEAL_1:def 5
a₂ <> the carrier of a₁;

end;

:: deftheorem Def5 defines proper IDEAL_1:def 5 :

registration

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

proof end;

end;

registration

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

proof end;

end;

theorem Th13: :: IDEAL_1:13

for b₁ being non empty add-associative right_zeroed right_complementable left-distributive left_unital doubleLoopStr
for b₂ being non empty left-ideal Subset of b₁
for b₃ being Element of b₁ st b₃ in b₂ holds
- b₃ in b₂

proof end;

theorem Th14: :: IDEAL_1:14

for b₁ being non empty add-associative right_zeroed right_complementable right-distributive right_unital doubleLoopStr
for b₂ being non empty right-ideal Subset of b₁
for b₃ being Element of b₁ st b₃ in b₂ holds
- b₃ in b₂

proof end;

theorem Th15: :: IDEAL_1:15

for b₁ being non empty add-associative right_zeroed right_complementable left-distributive left_unital doubleLoopStr
for b₂ being LeftIdeal of b₁
for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₄ in b₂ holds
b₃ - b₄ in b₂

proof end;

theorem Th16: :: IDEAL_1:16

for b₁ being non empty add-associative right_zeroed right_complementable right-distributive right_unital doubleLoopStr
for b₂ being RightIdeal of b₁
for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₄ in b₂ holds
b₃ - b₄ in b₂

proof end;

theorem Th17: :: IDEAL_1:17

for b₁ being non empty add-associative right_zeroed distributive add-cancelable left_zeroed doubleLoopStr
for b₂ being non empty add-closed right-ideal Subset of b₁
for b₃ being Element of b₂
for b₄ being Nat holds b₄ * b₃ in b₂

proof end;

theorem Th18: :: IDEAL_1:18

for b₁ being non empty unital associative right_zeroed distributive add-cancelable left_zeroed doubleLoopStr
for b₂ being non empty right-ideal Subset of b₁
for b₃ being Element of b₂
for b₄ being Nat st b₄ <> 0 holds
b₃ |^ b₄ in b₂

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂ be non empty add-closed Subset of c₁;
func add| c₂,c₁ -> BinOp of a₂ equals :: IDEAL_1:def 6
the add of a₁ || a₂;
coherence

proof end;

end;

:: deftheorem Def6 defines add| IDEAL_1:def 6 :

definition

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

proof end;

end;

:: deftheorem Def7 defines mult| IDEAL_1:def 7 :

definition

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

end;

:: deftheorem Def8 defines Gr IDEAL_1:def 8 :

registration

let c₁ be non empty add-associative right_zeroed distributive add-cancelable left_zeroed doubleLoopStr ;
let c₂ be non empty add-closed Subset of c₁;
cluster Gr a₂,a₁ -> non empty add-associative ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed distributive add-cancelable left_zeroed doubleLoopStr ;
let c₂ be non empty add-closed right-ideal Subset of c₁;
cluster Gr a₂,a₁ -> non empty add-associative right_zeroed ;
coherence

proof end;

end;

registration

let c₁ be non empty Abelian doubleLoopStr ;
let c₂ be non empty add-closed Subset of c₁;
cluster Gr a₂,a₁ -> non empty Abelian ;
coherence

proof end;

end;

registration

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

proof end;

end;

Lemma18: for b₁ being comRing
for b₂ being Element of b₁ holds { (b₂ * b₃) where B is Element of b₁ : verum } is Ideal of b₁

proof end;

theorem Th19: :: IDEAL_1:19

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

proof end;

theorem Th20: :: IDEAL_1:20

for b₁ being non empty right_unital left_unital doubleLoopStr
for b₂ being non empty right-ideal Subset of b₁ holds
( b₂ is proper iff for b₃ being Element of b₁ st b₃ is unital holds
not b₃ in b₂ )

proof end;

theorem Th21: :: IDEAL_1:21

for b₁ being non empty right_unital doubleLoopStr
for b₂ being non empty left-ideal right-ideal Subset of b₁ holds
( b₂ is proper iff for b₃ being Element of b₁ st b₃ is unital holds
not b₃ in b₂ )

proof end;

theorem Th22: :: IDEAL_1:22

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

proof end;

definition

let c₁ be non empty multLoopStr ;
let c₂ be non empty Subset of c₁;
mode LinearCombination of c₂ -> FinSequence of the carrier of a₁ means :Def9: :: IDEAL_1:def 9
for b₁ being set st b₁ in dom a₃ holds
ex b₂, b₃ being Element of a₁ex b₄ being Element of a₂ st a₃ /. b₁ = (b₂ * b₄) * b₃;
existence

proof end;

mode LeftLinearCombination of c₂ -> FinSequence of the carrier of a₁ means :Def10: :: IDEAL_1:def 10
for b₁ being set st b₁ in dom a₃ holds
ex b₂ being Element of a₁ex b₃ being Element of a₂ st a₃ /. b₁ = b₂ * b₃;
existence

proof end;

mode RightLinearCombination of c₂ -> FinSequence of the carrier of a₁ means :Def11: :: IDEAL_1:def 11
for b₁ being set st b₁ in dom a₃ holds
ex b₂ being Element of a₁ex b₃ being Element of a₂ st a₃ /. b₁ = b₃ * b₂;
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 c₁ be non empty multLoopStr ;
let c₂ be non empty Subset of c₁;
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 c₁ be non empty multLoopStr ;
let c₂, c₃ be non empty Subset of c₁;
let c₄ be LinearCombination of c₂;
let c₅ be LinearCombination of c₃;
redefine func ^ as c₄ ^ c₅ -> LinearCombination of a₂ \/ a₃;
coherence

proof end;

end;

theorem Th23: :: IDEAL_1:23

for b₁ being non empty associative multLoopStr
for b₂ being non empty Subset of b₁
for b₃ being Element of b₁
for b₄ being LinearCombination of b₂ holds b₃ * b₄ is LinearCombination of b₂

proof end;

theorem Th24: :: IDEAL_1:24

for b₁ being non empty associative multLoopStr
for b₂ being non empty Subset of b₁
for b₃ being Element of b₁
for b₄ being LinearCombination of b₂ holds b₄ * b₃ is LinearCombination of b₂

proof end;

theorem Th25: :: IDEAL_1:25

for b₁ being non empty right_unital multLoopStr
for b₂ being non empty Subset of b₁
for b₃ being LeftLinearCombination of b₂ holds b₃ is LinearCombination of b₂

proof end;

definition

let c₁ be non empty multLoopStr ;
let c₂, c₃ be non empty Subset of c₁;
let c₄ be LeftLinearCombination of c₂;
let c₅ be LeftLinearCombination of c₃;
redefine func ^ as c₄ ^ c₅ -> LeftLinearCombination of a₂ \/ a₃;
coherence

proof end;

end;

theorem Th26: :: IDEAL_1:26

for b₁ being non empty associative multLoopStr
for b₂ being non empty Subset of b₁
for b₃ being Element of b₁
for b₄ being LeftLinearCombination of b₂ holds b₃ * b₄ is LeftLinearCombination of b₂

proof end;

theorem Th27: :: IDEAL_1:27

for b₁ being non empty multLoopStr
for b₂ being non empty Subset of b₁
for b₃ being Element of b₁
for b₄ being LeftLinearCombination of b₂ holds b₄ * b₃ is LinearCombination of b₂

proof end;

theorem Th28: :: IDEAL_1:28

for b₁ being non empty left_unital multLoopStr
for b₂ being non empty Subset of b₁
for b₃ being RightLinearCombination of b₂ holds b₃ is LinearCombination of b₂

proof end;

definition

let c₁ be non empty multLoopStr ;
let c₂, c₃ be non empty Subset of c₁;
let c₄ be RightLinearCombination of c₂;
let c₅ be RightLinearCombination of c₃;
redefine func ^ as c₄ ^ c₅ -> RightLinearCombination of a₂ \/ a₃;
coherence

proof end;

end;

theorem Th29: :: IDEAL_1:29

for b₁ being non empty associative multLoopStr
for b₂ being non empty Subset of b₁
for b₃ being Element of b₁
for b₄ being RightLinearCombination of b₂ holds b₄ * b₃ is RightLinearCombination of b₂

proof end;

theorem Th30: :: IDEAL_1:30

for b₁ being non empty associative multLoopStr
for b₂ being non empty Subset of b₁
for b₃ being Element of b₁
for b₄ being RightLinearCombination of b₂ holds b₃ * b₄ is LinearCombination of b₂

proof end;

theorem Th31: :: IDEAL_1:31

for b₁ being non empty associative commutative multLoopStr
for b₂ being non empty Subset of b₁
for b₃ being LinearCombination of b₂ holds
( b₃ is LeftLinearCombination of b₂ & b₃ is RightLinearCombination of b₂ )

proof end;

theorem Th32: :: IDEAL_1:32

for b₁ being non empty doubleLoopStr
for b₂ being non empty Subset of b₁
for b₃ being non empty LinearCombination of b₂ ex b₄ being LinearCombination of b₂ex b₅ being Element of b₁ st
( b₃ = b₄ ^ <*b₅*> & <*b₅*> is LinearCombination of b₂ )

proof end;

theorem Th33: :: IDEAL_1:33

for b₁ being non empty doubleLoopStr
for b₂ being non empty Subset of b₁
for b₃ being non empty LeftLinearCombination of b₂ ex b₄ being LeftLinearCombination of b₂ex b₅ being Element of b₁ st
( b₃ = b₄ ^ <*b₅*> & <*b₅*> is LeftLinearCombination of b₂ )

proof end;

theorem Th34: :: IDEAL_1:34

for b₁ being non empty doubleLoopStr
for b₂ being non empty Subset of b₁
for b₃ being non empty RightLinearCombination of b₂ ex b₄ being RightLinearCombination of b₂ex b₅ being Element of b₁ st
( b₃ = b₄ ^ <*b₅*> & <*b₅*> is RightLinearCombination of b₂ )

proof end;

definition

let c₁ be non empty multLoopStr ;
let c₂ be non empty Subset of c₁;
let c₃ be LinearCombination of c₂;
let c₄ be FinSequence of [:the carrier of c₁,the carrier of c₁,the carrier of c₁:];
pred c₄ represents c₃ means :Def12: :: IDEAL_1:def 12
( len a₄ = len a₃ & ( for b₁ being set st b₁ in dom a₃ holds
( a₃ . b₁ = (((a₄ /. b₁) `1 ) * ((a₄ /. b₁) `2 )) * ((a₄ /. b₁) `3 ) & (a₄ /. b₁) `2 in a₂ ) ) );

end;

:: deftheorem Def12 defines represents IDEAL_1:def 12 :

theorem Th35: :: IDEAL_1:35

for b₁ being non empty multLoopStr
for b₂ being non empty Subset of b₁
for b₃ being LinearCombination of b₂ ex b₄ being FinSequence of [:the carrier of b₁,the carrier of b₁,the carrier of b₁:] st b₄ represents b₃

proof end;

theorem Th36: :: IDEAL_1:36

for b₁, b₂ being non empty multLoopStr
for b₃ being non empty Subset of b₁
for b₄ being LinearCombination of b₃
for b₅ being non empty Subset of b₂
for b₆ being Function of the carrier of b₁,the carrier of b₂
for b₇ being FinSequence of [:the carrier of b₁,the carrier of b₁,the carrier of b₁:] st b₆ .: b₃ c= b₅ & b₇ represents b₄ holds
ex b₈ being LinearCombination of b₅ st
( len b₄ = len b₈ & ( for b₉ being set st b₉ in dom b₈ holds
b₈ . b₉ = ((b₆ . ((b₇ /. b₉) `1 )) * (b₆ . ((b₇ /. b₉) `2 ))) * (b₆ . ((b₇ /. b₉) `3 )) ) )

proof end;

definition

let c₁ be non empty multLoopStr ;
let c₂ be non empty Subset of c₁;
let c₃ be LeftLinearCombination of c₂;
let c₄ be FinSequence of [:the carrier of c₁,the carrier of c₁:];
pred c₄ represents c₃ means :Def13: :: IDEAL_1:def 13
( len a₄ = len a₃ & ( for b₁ being set st b₁ in dom a₃ holds
( a₃ . b₁ = ((a₄ /. b₁) `1 ) * ((a₄ /. b₁) `2 ) & (a₄ /. b₁) `2 in a₂ ) ) );

end;

:: deftheorem Def13 defines represents IDEAL_1:def 13 :

theorem Th37: :: IDEAL_1:37

for b₁ being non empty multLoopStr
for b₂ being non empty Subset of b₁
for b₃ being LeftLinearCombination of b₂ ex b₄ being FinSequence of [:the carrier of b₁,the carrier of b₁:] st b₄ represents b₃

proof end;

theorem Th38: :: IDEAL_1:38

for b₁, b₂ being non empty multLoopStr
for b₃ being non empty Subset of b₁
for b₄ being LeftLinearCombination of b₃
for b₅ being non empty Subset of b₂
for b₆ being Function of the carrier of b₁,the carrier of b₂
for b₇ being FinSequence of [:the carrier of b₁,the carrier of b₁:] st b₆ .: b₃ c= b₅ & b₇ represents b₄ holds
ex b₈ being LeftLinearCombination of b₅ st
( len b₄ = len b₈ & ( for b₉ being set st b₉ in dom b₈ holds
b₈ . b₉ = (b₆ . ((b₇ /. b₉) `1 )) * (b₆ . ((b₇ /. b₉) `2 )) ) )

proof end;

definition

let c₁ be non empty multLoopStr ;
let c₂ be non empty Subset of c₁;
let c₃ be RightLinearCombination of c₂;
let c₄ be FinSequence of [:the carrier of c₁,the carrier of c₁:];
pred c₄ represents c₃ means :Def14: :: IDEAL_1:def 14
( len a₄ = len a₃ & ( for b₁ being set st b₁ in dom a₃ holds
( a₃ . b₁ = ((a₄ /. b₁) `1 ) * ((a₄ /. b₁) `2 ) & (a₄ /. b₁) `1 in a₂ ) ) );

end;

:: deftheorem Def14 defines represents IDEAL_1:def 14 :

theorem Th39: :: IDEAL_1:39

for b₁ being non empty multLoopStr
for b₂ being non empty Subset of b₁
for b₃ being RightLinearCombination of b₂ ex b₄ being FinSequence of [:the carrier of b₁,the carrier of b₁:] st b₄ represents b₃

proof end;

theorem Th40: :: IDEAL_1:40

for b₁, b₂ being non empty multLoopStr
for b₃ being non empty Subset of b₁
for b₄ being RightLinearCombination of b₃
for b₅ being non empty Subset of b₂
for b₆ being Function of the carrier of b₁,the carrier of b₂
for b₇ being FinSequence of [:the carrier of b₁,the carrier of b₁:] st b₆ .: b₃ c= b₅ & b₇ represents b₄ holds
ex b₈ being RightLinearCombination of b₅ st
( len b₄ = len b₈ & ( for b₉ being set st b₉ in dom b₈ holds
b₈ . b₉ = (b₆ . ((b₇ /. b₉) `1 )) * (b₆ . ((b₇ /. b₉) `2 )) ) )

proof end;

theorem Th41: :: IDEAL_1:41

for b₁ being non empty multLoopStr
for b₂ being non empty Subset of b₁
for b₃ being LinearCombination of b₂
for b₄ being Nat holds b₃ | (Seg b₄) is LinearCombination of b₂

proof end;

theorem Th42: :: IDEAL_1:42

for b₁ being non empty multLoopStr
for b₂ being non empty Subset of b₁
for b₃ being LeftLinearCombination of b₂
for b₄ being Nat holds b₃ | (Seg b₄) is LeftLinearCombination of b₂

proof end;

theorem Th43: :: IDEAL_1:43

for b₁ being non empty multLoopStr
for b₂ being non empty Subset of b₁
for b₃ being RightLinearCombination of b₂
for b₄ being Nat holds b₃ | (Seg b₄) is RightLinearCombination of b₂

proof end;

definition

let c₁ be non empty doubleLoopStr ;
let c₂ be Subset of c₁;
assume E36: not c₂ is empty ;
func c₂ -Ideal -> Ideal of a₁ means :Def15: :: IDEAL_1:def 15
( a₂ c= a₃ & ( for b₁ being Ideal of a₁ st a₂ c= b₁ holds
a₃ c= b₁ ) );
existence

proof end;

uniqueness

proof end;

func c₂ -LeftIdeal -> LeftIdeal of a₁ means :Def16: :: IDEAL_1:def 16
( a₂ c= a₃ & ( for b₁ being LeftIdeal of a₁ st a₂ c= b₁ holds
a₃ c= b₁ ) );
existence

proof end;

uniqueness

proof end;

func c₂ -RightIdeal -> RightIdeal of a₁ means :Def17: :: IDEAL_1:def 17
( a₂ c= a₃ & ( for b₁ being RightIdeal of a₁ st a₂ c= b₁ holds
a₃ c= b₁ ) );
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 b₁ being non empty doubleLoopStr
for b₂ being Ideal of b₁ holds b₂ -Ideal = b₂

proof end;

theorem Th45: :: IDEAL_1:45

for b₁ being non empty doubleLoopStr
for b₂ being LeftIdeal of b₁ holds b₂ -LeftIdeal = b₂

proof end;

theorem Th46: :: IDEAL_1:46

for b₁ being non empty doubleLoopStr
for b₂ being RightIdeal of b₁ holds b₂ -RightIdeal = b₂

proof end;

definition

let c₁ be non empty doubleLoopStr ;
let c₂ be Ideal of c₁;
mode Basis of c₂ -> non empty Subset of a₁ means :: IDEAL_1:def 18
a₃ -Ideal = a₂;
existence

proof end;

end;

:: deftheorem Def18 defines Basis IDEAL_1:def 18 :

theorem Th47: :: IDEAL_1:47

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

proof end;

theorem Th48: :: IDEAL_1:48

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

proof end;

theorem Th49: :: IDEAL_1:49

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

proof end;

theorem Th50: :: IDEAL_1:50

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

proof end;

theorem Th51: :: IDEAL_1:51

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

proof end;

theorem Th52: :: IDEAL_1:52

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

proof end;

theorem Th53: :: IDEAL_1:53

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

proof end;

theorem Th54: :: IDEAL_1:54

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

proof end;

theorem Th55: :: IDEAL_1:55

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

proof end;

theorem Th56: :: IDEAL_1:56

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

proof end;

theorem Th57: :: IDEAL_1:57

for b₁ being non empty doubleLoopStr
for b₂, b₃ being non empty Subset of b₁ st b₂ c= b₃ holds
b₂ -Ideal c= b₃ -Ideal

proof end;

theorem Th58: :: IDEAL_1:58

for b₁ being non empty doubleLoopStr
for b₂, b₃ being non empty Subset of b₁ st b₂ c= b₃ holds
b₂ -LeftIdeal c= b₃ -LeftIdeal

proof end;

theorem Th59: :: IDEAL_1:59

for b₁ being non empty doubleLoopStr
for b₂, b₃ being non empty Subset of b₁ st b₂ c= b₃ holds
b₂ -RightIdeal c= b₃ -RightIdeal

proof end;

theorem Th60: :: IDEAL_1:60

for b₁ being non empty unital associative add-associative right_zeroed distributive add-cancelable left_zeroed doubleLoopStr
for b₂ being non empty Subset of b₁
for b₃ being set holds
( b₃ in b₂ -Ideal iff ex b₄ being LinearCombination of b₂ st b₃ = Sum b₄ )

proof end;

theorem Th61: :: IDEAL_1:61

for b₁ being non empty unital associative add-associative right_zeroed distributive add-cancelable left_zeroed doubleLoopStr
for b₂ being non empty Subset of b₁
for b₃ being set holds
( b₃ in b₂ -LeftIdeal iff ex b₄ being LeftLinearCombination of b₂ st b₃ = Sum b₄ )

proof end;

theorem Th62: :: IDEAL_1:62

for b₁ being non empty unital associative add-associative right_zeroed distributive add-cancelable left_zeroed doubleLoopStr
for b₂ being non empty Subset of b₁
for b₃ being set holds
( b₃ in b₂ -RightIdeal iff ex b₄ being RightLinearCombination of b₂ st b₃ = Sum b₄ )

proof end;

theorem Th63: :: IDEAL_1:63

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

proof end;

theorem Th64: :: IDEAL_1:64

for b₁ being non empty unital associative commutative add-associative right_zeroed distributive add-cancelable left_zeroed doubleLoopStr
for b₂ being Element of b₁ holds {b₂} -Ideal = { (b₂ * b₃) where B is Element of b₁ : verum }

proof end;

theorem Th65: :: IDEAL_1:65

for b₁ being non empty unital associative commutative Abelian add-associative right_zeroed distributive add-cancelable left_zeroed doubleLoopStr
for b₂, b₃ being Element of b₁ holds {b₂,b₃} -Ideal = { ((b₂ * b₄) + (b₃ * b₅)) where B is Element of b₁, B is Element of b₁ : verum }

proof end;

theorem Th66: :: IDEAL_1:66

for b₁ being non empty doubleLoopStr
for b₂ being Element of b₁ holds b₂ in {b₂} -Ideal

proof end;

theorem Th67: :: IDEAL_1:67

for b₁ being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive left_zeroed doubleLoopStr
for b₂ being non empty Subset of b₁
for b₃ being Element of b₁ st b₃ in b₂ -Ideal holds
{b₃} -Ideal c= b₂ -Ideal

proof end;

Lemma51: for b₁, b₂ being set holds {b₁} c= {b₁,b₂}

proof end;

theorem Th68: :: IDEAL_1:68

for b₁ being non empty doubleLoopStr
for b₂, b₃ being Element of b₁ holds
( b₂ in {b₂,b₃} -Ideal & b₃ in {b₂,b₃} -Ideal )

proof end;

theorem Th69: :: IDEAL_1:69

for b₁ being non empty doubleLoopStr
for b₂, b₃ being Element of b₁ holds
( {b₂} -Ideal c= {b₂,b₃} -Ideal & {b₃} -Ideal c= {b₂,b₃} -Ideal )

proof end;

definition

let c₁ be non empty HGrStr ;
let c₂ be Subset of c₁;
let c₃ be Element of c₁;
func c₃ * c₂ -> Subset of a₁ equals :: IDEAL_1:def 19
{ (a₃ * b₁) where B is Element of a₁ : b₁ in a₂ } ;
coherence

proof end;

end;

:: deftheorem Def19 defines * IDEAL_1:def 19 :

registration

let c₁ be non empty multLoopStr ;
let c₂ be non empty Subset of c₁;
let c₃ be Element of c₁;
cluster a₃ * a₂ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be non empty distributive doubleLoopStr ;
let c₂ be add-closed Subset of c₁;
let c₃ be Element of c₁;
cluster a₃ * a₂ -> add-closed ;
coherence

proof end;

end;

registration

let c₁ be non empty associative doubleLoopStr ;
let c₂ be right-ideal Subset of c₁;
let c₃ be Element of c₁;
cluster a₃ * a₂ -> right-ideal ;
coherence

proof end;

end;

theorem Th70: :: IDEAL_1:70

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

proof end;

theorem Th71: :: IDEAL_1:71

for b₁ being non empty left_unital doubleLoopStr
for b₂ being Subset of b₁ holds (1. b₁) * b₂ = b₂

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂, c₃ be Subset of c₁;
func c₂ + c₃ -> Subset of a₁ equals :: IDEAL_1:def 20
{ (b₁ + b₂) where B is Element of a₁, B is Element of a₁ : ( b₁ in a₂ & b₂ in a₃ ) } ;
coherence

proof end;

end;

:: deftheorem Def20 defines + IDEAL_1:def 20 :

registration

let c₁ be non empty LoopStr ;
let c₂, c₃ be non empty Subset of c₁;
cluster a₂ + a₃ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be non empty Abelian LoopStr ;
let c₂, c₃ be Subset of c₁;
redefine func + as c₂ + c₃ -> Subset of a₁;
commutativity

proof end;

end;

registration

let c₁ be non empty Abelian add-associative LoopStr ;
let c₂, c₃ be add-closed Subset of c₁;
cluster a₂ + a₃ -> add-closed ;
coherence

proof end;

end;

registration

let c₁ be non empty left-distributive doubleLoopStr ;
let c₂, c₃ be right-ideal Subset of c₁;
cluster a₂ + a₃ -> right-ideal ;
coherence

proof end;

end;

registration

let c₁ be non empty right-distributive doubleLoopStr ;
let c₂, c₃ be left-ideal Subset of c₁;
cluster a₂ + a₃ -> left-ideal ;
coherence

proof end;

end;

theorem Th72: :: IDEAL_1:72

for b₁ being non empty add-associative LoopStr
for b₂, b₃, b₄ being Subset of b₁ holds b₂ + (b₃ + b₄) = (b₂ + b₃) + b₄

proof end;

theorem Th73: :: IDEAL_1:73

for b₁ being non empty right_zeroed right-distributive left_zeroed add-right-cancelable doubleLoopStr
for b₂, b₃ being non empty right-ideal Subset of b₁ holds b₂ c= b₂ + b₃

proof end;

theorem Th74: :: IDEAL_1:74

for b₁ being non empty right-distributive left_zeroed add-right-cancelable doubleLoopStr
for b₂, b₃ being non empty right-ideal Subset of b₁ holds b₃ c= b₂ + b₃

proof end;

theorem Th75: :: IDEAL_1:75

for b₁ being non empty LoopStr
for b₂, b₃ being Subset of b₁
for b₄ being add-closed Subset of b₁ st b₂ c= b₄ & b₃ c= b₄ holds
b₂ + b₃ c= b₄

proof end;

theorem Th76: :: IDEAL_1:76

proof end;

definition

let c₁ be non empty 1-sorted ;
let c₂, c₃ be Subset of c₁;
redefine func /\ as c₂ /\ c₃ -> Subset of a₁ equals :: IDEAL_1:def 21
{ b₁ where B is Element of a₁ : ( b₁ in a₂ & b₁ in a₃ ) } ;
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def21 defines /\ IDEAL_1:def 21 :

registration

let c₁ be non empty right_zeroed left-distributive add-left-cancelable doubleLoopStr ;
let c₂, c₃ be non empty left-ideal Subset of c₁;
cluster a₂ /\ a₃ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be non empty LoopStr ;
let c₂, c₃ be add-closed Subset of c₁;
cluster a₂ /\ a₃ -> add-closed ;
coherence

proof end;

end;

registration

let c₁ be non empty multLoopStr ;
let c₂, c₃ be left-ideal Subset of c₁;
cluster a₂ /\ a₃ -> left-ideal ;
coherence

proof end;

end;

registration

let c₁ be non empty multLoopStr ;
let c₂, c₃ be right-ideal Subset of c₁;
cluster a₂ /\ a₃ -> right-ideal ;
coherence

proof end;

end;

theorem Th77: :: IDEAL_1:77

for b₁ being non empty 1-sorted
for b₂, b₃ being Subset of b₁ holds
( b₂ /\ b₃ c= b₂ & b₂ /\ b₃ c= b₃ ) by XBOOLE_1:17;

theorem Th78: :: IDEAL_1:78

for b₁ being non empty 1-sorted
for b₂, b₃, b₄ being Subset of b₁ holds b₂ /\ (b₃ /\ b₄) = (b₂ /\ b₃) /\ b₄ by XBOOLE_1:16;

theorem Th79: :: IDEAL_1:79

for b₁ being non empty 1-sorted
for b₂, b₃, b₄ being Subset of b₁ st b₄ c= b₂ & b₄ c= b₃ holds
b₄ c= b₂ /\ b₃ by XBOOLE_1:19;

theorem Th80: :: IDEAL_1:80

for b₁ being non empty Abelian add-associative right_zeroed right_complementable left-distributive left_unital left_zeroed doubleLoopStr
for b₂ being non empty add-closed left-ideal Subset of b₁
for b₃ being Subset of b₁
for b₄ being non empty Subset of b₁ st b₃ c= b₂ holds
b₂ /\ (b₃ + b₄) = b₃ + (b₂ /\ b₄)

proof end;

definition

let c₁ be non empty doubleLoopStr ;
let c₂, c₃ be Subset of c₁;
func c₂ *' c₃ -> Subset of a₁ equals :: IDEAL_1:def 22
{ (Sum b₁) where B is FinSequence of the carrier of a₁ : for b₁ being Nat st 1 <= b₂ & b₂ <= len b₁ holds
ex b₂, b₃ being Element of a₁ st
( b₁ . b₂ = b₃ * b₄ & b₃ in a₂ & b₄ in a₃ ) } ;
coherence

proof end;

end;

:: deftheorem Def22 defines *' IDEAL_1:def 22 :

registration

let c₁ be non empty doubleLoopStr ;
let c₂, c₃ be Subset of c₁;
cluster a₂ *' a₃ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be non empty commutative doubleLoopStr ;
let c₂, c₃ be Subset of c₁;
redefine func *' as c₂ *' c₃ -> Subset of a₁;
commutativity

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed doubleLoopStr ;
let c₂, c₃ be Subset of c₁;
cluster a₂ *' a₃ -> non empty add-closed ;
coherence

proof end;

end;

registration

let c₁ be non empty associative right_zeroed left-distributive add-left-cancelable doubleLoopStr ;
let c₂, c₃ be right-ideal Subset of c₁;
cluster a₂ *' a₃ -> non empty right-ideal ;
coherence

proof end;

end;

registration

let c₁ be non empty associative right-distributive left_zeroed add-right-cancelable doubleLoopStr ;
let c₂, c₃ be left-ideal Subset of c₁;
cluster a₂ *' a₃ -> non empty left-ideal ;
coherence

proof end;

end;

theorem Th81: :: IDEAL_1:81

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

proof end;

theorem Th82: :: IDEAL_1:82

for b₁ being non empty right_zeroed distributive add-cancelable left_zeroed doubleLoopStr
for b₂ being non empty add-closed right-ideal Subset of b₁
for b₃ being non empty add-closed left-ideal Subset of b₁ holds b₂ *' b₃ c= b₂ /\ b₃

proof end;

theorem Th83: :: IDEAL_1:83

for b₁ being non empty associative Abelian add-associative right_zeroed distributive add-cancelable left_zeroed doubleLoopStr
for b₂, b₃, b₄ being non empty right-ideal Subset of b₁ holds b₂ *' (b₃ + b₄) = (b₂ *' b₃) + (b₂ *' b₄)

proof end;

theorem Th84: :: IDEAL_1:84

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

proof end;

theorem Th85: :: IDEAL_1:85

for b₁ being non empty right_zeroed left-distributive add-left-cancelable doubleLoopStr
for b₂, b₃ being non empty add-closed left-ideal Subset of b₁ holds (b₂ + b₃) *' (b₂ /\ b₃) c= b₂ /\ b₃

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂, c₃ be Subset of c₁;
pred c₂,c₃ are_co-prime means :Def23: :: IDEAL_1:def 23
a₂ + a₃ = the carrier of a₁;

end;

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

theorem Th86: :: IDEAL_1:86

for b₁ being non empty left_unital left_zeroed doubleLoopStr
for b₂, b₃ being non empty Subset of b₁ st b₂,b₃ are_co-prime holds
b₂ /\ b₃ c= (b₂ + b₃) *' (b₂ /\ b₃)

proof end;

theorem Th87: :: IDEAL_1:87

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

proof end;

definition

let c₁ be non empty HGrStr ;
let c₂, c₃ be Subset of c₁;
func c₂ % c₃ -> Subset of a₁ equals :: IDEAL_1:def 24
{ b₁ where B is Element of a₁ : b₁ * a₃ c= a₂ } ;
coherence

proof end;

end;

:: deftheorem Def24 defines % IDEAL_1:def 24 :

registration

let c₁ be non empty right_zeroed left-distributive add-left-cancelable doubleLoopStr ;
let c₂, c₃ be non empty left-ideal Subset of c₁;
cluster a₂ % a₃ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be non empty right_zeroed left-distributive add-left-cancelable doubleLoopStr ;
let c₂, c₃ be non empty add-closed left-ideal Subset of c₁;
cluster a₂ % a₃ -> non empty add-closed ;
coherence

proof end;

end;

registration

let c₁ be non empty associative commutative right_zeroed left-distributive add-left-cancelable doubleLoopStr ;
let c₂, c₃ be non empty left-ideal Subset of c₁;
cluster a₂ % a₃ -> non empty left-ideal right-ideal ;
coherence

proof end;

cluster a₂ % a₃ -> non empty left-ideal right-ideal ;
coherence ;

end;

theorem Th88: :: IDEAL_1:88

for b₁ being non empty multLoopStr
for b₂ being non empty right-ideal Subset of b₁
for b₃ being Subset of b₁ holds b₂ c= b₂ % b₃

proof end;

theorem Th89: :: IDEAL_1:89

for b₁ being non empty right_zeroed left-distributive add-left-cancelable doubleLoopStr
for b₂ being non empty add-closed left-ideal Subset of b₁
for b₃ being Subset of b₁ holds (b₂ % b₃) *' b₃ c= b₂

proof end;

theorem Th90: :: IDEAL_1:90

for b₁ being non empty right-distributive left_zeroed add-right-cancelable doubleLoopStr
for b₂ being non empty add-closed right-ideal Subset of b₁
for b₃ being Subset of b₁ holds (b₂ % b₃) *' b₃ c= b₂

proof end;

theorem Th91: :: IDEAL_1:91

for b₁ being non empty associative commutative right-distributive left_zeroed add-right-cancelable doubleLoopStr
for b₂ being non empty add-closed right-ideal Subset of b₁
for b₃, b₄ being Subset of b₁ holds (b₂ % b₃) % b₄ = b₂ % (b₃ *' b₄)

proof end;

theorem Th92: :: IDEAL_1:92

for b₁ being non empty multLoopStr
for b₂, b₃, b₄ being Subset of b₁ holds (b₃ /\ b₄) % b₂ = (b₃ % b₂) /\ (b₄ % b₂)

proof end;

theorem Th93: :: IDEAL_1:93

for b₁ being non empty right_zeroed right-distributive left_zeroed add-right-cancelable doubleLoopStr
for b₂ being add-closed Subset of b₁
for b₃, b₄ being non empty right-ideal Subset of b₁ holds b₂ % (b₃ + b₄) = (b₂ % b₃) /\ (b₂ % b₄)

proof end;

definition

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

proof end;

end;

:: deftheorem Def25 defines sqrt IDEAL_1:def 25 :

registration

let c₁ be non empty unital doubleLoopStr ;
let c₂ be non empty Subset of c₁;
cluster sqrt a₂ -> non empty ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

let c₁ be non empty unital associative commutative doubleLoopStr ;
let c₂ be non empty left-ideal Subset of c₁;
cluster sqrt a₂ -> non empty left-ideal right-ideal ;
coherence

proof end;

cluster sqrt a₂ -> non empty left-ideal right-ideal ;
coherence ;

end;

theorem Th94: :: IDEAL_1:94

for b₁ being non empty unital associative doubleLoopStr
for b₂ being non empty Subset of b₁
for b₃ being Element of b₁ holds
( b₃ in sqrt b₂ iff ex b₄ being Nat st b₃ |^ b₄ in sqrt b₂ )

proof end;

theorem Th95: :: IDEAL_1:95

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

proof end;

definition

let c₁ be non empty doubleLoopStr ;
let c₂ be Ideal of c₁;
attr a₂ is finitely_generated means :Def26: :: IDEAL_1:def 26
ex b₁ being non empty finite Subset of a₁ st a₂ = b₁ -Ideal ;

end;

:: deftheorem Def26 defines finitely_generated IDEAL_1:def 26 :

registration

let c₁ be non empty doubleLoopStr ;
cluster finitely_generated Element of bool the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be non empty doubleLoopStr ;
let c₂ be non empty finite Subset of c₁;
cluster a₂ -Ideal -> finitely_generated ;
coherence by Def26;

end;

definition

let c₁ be non empty doubleLoopStr ;
attr a₁ is Noetherian means :Def27: :: IDEAL_1:def 27
for b₁ being Ideal of a₁ holds b₁ 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 c₁ be non empty doubleLoopStr ;
let c₂ be Ideal of c₁;
attr a₂ is principal means :Def28: :: IDEAL_1:def 28
ex b₁ being Element of a₁ st a₂ = {b₁} -Ideal ;

end;

:: deftheorem Def28 defines principal IDEAL_1:def 28 :

definition

let c₁ be non empty doubleLoopStr ;
attr a₁ is PID means :Def29: :: IDEAL_1:def 29
for b₁ being Ideal of a₁ holds b₁ is principal;

end;

:: deftheorem Def29 defines PID IDEAL_1:def 29 :

theorem Th96: :: IDEAL_1:96

for b₁ being non empty doubleLoopStr
for b₂ being non empty Subset of b₁ st b₂ <> {(0. b₁)} holds
ex b₃ being Element of b₁ st
( b₃ <> 0. b₁ & b₃ in b₂ )

proof end;

theorem Th97: :: IDEAL_1:97

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

proof end;

theorem Th98: :: IDEAL_1:98

for b₁ being non empty doubleLoopStr st b₁ is PID holds
b₁ 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 Th99: :: IDEAL_1:99

for b₁ being non empty unital associative add-associative right_zeroed distributive add-cancelable left_zeroed Noetherian doubleLoopStr
for b₂ being non empty Subset of b₁ ex b₃ being non empty finite Subset of b₁ st
( b₃ c= b₂ & b₃ -Ideal = b₂ -Ideal )

proof end;

theorem Th100: :: IDEAL_1:100

for b₁ being non empty doubleLoopStr st ( for b₂ being non empty Subset of b₁ ex b₃ being non empty finite Subset of b₁ st
( b₃ c= b₂ & b₃ -Ideal = b₂ -Ideal ) ) holds
for b₂ being sequence of b₁ ex b₃ being Nat st b₂ . (b₃ + 1) in (rng (b₂ | (Segm (b₃ + 1)))) -Ideal

proof end;

registration

let c₁, c₂ be non empty set ;
let c₃ be Function of c₁,c₂;
let c₄ be non empty Subset of c₁;
cluster a₃ | a₄ -> non empty ;
coherence

proof end;

end;

theorem Th101: :: IDEAL_1:101

for b₁ being non empty doubleLoopStr st ( for b₂ being sequence of b₁ ex b₃ being Nat st b₂ . (b₃ + 1) in (rng (b₂ | (Segm (b₃ + 1)))) -Ideal ) holds
for b₂ being Function of NAT , bool the carrier of b₁ holds
( ex b₃ being Nat st b₂ . b₃ is not Ideal of b₁ or ex b₃, b₄ being Nat st
( b₃ < b₄ & not b₂ . b₃ c< b₂ . b₄ ) )

proof end;

theorem Th102: :: IDEAL_1:102

for b₁ being non empty doubleLoopStr st ( for b₂ being Function of NAT , bool the carrier of b₁ holds
( ex b₃ being Nat st b₂ . b₃ is not Ideal of b₁ or ex b₃, b₄ being Nat st
( b₃ < b₄ & not b₂ . b₃ c< b₂ . b₄ ) ) ) holds
b₁ is Noetherian

proof end;