let L be non empty add-cancelable add-associative right_zeroed well-unital distributive associative left_zeroed doubleLoopStr ; :: thesis: 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 )
let F be non empty Subset of L; :: thesis: for x being set holds
( x in F -Ideal iff ex f being LinearCombination of F st x = Sum f )
set I = { x where x is Element of L : ex lc being LinearCombination of F st Sum lc = x } ;
A1: { x where x is Element of L : ex lc being LinearCombination of F st Sum lc = x } c= the carrier of L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of L : ex lc being LinearCombination of F st Sum lc = x } or x in the carrier of L )
assume x in { x where x is Element of L : ex lc being LinearCombination of F st Sum lc = x } ; :: thesis: x in the carrier of L
then ex x9 being Element of L st
( x9 = x & ex lc being LinearCombination of F st Sum lc = x9 ) ;
hence x in the carrier of L ; :: thesis: verum

end;

let x be set ; :: thesis: ( x in F -Ideal iff ex f being LinearCombination of F st x = Sum f )
A2: F c= { x where x is Element of L : ex lc being LinearCombination of F st Sum lc = x }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in { x where x is Element of L : ex lc being LinearCombination of F st Sum lc = x } )
assume A3: x in F ; :: thesis: x in { x where x is Element of L : ex lc being LinearCombination of F st Sum lc = x }
then reconsider x = x as Element of L ;
set lc = <*x*>;

now :: thesis: for i being set st i in dom <*x*> holds
ex u, v being Element of L ex a being Element of F st <*x*> /. i = (u * a) * v

let i be set ; :: thesis: ( i in dom <*x*> implies ex u, v being Element of L ex a being Element of F st <*x*> /. i = (u * a) * v )
assume A4: i in dom <*x*> ; :: thesis: ex u, v being Element of L ex a being Element of F st <*x*> /. i = (u * a) * v
dom <*x*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then i = 1 by A4, TARSKI:def 1;
then <*x*> . i = x
.= (1. L) * x
.= ((1. L) * x) * (1. L) ;
hence ex u, v being Element of L ex a being Element of F st <*x*> /. i = (u * a) * v by A3, A4, PARTFUN1:def 6; :: thesis: verum

end;

then reconsider lc = <*x*> as LinearCombination of F by Def8;
Sum lc = x by BINOM:3;
hence x in { x where x is Element of L : ex lc being LinearCombination of F st Sum lc = x } ; :: thesis: verum

end;

A5: { x where x is Element of L : ex lc being LinearCombination of F st Sum lc = x } c= F -Ideal

proof

defpred S₁[ Nat] means for lc being LinearCombination of F st len lc <= $1 holds
Sum lc in F -Ideal ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of L : ex lc being LinearCombination of F st Sum lc = x } or x in F -Ideal )
assume x in { x where x is Element of L : ex lc being LinearCombination of F st Sum lc = x } ; :: thesis: x in F -Ideal
then consider x9 being Element of L such that
A6: x9 = x and
A7: ex lc being LinearCombination of F st Sum lc = x9 ;
consider lc being LinearCombination of F such that
A8: Sum lc = x9 by A7;
A9: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A10: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

let lc be LinearCombination of F; :: thesis: ( len lc <= k + 1 implies Sum lc in F -Ideal )
assume A11: len lc <= k + 1 ; :: thesis: Sum lc in F -Ideal

per cases ( len lc <= k or len lc = k + 1 ) by A11, NAT_1:8;

suppose len lc <= k ; :: thesis: Sum lc in F -Ideal

hence Sum lc in F -Ideal by A10; :: thesis: verum

end;

suppose A12: len lc = k + 1 ; :: thesis: Sum lc in F -Ideal

then not lc is empty ;
then consider q being LinearCombination of F, r being Element of L such that
A13: lc = q ^ <*r*> and
A14: <*r*> is LinearCombination of F by Th32;
k + 1 = (len q) + (len <*r*>) by A12, A13, FINSEQ_1:22
.= (len q) + 1 by FINSEQ_1:39 ;
then A15: Sum q in F -Ideal by A10;
dom <*r*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then A16: 1 in dom <*r*> by TARSKI:def 1;
then consider u, v being Element of L, a being Element of F such that
A17: <*r*> /. 1 = (u * a) * v by A14, Def8;
F c= F -Ideal by Def14;
then a in F -Ideal ;
then A18: u * a in F -Ideal by Def2;
A19: <*r*> /. 1 = <*r*> . 1 by A16, PARTFUN1:def 6;
Sum <*r*> = r by BINOM:3
.= (u * a) * v by A17, A19 ;
then A20: Sum <*r*> in F -Ideal by A18, Def3;
Sum lc = (Sum q) + (Sum <*r*>) by A13, RLVECT_1:41;
hence Sum lc in F -Ideal by A15, A20, Def1; :: thesis: verum

