let R be non empty add-cancelable right_zeroed well-unital distributive associative 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 sqrt (I *' J) = sqrt (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 sqrt (I *' J) = sqrt (I /\ J)
let J be non empty add-closed left-ideal Subset of R; :: thesis: sqrt (I *' J) = sqrt (I /\ J)
A1: now :: thesis: for u being object st u in sqrt (I *' J) holds
u in sqrt (I /\ J)
let u be object ; :: thesis: ( u in sqrt (I *' J) implies u in sqrt (I /\ J) )
assume u in sqrt (I *' J) ; :: thesis: u in sqrt (I /\ J)
then consider d being Element of R such that
A2: u = d and
A3: ex m being Element of NAT st d |^ m in I *' J ;
consider m being Element of NAT such that
A4: d |^ m in I *' J by A3;
consider s being FinSequence of the carrier of R such that
A5: d |^ m = Sum s and
A6: 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 ) by A4;
consider f being sequence of the carrier of R such that
A7: Sum s = f . (len s) and
A8: f . 0 = 0. R and
A9: 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 f . $1 in I /\ J;
A10: now :: thesis: for j being Element of NAT st 0 <= j & j < len s & S1[j] holds
S1[j + 1]
let j be Element of NAT ; :: thesis: ( 0 <= j & j < len s & S1[j] implies S1[j + 1] )
assume that
0 <= j and
A11: j < len s ; :: thesis: ( S1[j] implies S1[j + 1] )
thus ( S1[j] implies S1[j + 1] ) :: thesis: verum
proof
assume f . j in I /\ J ; :: thesis: S1[j + 1]
then A12: ex g being Element of R st
( g = f . j & g in I & g in J ) ;
A13: ( j + 1 <= len s & 0 + 1 <= j + 1 ) by A11, NAT_1:13;
then A14: ex a, b being Element of R st
( s . (j + 1) = a * b & a in I & b in J ) by A6;
j + 1 in Seg (len s) by A13, FINSEQ_1:1;
then j + 1 in dom s by FINSEQ_1:def 3;
then A15: s . (j + 1) = s /. (j + 1) by PARTFUN1:def 6;
then A16: f . (j + 1) = (f . j) + (s /. (j + 1)) by A9, A11;
s /. (j + 1) in J by A15, A14, Def2;
then A17: f . (j + 1) in J by A12, A16, Def1;
s /. (j + 1) in I by A15, A14, Def3;
then f . (j + 1) in I by A12, A16, Def1;
hence S1[j + 1] by A17; :: thesis: verum
end;
end;
( f . 0 in I & f . 0 in J ) by A8, Th2, Th3;
then A18: S1[ 0 ] ;
for j being Element of NAT st 0 <= j & j <= len s holds
S1[j] from INT_1:sch 7(A18, A10);
then Sum s in I /\ J by A7;
hence u in sqrt (I /\ J) by A2, A5; :: thesis: verum
end;
now :: thesis: for u being object st u in sqrt (I /\ J) holds
u in sqrt (I *' J)
let u be object ; :: thesis: ( u in sqrt (I /\ J) implies u in sqrt (I *' J) )
assume u in sqrt (I /\ J) ; :: thesis: u in sqrt (I *' J)
then consider d being Element of R such that
A19: u = d and
A20: ex m being Element of NAT st d |^ m in I /\ J ;
consider m being Element of NAT such that
A21: d |^ m in I /\ J by A20;
set q = <*((d |^ m) * (d |^ m))*>;
A22: len <*((d |^ m) * (d |^ m))*> = 1 by FINSEQ_1:40;
A23: ex g being Element of R st
( d |^ m = g & g in I & g in J ) by A21;
A24: for i being Element of NAT st 1 <= i & i <= len <*((d |^ m) * (d |^ m))*> holds
ex x, y being Element of R st
( <*((d |^ m) * (d |^ m))*> . i = x * y & x in I & y in J )
proof
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len <*((d |^ m) * (d |^ m))*> implies ex x, y being Element of R st
( <*((d |^ m) * (d |^ m))*> . i = x * y & x in I & y in J ) )
assume A25: ( 1 <= i & i <= len <*((d |^ m) * (d |^ m))*> ) ; :: thesis: ex x, y being Element of R st
( <*((d |^ m) * (d |^ m))*> . i = x * y & x in I & y in J )
then i in Seg (len <*((d |^ m) * (d |^ m))*>) by FINSEQ_1:1;
then i in dom <*((d |^ m) * (d |^ m))*> by FINSEQ_1:def 3;
then A26: <*((d |^ m) * (d |^ m))*> . i = <*((d |^ m) * (d |^ m))*> /. i by PARTFUN1:def 6;
then <*((d |^ m) * (d |^ m))*> /. i = <*((d |^ m) * (d |^ m))*> . 1 by A22, A25, XXREAL_0:1
.= (d |^ m) * (d |^ m) by FINSEQ_1:40 ;
hence ex x, y being Element of R st
( <*((d |^ m) * (d |^ m))*> . i = x * y & x in I & y in J ) by A23, A26; :: thesis: verum
end;
d |^ (m + m) = (d |^ m) * (d |^ m) by BINOM:10
.= Sum <*((d |^ m) * (d |^ m))*> by BINOM:3 ;
then d |^ (m + m) in I *' J by A24;
hence u in sqrt (I *' J) by A19; :: thesis: verum
end;
hence sqrt (I *' J) = sqrt (I /\ J) by A1, TARSKI:2; :: thesis: verum