:: IDEAL_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
cluster non empty add-associative right_zeroed left_zeroed LoopStr ;
existence
ex b1 being non empty LoopStr st
( b1 is add-associative & b1 is left_zeroed & b1 is right_zeroed )
proof end;
end;

registration
cluster non empty unital associative commutative Abelian add-associative right_zeroed distributive add-cancelable left_zeroed non trivial doubleLoopStr ;
existence
ex b1 being non empty doubleLoopStr st
( b1 is Abelian & b1 is left_zeroed & b1 is right_zeroed & b1 is add-cancelable & b1 is unital & b1 is add-associative & b1 is associative & b1 is commutative & b1 is distributive & not b1 is trivial )
proof end;
end;

theorem Th1: :: IDEAL_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
for L being non empty LoopStr
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 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 :
for L being non empty HGrStr
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 HGrStr
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 LoopStr ;
cluster non empty add-closed Element of bool the carrier of L;
existence
ex b1 being non empty Subset of L st b1 is add-closed
proof end;
end;

registration
let L be non empty HGrStr ;
cluster non empty left-ideal Element of bool the carrier of L;
existence
ex b1 being non empty Subset of L st b1 is left-ideal
proof end;
cluster non empty right-ideal Element of bool the carrier of L;
existence
ex b1 being non empty Subset of L st b1 is right-ideal
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
ex b1 being non empty Subset of L st
( b1 is add-closed & b1 is left-ideal & b1 is right-ideal )
proof end;
cluster non empty add-closed right-ideal Element of bool the carrier of L;
existence
ex b1 being non empty Subset of L st
( b1 is add-closed & b1 is right-ideal )
proof end;
cluster non empty add-closed left-ideal Element of bool the carrier of L;
existence
ex b1 being non empty Subset of L st
( b1 is add-closed & b1 is left-ideal )
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
for b1 being non empty Subset of R st b1 is left-ideal holds
b1 is right-ideal
proof end;
cluster non empty right-ideal -> non empty left-ideal Element of bool the carrier of R;
coherence
for b1 being non empty Subset of R st b1 is right-ideal holds
b1 is left-ideal
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty right_zeroed LoopStr holds {(0. L)} is add-closed
proof end;

theorem Th5: :: IDEAL_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
{(0. L)} is add-closed Subset of L
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
{(0. L)} is left-ideal Subset of L
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
{(0. L)} is right-ideal Subset of L
by Th6;
end;

theorem Th7: :: IDEAL_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty doubleLoopStr holds the carrier of L is Ideal of L
proof end;

theorem Th11: :: IDEAL_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty doubleLoopStr holds the carrier of L is LeftIdeal of L
proof end;

theorem Th12: :: IDEAL_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
( I is trivial iff I = {(0. R)} )
proof end;
end;

:: deftheorem defines trivial IDEAL_1:def 4 :
for R being non empty right_zeroed distributive add-cancelable left_zeroed doubleLoopStr
for I being Ideal of R holds
( I is trivial iff I = {(0. R)} );

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 :
for S being 1-sorted
for T being Subset of S holds
( T is proper iff T <> the carrier of S );

registration
let S be non empty 1-sorted ;
cluster proper Element of bool the carrier of S;
existence
ex b1 being Subset of S st b1 is proper
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
ex b1 being Ideal of R st b1 is proper
proof end;
end;

theorem Th13: :: IDEAL_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
the add of R || I is BinOp of I
proof end;
end;

:: deftheorem defines add| IDEAL_1:def 6 :
for R being non empty LoopStr
for I being non empty add-closed Subset of R holds add| I,R = the add of R || I;

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
the mult of R || I is BinOp of I
proof end;
end;

