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 -LeftIdeal iff ex f being LeftLinearCombination of F st x = Sum f )
let F be non empty Subset of L; :: thesis: for x being set holds
( x in F -LeftIdeal iff ex f being LeftLinearCombination of F st x = Sum f )
set I = { x where x is Element of L : ex lc being LeftLinearCombination of F st Sum lc = x } ;
A1: { x where x is Element of L : ex lc being LeftLinearCombination 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 LeftLinearCombination 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 LeftLinearCombination 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 LeftLinearCombination of F st Sum lc = x9 ) ;
hence x in the carrier of L ; :: thesis: verum

end;

let x be set ; :: thesis: ( x in F -LeftIdeal iff ex f being LeftLinearCombination of F st x = Sum f )
A2: F c= { x where x is Element of L : ex lc being LeftLinearCombination 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 LeftLinearCombination of F st Sum lc = x } )
assume A3: x in F ; :: thesis: x in { x where x is Element of L : ex lc being LeftLinearCombination 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 being Element of L ex a being Element of F st <*x*> /. i = u * a

let i be set ; :: thesis: ( i in dom <*x*> implies ex u being Element of L ex a being Element of F st <*x*> /. i = u * a )
assume A4: i in dom <*x*> ; :: thesis: ex u being Element of L ex a being Element of F st <*x*> /. i = u * a
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 ;
hence ex u being Element of L ex a being Element of F st <*x*> /. i = u * a by A3, A4, PARTFUN1:def 6; :: thesis: verum

end;

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

end;

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

proof

defpred S₁[ Nat] means for lc being LeftLinearCombination of F st len lc <= $1 holds
Sum lc in F -LeftIdeal ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of L : ex lc being LeftLinearCombination of F st Sum lc = x } or x in F -LeftIdeal )
assume x in { x where x is Element of L : ex lc being LeftLinearCombination of F st Sum lc = x } ; :: thesis: x in F -LeftIdeal
then consider x9 being Element of L such that
A6: x9 = x and
A7: ex lc being LeftLinearCombination of F st Sum lc = x9 ;
consider lc being LeftLinearCombination 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 LeftLinearCombination of F; :: thesis: ( len lc <= k + 1 implies Sum lc in F -LeftIdeal )
assume A11: len lc <= k + 1 ; :: thesis: Sum lc in F -LeftIdeal

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

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

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

end;

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

then not lc is empty ;
then consider q being LeftLinearCombination of F, r being Element of L such that
A13: lc = q ^ <*r*> and
A14: <*r*> is LeftLinearCombination of F by Th33;
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 -LeftIdeal 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 being Element of L, a being Element of F such that
A17: <*r*> /. 1 = u * a by A14, Def9;
F c= F -LeftIdeal by Def15;
then A18: a in F -LeftIdeal ;
A19: <*r*> /. 1 = <*r*> . 1 by A16, PARTFUN1:def 6;
Sum <*r*> = r by BINOM:3
.= u * a by A17, A19 ;
then A20: Sum <*r*> in F -LeftIdeal by A18, Def2;
Sum lc = (Sum q) + (Sum <*r*>) by A13, RLVECT_1:41;
hence Sum lc in F -LeftIdeal by A15, A20, Def1; :: thesis: verum

end;

end;

end;

end;

A21: S₁[ 0 ]

proof

set y = the Element of F;
let lc be LeftLinearCombination of F; :: thesis: ( len lc <= 0 implies Sum lc in F -LeftIdeal )
assume len lc <= 0 ; :: thesis: Sum lc in F -LeftIdeal
then lc = <*> the carrier of L ;
then A22: Sum lc = 0. L by RLVECT_1:43;
F c= F -LeftIdeal by Def15;
then A23: the Element of F in F -LeftIdeal ;
(0. L) * the Element of F = 0. L by BINOM:1;
hence Sum lc in F -LeftIdeal 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 -LeftIdeal by A6, A8; :: thesis: verum

end;

reconsider I = { x where x is Element of L : ex lc being LeftLinearCombination 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 LeftLinearCombination of F st Sum lc = x9 by A25;
consider lcx being LeftLinearCombination 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 LeftLinearCombination of F st Sum lc = y9 by A26;
consider lcy being LeftLinearCombination 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;

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
A33: x9 = x and
A34: ex lc being LeftLinearCombination of F st Sum lc = x9 ;
consider lcx being LeftLinearCombination of F such that
A35: Sum lcx = x9 by A34;
reconsider plcx = p * lcx as LeftLinearCombination of F by Th26;
p * x = Sum plcx by A33, A35, BINOM:4;
hence p * x in I9 ; :: thesis: verum

end;

then F -LeftIdeal c= I by A2, A24, Def15;
then A36: I = F -LeftIdeal by A5;

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

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

end;

assume ex f being LeftLinearCombination of F st x = Sum f ; :: thesis: x in F -LeftIdeal
hence x in F -LeftIdeal by A36; :: thesis: verum