let R be non empty add-cancelable Abelian add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr ; for a, b being Element of R holds {a,b} -Ideal = { ((a * r) + (b * s)) where r, s is Element of R : verum }
let a, b be Element of R; {a,b} -Ideal = { ((a * r) + (b * s)) where r, s is Element of R : verum }
set A = {a,b};
reconsider a9 = a, b9 = b as Element of {a,b} by TARSKI:def 2;
set M = { (Sum s) where s is LinearCombination of {a,b} : verum } ;
set N = { ((a * r) + (b * s)) where r, s is Element of R : verum } ;
A1:
for u being object st u in { (Sum s) where s is LinearCombination of {a,b} : verum } holds
u in { ((a * r) + (b * s)) where r, s is Element of R : verum }
proof
let u be
object ;
( u in { (Sum s) where s is LinearCombination of {a,b} : verum } implies u in { ((a * r) + (b * s)) where r, s is Element of R : verum } )
assume
u in { (Sum s) where s is LinearCombination of {a,b} : verum }
;
u in { ((a * r) + (b * s)) where r, s is Element of R : verum }
then consider s being
LinearCombination of
{a,b} such that A2:
u = Sum s
;
consider f being
sequence of the
carrier of
R such that A3:
Sum s = f . (len s)
and A4:
f . 0 = 0. R
and A5:
for
j being
Nat for
v being
Element of
R st
j < len s &
v = s . (j + 1) holds
f . (j + 1) = (f . j) + v
by RLVECT_1:def 12;
defpred S1[
Element of
NAT ]
means ex
r,
s being
Element of
R st
f . $1
= (a * r) + (b * s);
A6:
now for j being Element of NAT st 0 <= j & j < len s & S1[j] holds
S1[j + 1]let j be
Element of
NAT ;
( 0 <= j & j < len s & S1[j] implies S1[j + 1] )assume that
0 <= j
and A7:
j < len s
;
( S1[j] implies S1[j + 1] )thus
(
S1[
j] implies
S1[
j + 1] )
verum end;
f . 0 =
a * (0. R)
by A4, BINOM:2
.=
(a * (0. R)) + (0. R)
by RLVECT_1:def 4
.=
(a * (0. R)) + (b * (0. R))
by BINOM:2
;
then A12:
S1[
0 ]
;
for
k being
Element of
NAT st
0 <= k &
k <= len s holds
S1[
k]
from INT_1:sch 7(A12, A6);
then
ex
r,
t being
Element of
R st
Sum s = (a * r) + (b * t)
by A3;
hence
u in { ((a * r) + (b * s)) where r, s is Element of R : verum }
by A2;
verum
end;
for u being object st u in { ((a * r) + (b * s)) where r, s is Element of R : verum } holds
u in { (Sum s) where s is LinearCombination of {a,b} : verum }
proof
let u be
object ;
( u in { ((a * r) + (b * s)) where r, s is Element of R : verum } implies u in { (Sum s) where s is LinearCombination of {a,b} : verum } )
assume
u in { ((a * r) + (b * s)) where r, s is Element of R : verum }
;
u in { (Sum s) where s is LinearCombination of {a,b} : verum }
then consider r,
t being
Element of
R such that A15:
u = (a * r) + (b * t)
;
set s =
<*(a * r),(b * t)*>;
for
i being
set st
i in dom <*(a * r),(b * t)*> holds
ex
r,
t being
Element of
R ex
a being
Element of
{a,b} st
<*(a * r),(b * t)*> /. i = (r * a) * t
proof
let i be
set ;
( i in dom <*(a * r),(b * t)*> implies ex r, t being Element of R ex a being Element of {a,b} st <*(a * r),(b * t)*> /. i = (r * a) * t )
assume A16:
i in dom <*(a * r),(b * t)*>
;
ex r, t being Element of R ex a being Element of {a,b} st <*(a * r),(b * t)*> /. i = (r * a) * t
then
i in Seg (len <*(a * r),(b * t)*>)
by FINSEQ_1:def 3;
then A17:
i in {1,2}
by FINSEQ_1:2, FINSEQ_1:44;
end;
then reconsider s =
<*(a * r),(b * t)*> as
LinearCombination of
{a,b} by Def8;
Sum s = (a * r) + (b * t)
by Th1;
hence
u in { (Sum s) where s is LinearCombination of {a,b} : verum }
by A15;
verum
end;
then
{ (Sum s) where s is LinearCombination of {a,b} : verum } = { ((a * r) + (b * s)) where r, s is Element of R : verum }
by A1, TARSKI:2;
hence
{a,b} -Ideal = { ((a * r) + (b * s)) where r, s is Element of R : verum }
by A13, TARSKI:2; verum