begin
theorem Th1:
begin
:: deftheorem Def1 defines add-closed IDEAL_1:def 1 :
for L being non empty addLoopStr
for F being Subset of L holds
( F is add-closed iff for x, y being Element of L st x in F & y in F holds
x + y in F );
:: deftheorem Def2 defines left-ideal IDEAL_1:def 2 :
for L being non empty multMagma
for F being Subset of L holds
( F is left-ideal iff for p, x being Element of L st x in F holds
p * x in F );
:: deftheorem Def3 defines right-ideal IDEAL_1:def 3 :
for L being non empty multMagma
for F being Subset of L holds
( F is right-ideal iff for p, x being Element of L st x in F holds
x * p in F );
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem
theorem
theorem Th10:
theorem Th11:
theorem Th12:
:: deftheorem defines trivial IDEAL_1:def 4 :
for R being non empty add-cancelable right_zeroed distributive left_zeroed doubleLoopStr
for I being Ideal of R holds
( I is trivial iff I = {(0. R)} );
theorem Th13:
theorem Th14:
theorem
theorem
theorem Th17:
theorem
:: deftheorem IDEAL_1:def 5 :
canceled;
:: deftheorem defines add| IDEAL_1:def 6 :
for R being non empty addLoopStr
for I being non empty add-closed Subset of R holds add| (I,R) = the addF of R || I;
:: deftheorem defines mult| IDEAL_1:def 7 :
for R being non empty multMagma
for I being non empty right-ideal Subset of R holds mult| (I,R) = the multF of R || I;
:: deftheorem defines Gr IDEAL_1:def 8 :
for R being non empty addLoopStr
for I being non empty add-closed Subset of R holds Gr (I,R) = addLoopStr(# I,(add| (I,R)),(In ((0. R),I)) #);
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
theorem Th19:
theorem
theorem
theorem
begin
:: 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 );
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem Th29:
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
:: 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
theorem
:: 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
theorem
:: 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
theorem
theorem
theorem
theorem
begin
:: 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:
theorem Th45:
theorem Th46:
:: 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
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th57:
theorem
theorem
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem
Lm2:
for a, b being set holds {a} c= {a,b}
theorem
theorem
begin
:: deftheorem defines * IDEAL_1:def 19 :
for R being non empty multMagma
for I being Subset of R
for a being Element of R holds a * I = { (a * i) where i is Element of R : i in I } ;
theorem Th70:
theorem
:: deftheorem defines + IDEAL_1:def 20 :
for R being non empty addLoopStr
for I, J being Subset of R holds I + J = { (a + b) where a, b is Element of R : ( a in I & b in J ) } ;
theorem
theorem Th73:
theorem Th74:
theorem
theorem
:: 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 ) } ;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
:: 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 Element of NAT st 1 <= i & i <= len s holds
ex a, b being Element of R st
( s . i = a * b & a in I & b in J ) } ;
theorem
theorem Th82:
theorem Th83:
theorem Th84:
theorem
:: deftheorem Def23 defines are_co-prime IDEAL_1:def 23 :
for R being non empty addLoopStr
for I, J being Subset of R holds
( I,J are_co-prime iff I + J = the carrier of R );
theorem Th86:
theorem
:: deftheorem defines % IDEAL_1:def 24 :
for R being non empty multMagma
for I, J being Subset of R holds I % J = { a where a is Element of R : a * J c= I } ;
theorem
theorem
theorem Th90:
theorem
theorem
theorem
:: deftheorem defines sqrt IDEAL_1:def 25 :
for R being non empty well-unital doubleLoopStr
for I being Subset of R holds sqrt I = { a where a is Element of R : ex n being Element of NAT st a |^ n in I } ;
theorem
theorem
begin
:: 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 );
:: 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 );
:: 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 );
:: 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:
theorem Th97:
theorem Th98:
theorem
theorem
theorem
theorem