let R be non empty add-cancelable Abelian add-associative right_zeroed distributive associative left_zeroed doubleLoopStr ; :: thesis: for I, J, K being non empty right-ideal Subset of R holds I *' (J + K) = (I *' J) + (I *' K)
let I, J, K be non empty right-ideal Subset of R; :: thesis: I *' (J + K) = (I *' J) + (I *' K)
A1: now :: thesis: for u being object st u in I *' (J + K) holds
u in (I *' J) + (I *' K)
let u be object ; :: thesis: ( u in I *' (J + K) implies u in (I *' J) + (I *' K) )
assume u in I *' (J + K) ; :: thesis: u in (I *' J) + (I *' K)
then consider s being FinSequence of the carrier of R such that
A2: Sum s = u and
A3: 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 + K ) ;
consider f being sequence of the carrier of R such that
A4: Sum s = f . (len s) and
A5: f . 0 = 0. R and
A6: 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 x, y being Element of R st
( f . $1 = x + y & x in I *' J & y in I *' K );
A7: now :: thesis: for n being Element of NAT st 0 <= n & n < len s & S1[n] holds
S1[n + 1]
let n be Element of NAT ; :: thesis: ( 0 <= n & n < len s & S1[n] implies S1[n + 1] )
assume that
0 <= n and
A8: n < len s ; :: thesis: ( S1[n] implies S1[n + 1] )
thus ( S1[n] implies S1[n + 1] ) :: thesis: verum
proof
assume ex x, y being Element of R st
( f . n = x + y & x in I *' J & y in I *' K ) ; :: thesis: S1[n + 1]
then consider x, y being Element of R such that
A9: f . n = x + y and
A10: x in I *' J and
A11: y in I *' K ;
consider p being FinSequence of the carrier of R such that
A12: Sum p = y and
A13: for i being Element of NAT st 1 <= i & i <= len p holds
ex a, b being Element of R st
( p . i = a * b & a in I & b in K ) by A11;
consider q being FinSequence of the carrier of R such that
A14: Sum q = x and
A15: for i being Element of NAT st 1 <= i & i <= len q holds
ex a, b being Element of R st
( q . i = a * b & a in I & b in J ) by A10;
A16: ( 0 + 1 <= n + 1 & n + 1 <= len s ) by A8, NAT_1:13;
then consider a, b being Element of R such that
A17: s . (n + 1) = a * b and
A18: a in I and
A19: b in J + K by A3;
consider c, d being Element of R such that
A20: b = c + d and
A21: c in J and
A22: d in K by A19;
set q1 = q ^ <*(a * c)*>;
set p1 = p ^ <*(a * d)*>;
n + 1 in Seg (len s) by A16, FINSEQ_1:1;
then A23: n + 1 in dom s by FINSEQ_1:def 3;
then A24: s . (n + 1) = s /. (n + 1) by PARTFUN1:def 6;
A25: len (p ^ <*(a * d)*>) = (len p) + (len <*(a * d)*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:40 ;
for i being Element of NAT st 1 <= i & i <= len (p ^ <*(a * d)*>) holds
ex a, b being Element of R st
( (p ^ <*(a * d)*>) . i = a * b & a in I & b in K )
proof
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len (p ^ <*(a * d)*>) implies ex a, b being Element of R st
( (p ^ <*(a * d)*>) . i = a * b & a in I & b in K ) )
assume that
A26: 1 <= i and
A27: i <= len (p ^ <*(a * d)*>) ; :: thesis: ex a, b being Element of R st
( (p ^ <*(a * d)*>) . i = a * b & a in I & b in K )
per cases ( i = len (p ^ <*(a * d)*>) or i <> len (p ^ <*(a * d)*>) ) ;
suppose i = len (p ^ <*(a * d)*>) ; :: thesis: ex a, b being Element of R st
( (p ^ <*(a * d)*>) . i = a * b & a in I & b in K )
hence ex a, b being Element of R st
( (p ^ <*(a * d)*>) . i = a * b & a in I & b in K ) by A18, A22, A25, FINSEQ_1:42; :: thesis: verum
end;
suppose i <> len (p ^ <*(a * d)*>) ; :: thesis: ex a, b being Element of R st
( (p ^ <*(a * d)*>) . i = a * b & a in I & b in K )
then i < len (p ^ <*(a * d)*>) by A27, XXREAL_0:1;
then A28: i <= len p by A25, NAT_1:13;
then consider a, b being Element of R such that
A29: p . i = a * b and
A30: ( a in I & b in K ) by A13, A26;
i in Seg (len p) by A26, A28, FINSEQ_1:1;
then i in dom p by FINSEQ_1:def 3;
then (p ^ <*(a * d)*>) . i = a * b by A29, FINSEQ_1:def 7;
hence ex a, b being Element of R st
( (p ^ <*(a * d)*>) . i = a * b & a in I & b in K ) by A30; :: thesis: verum
end;
end;
end;
then A31: Sum (p ^ <*(a * d)*>) in I *' K ;
A32: len (q ^ <*(a * c)*>) = (len q) + (len <*(a * c)*>) by FINSEQ_1:22
.= (len q) + 1 by FINSEQ_1:40 ;
for i being Element of NAT st 1 <= i & i <= len (q ^ <*(a * c)*>) holds
ex a, b being Element of R st
( (q ^ <*(a * c)*>) . i = a * b & a in I & b in J )
proof
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len (q ^ <*(a * c)*>) implies ex a, b being Element of R st
( (q ^ <*(a * c)*>) . i = a * b & a in I & b in J ) )
assume that
A33: 1 <= i and
A34: i <= len (q ^ <*(a * c)*>) ; :: thesis: ex a, b being Element of R st
( (q ^ <*(a * c)*>) . i = a * b & a in I & b in J )
per cases ( i = len (q ^ <*(a * c)*>) or i <> len (q ^ <*(a * c)*>) ) ;
suppose i = len (q ^ <*(a * c)*>) ; :: thesis: ex a, b being Element of R st
( (q ^ <*(a * c)*>) . i = a * b & a in I & b in J )
hence ex a, b being Element of R st
( (q ^ <*(a * c)*>) . i = a * b & a in I & b in J ) by A18, A21, A32, FINSEQ_1:42; :: thesis: verum
end;
suppose i <> len (q ^ <*(a * c)*>) ; :: thesis: ex a, b being Element of R st
( (q ^ <*(a * c)*>) . i = a * b & a in I & b in J )
then i < len (q ^ <*(a * c)*>) by A34, XXREAL_0:1;
then A35: i <= len q by A32, NAT_1:13;
then consider a, b being Element of R such that
A36: q . i = a * b and
A37: ( a in I & b in J ) by A15, A33;
i in Seg (len q) by A33, A35, FINSEQ_1:1;
then i in dom q by FINSEQ_1:def 3;
then (q ^ <*(a * c)*>) . i = a * b by A36, FINSEQ_1:def 7;
hence ex a, b being Element of R st
( (q ^ <*(a * c)*>) . i = a * b & a in I & b in J ) by A37; :: thesis: verum
end;
end;
end;
then A38: Sum (q ^ <*(a * c)*>) in { (Sum t) where t is FinSequence of the carrier of R : for i being Element of NAT st 1 <= i & i <= len t holds
ex a, b being Element of R st
( t . i = a * b & a in I & b in J ) } ;
A39: s /. (n + 1) = a * (c + d) by A23, A17, A20, PARTFUN1:def 6
.= (a * c) + (a * d) by VECTSP_1:def 7 ;
(Sum (q ^ <*(a * c)*>)) + (Sum (p ^ <*(a * d)*>)) = ((Sum q) + (Sum <*(a * c)*>)) + (Sum (p ^ <*(a * d)*>)) by RLVECT_1:41
.= ((Sum q) + (a * c)) + (Sum (p ^ <*(a * d)*>)) by BINOM:3
.= ((Sum q) + (a * c)) + ((Sum p) + (Sum <*(a * d)*>)) by RLVECT_1:41
.= ((Sum q) + (a * c)) + ((Sum p) + (a * d)) by BINOM:3
.= (((Sum q) + (a * c)) + (Sum p)) + (a * d) by RLVECT_1:def 3
.= ((a * c) + ((Sum q) + (Sum p))) + (a * d) by RLVECT_1:def 3
.= (f . n) + ((a * c) + (a * d)) by A9, A14, A12, RLVECT_1:def 3
.= f . (n + 1) by A6, A8, A24, A39 ;
hence S1[n + 1] by A38, A31; :: thesis: verum
end;
end;
A40: S1[ 0 ]
proof
take 0. R ; :: thesis: ex y being Element of R st
( f . 0 = (0. R) + y & 0. R in I *' J & y in I *' K )
take 0. R ; :: thesis: ( f . 0 = (0. R) + (0. R) & 0. R in I *' J & 0. R in I *' K )
thus ( f . 0 = (0. R) + (0. R) & 0. R in I *' J & 0. R in I *' K ) by A5, Th3, RLVECT_1:def 4; :: thesis: verum
end;
for n being Element of NAT st 0 <= n & n <= len s holds
S1[n] from INT_1:sch 7(A40, A7);
then ex x, y being Element of R st
( Sum s = x + y & x in I *' J & y in I *' K ) by A4;
hence u in (I *' J) + (I *' K) by A2; :: thesis: verum
end;
now :: thesis: for u being object st u in (I *' J) + (I *' K) holds
u in I *' (J + K)
let u be object ; :: thesis: ( u in (I *' J) + (I *' K) implies u in I *' (J + K) )
assume u in (I *' J) + (I *' K) ; :: thesis: u in I *' (J + K)
then consider a, b being Element of R such that
A41: u = a + b and
A42: a in I *' J and
A43: b in I *' K ;
consider p being FinSequence of the carrier of R such that
A44: b = Sum p and
A45: for i being Element of NAT st 1 <= i & i <= len p holds
ex a, b being Element of R st
( p . i = a * b & a in I & b in K ) by A43;
consider q being FinSequence of the carrier of R such that
A46: a = Sum q and
A47: for i being Element of NAT st 1 <= i & i <= len q holds
ex a, b being Element of R st
( q . i = a * b & a in I & b in J ) by A42;
set s = p ^ q;
A48: for i being Element of NAT st 1 <= i & i <= len (p ^ q) holds
ex a, b being Element of R st
( (p ^ q) . i = a * b & a in I & b in J + K )
proof
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len (p ^ q) implies ex a, b being Element of R st
( (p ^ q) . i = a * b & a in I & b in J + K ) )
assume that
A49: 1 <= i and
A50: i <= len (p ^ q) ; :: thesis: ex a, b being Element of R st
( (p ^ q) . i = a * b & a in I & b in J + K )
i in Seg (len (p ^ q)) by A49, A50, FINSEQ_1:1;
then A51: i in dom (p ^ q) by FINSEQ_1:def 3;
now :: thesis: ( ( i <= len p & ex a, b being Element of R st
( (p ^ q) . i = a * b & a in I & b in J + K ) ) or ( i > len p & ex a, b being Element of R st
( (p ^ q) . i = a * b & a in I & b in J + K ) ) )
per cases ( i <= len p or i > len p ) ;
case A52: i <= len p ; :: thesis: ex a, b being Element of R st
( (p ^ q) . i = a * b & a in I & b in J + K )
then consider a, b being Element of R such that
A53: p . i = a * b and
A54: a in I and
A55: b in K by A45, A49;
i in Seg (len p) by A49, A52, FINSEQ_1:1;
then i in dom p by FINSEQ_1:def 3;
then A56: (p ^ q) . i = a * b by A53, FINSEQ_1:def 7
.= a * ((0. R) + b) by ALGSTR_1:def 2 ;
0. R in J by Th3;
then (0. R) + b in { (a9 + b9) where a9, b9 is Element of R : ( a9 in J & b9 in K ) } by A55;
hence ex a, b being Element of R st
( (p ^ q) . i = a * b & a in I & b in J + K ) by A54, A56; :: thesis: verum
end;
case i > len p ; :: thesis: ex a, b being Element of R st
( (p ^ q) . i = a * b & a in I & b in J + K )
then not i in Seg (len p) by FINSEQ_1:1;
then not i in dom p by FINSEQ_1:def 3;
then consider n being Nat such that
A57: n in dom q and
A58: i = (len p) + n by A51, FINSEQ_1:25;
n in Seg (len q) by A57, FINSEQ_1:def 3;
then ( 1 <= n & n <= len q ) by FINSEQ_1:1;
then consider a, b being Element of R such that
A59: q . n = a * b and
A60: a in I and
A61: b in J by A47, A57;
0. R in K by Th3;
then A62: b + (0. R) in { (a9 + b9) where a9, b9 is Element of R : ( a9 in J & b9 in K ) } by A61;
(p ^ q) . i = q . n by A57, A58, FINSEQ_1:def 7
.= a * (b + (0. R)) by A59, RLVECT_1:def 4 ;
hence ex a, b being Element of R st
( (p ^ q) . i = a * b & a in I & b in J + K ) by A60, A62; :: thesis: verum
end;
end;
end;
hence ex a, b being Element of R st
( (p ^ q) . i = a * b & a in I & b in J + K ) ; :: thesis: verum
end;
Sum (p ^ q) = u by A41, A46, A44, RLVECT_1:41;
hence u in I *' (J + K) by A48; :: thesis: verum
end;
hence I *' (J + K) = (I *' J) + (I *' K) by A1, TARSKI:2; :: thesis: verum