let R be non empty add-cancelable Abelian add-associative right_zeroed associative distributive 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
let u be set ; :: 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 & ( 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 Function of NAT ,the carrier of R such that
A3: ( 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 ex x, y being Element of R st
( f . $1 = x + y & x in I *' J & y in I *' K );
A4: 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 A3, Th3, RLVECT_1:def 7; :: thesis: verum
end;
A5: now
let n be Element of NAT ; :: thesis: ( 0 <= n & n < len s & S1[n] implies S1[n + 1] )
assume A6: ( 0 <= n & 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
A7: ( f . n = x + y & x in I *' J & y in I *' K ) ;
consider q being FinSequence of the carrier of R such that
A8: ( Sum q = x & ( 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 A7;
consider p being FinSequence of the carrier of R such that
A9: ( Sum p = y & ( 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 A7;
A10: 0 + 1 <= n + 1 by XREAL_1:8;
A11: n + 1 <= len s by A6, NAT_1:13;
then n + 1 in Seg (len s) by A10, FINSEQ_1:3;
then A12: n + 1 in dom s by FINSEQ_1:def 3;
then A13: s . (n + 1) = s /. (n + 1) by PARTFUN1:def 8;
consider a, b being Element of R such that
A14: ( s . (n + 1) = a * b & a in I & b in J + K ) by A2, A10, A11;
consider c, d being Element of R such that
A15: ( b = c + d & c in J & d in K ) by A14;
A16: s /. (n + 1) = a * (c + d) by A12, A14, A15, PARTFUN1:def 8
.= (a * c) + (a * d) by VECTSP_1:def 18 ;
set q1 = q ^ <*(a * c)*>;
set p1 = p ^ <*(a * d)*>;
A17: len (q ^ <*(a * c)*>) = (len q) + (len <*(a * c)*>) by FINSEQ_1:35
.= (len q) + 1 by FINSEQ_1:57 ;
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 A18: ( 1 <= i & 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 A14, A15, A17, FINSEQ_1:59; :: 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 A18, XXREAL_0:1;
then A19: i <= len q by A17, NAT_1:13;
then i in Seg (len q) by A18, FINSEQ_1:3;
then A20: i in dom q by FINSEQ_1:def 3;
consider a, b being Element of R such that
A21: ( q . i = a * b & a in I & b in J ) by A8, A18, A19;
(q ^ <*(a * c)*>) . i = a * b by A20, A21, 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 A21; :: thesis: verum
end;
end;
end;
then A22: 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 ) } ;
A23: len (p ^ <*(a * d)*>) = (len p) + (len <*(a * d)*>) by FINSEQ_1:35
.= (len p) + 1 by FINSEQ_1:57 ;
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 A24: ( 1 <= i & 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 A14, A15, A23, FINSEQ_1:59; :: 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 A24, XXREAL_0:1;
then A25: i <= len p by A23, NAT_1:13;
then i in Seg (len p) by A24, FINSEQ_1:3;
then A26: i in dom p by FINSEQ_1:def 3;
consider a, b being Element of R such that
A27: ( p . i = a * b & a in I & b in K ) by A9, A24, A25;
(p ^ <*(a * d)*>) . i = a * b by A26, A27, 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 A27; :: thesis: verum
end;
end;
end;
then A28: Sum (p ^ <*(a * d)*>) in I *' K ;
(Sum (q ^ <*(a * c)*>)) + (Sum (p ^ <*(a * d)*>)) = ((Sum q) + (Sum <*(a * c)*>)) + (Sum (p ^ <*(a * d)*>)) by RLVECT_1:58
.= ((Sum q) + (a * c)) + (Sum (p ^ <*(a * d)*>)) by BINOM:3
.= ((Sum q) + (a * c)) + ((Sum p) + (Sum <*(a * d)*>)) by RLVECT_1:58
.= ((Sum q) + (a * c)) + ((Sum p) + (a * d)) by BINOM:3
.= (((Sum q) + (a * c)) + (Sum p)) + (a * d) by RLVECT_1:def 6
.= ((a * c) + ((Sum q) + (Sum p))) + (a * d) by RLVECT_1:def 6
.= (f . n) + ((a * c) + (a * d)) by A7, A8, A9, RLVECT_1:def 6
.= f . (n + 1) by A3, A6, A13, A16 ;
hence S1[n + 1] by A22, A28; :: thesis: verum
end;
end;
for n being Element of NAT st 0 <= n & n <= len s holds
S1[n] from POLYNOM2:sch 4(A4, A5);
then ex x, y being Element of R st
( Sum s = x + y & x in I *' J & y in I *' K ) by A3;
hence u in (I *' J) + (I *' K) by A2; :: thesis: verum
end;
now
let u be set ; :: 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
A29: ( u = a + b & a in I *' J & b in I *' K ) ;
consider q being FinSequence of the carrier of R such that
A30: ( a = Sum q & ( 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 A29;
consider p being FinSequence of the carrier of R such that
A31: ( b = Sum p & ( 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 A29;
set s = p ^ q;
A32: 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 A33: ( 1 <= i & 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 )
then i in Seg (len (p ^ q)) by FINSEQ_1:3;
then A34: i in dom (p ^ q) by FINSEQ_1:def 3;
now
per cases ( i <= len p or i > len p ) ;
case A35: 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 i in Seg (len p) by A33, FINSEQ_1:3;
then A36: i in dom p by FINSEQ_1:def 3;
consider a, b being Element of R such that
A37: ( p . i = a * b & a in I & b in K ) by A31, A33, A35;
0. R in J by Th3;
then A38: (0. R) + b in { (a' + b') where a', b' is Element of R : ( a' in J & b' in K ) } by A37;
(p ^ q) . i = a * b by A36, A37, FINSEQ_1:def 7
.= a * ((0. R) + b) by ALGSTR_1:def 5 ;
hence ex a, b being Element of R st
( (p ^ q) . i = a * b & a in I & b in J + K ) by A37, A38; :: 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:3;
then not i in dom p by FINSEQ_1:def 3;
then consider n being Nat such that
A39: ( n in dom q & i = (len p) + n ) by A34, FINSEQ_1:38;
n in Seg (len q) by A39, FINSEQ_1:def 3;
then ( 1 <= n & n <= len q ) by FINSEQ_1:3;
then consider a, b being Element of R such that
A40: ( q . n = a * b & a in I & b in J ) by A30, A39;
0. R in K by Th3;
then A41: b + (0. R) in { (a' + b') where a', b' is Element of R : ( a' in J & b' in K ) } by A40;
(p ^ q) . i = q . n by A39, FINSEQ_1:def 7
.= a * (b + (0. R)) by A40, RLVECT_1:def 7 ;
hence ex a, b being Element of R st
( (p ^ q) . i = a * b & a in I & b in J + K ) by A40, A41; :: 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 A29, A30, A31, RLVECT_1:58;
hence u in I *' (J + K) by A32; :: thesis: verum
end;
hence I *' (J + K) = (I *' J) + (I *' K) by A1, TARSKI:2; :: thesis: verum