let L be non empty add-cancelable add-associative right_zeroed associative well-unital distributive 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
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 }
A5:
{ x where x is Element of L : ex lc being LeftLinearCombination of F st Sum lc = x } c= F -LeftIdeal
proof
defpred S1[
Nat]
means for
lc being
LeftLinearCombination of
F st
len lc <= $1 holds
Sum lc in F -LeftIdeal ;
let x be
set ;
:: 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 x' being
Element of
L such that A6:
x' = x
and A7:
ex
lc being
LeftLinearCombination of
F st
Sum lc = x'
;
consider lc being
LeftLinearCombination of
F such that A8:
Sum lc = x'
by A7;
A9:
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A10:
S1[
k]
;
:: thesis: S1[k + 1]
thus
S1[
k + 1]
:: thesis: verumproof
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 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:35
.=
(len q) + 1
by FINSEQ_1:56
;
then A15:
Sum q in F -LeftIdeal
by A10;
dom <*r*> = {1}
by FINSEQ_1:4, FINSEQ_1:55;
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, Def10;
F c= F -LeftIdeal
by Def16;
then A18:
a in F -LeftIdeal
by TARSKI:def 3;
A19:
<*r*> /. 1
= <*r*> . 1
by A16, PARTFUN1:def 8;
Sum <*r*> =
r
by BINOM:3
.=
u * a
by A17, A19, FINSEQ_1:57
;
then A20:
Sum <*r*> in F -LeftIdeal
by A18, Def2;
Sum lc = (Sum q) + (Sum <*r*>)
by A13, RLVECT_1:58;
hence
Sum lc in F -LeftIdeal
by A15, A20, Def1;
:: thesis: verum end;
end;
end;
A21:
S1[
0 ]
for
k being
Element of
NAT holds
S1[
k]
from NAT_1:sch 1(A21, A9);
then
S1[
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 I' = I as non empty Subset of L ;
A24:
I' is add-closed
I' is left-ideal
then
F -LeftIdeal c= I
by A2, A24, Def16;
then A36:
I = F -LeftIdeal
by A5, XBOOLE_0:def 10;
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