let R be non empty add-cancelable add-associative right_zeroed associative well-unital distributive left_zeroed Noetherian doubleLoopStr ; :: thesis: 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; :: thesis: ex C being non empty finite Subset of R st
( C c= B & C -Ideal = B -Ideal )
B -Ideal is finitely_generated by Def27;
then consider D being non empty finite Subset of R such that
A1: D -Ideal = B -Ideal by Def26;
A2: D c= B -Ideal by A1, Def15;
defpred S1[ set , set ] 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 Element of NAT st i in dom cL holds
ex u, v being Element of R st cL /. i = (u * (fsB /. i)) * v ) ) );
A3: for e being set st e in D holds
ex u being set st
( u in bool B & S1[e,u] )
proof
let e be set ; :: thesis: ( e in D implies ex u being set st
( u in bool B & S1[e,u] ) )
assume e in D ; :: thesis: ex u being set st
( u in bool B & S1[e,u] )
then consider cL being LinearCombination of B such that
A4: e = Sum cL by A2, Th60;
per cases ( not cL is empty or cL is empty ) ;
suppose A5: not cL is empty ; :: thesis: ex u being set st
( u in bool B & S1[e,u] )
defpred S2[ set , Element of B] means ex u, v being Element of R st cL /. $1 = (u * $2) * v;
A6: now
let k be Element of NAT ; :: thesis: ( k in Seg (len cL) implies ex d being Element of B st S2[k,d] )
assume k in Seg (len cL) ; :: thesis: ex d being Element of B st S2[k,d]
then k in dom cL by FINSEQ_1:def 3;
then consider u, v being Element of R, a being Element of B such that
A7: cL /. k = (u * a) * v by Def9;
take d = a; :: thesis: S2[k,d]
thus S2[k,d] by A7; :: thesis: verum
end;
consider fsB being FinSequence of B such that
A8: dom fsB = Seg (len cL) and
A9: for k being Element of NAT st k in Seg (len cL) holds
S2[k,fsB /. k] from POLYNOM2:sch 1(A6);
take u = rng fsB; :: thesis: ( u in bool B & S1[e,u] )
thus u in bool B ; :: thesis: S1[e,u]
dom cL = Seg (len cL) by FINSEQ_1:def 3;
hence S1[e,u] by A4, A5, A8, A9; :: thesis: verum
end;
suppose A10: cL is empty ; :: thesis: ex u being set st
( u in bool B & S1[e,u] )
consider b being Element of B;
set kL = <*(((0. R) * b) * (0. R))*>;
now
let i be set ; :: thesis: ( i in dom <*(((0. R) * b) * (0. R))*> implies ex u, v being Element of the carrier of R ex b being Element of B st <*(((0. R) * b) * (0. R))*> /. i = (u * b) * v )
assume i in dom <*(((0. R) * b) * (0. R))*> ; :: thesis: ex u, v being Element of the carrier of R ex b being Element of B st <*(((0. R) * b) * (0. R))*> /. i = (u * b) * v
then i in Seg (len <*(((0. R) * b) * (0. R))*>) by FINSEQ_1:def 3;
then i in {1} by FINSEQ_1:4, FINSEQ_1:57;
then A11: i = 1 by TARSKI:def 1;
take u = 0. R; :: thesis: ex v being Element of the carrier of R ex b being Element of B st <*(((0. R) * b) * (0. R))*> /. i = (u * b) * v
take v = 0. R; :: thesis: ex b being Element of B st <*(((0. R) * b) * (0. R))*> /. i = (u * b) * v
take b = b; :: thesis: <*(((0. R) * b) * (0. R))*> /. i = (u * b) * v
thus <*(((0. R) * b) * (0. R))*> /. i = (u * b) * v by A11, FINSEQ_4:25; :: thesis: verum
end;
then reconsider kL = <*(((0. R) * b) * (0. R))*> as non empty LinearCombination of B by Def9;
cL = <*> the carrier of R by A10;
then A12: e = 0. R by A4, RLVECT_1:60
.= ((0. R) * b) * (0. R) by BINOM:2
.= Sum kL by BINOM:3 ;
defpred S2[ Element of NAT , Element of B] means ex u, v being Element of R st kL /. $1 = (u * $2) * v;
A13: now
let k be Element of NAT ; :: thesis: ( k in Seg (len kL) implies ex b being Element of B st S2[k,b] )
assume k in Seg (len kL) ; :: thesis: ex b being Element of B st S2[k,b]
then k in {1} by FINSEQ_1:4, FINSEQ_1:57;
then A14: k = 1 by TARSKI:def 1;
take b = b; :: thesis: S2[k,b]
thus S2[k,b] by A14, FINSEQ_4:25; :: thesis: verum
end;
consider fsB being FinSequence of B such that
A15: dom fsB = Seg (len kL) and
A16: for k being Element of NAT st k in Seg (len kL) holds
S2[k,fsB /. k] from POLYNOM2:sch 1(A13);
take u = rng fsB; :: thesis: ( u in bool B & S1[e,u] )
thus u in bool B ; :: thesis: S1[e,u]
dom kL = Seg (len kL) by FINSEQ_1:def 3;
hence S1[e,u] by A12, A15, A16; :: thesis: verum
end;
end;
end;
consider f being Function of D,(bool B) such that
A17: for e being set 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 set such that
A18: r in rng f by XBOOLE_0:def 1;
consider x being set such that
A19: ( x in dom f & r = f . x ) by A18, FUNCT_1:def 5;
consider cL being non empty LinearCombination of B such that
x = Sum cL and
A20: ex fsB being FinSequence of B st
( dom fsB = dom cL & r = rng fsB & ( for i being Element of NAT st i in dom cL holds
ex u, v being Element of R st cL /. i = (u * (fsB /. i)) * v ) ) by A17, A19;
consider fsB being FinSequence of B such that
A21: dom fsB = dom cL and
A22: r = rng fsB and
for i being Element of NAT st i in dom cL holds
ex u, v being Element of R st cL /. i = (u * (fsB /. i)) * v by A20;
not r is empty by A21, A22, RELAT_1:65;
then consider x being set such that
A23: x in r by XBOOLE_0:def 1;
now
let r be set ; :: thesis: ( r in rng f implies r is finite )
assume r in rng f ; :: thesis: r is finite
then consider x being set such that
A24: ( x in dom f & r = f . x ) by FUNCT_1:def 5;
consider cL being non empty LinearCombination of B such that
x = Sum cL and
A25: ex fsB being FinSequence of B st
( dom fsB = dom cL & r = rng fsB & ( for i being Element of NAT st i in dom cL holds
ex u, v being Element of R st cL /. i = (u * (fsB /. i)) * v ) ) by A17, A24;
consider fsB being FinSequence of B such that
dom fsB = dom cL and
A26: r = rng fsB and
for i being Element of NAT st i in dom cL holds
ex u, v being Element of R st cL /. i = (u * (fsB /. i)) * v by A25;
thus r is finite by A26; :: thesis: verum
end;
then reconsider C = C as non empty finite Subset of R by A18, A23, FINSET_1:25, TARSKI:def 4, XBOOLE_1:1;
now
let d be set ; :: thesis: ( d in D implies d in C -Ideal )
assume A27: d in D ; :: thesis: d in C -Ideal
then d in dom f by FUNCT_2:def 1;
then f . d in rng f by FUNCT_1:def 5;
then A28: f . d c= C by ZFMISC_1:92;
consider cL being non empty LinearCombination of B such that
A29: d = Sum cL and
A30: ex fsB being FinSequence of B st
( dom fsB = dom cL & f . d = rng fsB & ( for i being Element of NAT st i in dom cL holds
ex u, v being Element of R st cL /. i = (u * (fsB /. i)) * v ) ) by A17, A27;
now
let i be set ; :: thesis: ( i in dom cL implies ex u, v being Element of R ex a being Element of C st cL /. i = (u * a) * v )
assume A31: i in dom cL ; :: thesis: 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
A32: dom fsB = dom cL and
A33: f . d = rng fsB and
A34: for i being Element of NAT st i in dom cL holds
ex u, v being Element of R st cL /. i = (u * (fsB /. i)) * v by A30;
consider u, v being Element of R such that
A35: cL /. i = (u * (fsB /. i)) * v by A31, A34;
fsB /. i = fsB . i by A31, A32, PARTFUN1:def 8;
then fsB /. i in f . d by A31, A32, A33, FUNCT_1:def 5;
hence ex u, v being Element of R ex a being Element of C st cL /. i = (u * a) * v by A28, A35; :: thesis: verum
end;
then reconsider cL' = cL as LinearCombination of C by Def9;
d = Sum cL' by A29;
hence d in C -Ideal by Th60; :: thesis: verum
end;
then D c= C -Ideal by TARSKI:def 3;
then D -Ideal c= (C -Ideal ) -Ideal by Th57;
then A36: B -Ideal c= C -Ideal by A1, Th44;
take C ; :: thesis: ( C c= B & C -Ideal = B -Ideal )
C -Ideal c= B -Ideal by Th57;
hence ( C c= B & C -Ideal = B -Ideal ) by A36, XBOOLE_0:def 10; :: thesis: verum