let R be non empty add-cancelable add-associative right_zeroed well-unital distributive associative 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 )
let B be non empty Subset of R; ex C being non empty finite Subset of R st
( C c= B & C -Ideal = B -Ideal )
defpred S1[ object , object ] means ex cL being non empty LinearCombination of B st
( $1 = Sum cL & ex fsB being FinSequence of B st
( dom fsB = dom cL & $2 = rng fsB & ( for i being Nat st i in dom cL holds
ex u, v being Element of R st cL /. i = (u * (fsB /. i)) * v ) ) );
B -Ideal is finitely_generated
by Def26;
then consider D being non empty finite Subset of R such that
A1:
D -Ideal = B -Ideal
;
A2:
D c= B -Ideal
by A1, Def14;
A3:
for e being object st e in D holds
ex u being object st
( u in bool B & S1[e,u] )
consider f being Function of D,(bool B) such that
A15:
for e being object st e in D holds
S1[e,f . e]
from FUNCT_2:sch 1(A3);
reconsider rf = rng f as Subset-Family of B ;
reconsider C = union rf as Subset of B ;
consider r being object such that
A18:
r in rng f
by XBOOLE_0:def 1;
consider x being object such that
A19:
( x in dom f & r = f . x )
by A18, FUNCT_1:def 3;
reconsider r = r as set by TARSKI:1;
ex cL being non empty LinearCombination of B st
( x = Sum cL & ex fsB being FinSequence of B st
( dom fsB = dom cL & r = rng fsB & ( for i being Nat st i in dom cL holds
ex u, v being Element of R st cL /. i = (u * (fsB /. i)) * v ) ) )
by A15, A19;
then
not r is empty
by RELAT_1:42;
then
ex x being object st x in r
;
then reconsider C = C as non empty finite Subset of R by A18, A16, FINSET_1:7, TARSKI:def 4, XBOOLE_1:1;
now for d being object st d in D holds
d in C -Ideal let d be
object ;
( d in D implies d in C -Ideal )assume A20:
d in D
;
d in C -Ideal then consider cL being non
empty LinearCombination of
B such that A21:
d = Sum cL
and A22:
ex
fsB being
FinSequence of
B st
(
dom fsB = dom cL &
f . d = rng fsB & ( for
i being
Nat st
i in dom cL holds
ex
u,
v being
Element of
R st
cL /. i = (u * (fsB /. i)) * v ) )
by A15;
d in dom f
by A20, FUNCT_2:def 1;
then
f . d in rng f
by FUNCT_1:def 3;
then A23:
f . d c= C
by ZFMISC_1:74;
now for i being set st i in dom cL holds
ex u, v being Element of R ex a being Element of C st cL /. i = (u * a) * vlet i be
set ;
( i in dom cL implies ex u, v being Element of R ex a being Element of C st cL /. i = (u * a) * v )consider fsB being
FinSequence of
B such that A24:
dom fsB = dom cL
and A25:
f . d = rng fsB
and A26:
for
i being
Nat st
i in dom cL holds
ex
u,
v being
Element of
R st
cL /. i = (u * (fsB /. i)) * v
by A22;
assume A27:
i in dom cL
;
ex u, v being Element of R ex a being Element of C st cL /. i = (u * a) * vthen
fsB /. i = fsB . i
by A24, PARTFUN1:def 6;
then A28:
fsB /. i in f . d
by A27, A24, A25, FUNCT_1:def 3;
ex
u,
v being
Element of
R st
cL /. i = (u * (fsB /. i)) * v
by A27, A26;
hence
ex
u,
v being
Element of
R ex
a being
Element of
C st
cL /. i = (u * a) * v
by A23, A28;
verum end; then reconsider cL9 =
cL as
LinearCombination of
C by Def8;
d = Sum cL9
by A21;
hence
d in C -Ideal
by Th60;
verum end;
then
D c= C -Ideal
;
then
D -Ideal c= (C -Ideal) -Ideal
by Th57;
then A29:
B -Ideal c= C -Ideal
by A1, Th44;
take
C
; ( C c= B & C -Ideal = B -Ideal )
C -Ideal c= B -Ideal
by Th57;
hence
( C c= B & C -Ideal = B -Ideal )
by A29; verum