let L be non empty add-cancelable add-associative right_zeroed well-unital distributive associative left_zeroed doubleLoopStr ; for F being non empty Subset of L
for x being set holds
( x in F -RightIdeal iff ex f being RightLinearCombination of F st x = Sum f )
let F be non empty Subset of L; for x being set holds
( x in F -RightIdeal iff ex f being RightLinearCombination of F st x = Sum f )
set I = { x where x is Element of L : ex lc being RightLinearCombination of F st Sum lc = x } ;
A1:
{ x where x is Element of L : ex lc being RightLinearCombination of F st Sum lc = x } c= the carrier of L
let x be set ; ( x in F -RightIdeal iff ex f being RightLinearCombination of F st x = Sum f )
A2:
F c= { x where x is Element of L : ex lc being RightLinearCombination of F st Sum lc = x }
A5:
{ x where x is Element of L : ex lc being RightLinearCombination of F st Sum lc = x } c= F -RightIdeal
proof
defpred S1[
Nat]
means for
lc being
RightLinearCombination of
F st
len lc <= $1 holds
Sum lc in F -RightIdeal ;
let x be
object ;
TARSKI:def 3 ( not x in { x where x is Element of L : ex lc being RightLinearCombination of F st Sum lc = x } or x in F -RightIdeal )
assume
x in { x where x is Element of L : ex lc being RightLinearCombination of F st Sum lc = x }
;
x in F -RightIdeal
then consider x9 being
Element of
L such that A6:
x9 = x
and A7:
ex
lc being
RightLinearCombination of
F st
Sum lc = x9
;
consider lc being
RightLinearCombination of
F such that A8:
Sum lc = x9
by A7;
A9:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A10:
S1[
k]
;
S1[k + 1]
thus
S1[
k + 1]
verumproof
let lc be
RightLinearCombination of
F;
( len lc <= k + 1 implies Sum lc in F -RightIdeal )
assume A11:
len lc <= k + 1
;
Sum lc in F -RightIdeal
per cases
( len lc <= k or len lc = k + 1 )
by A11, NAT_1:8;
suppose A12:
len lc = k + 1
;
Sum lc in F -RightIdeal then
not
lc is
empty
;
then consider q being
RightLinearCombination of
F,
r being
Element of
L such that A13:
lc = q ^ <*r*>
and A14:
<*r*> is
RightLinearCombination of
F
by Th34;
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 -RightIdeal
by A10;
dom <*r*> = {1}
by FINSEQ_1:2, FINSEQ_1:38;
then A16:
1
in dom <*r*>
by TARSKI:def 1;
then consider v being
Element of
L,
a being
Element of
F such that A17:
<*r*> /. 1
= a * v
by A14, Def10;
F c= F -RightIdeal
by Def16;
then A18:
a in F -RightIdeal
;
A19:
<*r*> /. 1
= <*r*> . 1
by A16, PARTFUN1:def 6;
Sum <*r*> =
r
by BINOM:3
.=
a * v
by A17, A19, FINSEQ_1:40
;
then A20:
Sum <*r*> in F -RightIdeal
by A18, Def3;
Sum lc = (Sum q) + (Sum <*r*>)
by A13, RLVECT_1:41;
hence
Sum lc in F -RightIdeal
by A15, A20, Def1;
verum end; end;
end;
end;
A21:
S1[
0 ]
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A21, A9);
then
S1[
len lc]
;
hence
x in F -RightIdeal
by A6, A8;
verum
end;
reconsider I = { x where x is Element of L : ex lc being RightLinearCombination 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
I9 is right-ideal
then
F -RightIdeal c= I
by A2, A24, Def16;
then A36:
I = F -RightIdeal
by A5;
assume
ex f being RightLinearCombination of F st x = Sum f
; x in F -RightIdeal
hence
x in F -RightIdeal
by A36; verum