let R be non empty add-cancelable right_zeroed distributive left_zeroed doubleLoopStr ; :: thesis: for I being non empty add-closed right-ideal Subset of R
for J being non empty add-closed left-ideal Subset of R holds I *' J c= I /\ J
let I be non empty add-closed right-ideal Subset of R; :: thesis: for J being non empty add-closed left-ideal Subset of R holds I *' J c= I /\ J
let J be non empty add-closed left-ideal Subset of R; :: thesis: I *' J c= I /\ J
now let u be
set ;
:: thesis: ( u in I *' J implies u in I /\ J )assume
u in I *' J
;
:: thesis: u in I /\ Jthen consider s being
FinSequence of the
carrier of
R such that A1:
(
Sum s = u & ( for
i being
Element of
NAT st 1
<= i &
i <= len s holds
ex
a,
b being
Element of
R st
(
s . i = a * b &
a in I &
b in J ) ) )
;
consider f being
Function of
NAT ,the
carrier of
R such that A2:
(
Sum s = f . (len s) &
f . 0 = 0. R & ( 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 (
f . $1
in I &
f . $1
in J );
A3:
S1[
0 ]
by A2, Th2, Th3;
A4:
now let j be
Element of
NAT ;
:: thesis: ( 0 <= j & j < len s & S1[j] implies S1[j + 1] )assume A5:
(
0 <= j &
j < len s )
;
:: thesis: ( S1[j] implies S1[j + 1] )thus
(
S1[
j] implies
S1[
j + 1] )
:: thesis: verumproof
assume A6:
(
f . j in I &
f . j in J )
;
:: thesis: S1[j + 1]
A7:
j + 1
<= len s
by A5, NAT_1:13;
A8:
0 + 1
<= j + 1
by XREAL_1:8;
then
j + 1
in Seg (len s)
by A7, FINSEQ_1:3;
then
j + 1
in dom s
by FINSEQ_1:def 3;
then A9:
s . (j + 1) = s /. (j + 1)
by PARTFUN1:def 8;
then A10:
f . (j + 1) = (f . j) + (s /. (j + 1))
by A2, A5;
consider a,
b being
Element of
R such that A11:
(
s . (j + 1) = a * b &
a in I &
b in J )
by A1, A7, A8;
(
s /. (j + 1) in I &
s /. (j + 1) in J )
by A9, A11, Def2, Def3;
hence
S1[
j + 1]
by A6, A10, Def1;
:: thesis: verum
end; end;
for
j being
Element of
NAT st
0 <= j &
j <= len s holds
S1[
j]
from POLYNOM2:sch 4(A3, A4);
then
(
Sum s in I &
Sum s in J )
by A2;
hence
u in I /\ J
by A1;
:: thesis: verum end;
hence
I *' J c= I /\ J
by TARSKI:def 3; :: thesis: verum