let R be non empty add-cancelable Abelian add-associative right_zeroed associative commutative well-unital distributive left_zeroed doubleLoopStr ; :: thesis: 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; :: thesis: {a,b} -Ideal = { ((a * r) + (b * s)) where r, s is Element of R : verum }
set A = {a,b};
reconsider a' = a, b' = 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 set 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
set ;
:: thesis: ( 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 }
;
:: thesis: 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
Function of
NAT ,the
carrier of
R such that A3:
Sum s = f . (len s)
and A4:
f . 0 = 0. R
and A5:
for
j being
Element of
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 13;
defpred S1[
Element of
NAT ]
means ex
r,
s being
Element of
R st
f . $1
= (a * r) + (b * s);
f . 0 =
a * (0. R)
by A4, BINOM:2
.=
(a * (0. R)) + (0. R)
by RLVECT_1:def 7
.=
(a * (0. R)) + (b * (0. R))
by BINOM:2
;
then A6:
S1[
0 ]
;
for
k being
Element of
NAT st
0 <= k &
k <= len s holds
S1[
k]
from POLYNOM2:sch 4(A6, A7);
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;
:: thesis: verum
end;
for u being set 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
set ;
:: thesis: ( 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 }
;
:: thesis: u in { (Sum s) where s is LinearCombination of {a,b} : verum }
then consider r,
t being
Element of
R such that A14:
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 ;
:: thesis: ( 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 A15:
i in dom <*(a * r),(b * t)*>
;
:: thesis: 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 A16:
i in {1,2}
by FINSEQ_1:4, FINSEQ_1:61;
end;
then reconsider s =
<*(a * r),(b * t)*> as
LinearCombination of
{a,b} by Def9;
Sum s = (a * r) + (b * t)
by Th1;
hence
u in { (Sum s) where s is LinearCombination of {a,b} : verum }
by A14;
:: thesis: verum
end;
then A17:
{ (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 A17, TARSKI:2; :: thesis: verum