:: deftheorem defines mult| IDEAL_1:def 7 :
for R being non empty HGrStr
for I being non empty right-ideal Subset of R holds mult| I,R = the mult of R || I;

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
LoopStr(# I,(add| I,R),(In (0. R),I) #) is non empty LoopStr
;
end;

:: deftheorem defines Gr IDEAL_1:def 8 :
for R being non empty LoopStr
for I being non empty add-closed Subset of R holds Gr I,R = LoopStr(# I,(add| I,R),(In (0. R),I) #);

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
Gr I,R is add-associative
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
Gr I,R is right_zeroed
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
Gr I,R is Abelian
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
Gr I,R is right_complementable
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being FinSequence of the carrier of R st
for i being set st i in dom b1 holds
ex u, v being Element of R ex a being Element of A st b1 /. i = (u * a) * v
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
ex b1 being FinSequence of the carrier of R st
for i being set st i in dom b1 holds
ex u being Element of R ex a being Element of A st b1 /. i = u * a
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
ex b1 being FinSequence of the carrier of R st
for i being set st i in dom b1 holds
ex u being Element of R ex a being Element of A st b1 /. i = a * u
proof end;
end;

:: deftheorem Def9 defines LinearCombination IDEAL_1:def 9 :
for R being non empty multLoopStr
for A being non empty Subset of R
for b3 being FinSequence of the carrier of R holds
( b3 is LinearCombination of A iff for i being set st i in dom b3 holds
ex u, v being Element of R ex a being Element of A st b3 /. i = (u * a) * v );

:: deftheorem Def10 defines LeftLinearCombination IDEAL_1:def 10 :
for R being non empty multLoopStr
for A being non empty Subset of R
for b3 being FinSequence of the carrier of R holds
( b3 is LeftLinearCombination of A iff for i being set st i in dom b3 holds
ex u being Element of R ex a being Element of A st b3 /. i = u * a );

:: deftheorem Def11 defines RightLinearCombination IDEAL_1:def 11 :
for R being non empty multLoopStr
for A being non empty Subset of R
for b3 being FinSequence of the carrier of R holds
( b3 is RightLinearCombination of A iff for i being set st i in dom b3 holds
ex u being Element of R ex a being Element of A st b3 /. i = a * u );

registration
let R be non empty multLoopStr ;
let A be non empty Subset of R;
cluster non empty LinearCombination of A;
existence
not for b1 being LinearCombination of A holds b1 is empty
proof end;
cluster non empty LeftLinearCombination of A;
existence
not for b1 being LeftLinearCombination of A holds b1 is empty
proof end;
cluster non empty RightLinearCombination of A;
existence
not for b1 being RightLinearCombination of A holds b1 is empty
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
F ^ G is LinearCombination of A \/ B
proof end;
end;

theorem Th23: :: IDEAL_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
F ^ G is LeftLinearCombination of A \/ B
proof end;
end;

theorem Th26: :: IDEAL_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
F ^ G is RightLinearCombination of A \/ B
proof end;
end;

theorem Th29: :: IDEAL_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
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 ) * ((E /. i) `2 )) * ((E /. i) `3 ) & (E /. i) `2 in A ) ) ) );

theorem :: IDEAL_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Ideal of L st
( F c= b1 & ( for I being Ideal of L st F c= I holds
b1 c= I ) )
proof end;
uniqueness
for b1, b2 being Ideal of L st F c= b1 & ( for I being Ideal of L st F c= I holds
b1 c= I ) & F c= b2 & ( for I being Ideal of L st F c= I holds
b2 c= I ) holds
b1 = b2
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
ex b1 being LeftIdeal of L st
( F c= b1 & ( for I being LeftIdeal of L st F c= I holds
b1 c= I ) )
proof end;
uniqueness
for b1, b2 being LeftIdeal of L st F c= b1 & ( for I being LeftIdeal of L st F c= I holds
b1 c= I ) & F c= b2 & ( for I being LeftIdeal of L st F c= I holds
b2 c= I ) holds
b1 = b2
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
ex b1 being RightIdeal of L st
( F c= b1 & ( for I being RightIdeal of L st F c= I holds
b1 c= I ) )
proof end;
uniqueness
for b1, b2 being RightIdeal of L st F c= b1 & ( for I being RightIdeal of L st F c= I holds
b1 c= I ) & F c= b2 & ( for I being RightIdeal of L st F c= I holds
b2 c= I ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines -Ideal IDEAL_1:def 15 :
for L being non empty doubleLoopStr
for F being Subset of L st not F is empty holds
for b3 being Ideal of L holds
( b3 = F -Ideal iff ( F c= b3 & ( for I being Ideal of L st F c= I holds
b3 c= I ) ) );

:: deftheorem Def16 defines -LeftIdeal IDEAL_1:def 16 :
for L being non empty doubleLoopStr
for F being Subset of L st not F is empty holds
for b3 being LeftIdeal of L holds
( b3 = F -LeftIdeal iff ( F c= b3 & ( for I being LeftIdeal of L st F c= I holds
b3 c= I ) ) );

:: deftheorem Def17 defines -RightIdeal IDEAL_1:def 17 :
for L being non empty doubleLoopStr
for F being Subset of L st not F is empty holds
for b3 being RightIdeal of L holds
( b3 = F -RightIdeal iff ( F c= b3 & ( for I being RightIdeal of L st F c= I holds
b3 c= I ) ) );

theorem Th44: :: IDEAL_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty doubleLoopStr
for I being Ideal of L holds I -Ideal = I
proof end;

theorem Th45: :: IDEAL_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty doubleLoopStr
for I being LeftIdeal of L holds I -LeftIdeal = I
proof end;

theorem Th46: :: IDEAL_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being non empty Subset of L st b1 -Ideal = I
proof end;
end;

:: deftheorem defines Basis IDEAL_1:def 18 :
for L being non empty doubleLoopStr
for I being Ideal of L
for b3 being non empty Subset of L holds
( b3 is Basis of I iff b3 -Ideal = I );

theorem Th47: :: IDEAL_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital doubleLoopStr holds {(1. L)} -Ideal = the carrier of L
proof end;

theorem :: IDEAL_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty right_unital doubleLoopStr holds {(1. L)} -LeftIdeal = the carrier of L
proof end;

theorem :: IDEAL_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty left_unital doubleLoopStr holds {(1. L)} -RightIdeal = the carrier of L
proof end;

theorem :: IDEAL_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty doubleLoopStr holds ([#] L) -Ideal = the carrier of L
proof end;

theorem :: IDEAL_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty doubleLoopStr holds ([#] L) -LeftIdeal = the carrier of L
proof end;

theorem :: IDEAL_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty doubleLoopStr holds ([#] L) -RightIdeal = the carrier of L
proof end;

theorem Th57: :: IDEAL_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty doubleLoopStr
for a being Element of R holds a in {a} -Ideal
proof end;

theorem :: IDEAL_1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
{ (a * i) where i is Element of R : i in I } is Subset of R
proof end;
end;

:: deftheorem defines * IDEAL_1:def 19 :
for R being non empty HGrStr
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;
cluster a * I -> non empty ;
coherence
not a * I is empty
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
a * I is add-closed
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
a * I is right-ideal
proof end;
end;

theorem Th70: :: IDEAL_1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
{ (a + b) where a, b is Element of R : ( a in I & b in J ) } is Subset of R
proof end;
end;

:: deftheorem defines + IDEAL_1:def 20 :
for R being non empty LoopStr
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 LoopStr ;
let I, J be non empty Subset of R;
cluster I + J -> non empty ;
coherence
not I + J is empty
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
for I, J being Subset of R holds I + J = J + I
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
I + J is add-closed
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
I + J is right-ideal
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
I + J is left-ideal
proof end;
end;

theorem :: IDEAL_1:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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} -Ideal ) + ({b} -Ideal )
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
I /\ J is Subset of R
proof end;
compatibility
for b1 being Subset of R holds
( b1 = I /\ J iff b1 = { x where x is Element of R : ( x in I & x in J ) } )
proof end;
end;

:: deftheorem defines /\ IDEAL_1:def 21 :
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 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
not I /\ J is empty
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
I /\ J is add-closed Subset of R
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
I /\ J is left-ideal Subset of R
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
I /\ J is right-ideal Subset of R
proof end;
end;

theorem :: IDEAL_1:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
{ (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 )
}
is Subset of R
proof end;
end;

:: deftheorem defines *' IDEAL_1:def 22 :
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 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
let R be non empty doubleLoopStr ;
let I, J be Subset of R;
cluster I *' J -> non empty ;
coherence
not I *' J is empty
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
for I, J being Subset of R holds I *' J = J *' I
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
I *' J is add-closed
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
I *' J is right-ideal
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
I *' J is left-ideal
proof end;
end;

theorem :: IDEAL_1:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
for R being non empty LoopStr
for I, J being Subset of R holds
( I,J are_co-prime iff I + J = the carrier of R );

theorem Th86: :: IDEAL_1:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
{ a where a is Element of R : a * J c= I } is Subset of R
proof end;
end;

:: deftheorem defines % IDEAL_1:def 24 :
for R being non empty HGrStr
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 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
not I % J is empty
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
I % J is add-closed
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
I % J is left-ideal
proof end;
cluster I % J -> non empty left-ideal right-ideal ;
coherence
I % J is right-ideal
;
end;

theorem :: IDEAL_1:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
{ a where a is Element of R : ex n being Nat st a |^ n in I } is Subset of R
proof end;
end;

:: deftheorem defines sqrt IDEAL_1:def 25 :
for R being non empty unital doubleLoopStr
for I being Subset of R holds sqrt I = { a where a is Element of R : ex n being Nat st a |^ n in I } ;

registration
let R be non empty unital doubleLoopStr ;
let I be non empty Subset of R;
cluster sqrt I -> non empty ;
coherence
not sqrt I is empty
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
sqrt I is add-closed
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
sqrt I is left-ideal
proof end;
cluster sqrt I -> non empty left-ideal right-ideal ;
coherence
sqrt I is right-ideal
;
end;

theorem :: IDEAL_1:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
for L being non empty doubleLoopStr
for I being Ideal of L holds
( I is finitely_generated iff ex F being non empty finite Subset of L st I = F -Ideal );

registration
let L be non empty doubleLoopStr ;
cluster finitely_generated Element of bool the carrier of L;
existence
ex b1 being Ideal of L st b1 is finitely_generated
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
F -Ideal is finitely_generated
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 :
for L being non empty doubleLoopStr holds
( L is Noetherian iff for I being Ideal of L holds I is finitely_generated );

registration
cluster non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive non degenerated Euclidian doubleLoopStr ;
existence
ex b1 being non empty doubleLoopStr st
( b1 is Euclidian & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is unital & b1 is distributive & b1 is commutative & b1 is associative & not b1 is degenerated )
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 :
for L being non empty doubleLoopStr
for I being Ideal of L holds
( I is principal iff ex e being Element of L st I = {e} -Ideal );

definition
let L be non empty doubleLoopStr ;
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 :
for L being non empty doubleLoopStr holds
( L is PID iff for I being Ideal of L holds I is principal );

theorem Th96: :: IDEAL_1:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty doubleLoopStr st L is PID holds
L is Noetherian
proof end;

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

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

theorem :: IDEAL_1:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
not f | A is empty
proof end;
end;

theorem :: IDEAL_1:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;