end;

end;

end;

end;

A21: S₁[ 0 ]

proof

set y = the Element of F;
let lc be LinearCombination of F; :: thesis: ( len lc <= 0 implies Sum lc in F -Ideal )
assume len lc <= 0 ; :: thesis: Sum lc in F -Ideal
then lc = <*> the carrier of L ;
then A22: Sum lc = 0. L by RLVECT_1:43;
F c= F -Ideal by Def14;
then A23: the Element of F in F -Ideal ;
(0. L) * the Element of F = 0. L by BINOM:1;
hence Sum lc in F -Ideal by A22, A23, Def2; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A21, A9);
then S₁[ len lc] ;
hence x in F -Ideal by A6, A8; :: thesis: verum

end;

reconsider I = { x where x is Element of L : ex lc being LinearCombination of F st Sum lc = x } as non empty Subset of L by A2, A1;
reconsider I9 = I as non empty Subset of L ;
A24: I9 is add-closed

proof

let x, y be Element of L; :: according to IDEAL_1:def 1 :: thesis: ( x in I9 & y in I9 implies x + y in I9 )
assume that
A25: x in I9 and
A26: y in I9 ; :: thesis: x + y in I9
consider x9 being Element of L such that
A27: x9 = x and
A28: ex lc being LinearCombination of F st Sum lc = x9 by A25;
consider lcx being LinearCombination of F such that
A29: Sum lcx = x9 by A28;
consider y9 being Element of L such that
A30: y9 = y and
A31: ex lc being LinearCombination of F st Sum lc = y9 by A26;
consider lcy being LinearCombination of F such that
A32: Sum lcy = y9 by A31;
Sum (lcx ^ lcy) = x9 + y9 by A29, A32, RLVECT_1:41;
hence x + y in I9 by A27, A30; :: thesis: verum

end;

A33: I9 is right-ideal

proof

let p, x be Element of L; :: according to IDEAL_1:def 3 :: thesis: ( x in I9 implies x * p in I9 )
assume x in I9 ; :: thesis: x * p in I9
then consider x9 being Element of L such that
A34: x9 = x and
A35: ex lc being LinearCombination of F st Sum lc = x9 ;
consider lcx being LinearCombination of F such that
A36: Sum lcx = x9 by A35;
reconsider lcxp = lcx * p as LinearCombination of F by Th24;
x * p = Sum lcxp by A34, A36, BINOM:5;
hence x * p in I9 ; :: thesis: verum

end;

I9 is left-ideal

proof

let p, x be Element of L; :: according to IDEAL_1:def 2 :: thesis: ( x in I9 implies p * x in I9 )
assume x in I9 ; :: thesis: p * x in I9
then consider x9 being Element of L such that
A37: x9 = x and
A38: ex lc being LinearCombination of F st Sum lc = x9 ;
consider lcx being LinearCombination of F such that
A39: Sum lcx = x9 by A38;
reconsider plcx = p * lcx as LinearCombination of F by Th23;
p * x = Sum plcx by A37, A39, BINOM:4;
hence p * x in I9 ; :: thesis: verum

end;

then F -Ideal c= I by A2, A24, A33, Def14;
then A40: I = F -Ideal by A5;

hereby :: thesis: ( ex f being LinearCombination of F st x = Sum f implies x in F -Ideal )

assume x in F -Ideal ; :: thesis: ex f being LinearCombination of F st x = Sum f
then ex x9 being Element of L st
( x9 = x & ex lc being LinearCombination of F st Sum lc = x9 ) by A40;
hence ex f being LinearCombination of F st x = Sum f ; :: thesis: verum

end;

assume ex f being LinearCombination of F st x = Sum f ; :: thesis: x in F -Ideal
hence x in F -Ideal by A40; :: thesis: verum