:: POLYNOM3 semantic presentation
begin
theorem Th1: :: POLYNOM3:1
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being FinSequence of the carrier of L st ( for i being Element of NAT st i in dom p holds
p . i = 0. L ) holds
Sum p = 0. L
proof
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being FinSequence of the carrier of L st ( for i being Element of NAT st i in dom p holds
p . i = 0. L ) holds
Sum p = 0. L
let p be FinSequence of the carrier of L; ::_thesis: ( ( for i being Element of NAT st i in dom p holds
p . i = 0. L ) implies Sum p = 0. L )
assume A1: for k being Element of NAT st k in dom p holds
p . k = 0. L ; ::_thesis: Sum p = 0. L
now__::_thesis:_for_k_being_Nat_st_k_in_dom_p_holds_
p_/._k_=_0._L
let k be Nat; ::_thesis: ( k in dom p implies p /. k = 0. L )
assume A2: k in dom p ; ::_thesis: p /. k = 0. L
hence p /. k = p . k by PARTFUN1:def_6
.= 0. L by A1, A2 ;
::_thesis: verum
end;
hence Sum p = 0. L by MATRLIN:11; ::_thesis: verum
end;
theorem Th2: :: POLYNOM3:2
for V being non empty Abelian add-associative right_zeroed addLoopStr
for p being FinSequence of the carrier of V holds Sum p = Sum (Rev p)
proof
let V be non empty Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for p being FinSequence of the carrier of V holds Sum p = Sum (Rev p)
defpred S1[ FinSequence of the carrier of V] means Sum $1 = Sum (Rev $1);
A1: for p being FinSequence of the carrier of V
for x being Element of V st S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence of the carrier of V; ::_thesis: for x being Element of V st S1[p] holds
S1[p ^ <*x*>]
let x be Element of V; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A2: Sum p = Sum (Rev p) ; ::_thesis: S1[p ^ <*x*>]
thus Sum (p ^ <*x*>) = (Sum p) + (Sum <*x*>) by RLVECT_1:41
.= Sum (<*x*> ^ (Rev p)) by A2, RLVECT_1:41
.= Sum (Rev (p ^ <*x*>)) by FINSEQ_5:63 ; ::_thesis: verum
end;
A3: S1[ <*> the carrier of V] ;
thus for p being FinSequence of the carrier of V holds S1[p] from FINSEQ_2:sch_2(A3, A1); ::_thesis: verum
end;
theorem Th3: :: POLYNOM3:3
for p being FinSequence of REAL holds Sum p = Sum (Rev p)
proof
defpred S1[ FinSequence of REAL ] means Sum $1 = Sum (Rev $1);
A1: for p being FinSequence of REAL
for x being Element of REAL st S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence of REAL ; ::_thesis: for x being Element of REAL st S1[p] holds
S1[p ^ <*x*>]
let x be Element of REAL ; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A2: Sum p = Sum (Rev p) ; ::_thesis: S1[p ^ <*x*>]
thus Sum (p ^ <*x*>) = (Sum p) + (Sum <*x*>) by RVSUM_1:75
.= Sum (<*x*> ^ (Rev p)) by A2, RVSUM_1:75
.= Sum (Rev (p ^ <*x*>)) by FINSEQ_5:63 ; ::_thesis: verum
end;
A3: S1[ <*> REAL] ;
thus for p being FinSequence of REAL holds S1[p] from FINSEQ_2:sch_2(A3, A1); ::_thesis: verum
end;
theorem Th4: :: POLYNOM3:4
for p being FinSequence of NAT
for i being Element of NAT st i in dom p holds
Sum p >= p . i
proof
defpred S1[ FinSequence of NAT ] means for i being Element of NAT st i in dom $1 holds
Sum $1 >= $1 . i;
A1: for p being FinSequence of NAT
for x being Element of NAT st S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence of NAT ; ::_thesis: for x being Element of NAT st S1[p] holds
S1[p ^ <*x*>]
let x be Element of NAT ; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A2: for i being Element of NAT st i in dom p holds
Sum p >= p . i ; ::_thesis: S1[p ^ <*x*>]
let i be Element of NAT ; ::_thesis: ( i in dom (p ^ <*x*>) implies Sum (p ^ <*x*>) >= (p ^ <*x*>) . i )
A3: (p . i) + x >= p . i by NAT_1:11;
len (p ^ <*x*>) = (len p) + 1 by FINSEQ_2:16;
then A4: dom (p ^ <*x*>) = Seg ((len p) + 1) by FINSEQ_1:def_3
.= (Seg (len p)) \/ {((len p) + 1)} by FINSEQ_1:9
.= (dom p) \/ {((len p) + 1)} by FINSEQ_1:def_3 ;
assume A5: i in dom (p ^ <*x*>) ; ::_thesis: Sum (p ^ <*x*>) >= (p ^ <*x*>) . i
percases ( i in dom p or i in {((len p) + 1)} ) by A5, A4, XBOOLE_0:def_3;
supposeA6: i in dom p ; ::_thesis: Sum (p ^ <*x*>) >= (p ^ <*x*>) . i
then Sum p >= p . i by A2;
then (Sum p) + x >= (p . i) + x by XREAL_1:6;
then Sum (p ^ <*x*>) >= (p . i) + x by RVSUM_1:74;
then Sum (p ^ <*x*>) >= p . i by A3, XXREAL_0:2;
hence Sum (p ^ <*x*>) >= (p ^ <*x*>) . i by A6, FINSEQ_1:def_7; ::_thesis: verum
end;
suppose i in {((len p) + 1)} ; ::_thesis: Sum (p ^ <*x*>) >= (p ^ <*x*>) . i
then i = (len p) + 1 by TARSKI:def_1;
then (p ^ <*x*>) . i = x by FINSEQ_1:42;
then (Sum p) + x >= (p ^ <*x*>) . i by NAT_1:11;
hence Sum (p ^ <*x*>) >= (p ^ <*x*>) . i by RVSUM_1:74; ::_thesis: verum
end;
end;
end;
A7: S1[ <*> NAT] ;
thus for p being FinSequence of NAT holds S1[p] from FINSEQ_2:sch_2(A7, A1); ::_thesis: verum
end;
definition
let D be non empty set ;
let i be Element of NAT ;
let p be FinSequence of D;
:: original: Del
redefine func Del (p,i) -> FinSequence of D;
coherence
Del (p,i) is FinSequence of D by FINSEQ_3:105;
end;
definition
let D be non empty set ;
let a, b be Element of D;
:: original: <*
redefine func<*a,b*> -> Element of 2 -tuples_on D;
coherence
<*a,b*> is Element of 2 -tuples_on D by FINSEQ_2:101;
end;
definition
let D be non empty set ;
let k, n be Element of NAT ;
let p be Element of k -tuples_on D;
let q be Element of n -tuples_on D;
:: original: ^
redefine funcp ^ q -> Element of (k + n) -tuples_on D;
coherence
p ^ q is Element of (k + n) -tuples_on D
proof
p ^ q is Tuple of k + n,D ;
hence p ^ q is Element of (k + n) -tuples_on D by FINSEQ_2:131; ::_thesis: verum
end;
end;
definition
let D be non empty set ;
let k, n be Element of NAT ;
let p be FinSequence of k -tuples_on D;
let q be FinSequence of n -tuples_on D;
:: original: ^^
redefine funcp ^^ q -> Element of ((k + n) -tuples_on D) * ;
coherence
p ^^ q is Element of ((k + n) -tuples_on D) *
proof
rng (p ^^ q) c= (k + n) -tuples_on D
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (p ^^ q) or y in (k + n) -tuples_on D )
assume y in rng (p ^^ q) ; ::_thesis: y in (k + n) -tuples_on D
then consider x being set such that
A1: x in dom (p ^^ q) and
A2: y = (p ^^ q) . x by FUNCT_1:def_3;
A3: x in (dom p) /\ (dom q) by A1, PRE_POLY:def_4;
then A4: x in dom p by XBOOLE_0:def_4;
A5: x in dom q by A3, XBOOLE_0:def_4;
y = (p . x) ^ (q . x) by A1, A2, PRE_POLY:def_4
.= (p /. x) ^ (q . x) by A4, PARTFUN1:def_6
.= (p /. x) ^ (q /. x) by A5, PARTFUN1:def_6 ;
hence y in (k + n) -tuples_on D ; ::_thesis: verum
end;
then p ^^ q is FinSequence of (k + n) -tuples_on D by FINSEQ_1:def_4;
hence p ^^ q is Element of ((k + n) -tuples_on D) * by FINSEQ_1:def_11; ::_thesis: verum
end;
end;
scheme :: POLYNOM3:sch 1
SeqOfSeqLambdaD{ F1() -> non empty set , F2() -> Element of NAT , F3( Element of NAT ) -> Element of NAT , F4( set , set ) -> Element of F1() } :
ex p being FinSequence of F1() * st
( len p = F2() & ( for k being Element of NAT st k in Seg F2() holds
( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F4(k,n) ) ) ) )
proof
defpred S1[ Element of NAT , FinSequence] means ( len $2 = F3($1) & ( for n being Element of NAT st n in dom $2 holds
$2 . n = F4($1,n) ) );
A1: for k being Element of NAT st k in Seg F2() holds
ex d being Element of F1() * st S1[k,d]
proof
let k be Element of NAT ; ::_thesis: ( k in Seg F2() implies ex d being Element of F1() * st S1[k,d] )
assume k in Seg F2() ; ::_thesis: ex d being Element of F1() * st S1[k,d]
deffunc H1( Nat) -> Element of F1() = F4(k,$1);
consider d being FinSequence of F1() such that
A2: len d = F3(k) and
A3: for n being Nat st n in dom d holds
d . n = H1(n) from FINSEQ_2:sch_1();
reconsider d = d as Element of F1() * by FINSEQ_1:def_11;
take d ; ::_thesis: S1[k,d]
thus len d = F3(k) by A2; ::_thesis: for n being Element of NAT st n in dom d holds
d . n = F4(k,n)
let n be Element of NAT ; ::_thesis: ( n in dom d implies d . n = F4(k,n) )
assume n in dom d ; ::_thesis: d . n = F4(k,n)
hence d . n = F4(k,n) by A3; ::_thesis: verum
end;
consider p being FinSequence of F1() * such that
A4: dom p = Seg F2() and
A5: for k being Element of NAT st k in Seg F2() holds
S1[k,p /. k] from RECDEF_1:sch_17(A1);
take p ; ::_thesis: ( len p = F2() & ( for k being Element of NAT st k in Seg F2() holds
( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F4(k,n) ) ) ) )
thus len p = F2() by A4, FINSEQ_1:def_3; ::_thesis: for k being Element of NAT st k in Seg F2() holds
( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F4(k,n) ) )
let k be Element of NAT ; ::_thesis: ( k in Seg F2() implies ( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F4(k,n) ) ) )
assume k in Seg F2() ; ::_thesis: ( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F4(k,n) ) )
hence ( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F4(k,n) ) ) by A5; ::_thesis: verum
end;
begin
definition
let n be Element of NAT ;
let p, q be Element of n -tuples_on NAT;
predp < q means :Def1: :: POLYNOM3:def 1
ex i being Element of NAT st
( i in Seg n & p . i < q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) );
asymmetry
for p, q being Element of n -tuples_on NAT st ex i being Element of NAT st
( i in Seg n & p . i < q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) ) holds
for i being Element of NAT holds
( not i in Seg n or not q . i < p . i or ex k being Element of NAT st
( 1 <= k & k < i & not q . k = p . k ) )
proof
let p, q be Element of n -tuples_on NAT; ::_thesis: ( ex i being Element of NAT st
( i in Seg n & p . i < q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) ) implies for i being Element of NAT holds
( not i in Seg n or not q . i < p . i or ex k being Element of NAT st
( 1 <= k & k < i & not q . k = p . k ) ) )
given i being Element of NAT such that A1: i in Seg n and
A2: p . i < q . i and
A3: for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ; ::_thesis: for i being Element of NAT holds
( not i in Seg n or not q . i < p . i or ex k being Element of NAT st
( 1 <= k & k < i & not q . k = p . k ) )
A4: 1 <= i by A1, FINSEQ_1:1;
given j being Element of NAT such that A5: j in Seg n and
A6: q . j < p . j and
A7: for k being Element of NAT st 1 <= k & k < j holds
q . k = p . k ; ::_thesis: contradiction
A8: 1 <= j by A5, FINSEQ_1:1;
percases ( i < j or j < i or i = j ) by XXREAL_0:1;
suppose i < j ; ::_thesis: contradiction
hence contradiction by A2, A7, A4; ::_thesis: verum
end;
suppose j < i ; ::_thesis: contradiction
hence contradiction by A3, A6, A8; ::_thesis: verum
end;
suppose i = j ; ::_thesis: contradiction
hence contradiction by A2, A6; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem Def1 defines < POLYNOM3:def_1_:_
for n being Element of NAT
for p, q being Element of n -tuples_on NAT holds
( p < q iff ex i being Element of NAT st
( i in Seg n & p . i < q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) ) );
notation
let n be Element of NAT ;
let p, q be Element of n -tuples_on NAT;
synonym q > p for p < q;
end;
definition
let n be Element of NAT ;
let p, q be Element of n -tuples_on NAT;
predp <= q means :Def2: :: POLYNOM3:def 2
( p < q or p = q );
reflexivity
for p being Element of n -tuples_on NAT holds
( p < p or p = p ) ;
end;
:: deftheorem Def2 defines <= POLYNOM3:def_2_:_
for n being Element of NAT
for p, q being Element of n -tuples_on NAT holds
( p <= q iff ( p < q or p = q ) );
notation
let n be Element of NAT ;
let p, q be Element of n -tuples_on NAT;
synonym q >= p for p <= q;
end;
theorem Th5: :: POLYNOM3:5
for n being Element of NAT
for p, q, r being Element of n -tuples_on NAT holds
( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) )
proof
let n be Element of NAT ; ::_thesis: for p, q, r being Element of n -tuples_on NAT holds
( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) )
let p, q, r be Element of n -tuples_on NAT; ::_thesis: ( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) )
thus A1: ( p < q & q < r implies p < r ) ::_thesis: ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r )
proof
assume that
A2: p < q and
A3: q < r ; ::_thesis: p < r
consider i being Element of NAT such that
A4: i in Seg n and
A5: p . i < q . i and
A6: for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k by A2, Def1;
consider j being Element of NAT such that
A7: j in Seg n and
A8: q . j < r . j and
A9: for k being Element of NAT st 1 <= k & k < j holds
q . k = r . k by A3, Def1;
reconsider t = min (i,j) as Element of NAT ;
take t ; :: according to POLYNOM3:def_1 ::_thesis: ( t in Seg n & p . t < r . t & ( for k being Element of NAT st 1 <= k & k < t holds
p . k = r . k ) )
thus t in Seg n by A4, A7, XXREAL_0:15; ::_thesis: ( p . t < r . t & ( for k being Element of NAT st 1 <= k & k < t holds
p . k = r . k ) )
now__::_thesis:_p_._t_<_r_._t
percases ( i < j or i > j or i = j ) by XXREAL_0:1;
supposeA10: i < j ; ::_thesis: p . t < r . t
A11: i >= 1 by A4, FINSEQ_1:1;
t = i by A10, XXREAL_0:def_9;
hence p . t < r . t by A5, A9, A10, A11; ::_thesis: verum
end;
supposeA12: i > j ; ::_thesis: p . t < r . t
A13: j >= 1 by A7, FINSEQ_1:1;
t = j by A12, XXREAL_0:def_9;
hence p . t < r . t by A6, A8, A12, A13; ::_thesis: verum
end;
suppose i = j ; ::_thesis: p . t < r . t
hence p . t < r . t by A5, A8, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence p . t < r . t ; ::_thesis: for k being Element of NAT st 1 <= k & k < t holds
p . k = r . k
let k be Element of NAT ; ::_thesis: ( 1 <= k & k < t implies p . k = r . k )
assume that
A14: 1 <= k and
A15: k < t ; ::_thesis: p . k = r . k
t <= j by XXREAL_0:17;
then A16: k < j by A15, XXREAL_0:2;
t <= i by XXREAL_0:17;
then k < i by A15, XXREAL_0:2;
hence p . k = q . k by A6, A14
.= r . k by A9, A14, A16 ;
::_thesis: verum
end;
assume A17: ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) ; ::_thesis: p <= r
percases ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) by A17;
supposeA18: ( p < q & q <= r ) ; ::_thesis: p <= r
then ( q < r or q = r ) by Def2;
hence p <= r by A1, A18, Def2; ::_thesis: verum
end;
supposeA19: ( p <= q & q < r ) ; ::_thesis: p <= r
then ( p < q or p = q ) by Def2;
hence p <= r by A1, A19, Def2; ::_thesis: verum
end;
suppose ( p <= q & q <= r ) ; ::_thesis: p <= r
hence p <= r by A1, Def2; ::_thesis: verum
end;
end;
end;
theorem Th6: :: POLYNOM3:6
for n being Element of NAT
for p, q being Element of n -tuples_on NAT st p <> q holds
ex i being Element of NAT st
( i in Seg n & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) )
proof
defpred S1[ Nat] means for p, q being Element of $1 -tuples_on NAT st p <> q holds
ex i being Element of NAT st
( i in Seg $1 & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) );
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: for p, q being Element of n -tuples_on NAT st p <> q holds
ex i being Element of NAT st
( i in Seg n & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) ) ; ::_thesis: S1[n + 1]
let p, q be Element of (n + 1) -tuples_on NAT; ::_thesis: ( p <> q implies ex i being Element of NAT st
( i in Seg (n + 1) & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) ) )
consider t1 being Element of n -tuples_on NAT, d1 being Element of NAT such that
A3: p = t1 ^ <*d1*> by FINSEQ_2:117;
assume A4: p <> q ; ::_thesis: ex i being Element of NAT st
( i in Seg (n + 1) & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) )
consider t2 being Element of n -tuples_on NAT, d2 being Element of NAT such that
A5: q = t2 ^ <*d2*> by FINSEQ_2:117;
A6: len t1 = n by CARD_1:def_7;
A7: len t2 = n by CARD_1:def_7;
percases ( t1 <> t2 or t1 = t2 ) ;
suppose t1 <> t2 ; ::_thesis: ex i being Element of NAT st
( i in Seg (n + 1) & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) )
then consider i being Element of NAT such that
A8: i in Seg n and
A9: t1 . i <> t2 . i and
A10: for k being Element of NAT st 1 <= k & k < i holds
t1 . k = t2 . k by A2;
take i ; ::_thesis: ( i in Seg (n + 1) & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) )
thus i in Seg (n + 1) by A8, FINSEQ_2:8; ::_thesis: ( p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) )
i in dom t1 by A6, A8, FINSEQ_1:def_3;
then A11: p . i = t1 . i by A3, FINSEQ_1:def_7;
i in dom t2 by A7, A8, FINSEQ_1:def_3;
hence p . i <> q . i by A5, A9, A11, FINSEQ_1:def_7; ::_thesis: for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k
let k be Element of NAT ; ::_thesis: ( 1 <= k & k < i implies p . k = q . k )
assume that
A12: 1 <= k and
A13: k < i ; ::_thesis: p . k = q . k
i <= n by A8, FINSEQ_1:1;
then A14: k <= n by A13, XXREAL_0:2;
then A15: k in dom t1 by A6, A12, FINSEQ_3:25;
A16: k in dom t2 by A7, A12, A14, FINSEQ_3:25;
t1 . k = t2 . k by A10, A12, A13;
hence p . k = t2 . k by A3, A15, FINSEQ_1:def_7
.= q . k by A5, A16, FINSEQ_1:def_7 ;
::_thesis: verum
end;
supposeA17: t1 = t2 ; ::_thesis: ex i being Element of NAT st
( i in Seg (n + 1) & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) )
take i = n + 1; ::_thesis: ( i in Seg (n + 1) & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) )
thus i in Seg (n + 1) by FINSEQ_1:4; ::_thesis: ( p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) )
p . i = d1 by A3, FINSEQ_2:116;
hence p . i <> q . i by A3, A5, A4, A17, FINSEQ_2:116; ::_thesis: for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k
let k be Element of NAT ; ::_thesis: ( 1 <= k & k < i implies p . k = q . k )
assume that
A18: 1 <= k and
A19: k < i ; ::_thesis: p . k = q . k
A20: k <= n by A19, NAT_1:13;
then A21: k in dom t2 by A7, A18, FINSEQ_3:25;
k in dom t1 by A6, A18, A20, FINSEQ_3:25;
hence p . k = t2 . k by A3, A17, FINSEQ_1:def_7
.= q . k by A5, A21, FINSEQ_1:def_7 ;
::_thesis: verum
end;
end;
end;
A22: S1[ 0 ] ;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A22, A1); ::_thesis: verum
end;
theorem Th7: :: POLYNOM3:7
for n being Element of NAT
for p, q being Element of n -tuples_on NAT holds
( p <= q or p > q )
proof
let n be Element of NAT ; ::_thesis: for p, q being Element of n -tuples_on NAT holds
( p <= q or p > q )
let p, q be Element of n -tuples_on NAT; ::_thesis: ( p <= q or p > q )
assume A1: not p <= q ; ::_thesis: p > q
then consider i being Element of NAT such that
A2: i in Seg n and
A3: p . i <> q . i and
A4: for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k by Th6;
take i ; :: according to POLYNOM3:def_1 ::_thesis: ( i in Seg n & q . i < p . i & ( for k being Element of NAT st 1 <= k & k < i holds
q . k = p . k ) )
thus i in Seg n by A2; ::_thesis: ( q . i < p . i & ( for k being Element of NAT st 1 <= k & k < i holds
q . k = p . k ) )
not p < q by A1, Def2;
then p . i >= q . i by A2, A4, Def1;
hence q . i < p . i by A3, XXREAL_0:1; ::_thesis: for k being Element of NAT st 1 <= k & k < i holds
q . k = p . k
thus for k being Element of NAT st 1 <= k & k < i holds
q . k = p . k by A4; ::_thesis: verum
end;
definition
let n be Element of NAT ;
func TuplesOrder n -> Order of (n -tuples_on NAT) means :Def3: :: POLYNOM3:def 3
for p, q being Element of n -tuples_on NAT holds
( [p,q] in it iff p <= q );
existence
ex b1 being Order of (n -tuples_on NAT) st
for p, q being Element of n -tuples_on NAT holds
( [p,q] in b1 iff p <= q )
proof
defpred S1[ Element of n -tuples_on NAT, Element of n -tuples_on NAT] means $1 <= $2;
consider R being Relation of (n -tuples_on NAT),(n -tuples_on NAT) such that
A1: for x, y being Element of n -tuples_on NAT holds
( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2();
A2: R is_transitive_in n -tuples_on NAT
proof
let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in n -tuples_on NAT or not y in n -tuples_on NAT or not z in n -tuples_on NAT or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that
A3: ( x in n -tuples_on NAT & y in n -tuples_on NAT & z in n -tuples_on NAT ) and
A4: ( [x,y] in R & [y,z] in R ) ; ::_thesis: [x,z] in R
reconsider x1 = x, y1 = y, z1 = z as Element of n -tuples_on NAT by A3;
( x1 <= y1 & y1 <= z1 ) by A1, A4;
then x1 <= z1 by Th5;
hence [x,z] in R by A1; ::_thesis: verum
end;
A5: R is_reflexive_in n -tuples_on NAT
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in n -tuples_on NAT or [x,x] in R )
assume x in n -tuples_on NAT ; ::_thesis: [x,x] in R
then reconsider x1 = x as Element of n -tuples_on NAT ;
x1 <= x1 ;
hence [x,x] in R by A1; ::_thesis: verum
end;
then A6: ( dom R = n -tuples_on NAT & field R = n -tuples_on NAT ) by ORDERS_1:13;
R is_antisymmetric_in n -tuples_on NAT
proof
let x, y be set ; :: according to RELAT_2:def_4 ::_thesis: ( not x in n -tuples_on NAT or not y in n -tuples_on NAT or not [x,y] in R or not [y,x] in R or x = y )
assume that
A7: ( x in n -tuples_on NAT & y in n -tuples_on NAT ) and
A8: [x,y] in R and
A9: [y,x] in R ; ::_thesis: x = y
reconsider x1 = x, y1 = y as Element of n -tuples_on NAT by A7;
x1 <= y1 by A1, A8;
then A10: ( x1 < y1 or x1 = y1 ) by Def2;
y1 <= x1 by A1, A9;
hence x = y by A10, Def2; ::_thesis: verum
end;
then reconsider R = R as Order of (n -tuples_on NAT) by A5, A2, A6, PARTFUN1:def_2, RELAT_2:def_9, RELAT_2:def_12, RELAT_2:def_16;
take R ; ::_thesis: for p, q being Element of n -tuples_on NAT holds
( [p,q] in R iff p <= q )
thus for p, q being Element of n -tuples_on NAT holds
( [p,q] in R iff p <= q ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Order of (n -tuples_on NAT) st ( for p, q being Element of n -tuples_on NAT holds
( [p,q] in b1 iff p <= q ) ) & ( for p, q being Element of n -tuples_on NAT holds
( [p,q] in b2 iff p <= q ) ) holds
b1 = b2
proof
let T1, T2 be Order of (n -tuples_on NAT); ::_thesis: ( ( for p, q being Element of n -tuples_on NAT holds
( [p,q] in T1 iff p <= q ) ) & ( for p, q being Element of n -tuples_on NAT holds
( [p,q] in T2 iff p <= q ) ) implies T1 = T2 )
assume that
A11: for p, q being Element of n -tuples_on NAT holds
( [p,q] in T1 iff p <= q ) and
A12: for p, q being Element of n -tuples_on NAT holds
( [p,q] in T2 iff p <= q ) ; ::_thesis: T1 = T2
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in T1 or [x,y] in T2 ) & ( not [x,y] in T2 or [x,y] in T1 ) )
thus ( [x,y] in T1 implies [x,y] in T2 ) ::_thesis: ( not [x,y] in T2 or [x,y] in T1 )
proof
assume A13: [x,y] in T1 ; ::_thesis: [x,y] in T2
then consider p, q being set such that
A14: [x,y] = [p,q] and
A15: ( p in n -tuples_on NAT & q in n -tuples_on NAT ) by RELSET_1:2;
reconsider p = p, q = q as Element of n -tuples_on NAT by A15;
p <= q by A11, A13, A14;
hence [x,y] in T2 by A12, A14; ::_thesis: verum
end;
assume A16: [x,y] in T2 ; ::_thesis: [x,y] in T1
then consider p, q being set such that
A17: [x,y] = [p,q] and
A18: ( p in n -tuples_on NAT & q in n -tuples_on NAT ) by RELSET_1:2;
reconsider p = p, q = q as Element of n -tuples_on NAT by A18;
p <= q by A12, A16, A17;
hence [x,y] in T1 by A11, A17; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines TuplesOrder POLYNOM3:def_3_:_
for n being Element of NAT
for b2 being Order of (n -tuples_on NAT) holds
( b2 = TuplesOrder n iff for p, q being Element of n -tuples_on NAT holds
( [p,q] in b2 iff p <= q ) );
registration
let n be Element of NAT ;
cluster TuplesOrder n -> being_linear-order ;
coherence
TuplesOrder n is being_linear-order
proof
now__::_thesis:_for_x,_y_being_set_st_x_in_n_-tuples_on_NAT_&_y_in_n_-tuples_on_NAT_&_x_<>_y_&_not_[x,y]_in_TuplesOrder_n_holds_
[y,x]_in_TuplesOrder_n
let x, y be set ; ::_thesis: ( x in n -tuples_on NAT & y in n -tuples_on NAT & x <> y & not [x,y] in TuplesOrder n implies [y,x] in TuplesOrder n )
assume that
A1: ( x in n -tuples_on NAT & y in n -tuples_on NAT ) and
x <> y and
A2: not [x,y] in TuplesOrder n ; ::_thesis: [y,x] in TuplesOrder n
reconsider p = x, q = y as Element of n -tuples_on NAT by A1;
not p <= q by A2, Def3;
then p > q by Th7;
then q <= p by Def2;
hence [y,x] in TuplesOrder n by Def3; ::_thesis: verum
end;
then ( field (TuplesOrder n) = n -tuples_on NAT & TuplesOrder n is_connected_in n -tuples_on NAT ) by ORDERS_1:15, RELAT_2:def_6;
then TuplesOrder n is connected by RELAT_2:def_14;
hence TuplesOrder n is being_linear-order by ORDERS_1:def_5; ::_thesis: verum
end;
end;
begin
definition
let i be non empty Element of NAT ;
let n be Element of NAT ;
func Decomp (n,i) -> FinSequence of i -tuples_on NAT means :Def4: :: POLYNOM3:def 4
ex A being finite Subset of (i -tuples_on NAT) st
( it = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) );
existence
ex b1 being FinSequence of i -tuples_on NAT ex A being finite Subset of (i -tuples_on NAT) st
( b1 = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) )
proof
reconsider n1 = n + 1 as non empty set ;
defpred S1[ Element of i -tuples_on NAT] means Sum $1 = n;
consider A being Subset of (i -tuples_on NAT) such that
A1: for p being Element of i -tuples_on NAT holds
( p in A iff S1[p] ) from SUBSET_1:sch_3();
A2: A c= i -tuples_on (n + 1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in i -tuples_on (n + 1) )
assume A3: x in A ; ::_thesis: x in i -tuples_on (n + 1)
then reconsider p = x as Element of i -tuples_on NAT ;
A4: Sum p = n by A1, A3;
rng p c= n + 1
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in n + 1 )
assume that
A5: y in rng p and
A6: not y in n + 1 ; ::_thesis: contradiction
rng p c= NAT by FINSEQ_1:def_4;
then reconsider k = y as Element of NAT by A5;
not y in { t where t is Element of NAT : t < n + 1 } by A6, AXIOMS:4;
then A7: k >= n + 1 ;
ex j being Nat st
( j in dom p & p . j = k ) by A5, FINSEQ_2:10;
then Sum p >= k by Th4;
hence contradiction by A4, A7, NAT_1:13; ::_thesis: verum
end;
then ( len p = i & p is FinSequence of n + 1 ) by CARD_1:def_7, FINSEQ_1:def_4;
then p is Element of i -tuples_on n1 by FINSEQ_2:92;
hence x in i -tuples_on (n + 1) ; ::_thesis: verum
end;
reconsider A = A as finite Subset of (i -tuples_on NAT) by A2;
take SgmX ((TuplesOrder i),A) ; ::_thesis: ex A being finite Subset of (i -tuples_on NAT) st
( SgmX ((TuplesOrder i),A) = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) )
thus ex A being finite Subset of (i -tuples_on NAT) st
( SgmX ((TuplesOrder i),A) = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of i -tuples_on NAT st ex A being finite Subset of (i -tuples_on NAT) st
( b1 = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) & ex A being finite Subset of (i -tuples_on NAT) st
( b2 = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) holds
b1 = b2
proof
let p1, p2 be FinSequence of i -tuples_on NAT; ::_thesis: ( ex A being finite Subset of (i -tuples_on NAT) st
( p1 = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) & ex A being finite Subset of (i -tuples_on NAT) st
( p2 = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) implies p1 = p2 )
given A1 being finite Subset of (i -tuples_on NAT) such that A8: p1 = SgmX ((TuplesOrder i),A1) and
A9: for p being Element of i -tuples_on NAT holds
( p in A1 iff Sum p = n ) ; ::_thesis: ( for A being finite Subset of (i -tuples_on NAT) holds
( not p2 = SgmX ((TuplesOrder i),A) or ex p being Element of i -tuples_on NAT st
( ( p in A implies Sum p = n ) implies ( Sum p = n & not p in A ) ) ) or p1 = p2 )
given A2 being finite Subset of (i -tuples_on NAT) such that A10: p2 = SgmX ((TuplesOrder i),A2) and
A11: for p being Element of i -tuples_on NAT holds
( p in A2 iff Sum p = n ) ; ::_thesis: p1 = p2
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_A1_implies_x_in_A2_)_&_(_x_in_A2_implies_x_in_A1_)_)
let x be set ; ::_thesis: ( ( x in A1 implies x in A2 ) & ( x in A2 implies x in A1 ) )
thus ( x in A1 implies x in A2 ) ::_thesis: ( x in A2 implies x in A1 )
proof
assume A12: x in A1 ; ::_thesis: x in A2
then reconsider p = x as Element of i -tuples_on NAT ;
Sum p = n by A9, A12;
hence x in A2 by A11; ::_thesis: verum
end;
assume A13: x in A2 ; ::_thesis: x in A1
then reconsider p = x as Element of i -tuples_on NAT ;
Sum p = n by A11, A13;
hence x in A1 by A9; ::_thesis: verum
end;
hence p1 = p2 by A8, A10, TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines Decomp POLYNOM3:def_4_:_
for i being non empty Element of NAT
for n being Element of NAT
for b3 being FinSequence of i -tuples_on NAT holds
( b3 = Decomp (n,i) iff ex A being finite Subset of (i -tuples_on NAT) st
( b3 = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) );
registration
let i be non empty Element of NAT ;
let n be Element of NAT ;
cluster Decomp (n,i) -> one-to-one non empty FinSequence-yielding ;
coherence
( not Decomp (n,i) is empty & Decomp (n,i) is one-to-one & Decomp (n,i) is FinSequence-yielding )
proof
reconsider p2 = (i -' 1) |-> 0 as FinSequence of NAT ;
i >= 1 by NAT_1:14;
then (i -' 1) + 1 = i by XREAL_1:235;
then ((i -' 1) |-> 0) ^ <*n*> is Tuple of i, NAT ;
then reconsider p1 = ((i -' 1) |-> 0) ^ <*n*> as Element of i -tuples_on NAT by FINSEQ_2:131;
consider A being finite Subset of (i -tuples_on NAT) such that
A1: Decomp (n,i) = SgmX ((TuplesOrder i),A) and
A2: for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) by Def4;
Sum p1 = (Sum p2) + n by RVSUM_1:74
.= 0 + n by RVSUM_1:81 ;
then reconsider A = A as non empty finite Subset of (i -tuples_on NAT) by A2;
( not SgmX ((TuplesOrder i),A) is empty & SgmX ((TuplesOrder i),A) is finite ) ;
hence ( not Decomp (n,i) is empty & Decomp (n,i) is one-to-one & Decomp (n,i) is FinSequence-yielding ) by A1; ::_thesis: verum
end;
end;
theorem Th8: :: POLYNOM3:8
for n being Element of NAT holds len (Decomp (n,1)) = 1
proof
let n be Element of NAT ; ::_thesis: len (Decomp (n,1)) = 1
consider A being finite Subset of (1 -tuples_on NAT) such that
A1: Decomp (n,1) = SgmX ((TuplesOrder 1),A) and
A2: for p being Element of 1 -tuples_on NAT holds
( p in A iff Sum p = n ) by Def4;
A3: A = {<*n*>}
proof
thus A c= {<*n*>} :: according to XBOOLE_0:def_10 ::_thesis: {<*n*>} c= A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in A or y in {<*n*>} )
assume A4: y in A ; ::_thesis: y in {<*n*>}
then reconsider p = y as Element of 1 -tuples_on NAT ;
A5: Sum p = n by A2, A4;
consider k being Element of NAT such that
A6: p = <*k*> by FINSEQ_2:97;
Sum p = k by A6, RVSUM_1:73;
hence y in {<*n*>} by A5, A6, TARSKI:def_1; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {<*n*>} or y in A )
assume y in {<*n*>} ; ::_thesis: y in A
then A7: y = <*n*> by TARSKI:def_1;
A8: <*n*> is Element of 1 -tuples_on NAT by FINSEQ_2:131;
Sum <*n*> = n by RVSUM_1:73;
hence y in A by A2, A7, A8; ::_thesis: verum
end;
field (TuplesOrder 1) = 1 -tuples_on NAT by ORDERS_1:15;
then TuplesOrder 1 linearly_orders 1 -tuples_on NAT by ORDERS_1:37;
hence len (Decomp (n,1)) = card A by A1, ORDERS_1:38, PRE_POLY:11
.= 1 by A3, CARD_1:30 ;
::_thesis: verum
end;
theorem Th9: :: POLYNOM3:9
for n being Element of NAT holds len (Decomp (n,2)) = n + 1
proof
let n be Element of NAT ; ::_thesis: len (Decomp (n,2)) = n + 1
deffunc H1( Nat) -> set = <*$1,(n -' $1)*>;
consider q being FinSequence such that
A1: len q = n and
A2: for k being Nat st k in dom q holds
q . k = H1(k) from FINSEQ_1:sch_2();
A3: dom q = Seg n by A1, FINSEQ_1:def_3;
set q1 = q ^ <*<*0,n*>*>;
A4: dom q = Seg n by A1, FINSEQ_1:def_3;
A5: len (q ^ <*<*0,n*>*>) = n + 1 by A1, FINSEQ_2:16;
then A6: dom (q ^ <*<*0,n*>*>) = Seg (n + 1) by FINSEQ_1:def_3;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_(q_^_<*<*0,n*>*>)_&_x2_in_dom_(q_^_<*<*0,n*>*>)_&_(q_^_<*<*0,n*>*>)_._x1_=_(q_^_<*<*0,n*>*>)_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom (q ^ <*<*0,n*>*>) & x2 in dom (q ^ <*<*0,n*>*>) & (q ^ <*<*0,n*>*>) . x1 = (q ^ <*<*0,n*>*>) . x2 implies x1 = x2 )
assume that
A7: x1 in dom (q ^ <*<*0,n*>*>) and
A8: x2 in dom (q ^ <*<*0,n*>*>) and
A9: (q ^ <*<*0,n*>*>) . x1 = (q ^ <*<*0,n*>*>) . x2 ; ::_thesis: x1 = x2
reconsider k1 = x1, k2 = x2 as Element of NAT by A7, A8;
x2 in (Seg n) \/ {(n + 1)} by A6, A8, FINSEQ_1:9;
then A10: ( x2 in Seg n or x2 in {(n + 1)} ) by XBOOLE_0:def_3;
x1 in (Seg n) \/ {(n + 1)} by A6, A7, FINSEQ_1:9;
then A11: ( x1 in Seg n or x1 in {(n + 1)} ) by XBOOLE_0:def_3;
now__::_thesis:_x1_=_x2
percases ( ( x1 in Seg n & x2 in Seg n ) or ( x1 in Seg n & x2 = n + 1 ) or ( x1 = n + 1 & x2 in Seg n ) or ( x1 = n + 1 & x2 = n + 1 ) ) by A11, A10, TARSKI:def_1;
supposeA12: ( x1 in Seg n & x2 in Seg n ) ; ::_thesis: x1 = x2
then A13: ( (q ^ <*<*0,n*>*>) . k1 = q . k1 & (q ^ <*<*0,n*>*>) . k2 = q . k2 ) by A3, FINSEQ_1:def_7;
( q . k1 = <*k1,(n -' k1)*> & q . k2 = <*k2,(n -' k2)*> ) by A2, A4, A12;
hence x1 = x2 by A9, A13, FINSEQ_1:77; ::_thesis: verum
end;
supposeA14: ( x1 in Seg n & x2 = n + 1 ) ; ::_thesis: x1 = x2
then A15: (q ^ <*<*0,n*>*>) . k2 = <*0,n*> by A1, FINSEQ_1:42;
(q ^ <*<*0,n*>*>) . k1 = q . k1 by A3, A14, FINSEQ_1:def_7
.= <*k1,(n -' k1)*> by A2, A4, A14 ;
then k1 = 0 by A9, A15, FINSEQ_1:77;
hence x1 = x2 by A14, FINSEQ_1:1; ::_thesis: verum
end;
supposeA16: ( x1 = n + 1 & x2 in Seg n ) ; ::_thesis: x1 = x2
then A17: (q ^ <*<*0,n*>*>) . k1 = <*0,n*> by A1, FINSEQ_1:42;
(q ^ <*<*0,n*>*>) . k2 = q . k2 by A3, A16, FINSEQ_1:def_7
.= <*k2,(n -' k2)*> by A2, A4, A16 ;
then k2 = 0 by A9, A17, FINSEQ_1:77;
hence x1 = x2 by A16, FINSEQ_1:1; ::_thesis: verum
end;
suppose ( x1 = n + 1 & x2 = n + 1 ) ; ::_thesis: x1 = x2
hence x1 = x2 ; ::_thesis: verum
end;
end;
end;
hence x1 = x2 ; ::_thesis: verum
end;
then q ^ <*<*0,n*>*> is one-to-one by FUNCT_1:def_4;
then A18: card (rng (q ^ <*<*0,n*>*>)) = n + 1 by A5, FINSEQ_4:62;
A19: rng q c= rng (q ^ <*<*0,n*>*>) by FINSEQ_1:29;
A20: rng (q ^ <*<*0,n*>*>) = { <*i,(n -' i)*> where i is Element of NAT : i <= n }
proof
thus rng (q ^ <*<*0,n*>*>) c= { <*i,(n -' i)*> where i is Element of NAT : i <= n } :: according to XBOOLE_0:def_10 ::_thesis: { <*i,(n -' i)*> where i is Element of NAT : i <= n } c= rng (q ^ <*<*0,n*>*>)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (q ^ <*<*0,n*>*>) or x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } )
assume x in rng (q ^ <*<*0,n*>*>) ; ::_thesis: x in { <*i,(n -' i)*> where i is Element of NAT : i <= n }
then consider j being Nat such that
A21: j in dom (q ^ <*<*0,n*>*>) and
A22: (q ^ <*<*0,n*>*>) . j = x by FINSEQ_2:10;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
j in (Seg n) \/ {(n + 1)} by A6, A21, FINSEQ_1:9;
then A23: ( j in Seg n or j in {(n + 1)} ) by XBOOLE_0:def_3;
now__::_thesis:_x_in__{__<*i,(n_-'_i)*>_where_i_is_Element_of_NAT_:_i_<=_n__}_
percases ( j in Seg n or j = n + 1 ) by A23, TARSKI:def_1;
supposeA24: j in Seg n ; ::_thesis: x in { <*i,(n -' i)*> where i is Element of NAT : i <= n }
then A25: (q ^ <*<*0,n*>*>) . j = q . j by A3, FINSEQ_1:def_7;
( q . j = <*j,(n -' j)*> & j <= n ) by A2, A4, A24, FINSEQ_1:1;
hence x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } by A22, A25; ::_thesis: verum
end;
suppose j = n + 1 ; ::_thesis: x in { <*i,(n -' i)*> where i is Element of NAT : i <= n }
then (q ^ <*<*0,n*>*>) . j = <*0,n*> by A1, FINSEQ_1:42
.= <*0,(n -' 0)*> by NAT_D:40 ;
hence x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } by A22; ::_thesis: verum
end;
end;
end;
hence x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } or x in rng (q ^ <*<*0,n*>*>) )
assume x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } ; ::_thesis: x in rng (q ^ <*<*0,n*>*>)
then consider i being Element of NAT such that
A26: x = <*i,(n -' i)*> and
A27: i <= n ;
A28: ( i = 0 or i >= 0 + 1 ) by NAT_1:13;
now__::_thesis:_x_in_rng_(q_^_<*<*0,n*>*>)
percases ( i = 0 or i in Seg n ) by A27, A28, FINSEQ_1:1;
supposeA29: i = 0 ; ::_thesis: x in rng (q ^ <*<*0,n*>*>)
A30: n + 1 in dom (q ^ <*<*0,n*>*>) by A6, FINSEQ_1:4;
(q ^ <*<*0,n*>*>) . (n + 1) = <*0,n*> by A1, FINSEQ_1:42
.= x by A26, A29, NAT_D:40 ;
hence x in rng (q ^ <*<*0,n*>*>) by A30, FUNCT_1:def_3; ::_thesis: verum
end;
supposeA31: i in Seg n ; ::_thesis: x in rng (q ^ <*<*0,n*>*>)
then q . i = x by A2, A4, A26;
then x in rng q by A3, A31, FUNCT_1:def_3;
hence x in rng (q ^ <*<*0,n*>*>) by A19; ::_thesis: verum
end;
end;
end;
hence x in rng (q ^ <*<*0,n*>*>) ; ::_thesis: verum
end;
consider A being finite Subset of (2 -tuples_on NAT) such that
A32: Decomp (n,2) = SgmX ((TuplesOrder 2),A) and
A33: for p being Element of 2 -tuples_on NAT holds
( p in A iff Sum p = n ) by Def4;
A34: A = { <*i,(n -' i)*> where i is Element of NAT : i <= n }
proof
thus A c= { <*i,(n -' i)*> where i is Element of NAT : i <= n } :: according to XBOOLE_0:def_10 ::_thesis: { <*i,(n -' i)*> where i is Element of NAT : i <= n } c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } )
assume A35: x in A ; ::_thesis: x in { <*i,(n -' i)*> where i is Element of NAT : i <= n }
then reconsider p = x as Element of 2 -tuples_on NAT ;
consider d1, d2 being Element of NAT such that
A36: p = <*d1,d2*> by FINSEQ_2:100;
A37: d1 + d2 = Sum p by A36, RVSUM_1:77
.= n by A33, A35 ;
then n - d1 >= 0 ;
then A38: d2 = n -' d1 by A37, XREAL_0:def_2;
d1 <= n by A37, NAT_1:11;
hence x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } by A36, A38; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } or x in A )
assume x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } ; ::_thesis: x in A
then consider i being Element of NAT such that
A39: x = <*i,(n -' i)*> and
A40: i <= n ;
A41: n - i >= 0 by A40, XREAL_1:48;
Sum <*i,(n -' i)*> = i + (n -' i) by RVSUM_1:77
.= i + (n - i) by A41, XREAL_0:def_2
.= n ;
hence x in A by A33, A39; ::_thesis: verum
end;
field (TuplesOrder 2) = 2 -tuples_on NAT by ORDERS_1:15;
then TuplesOrder 2 linearly_orders 2 -tuples_on NAT by ORDERS_1:37;
hence len (Decomp (n,2)) = n + 1 by A32, A34, A20, A18, ORDERS_1:38, PRE_POLY:11; ::_thesis: verum
end;
theorem :: POLYNOM3:10
for n being Element of NAT holds Decomp (n,1) = <*<*n*>*>
proof
let n be Element of NAT ; ::_thesis: Decomp (n,1) = <*<*n*>*>
consider A being finite Subset of (1 -tuples_on NAT) such that
A1: Decomp (n,1) = SgmX ((TuplesOrder 1),A) and
A2: for p being Element of 1 -tuples_on NAT holds
( p in A iff Sum p = n ) by Def4;
A3: A = {<*n*>}
proof
thus A c= {<*n*>} :: according to XBOOLE_0:def_10 ::_thesis: {<*n*>} c= A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in A or y in {<*n*>} )
assume A4: y in A ; ::_thesis: y in {<*n*>}
then reconsider p = y as Element of 1 -tuples_on NAT ;
A5: Sum p = n by A2, A4;
consider k being Element of NAT such that
A6: p = <*k*> by FINSEQ_2:97;
Sum p = k by A6, RVSUM_1:73;
hence y in {<*n*>} by A5, A6, TARSKI:def_1; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {<*n*>} or y in A )
assume y in {<*n*>} ; ::_thesis: y in A
then A7: y = <*n*> by TARSKI:def_1;
A8: <*n*> is Element of 1 -tuples_on NAT by FINSEQ_2:131;
Sum <*n*> = n by RVSUM_1:73;
hence y in A by A2, A7, A8; ::_thesis: verum
end;
len (Decomp (n,1)) = 1 by Th8;
then A9: dom (Decomp (n,1)) = Seg 1 by FINSEQ_1:def_3
.= dom <*<*n*>*> by FINSEQ_1:38 ;
field (TuplesOrder 1) = 1 -tuples_on NAT by ORDERS_1:15;
then TuplesOrder 1 linearly_orders A by ORDERS_1:37, ORDERS_1:38;
then ( rng <*<*n*>*> = {<*n*>} & rng (Decomp (n,1)) = {<*n*>} ) by A1, A3, FINSEQ_1:39, PRE_POLY:def_2;
hence Decomp (n,1) = <*<*n*>*> by A9, FUNCT_1:7; ::_thesis: verum
end;
theorem Th11: :: POLYNOM3:11
for i, j, n, k1, k2 being Element of NAT st (Decomp (n,2)) . i = <*k1,(n -' k1)*> & (Decomp (n,2)) . j = <*k2,(n -' k2)*> holds
( i < j iff k1 < k2 )
proof
let i, j, n, k1, k2 be Element of NAT ; ::_thesis: ( (Decomp (n,2)) . i = <*k1,(n -' k1)*> & (Decomp (n,2)) . j = <*k2,(n -' k2)*> implies ( i < j iff k1 < k2 ) )
assume that
A1: (Decomp (n,2)) . i = <*k1,(n -' k1)*> and
A2: (Decomp (n,2)) . j = <*k2,(n -' k2)*> ; ::_thesis: ( i < j iff k1 < k2 )
A3: j in dom (Decomp (n,2)) by A2, FUNCT_1:def_2;
then A4: (Decomp (n,2)) . j = (Decomp (n,2)) /. j by PARTFUN1:def_6;
consider A being finite Subset of (2 -tuples_on NAT) such that
A5: Decomp (n,2) = SgmX ((TuplesOrder 2),A) and
for p being Element of 2 -tuples_on NAT holds
( p in A iff Sum p = n ) by Def4;
field (TuplesOrder 2) = 2 -tuples_on NAT by ORDERS_1:15;
then A6: TuplesOrder 2 linearly_orders A by ORDERS_1:37, ORDERS_1:38;
A7: i in dom (Decomp (n,2)) by A1, FUNCT_1:def_2;
then A8: (Decomp (n,2)) . i = (Decomp (n,2)) /. i by PARTFUN1:def_6;
thus ( i < j implies k1 < k2 ) ::_thesis: ( k1 < k2 implies i < j )
proof
assume A9: i < j ; ::_thesis: k1 < k2
then [<*k1,(n -' k1)*>,<*k2,(n -' k2)*>] in TuplesOrder 2 by A5, A6, A1, A2, A7, A3, A8, A4, PRE_POLY:def_2;
then A10: <*k1,(n -' k1)*> <= <*k2,(n -' k2)*> by Def3;
<*k1,(n -' k1)*> <> <*k2,(n -' k2)*> by A5, A6, A1, A2, A7, A3, A8, A4, A9, PRE_POLY:def_2;
then <*k1,(n -' k1)*> < <*k2,(n -' k2)*> by A10, Def2;
then consider t being Element of NAT such that
A11: t in Seg 2 and
A12: <*k1,(n -' k1)*> . t < <*k2,(n -' k2)*> . t and
A13: for k being Element of NAT st 1 <= k & k < t holds
<*k1,(n -' k1)*> . k = <*k2,(n -' k2)*> . k by Def1;
percases ( t = 1 or t = 2 ) by A11, FINSEQ_1:2, TARSKI:def_2;
supposeA14: t = 1 ; ::_thesis: k1 < k2
then <*k1,(n -' k1)*> . t = k1 by FINSEQ_1:44;
hence k1 < k2 by A12, A14, FINSEQ_1:44; ::_thesis: verum
end;
suppose t = 2 ; ::_thesis: k1 < k2
then <*k1,(n -' k1)*> . 1 = <*k2,(n -' k2)*> . 1 by A13;
then <*k1,(n -' k1)*> . 1 = k2 by FINSEQ_1:44;
then k1 = k2 by FINSEQ_1:44;
hence k1 < k2 by A12; ::_thesis: verum
end;
end;
end;
assume A15: k1 < k2 ; ::_thesis: i < j
A16: for k being Element of NAT st 1 <= k & k < 1 holds
<*k1,(n -' k1)*> . k = <*k2,(n -' k2)*> . k ;
A17: <*k1,(n -' k1)*> . 1 = k1 by FINSEQ_1:44;
( 1 in Seg 2 & <*k2,(n -' k2)*> . 1 = k2 ) by FINSEQ_1:1, FINSEQ_1:44;
then A18: <*k1,(n -' k1)*> < <*k2,(n -' k2)*> by A15, A17, A16, Def1;
assume A19: i >= j ; ::_thesis: contradiction
percases ( i = j or j < i ) by A19, XXREAL_0:1;
suppose i = j ; ::_thesis: contradiction
hence contradiction by A1, A2, A15, A17, FINSEQ_1:44; ::_thesis: verum
end;
supposeA20: j < i ; ::_thesis: contradiction
then [<*k2,(n -' k2)*>,<*k1,(n -' k1)*>] in TuplesOrder 2 by A5, A6, A1, A2, A7, A3, A8, A4, PRE_POLY:def_2;
then A21: <*k2,(n -' k2)*> <= <*k1,(n -' k1)*> by Def3;
<*k2,(n -' k2)*> <> <*k1,(n -' k1)*> by A5, A6, A1, A2, A7, A3, A8, A4, A20, PRE_POLY:def_2;
hence contradiction by A18, A21, Def2; ::_thesis: verum
end;
end;
end;
theorem Th12: :: POLYNOM3:12
for i, n, k1, k2 being Element of NAT st (Decomp (n,2)) . i = <*k1,(n -' k1)*> & (Decomp (n,2)) . (i + 1) = <*k2,(n -' k2)*> holds
k2 = k1 + 1
proof
let i, n, k1, k2 be Element of NAT ; ::_thesis: ( (Decomp (n,2)) . i = <*k1,(n -' k1)*> & (Decomp (n,2)) . (i + 1) = <*k2,(n -' k2)*> implies k2 = k1 + 1 )
assume that
A1: (Decomp (n,2)) . i = <*k1,(n -' k1)*> and
A2: (Decomp (n,2)) . (i + 1) = <*k2,(n -' k2)*> ; ::_thesis: k2 = k1 + 1
assume A3: k2 <> k1 + 1 ; ::_thesis: contradiction
i + 0 < i + 1 by XREAL_1:6;
then A4: k1 < k2 by A1, A2, Th11;
then k1 + 1 <= k2 by NAT_1:13;
then A5: k1 + 1 < k2 by A3, XXREAL_0:1;
consider A being finite Subset of (2 -tuples_on NAT) such that
A6: Decomp (n,2) = SgmX ((TuplesOrder 2),A) and
A7: for p being Element of 2 -tuples_on NAT holds
( p in A iff Sum p = n ) by Def4;
field (TuplesOrder 2) = 2 -tuples_on NAT by ORDERS_1:15;
then TuplesOrder 2 linearly_orders A by ORDERS_1:37, ORDERS_1:38;
then A8: rng (Decomp (n,2)) = A by A6, PRE_POLY:def_2;
k1 < n
proof
Sum <*k2,(n -' k2)*> = k2 + (n -' k2) by RVSUM_1:77;
then A9: Sum <*k2,(n -' k2)*> >= k2 by NAT_1:11;
assume k1 >= n ; ::_thesis: contradiction
then k2 > n by A4, XXREAL_0:2;
then not (Decomp (n,2)) . (i + 1) in rng (Decomp (n,2)) by A7, A8, A2, A9;
then not i + 1 in dom (Decomp (n,2)) by FUNCT_1:def_3;
hence contradiction by A2, FUNCT_1:def_2; ::_thesis: verum
end;
then A10: k1 + 1 <= n by NAT_1:13;
Sum <*(k1 + 1),(n -' (k1 + 1))*> = (k1 + 1) + (n -' (k1 + 1)) by RVSUM_1:77
.= n by A10, XREAL_1:235 ;
then <*(k1 + 1),(n -' (k1 + 1))*> in rng (Decomp (n,2)) by A7, A8;
then consider k being Nat such that
k in dom (Decomp (n,2)) and
A11: (Decomp (n,2)) . k = <*(k1 + 1),(n -' (k1 + 1))*> by FINSEQ_2:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
k1 + 0 < k1 + 1 by XREAL_1:6;
then i < k by A1, A11, Th11;
then i + 1 <= k by NAT_1:13;
hence contradiction by A2, A5, A11, Th11; ::_thesis: verum
end;
theorem Th13: :: POLYNOM3:13
for n being Element of NAT holds (Decomp (n,2)) . 1 = <*0,n*>
proof
let n be Element of NAT ; ::_thesis: (Decomp (n,2)) . 1 = <*0,n*>
consider A being finite Subset of (2 -tuples_on NAT) such that
A1: Decomp (n,2) = SgmX ((TuplesOrder 2),A) and
A2: for p being Element of 2 -tuples_on NAT holds
( p in A iff Sum p = n ) by Def4;
A3: now__::_thesis:_for_y_being_Element_of_2_-tuples_on_NAT_st_y_in_A_holds_
[<*0,n*>,y]_in_TuplesOrder_2
let y be Element of 2 -tuples_on NAT; ::_thesis: ( y in A implies [<*0,n*>,y] in TuplesOrder 2 )
consider d1, d2 being Element of NAT such that
A4: y = <*d1,d2*> by FINSEQ_2:100;
assume y in A ; ::_thesis: [<*0,n*>,y] in TuplesOrder 2
then Sum <*d1,d2*> = n by A2, A4;
then A5: d1 + d2 = n by RVSUM_1:77;
now__::_thesis:_<*0,n*>_<=_<*d1,d2*>
percases ( d1 = 0 or d1 > 0 ) ;
suppose d1 = 0 ; ::_thesis: <*0,n*> <= <*d1,d2*>
hence <*0,n*> <= <*d1,d2*> by A5; ::_thesis: verum
end;
suppose d1 > 0 ; ::_thesis: <*0,n*> <= <*d1,d2*>
then <*0,n*> . 1 < d1 by FINSEQ_1:44;
then A6: <*0,n*> . 1 < <*d1,d2*> . 1 by FINSEQ_1:44;
( 1 in Seg 2 & ( for k being Element of NAT st 1 <= k & k < 1 holds
<*0,n*> . k = <*d1,d2*> . k ) ) by FINSEQ_1:1;
then <*0,n*> < <*d1,d2*> by A6, Def1;
hence <*0,n*> <= <*d1,d2*> by Def2; ::_thesis: verum
end;
end;
end;
hence [<*0,n*>,y] in TuplesOrder 2 by A4, Def3; ::_thesis: verum
end;
1 <= n + 1 by NAT_1:11;
then 1 in Seg (n + 1) by FINSEQ_1:1;
then 1 in Seg (len (Decomp (n,2))) by Th9;
then A7: 1 in dom (Decomp (n,2)) by FINSEQ_1:def_3;
field (TuplesOrder 2) = 2 -tuples_on NAT by ORDERS_1:15;
then A8: TuplesOrder 2 linearly_orders A by ORDERS_1:37, ORDERS_1:38;
Sum <*0,n*> = 0 + n by RVSUM_1:77;
then <*0,n*> in A by A2;
then (SgmX ((TuplesOrder 2),A)) /. 1 = <*0,n*> by A8, A3, PRE_POLY:20;
hence (Decomp (n,2)) . 1 = <*0,n*> by A1, A7, PARTFUN1:def_6; ::_thesis: verum
end;
theorem Th14: :: POLYNOM3:14
for n, i being Element of NAT st i in Seg (n + 1) holds
(Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*>
proof
let n, i be Element of NAT ; ::_thesis: ( i in Seg (n + 1) implies (Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*> )
defpred S1[ Nat] means ( $1 <= n + 1 implies (Decomp (n,2)) . $1 = <*($1 -' 1),((n + 1) -' $1)*> );
assume i in Seg (n + 1) ; ::_thesis: (Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*>
then A1: ( 1 <= i & i <= n + 1 ) by FINSEQ_1:1;
consider A being finite Subset of (2 -tuples_on NAT) such that
A2: Decomp (n,2) = SgmX ((TuplesOrder 2),A) and
A3: for p being Element of 2 -tuples_on NAT holds
( p in A iff Sum p = n ) by Def4;
A4: for j being non empty Nat st S1[j] holds
S1[j + 1]
proof
field (TuplesOrder 2) = 2 -tuples_on NAT by ORDERS_1:15;
then A5: TuplesOrder 2 linearly_orders A by ORDERS_1:37, ORDERS_1:38;
let j be non empty Nat; ::_thesis: ( S1[j] implies S1[j + 1] )
assume that
A6: ( j <= n + 1 implies (Decomp (n,2)) . j = <*(j -' 1),((n + 1) -' j)*> ) and
A7: j + 1 <= n + 1 ; ::_thesis: (Decomp (n,2)) . (j + 1) = <*((j + 1) -' 1),((n + 1) -' (j + 1))*>
n >= j by A7, XREAL_1:6;
then A8: n - j >= 0 by XREAL_1:48;
(n + 1) - (j + 1) >= 0 by A7, XREAL_1:48;
then A9: (n + 1) -' (j + 1) = n - j by XREAL_0:def_2
.= n -' j by A8, XREAL_0:def_2 ;
reconsider jj = j as non empty Element of NAT by ORDINAL1:def_12;
j >= 1 by NAT_1:14;
then A10: j - 1 >= 1 - 1 by XREAL_1:9;
j + 1 >= 1 by NAT_1:11;
then j + 1 in Seg (n + 1) by A7, FINSEQ_1:1;
then j + 1 in Seg (len (Decomp (n,2))) by Th9;
then A11: j + 1 in dom (Decomp (n,2)) by FINSEQ_1:def_3;
then (Decomp (n,2)) . (j + 1) = (Decomp (n,2)) /. (j + 1) by PARTFUN1:def_6;
then consider d1, d2 being Element of NAT such that
A12: (Decomp (n,2)) . (j + 1) = <*d1,d2*> by FINSEQ_2:100;
(Decomp (n,2)) . (j + 1) in rng (Decomp (n,2)) by A11, FUNCT_1:def_3;
then (Decomp (n,2)) . (j + 1) in A by A2, A5, PRE_POLY:def_2;
then Sum <*d1,d2*> = n by A3, A12;
then A13: d1 + d2 = n by RVSUM_1:77;
then n - d1 >= 0 ;
then A14: d2 = n -' d1 by A13, XREAL_0:def_2;
j < n + 1 by A7, NAT_1:13;
then A15: (n + 1) - j >= 0 by XREAL_1:48;
then n - (j - 1) >= 0 ;
then A16: n - (j -' 1) >= 0 by A10, XREAL_0:def_2;
(n + 1) -' j = n - (j - 1) by A15, XREAL_0:def_2
.= n - (j -' 1) by A10, XREAL_0:def_2
.= n -' (j -' 1) by A16, XREAL_0:def_2 ;
then d1 = (jj -' 1) + 1 by A6, A7, A12, A14, Th12, NAT_1:13
.= j by NAT_1:14, XREAL_1:235 ;
hence (Decomp (n,2)) . (j + 1) = <*((j + 1) -' 1),((n + 1) -' (j + 1))*> by A12, A14, A9, NAT_D:34; ::_thesis: verum
end;
A17: S1[1]
proof
assume 1 <= n + 1 ; ::_thesis: (Decomp (n,2)) . 1 = <*(1 -' 1),((n + 1) -' 1)*>
thus (Decomp (n,2)) . 1 = <*0,n*> by Th13
.= <*(1 -' 1),n*> by XREAL_1:232
.= <*(1 -' 1),((n + 1) -' 1)*> by NAT_D:34 ; ::_thesis: verum
end;
for j being non empty Nat holds S1[j] from NAT_1:sch_10(A17, A4);
hence (Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*> by A1; ::_thesis: verum
end;
definition
let L be non empty multMagma ;
let p, q, r be sequence of L;
let t be FinSequence of 3 -tuples_on NAT;
func prodTuples (p,q,r,t) -> Element of the carrier of L * means :Def5: :: POLYNOM3:def 5
( len it = len t & ( for k being Element of NAT st k in dom t holds
it . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) );
existence
ex b1 being Element of the carrier of L * st
( len b1 = len t & ( for k being Element of NAT st k in dom t holds
b1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) )
proof
deffunc H1( Nat) -> Element of the carrier of L = ((p . ((t /. $1) /. 1)) * (q . ((t /. $1) /. 2))) * (r . ((t /. $1) /. 3));
consider p1 being FinSequence of the carrier of L such that
A1: len p1 = len t and
A2: for k being Nat st k in dom p1 holds
p1 . k = H1(k) from FINSEQ_2:sch_1();
A3: dom p1 = Seg (len t) by A1, FINSEQ_1:def_3;
reconsider p1 = p1 as Element of the carrier of L * by FINSEQ_1:def_11;
take p1 ; ::_thesis: ( len p1 = len t & ( for k being Element of NAT st k in dom t holds
p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) )
thus len p1 = len t by A1; ::_thesis: for k being Element of NAT st k in dom t holds
p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3))
let k be Element of NAT ; ::_thesis: ( k in dom t implies p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) )
assume k in dom t ; ::_thesis: p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3))
then k in Seg (len t) by FINSEQ_1:def_3;
hence p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) by A2, A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of the carrier of L * st len b1 = len t & ( for k being Element of NAT st k in dom t holds
b1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) & len b2 = len t & ( for k being Element of NAT st k in dom t holds
b2 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) holds
b1 = b2
proof
let p1, p2 be Element of the carrier of L * ; ::_thesis: ( len p1 = len t & ( for k being Element of NAT st k in dom t holds
p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) & len p2 = len t & ( for k being Element of NAT st k in dom t holds
p2 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) implies p1 = p2 )
assume that
A4: len p1 = len t and
A5: for k being Element of NAT st k in dom t holds
p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) and
A6: len p2 = len t and
A7: for k being Element of NAT st k in dom t holds
p2 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ; ::_thesis: p1 = p2
A8: dom p1 = Seg (len t) by A4, FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_p1_holds_
p1_._i_=_p2_._i
let i be Nat; ::_thesis: ( i in dom p1 implies p1 . i = p2 . i )
assume i in dom p1 ; ::_thesis: p1 . i = p2 . i
then A9: i in dom t by A8, FINSEQ_1:def_3;
hence p1 . i = ((p . ((t /. i) /. 1)) * (q . ((t /. i) /. 2))) * (r . ((t /. i) /. 3)) by A5
.= p2 . i by A7, A9 ;
::_thesis: verum
end;
hence p1 = p2 by A4, A6, FINSEQ_2:9; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines prodTuples POLYNOM3:def_5_:_
for L being non empty multMagma
for p, q, r being sequence of L
for t being FinSequence of 3 -tuples_on NAT
for b6 being Element of the carrier of L * holds
( b6 = prodTuples (p,q,r,t) iff ( len b6 = len t & ( for k being Element of NAT st k in dom t holds
b6 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) ) );
theorem Th15: :: POLYNOM3:15
for L being non empty multMagma
for p, q, r being sequence of L
for t being FinSequence of 3 -tuples_on NAT
for P being Permutation of (dom t)
for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds
prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P
proof
let L be non empty multMagma ; ::_thesis: for p, q, r being sequence of L
for t being FinSequence of 3 -tuples_on NAT
for P being Permutation of (dom t)
for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds
prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P
let p, q, r be sequence of L; ::_thesis: for t being FinSequence of 3 -tuples_on NAT
for P being Permutation of (dom t)
for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds
prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P
let t be FinSequence of 3 -tuples_on NAT; ::_thesis: for P being Permutation of (dom t)
for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds
prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P
let P be Permutation of (dom t); ::_thesis: for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds
prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P
let t1 be FinSequence of 3 -tuples_on NAT; ::_thesis: ( t1 = t * P implies prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P )
A1: rng P = dom t by FUNCT_2:def_3;
assume A2: t1 = t * P ; ::_thesis: prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P
then A3: dom P = dom t1 by A1, RELAT_1:27;
A4: now__::_thesis:_for_x_being_set_st_x_in_dom_t1_holds_
(prodTuples_(p,q,r,t1))_._x_=_((prodTuples_(p,q,r,t))_*_P)_._x
let x be set ; ::_thesis: ( x in dom t1 implies (prodTuples (p,q,r,t1)) . x = ((prodTuples (p,q,r,t)) * P) . x )
assume A5: x in dom t1 ; ::_thesis: (prodTuples (p,q,r,t1)) . x = ((prodTuples (p,q,r,t)) * P) . x
then reconsider i = x as Element of NAT ;
A6: ( (prodTuples (p,q,r,t1)) . i = ((p . ((t1 /. i) /. 1)) * (q . ((t1 /. i) /. 2))) * (r . ((t1 /. i) /. 3)) & ((prodTuples (p,q,r,t)) * P) . x = (prodTuples (p,q,r,t)) . (P . x) ) by A3, A5, Def5, FUNCT_1:13;
reconsider j = P . i as Element of NAT ;
A7: P . i in rng P by A3, A5, FUNCT_1:def_3;
t1 /. i = t1 . i by A5, PARTFUN1:def_6
.= t . (P . i) by A2, A5, FUNCT_1:12
.= t /. j by A1, A7, PARTFUN1:def_6 ;
hence (prodTuples (p,q,r,t1)) . x = ((prodTuples (p,q,r,t)) * P) . x by A1, A7, A6, Def5; ::_thesis: verum
end;
len (prodTuples (p,q,r,t1)) = len t1 by Def5;
then A8: dom (prodTuples (p,q,r,t1)) = Seg (len t1) by FINSEQ_1:def_3;
len (prodTuples (p,q,r,t)) = len t by Def5;
then rng P = dom (prodTuples (p,q,r,t)) by A1, FINSEQ_3:29;
then A9: dom ((prodTuples (p,q,r,t)) * P) = dom t1 by A3, RELAT_1:27;
dom t1 = Seg (len t1) by FINSEQ_1:def_3;
hence prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P by A8, A9, A4, FUNCT_1:2; ::_thesis: verum
end;
theorem Th16: :: POLYNOM3:16
for D being set
for f being FinSequence of D *
for i being Element of NAT holds Card (f | i) = (Card f) | i
proof
let D be set ; ::_thesis: for f being FinSequence of D *
for i being Element of NAT holds Card (f | i) = (Card f) | i
let f be FinSequence of D * ; ::_thesis: for i being Element of NAT holds Card (f | i) = (Card f) | i
let i be Element of NAT ; ::_thesis: Card (f | i) = (Card f) | i
A1: f | i = f | (Seg i) by FINSEQ_1:def_15;
reconsider k = min (i,(len f)) as Element of NAT ;
dom (Card (f | i)) = dom (f | i) by CARD_3:def_2;
then A2: len (Card (f | i)) = len (f | i) by FINSEQ_3:29
.= min (i,(len f)) by A1, FINSEQ_2:21 ;
then A3: dom (Card (f | i)) = Seg k by FINSEQ_1:def_3;
A4: dom (Card f) = dom f by CARD_3:def_2;
A5: (Card f) | i = (Card f) | (Seg i) by FINSEQ_1:def_15;
A6: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(Card_(f_|_i))_holds_
(Card_(f_|_i))_._j_=_((Card_f)_|_i)_._j
A7: len f = len (Card f) by A4, FINSEQ_3:29;
let j be Nat; ::_thesis: ( j in dom (Card (f | i)) implies (Card (f | i)) . b1 = ((Card f) | i) . b1 )
assume A8: j in dom (Card (f | i)) ; ::_thesis: (Card (f | i)) . b1 = ((Card f) | i) . b1
percases ( i <= len f or i > len f ) ;
supposeA9: i <= len f ; ::_thesis: (Card (f | i)) . b1 = ((Card f) | i) . b1
A10: 1 <= j by A3, A8, FINSEQ_1:1;
A11: k = i by A9, XXREAL_0:def_9;
then j <= i by A3, A8, FINSEQ_1:1;
then j <= len f by A9, XXREAL_0:2;
then A12: j in dom f by A10, FINSEQ_3:25;
len ((Card f) | i) = i by A7, A9, FINSEQ_1:59;
then A13: dom ((Card f) | i) = Seg i by FINSEQ_1:def_3;
reconsider Cf = Card f as FinSequence of NAT ;
A14: Seg (len (f | i)) = dom (f | i) by FINSEQ_1:def_3;
A15: len (f | i) = i by A9, FINSEQ_1:59;
hence (Card (f | i)) . j = card ((f | i) . j) by A3, A8, A11, A14, CARD_3:def_2
.= card ((f | i) /. j) by A3, A8, A11, A15, A14, PARTFUN1:def_6
.= card (f /. j) by A3, A8, A11, A15, A14, FINSEQ_4:70
.= card (f . j) by A12, PARTFUN1:def_6
.= (Card f) . j by A12, CARD_3:def_2
.= Cf /. j by A4, A12, PARTFUN1:def_6
.= (Cf | i) /. j by A3, A8, A11, A13, FINSEQ_4:70
.= ((Card f) | i) . j by A3, A8, A11, A13, PARTFUN1:def_6 ;
::_thesis: verum
end;
supposeA16: i > len f ; ::_thesis: (Card (f | i)) . b1 = ((Card f) | i) . b1
then f | i = f by A1, FINSEQ_2:20;
hence (Card (f | i)) . j = ((Card f) | i) . j by A5, A7, A16, FINSEQ_2:20; ::_thesis: verum
end;
end;
end;
len ((Card f) | i) = min (i,(len (Card f))) by A5, FINSEQ_2:21
.= min (i,(len f)) by A4, FINSEQ_3:29 ;
hence Card (f | i) = (Card f) | i by A2, A6, FINSEQ_2:9; ::_thesis: verum
end;
theorem :: POLYNOM3:17
for p being FinSequence of REAL
for q being FinSequence of NAT st p = q holds
for i being Element of NAT holds p | i = q | i ;
theorem Th18: :: POLYNOM3:18
for p being FinSequence of NAT
for i, j being Element of NAT st i <= j holds
Sum (p | i) <= Sum (p | j)
proof
let p be FinSequence of NAT ; ::_thesis: for i, j being Element of NAT st i <= j holds
Sum (p | i) <= Sum (p | j)
let i, j be Element of NAT ; ::_thesis: ( i <= j implies Sum (p | i) <= Sum (p | j) )
assume A1: i <= j ; ::_thesis: Sum (p | i) <= Sum (p | j)
then consider k being Nat such that
A2: j = i + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
percases ( j <= len p or j > len p ) ;
supposeA3: j <= len p ; ::_thesis: Sum (p | i) <= Sum (p | j)
then A4: len (p | j) = i + k by A2, FINSEQ_1:59;
then consider q, r being FinSequence of NAT such that
A5: len q = i and
len r = k and
A6: p | j = q ^ r by FINSEQ_2:23;
A7: len (p | i) = i by A1, A3, FINSEQ_1:59, XXREAL_0:2;
then A8: dom (p | i) = Seg i by FINSEQ_1:def_3;
A9: now__::_thesis:_for_n_being_Nat_st_n_in_dom_(p_|_i)_holds_
(p_|_i)_._n_=_q_._n
reconsider p1 = p as FinSequence of REAL ;
let n be Nat; ::_thesis: ( n in dom (p | i) implies (p | i) . n = q . n )
assume A10: n in dom (p | i) ; ::_thesis: (p | i) . n = q . n
then A11: (p1 | i) /. n = p /. n by FINSEQ_4:70;
A12: Seg i = dom q by A5, FINSEQ_1:def_3;
A13: ( Seg i c= Seg j & Seg j = dom (p | j) ) by A1, A2, A4, FINSEQ_1:5, FINSEQ_1:def_3;
Seg i = dom (p | i) by A7, FINSEQ_1:def_3;
then A14: (p1 | j) /. n = p /. n by A10, A13, FINSEQ_4:70;
thus (p | i) . n = (p1 | i) /. n by A10, PARTFUN1:def_6
.= (p | j) . n by A8, A10, A13, A11, A14, PARTFUN1:def_6
.= q . n by A6, A8, A10, A12, FINSEQ_1:def_7 ; ::_thesis: verum
end;
A15: (Sum q) + (Sum r) >= (Sum q) + 0 by XREAL_1:6;
Sum (p | j) = (Sum q) + (Sum r) by A6, RVSUM_1:75;
hence Sum (p | i) <= Sum (p | j) by A7, A5, A9, A15, FINSEQ_2:9; ::_thesis: verum
end;
suppose j > len p ; ::_thesis: Sum (p | i) <= Sum (p | j)
then A16: p | j = p by FINSEQ_1:58;
now__::_thesis:_Sum_(p_|_i)_<=_Sum_(p_|_j)
percases ( i >= len p or i < len p ) ;
suppose i >= len p ; ::_thesis: Sum (p | i) <= Sum (p | j)
hence Sum (p | i) <= Sum (p | j) by A16, FINSEQ_1:58; ::_thesis: verum
end;
supposeA17: i < len p ; ::_thesis: Sum (p | i) <= Sum (p | j)
then consider t being Nat such that
A18: len p = i + t by NAT_1:10;
consider q, r being FinSequence of NAT such that
A19: len q = i and
len r = t and
A20: p = q ^ r by A18, FINSEQ_2:23;
A21: len (p | i) = i by A17, FINSEQ_1:59;
then A22: dom (p | i) = Seg i by FINSEQ_1:def_3;
A23: now__::_thesis:_for_n_being_Nat_st_n_in_dom_(p_|_i)_holds_
(p_|_i)_._n_=_q_._n
A24: Seg i = dom q by A19, FINSEQ_1:def_3;
reconsider p1 = p as FinSequence of REAL ;
let n be Nat; ::_thesis: ( n in dom (p | i) implies (p | i) . n = q . n )
A25: dom (p | i) c= dom p by FINSEQ_5:18;
assume A26: n in dom (p | i) ; ::_thesis: (p | i) . n = q . n
then A27: (p1 | i) /. n = p /. n by FINSEQ_4:70;
thus (p | i) . n = (p1 | i) /. n by A26, PARTFUN1:def_6
.= p . n by A26, A27, A25, PARTFUN1:def_6
.= q . n by A20, A22, A26, A24, FINSEQ_1:def_7 ; ::_thesis: verum
end;
A28: (Sum q) + (Sum r) >= (Sum q) + 0 by XREAL_1:6;
Sum p = (Sum q) + (Sum r) by A20, RVSUM_1:75;
hence Sum (p | i) <= Sum (p | j) by A16, A19, A21, A23, A28, FINSEQ_2:9; ::_thesis: verum
end;
end;
end;
hence Sum (p | i) <= Sum (p | j) ; ::_thesis: verum
end;
end;
end;
theorem :: POLYNOM3:19
for D being set
for p being FinSequence of D
for i being Element of NAT st i < len p holds
p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> by FINSEQ_5:83;
theorem Th20: :: POLYNOM3:20
for p being FinSequence of REAL
for i being Element of NAT st i < len p holds
Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1))
proof
let p be FinSequence of REAL ; ::_thesis: for i being Element of NAT st i < len p holds
Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1))
let i be Element of NAT ; ::_thesis: ( i < len p implies Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1)) )
assume i < len p ; ::_thesis: Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1))
then p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> by FINSEQ_5:83;
hence Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1)) by RVSUM_1:74; ::_thesis: verum
end;
theorem Th21: :: POLYNOM3:21
for p being FinSequence of NAT
for i, j, k1, k2 being Element of NAT st i < len p & j < len p & 1 <= k1 & 1 <= k2 & k1 <= p . (i + 1) & k2 <= p . (j + 1) & (Sum (p | i)) + k1 = (Sum (p | j)) + k2 holds
( i = j & k1 = k2 )
proof
let p be FinSequence of NAT ; ::_thesis: for i, j, k1, k2 being Element of NAT st i < len p & j < len p & 1 <= k1 & 1 <= k2 & k1 <= p . (i + 1) & k2 <= p . (j + 1) & (Sum (p | i)) + k1 = (Sum (p | j)) + k2 holds
( i = j & k1 = k2 )
let i, j, k1, k2 be Element of NAT ; ::_thesis: ( i < len p & j < len p & 1 <= k1 & 1 <= k2 & k1 <= p . (i + 1) & k2 <= p . (j + 1) & (Sum (p | i)) + k1 = (Sum (p | j)) + k2 implies ( i = j & k1 = k2 ) )
assume that
A1: i < len p and
A2: j < len p and
A3: 1 <= k1 and
A4: 1 <= k2 and
A5: k1 <= p . (i + 1) and
A6: k2 <= p . (j + 1) and
A7: (Sum (p | i)) + k1 = (Sum (p | j)) + k2 and
A8: ( i <> j or k1 <> k2 ) ; ::_thesis: contradiction
A9: i <> j by A7, A8, XCMPLX_1:2;
reconsider p1 = p as FinSequence of REAL ;
A10: (Sum (p1 | i)) + (p . (i + 1)) >= (Sum (p | i)) + k1 by A5, XREAL_1:6;
A11: (Sum (p1 | j)) + (p . (j + 1)) >= (Sum (p | j)) + k2 by A6, XREAL_1:6;
percases ( i < j or i >= j ) ;
suppose i < j ; ::_thesis: contradiction
then i + 1 <= j by NAT_1:13;
then Sum (p | j) >= Sum (p1 | (i + 1)) by Th18;
then Sum (p | j) >= (Sum (p1 | i)) + (p . (i + 1)) by A1, Th20;
then A12: Sum (p | j) >= (Sum (p | j)) + k2 by A7, A10, XXREAL_0:2;
(Sum (p | j)) + k2 >= Sum (p | j) by NAT_1:11;
then Sum (p | j) = (Sum (p | j)) + k2 by A12, XXREAL_0:1;
then k2 = 0 ;
hence contradiction by A4; ::_thesis: verum
end;
suppose i >= j ; ::_thesis: contradiction
then j < i by A9, XXREAL_0:1;
then j + 1 <= i by NAT_1:13;
then Sum (p | i) >= Sum (p1 | (j + 1)) by Th18;
then Sum (p | i) >= (Sum (p1 | j)) + (p . (j + 1)) by A2, Th20;
then A13: Sum (p | i) >= (Sum (p | i)) + k1 by A7, A11, XXREAL_0:2;
(Sum (p | i)) + k1 >= Sum (p | i) by NAT_1:11;
then Sum (p | i) = (Sum (p | i)) + k1 by A13, XXREAL_0:1;
then k1 = 0 ;
hence contradiction by A3; ::_thesis: verum
end;
end;
end;
theorem Th22: :: POLYNOM3:22
for D1, D2 being set
for f1 being FinSequence of D1 *
for f2 being FinSequence of D2 *
for i1, i2, j1, j2 being Element of NAT st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds
( i1 = i2 & j1 = j2 )
proof
let D1, D2 be set ; ::_thesis: for f1 being FinSequence of D1 *
for f2 being FinSequence of D2 *
for i1, i2, j1, j2 being Element of NAT st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds
( i1 = i2 & j1 = j2 )
let f1 be FinSequence of D1 * ; ::_thesis: for f2 being FinSequence of D2 *
for i1, i2, j1, j2 being Element of NAT st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds
( i1 = i2 & j1 = j2 )
let f2 be FinSequence of D2 * ; ::_thesis: for i1, i2, j1, j2 being Element of NAT st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds
( i1 = i2 & j1 = j2 )
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 implies ( i1 = i2 & j1 = j2 ) )
assume that
A1: i1 in dom f1 and
A2: i2 in dom f2 and
A3: j1 in dom (f1 . i1) and
A4: j2 in dom (f2 . i2) and
A5: ( Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 ) ; ::_thesis: ( i1 = i2 & j1 = j2 )
A6: ( j1 >= 1 & j2 >= 1 ) by A3, A4, FINSEQ_3:25;
A7: 1 <= i1 by A1, FINSEQ_3:25;
then A8: i1 - 1 >= 0 by XREAL_1:48;
j1 <= len (f1 . i1) by A3, FINSEQ_3:25;
then j1 <= (Card f1) . i1 by A1, CARD_3:def_2;
then A9: j1 <= (Card f1) . ((i1 -' 1) + 1) by A7, XREAL_1:235;
A10: 1 <= i2 by A2, FINSEQ_3:25;
then A11: i2 - 1 >= 0 by XREAL_1:48;
dom (Card f2) = dom f2 by CARD_3:def_2;
then A12: len (Card f2) = len f2 by FINSEQ_3:29;
dom (Card f1) = dom f1 by CARD_3:def_2;
then A13: len (Card f1) = len f1 by FINSEQ_3:29;
i1 <= len f1 by A1, FINSEQ_3:25;
then i1 < (len f1) + 1 by NAT_1:13;
then i1 - 1 < ((len f1) + 1) - 1 by XREAL_1:9;
then A14: i1 -' 1 < len (Card f1) by A13, A8, XREAL_0:def_2;
j2 <= len (f2 . i2) by A4, FINSEQ_3:25;
then j2 <= (Card f2) . i2 by A2, CARD_3:def_2;
then A15: j2 <= (Card f2) . ((i2 -' 1) + 1) by A10, XREAL_1:235;
i2 <= len f2 by A2, FINSEQ_3:25;
then i2 < (len f2) + 1 by NAT_1:13;
then i2 - 1 < ((len f2) + 1) - 1 by XREAL_1:9;
then i2 -' 1 < len (Card f2) by A12, A11, XREAL_0:def_2;
then i1 -' 1 = i2 -' 1 by A5, A14, A6, A9, A15, Th21;
then i1 - 1 = i2 -' 1 by A8, XREAL_0:def_2;
then i1 - 1 = i2 - 1 by A11, XREAL_0:def_2;
hence ( i1 = i2 & j1 = j2 ) by A5, A14, A6, A9, A15, Th21; ::_thesis: verum
end;
begin
definition
let L be non empty ZeroStr ;
mode Polynomial of L is AlgSequence of L;
end;
theorem Th23: :: POLYNOM3:23
for L being non empty ZeroStr
for p being Polynomial of L
for n being Element of NAT holds
( n >= len p iff n is_at_least_length_of p )
proof
let L be non empty ZeroStr ; ::_thesis: for p being Polynomial of L
for n being Element of NAT holds
( n >= len p iff n is_at_least_length_of p )
let p be Polynomial of L; ::_thesis: for n being Element of NAT holds
( n >= len p iff n is_at_least_length_of p )
let n be Element of NAT ; ::_thesis: ( n >= len p iff n is_at_least_length_of p )
thus ( n >= len p implies n is_at_least_length_of p ) ::_thesis: ( n is_at_least_length_of p implies n >= len p )
proof
assume A1: n >= len p ; ::_thesis: n is_at_least_length_of p
let i be Nat; :: according to ALGSEQ_1:def_2 ::_thesis: ( not n <= i or p . i = 0. L )
assume i >= n ; ::_thesis: p . i = 0. L
hence p . i = 0. L by A1, ALGSEQ_1:8, XXREAL_0:2; ::_thesis: verum
end;
assume n is_at_least_length_of p ; ::_thesis: n >= len p
hence n >= len p by ALGSEQ_1:def_3; ::_thesis: verum
end;
scheme :: POLYNOM3:sch 2
PolynomialLambdaF{ F1() -> non empty addLoopStr , F2() -> Element of NAT , F3( Element of NAT ) -> Element of F1() } :
ex p being Polynomial of F1() st
( len p <= F2() & ( for n being Element of NAT st n < F2() holds
p . n = F3(n) ) )
proof
defpred S1[ Element of NAT , Element of F1()] means ( ( $1 < F2() & $2 = F3($1) ) or ( $1 >= F2() & $2 = 0. F1() ) );
A1: for x being Element of NAT ex y being Element of F1() st S1[x,y]
proof
let x be Element of NAT ; ::_thesis: ex y being Element of F1() st S1[x,y]
( x < F2() implies ( x < F2() & F3(x) = F3(x) ) ) ;
hence ex y being Element of F1() st S1[x,y] ; ::_thesis: verum
end;
ex f being Function of NAT, the carrier of F1() st
for x being Element of NAT holds S1[x,f . x] from FUNCT_2:sch_3(A1);
then consider f being Function of NAT, the carrier of F1() such that
A2: for x being Element of NAT holds
( ( x < F2() & f . x = F3(x) ) or ( x >= F2() & f . x = 0. F1() ) ) ;
ex n being Nat st
for i being Nat st i >= n holds
f . i = 0. F1()
proof
take F2() ; ::_thesis: for i being Nat st i >= F2() holds
f . i = 0. F1()
let i be Nat; ::_thesis: ( i >= F2() implies f . i = 0. F1() )
i in NAT by ORDINAL1:def_12;
hence ( i >= F2() implies f . i = 0. F1() ) by A2; ::_thesis: verum
end;
then reconsider f = f as AlgSequence of F1() by ALGSEQ_1:def_1;
take f ; ::_thesis: ( len f <= F2() & ( for n being Element of NAT st n < F2() holds
f . n = F3(n) ) )
now__::_thesis:_for_i_being_Nat_st_i_>=_F2()_holds_
f_._i_=_0._F1()
let i be Nat; ::_thesis: ( i >= F2() implies f . i = 0. F1() )
i in NAT by ORDINAL1:def_12;
hence ( i >= F2() implies f . i = 0. F1() ) by A2; ::_thesis: verum
end;
then F2() is_at_least_length_of f by ALGSEQ_1:def_2;
hence ( len f <= F2() & ( for n being Element of NAT st n < F2() holds
f . n = F3(n) ) ) by A2, ALGSEQ_1:def_3; ::_thesis: verum
end;
registration
let L be non empty right_zeroed addLoopStr ;
let p, q be Polynomial of L;
clusterp + q -> finite-Support ;
coherence
p + q is finite-Support
proof
take s = (len p) + (len q); :: according to ALGSEQ_1:def_1 ::_thesis: for b1 being set holds
( not s <= b1 or (p + q) . b1 = 0. L )
let i be Nat; ::_thesis: ( not s <= i or (p + q) . i = 0. L )
assume A1: i >= s ; ::_thesis: (p + q) . i = 0. L
(len p) + (len q) >= len p by NAT_1:11;
then A2: p . i = 0. L by A1, ALGSEQ_1:8, XXREAL_0:2;
A3: (len p) + (len q) >= len q by NAT_1:11;
i in NAT by ORDINAL1:def_12;
hence (p + q) . i = (p . i) + (q . i) by NORMSP_1:def_2
.= (0. L) + (0. L) by A1, A2, A3, ALGSEQ_1:8, XXREAL_0:2
.= 0. L by RLVECT_1:def_4 ;
::_thesis: verum
end;
end;
theorem Th24: :: POLYNOM3:24
for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of L
for n being Element of NAT st n is_at_least_length_of p & n is_at_least_length_of q holds
n is_at_least_length_of p + q
proof
let L be non empty right_zeroed addLoopStr ; ::_thesis: for p, q being Polynomial of L
for n being Element of NAT st n is_at_least_length_of p & n is_at_least_length_of q holds
n is_at_least_length_of p + q
let p, q be Polynomial of L; ::_thesis: for n being Element of NAT st n is_at_least_length_of p & n is_at_least_length_of q holds
n is_at_least_length_of p + q
let n be Element of NAT ; ::_thesis: ( n is_at_least_length_of p & n is_at_least_length_of q implies n is_at_least_length_of p + q )
assume A1: ( n is_at_least_length_of p & n is_at_least_length_of q ) ; ::_thesis: n is_at_least_length_of p + q
let i be Nat; :: according to ALGSEQ_1:def_2 ::_thesis: ( not n <= i or (p + q) . i = 0. L )
assume i >= n ; ::_thesis: (p + q) . i = 0. L
then A2: ( p . i = 0. L & q . i = 0. L ) by A1, ALGSEQ_1:def_2;
i in NAT by ORDINAL1:def_12;
hence (p + q) . i = (0. L) + (0. L) by A2, NORMSP_1:def_2
.= 0. L by RLVECT_1:def_4 ;
::_thesis: verum
end;
theorem :: POLYNOM3:25
for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of L holds support (p + q) c= (support p) \/ (support q)
proof
let L be non empty right_zeroed addLoopStr ; ::_thesis: for p, q being Polynomial of L holds support (p + q) c= (support p) \/ (support q)
let p, q be Polynomial of L; ::_thesis: support (p + q) c= (support p) \/ (support q)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (p + q) or x in (support p) \/ (support q) )
assume A1: x in support (p + q) ; ::_thesis: x in (support p) \/ (support q)
then reconsider x1 = x as Element of NAT ;
A2: x1 < len (p + q) by A1, ALGSEQ_1:1;
( x1 < len p or x1 < len q )
proof
assume ( not x1 < len p & not x1 < len q ) ; ::_thesis: contradiction
then ( x1 is_at_least_length_of p & x1 is_at_least_length_of q ) by Th23;
then x1 is_at_least_length_of p + q by Th24;
hence contradiction by A2, Th23; ::_thesis: verum
end;
then ( x in Segm (len p) or x in Segm (len q) ) by NAT_1:44;
hence x in (support p) \/ (support q) by XBOOLE_0:def_3; ::_thesis: verum
end;
definition
let L be non empty Abelian addLoopStr ;
let p, q be sequence of L;
:: original: +
redefine funcp + q -> Element of bool [:NAT, the carrier of L:];
commutativity
for p, q being sequence of L holds p + q = q + p
proof
let p, q be sequence of L; ::_thesis: p + q = q + p
now__::_thesis:_for_n_being_Element_of_NAT_holds_(p_+_q)_._n_=_(q_+_p)_._n
let n be Element of NAT ; ::_thesis: (p + q) . n = (q + p) . n
thus (p + q) . n = (p . n) + (q . n) by NORMSP_1:def_2
.= (q + p) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;
hence p + q = q + p by FUNCT_2:63; ::_thesis: verum
end;
end;
theorem Th26: :: POLYNOM3:26
for L being non empty add-associative addLoopStr
for p, q, r being sequence of L holds (p + q) + r = p + (q + r)
proof
let L be non empty add-associative addLoopStr ; ::_thesis: for p, q, r being sequence of L holds (p + q) + r = p + (q + r)
let p, q, r be sequence of L; ::_thesis: (p + q) + r = p + (q + r)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((p_+_q)_+_r)_._n_=_(p_+_(q_+_r))_._n
let n be Element of NAT ; ::_thesis: ((p + q) + r) . n = (p + (q + r)) . n
thus ((p + q) + r) . n = ((p + q) . n) + (r . n) by NORMSP_1:def_2
.= ((p . n) + (q . n)) + (r . n) by NORMSP_1:def_2
.= (p . n) + ((q . n) + (r . n)) by RLVECT_1:def_3
.= (p . n) + ((q + r) . n) by NORMSP_1:def_2
.= (p + (q + r)) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;
hence (p + q) + r = p + (q + r) by FUNCT_2:63; ::_thesis: verum
end;
registration
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p be Polynomial of L;
cluster - p -> finite-Support ;
coherence
- p is finite-Support
proof
take s = len p; :: according to ALGSEQ_1:def_1 ::_thesis: for b1 being set holds
( not s <= b1 or (- p) . b1 = 0. L )
let i be Nat; ::_thesis: ( not s <= i or (- p) . i = 0. L )
assume A1: i >= s ; ::_thesis: (- p) . i = 0. L
i in NAT by ORDINAL1:def_12;
hence (- p) . i = - (p . i) by BHSP_1:44
.= - (0. L) by A1, ALGSEQ_1:8
.= 0. L by RLVECT_1:12 ;
::_thesis: verum
end;
end;
Lm1: for L being non empty addLoopStr
for p, q being sequence of L holds p - q = p + (- q)
proof
let L be non empty addLoopStr ; ::_thesis: for p, q being sequence of L holds p - q = p + (- q)
let p, q be sequence of L; ::_thesis: p - q = p + (- q)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (p - q) . n = (p + (- q)) . n
thus (p - q) . n = (p . n) - (q . n) by NORMSP_1:def_3
.= (p . n) + ((- q) . n) by BHSP_1:44
.= (p + (- q)) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;
definition
let L be non empty addLoopStr ;
let p, q be sequence of L;
redefine func p - q equals :: POLYNOM3:def 6
p + (- q);
compatibility
for b1 being Element of bool [:NAT, the carrier of L:] holds
( b1 = p - q iff b1 = p + (- q) ) by Lm1;
end;
:: deftheorem defines - POLYNOM3:def_6_:_
for L being non empty addLoopStr
for p, q being sequence of L holds p - q = p + (- q);
registration
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p, q be Polynomial of L;
clusterp - q -> finite-Support ;
coherence
p - q is finite-Support ;
end;
theorem :: POLYNOM3:27
for L being non empty addLoopStr
for p, q being sequence of L
for n being Element of NAT holds (p - q) . n = (p . n) - (q . n) by NORMSP_1:def_3;
definition
let L be non empty ZeroStr ;
func 0_. L -> sequence of L equals :: POLYNOM3:def 7
NAT --> (0. L);
coherence
NAT --> (0. L) is sequence of L ;
end;
:: deftheorem defines 0_. POLYNOM3:def_7_:_
for L being non empty ZeroStr holds 0_. L = NAT --> (0. L);
registration
let L be non empty ZeroStr ;
cluster 0_. L -> finite-Support ;
coherence
0_. L is finite-Support
proof
take 0 ; :: according to ALGSEQ_1:def_1 ::_thesis: for b1 being set holds
( not 0 <= b1 or (0_. L) . b1 = 0. L )
let i be Nat; ::_thesis: ( not 0 <= i or (0_. L) . i = 0. L )
assume i >= 0 ; ::_thesis: (0_. L) . i = 0. L
i in NAT by ORDINAL1:def_12;
hence (0_. L) . i = 0. L by FUNCOP_1:7; ::_thesis: verum
end;
end;
theorem Th28: :: POLYNOM3:28
for L being non empty right_zeroed addLoopStr
for p being sequence of L holds p + (0_. L) = p
proof
let L be non empty right_zeroed addLoopStr ; ::_thesis: for p being sequence of L holds p + (0_. L) = p
let p be sequence of L; ::_thesis: p + (0_. L) = p
now__::_thesis:_for_n_being_Element_of_NAT_holds_(p_+_(0_._L))_._n_=_p_._n
let n be Element of NAT ; ::_thesis: (p + (0_. L)) . n = p . n
thus (p + (0_. L)) . n = (p . n) + ((0_. L) . n) by NORMSP_1:def_2
.= (p . n) + (0. L) by FUNCOP_1:7
.= p . n by RLVECT_1:def_4 ; ::_thesis: verum
end;
hence p + (0_. L) = p by FUNCT_2:63; ::_thesis: verum
end;
theorem Th29: :: POLYNOM3:29
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being sequence of L holds p - p = 0_. L
proof
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being sequence of L holds p - p = 0_. L
let p be sequence of L; ::_thesis: p - p = 0_. L
now__::_thesis:_for_n_being_Element_of_NAT_holds_(p_-_p)_._n_=_(0_._L)_._n
let n be Element of NAT ; ::_thesis: (p - p) . n = (0_. L) . n
thus (p - p) . n = (p . n) - (p . n) by NORMSP_1:def_3
.= 0. L by RLVECT_1:15
.= (0_. L) . n by FUNCOP_1:7 ; ::_thesis: verum
end;
hence p - p = 0_. L by FUNCT_2:63; ::_thesis: verum
end;
definition
let L be non empty multLoopStr_0 ;
func 1_. L -> sequence of L equals :: POLYNOM3:def 8
(0_. L) +* (0,(1. L));
coherence
(0_. L) +* (0,(1. L)) is sequence of L ;
end;
:: deftheorem defines 1_. POLYNOM3:def_8_:_
for L being non empty multLoopStr_0 holds 1_. L = (0_. L) +* (0,(1. L));
registration
let L be non empty multLoopStr_0 ;
cluster 1_. L -> finite-Support ;
coherence
1_. L is finite-Support
proof
take 1 ; :: according to ALGSEQ_1:def_1 ::_thesis: for b1 being set holds
( not 1 <= b1 or (1_. L) . b1 = 0. L )
let i be Nat; ::_thesis: ( not 1 <= i or (1_. L) . i = 0. L )
A1: i in NAT by ORDINAL1:def_12;
assume i >= 1 ; ::_thesis: (1_. L) . i = 0. L
hence (1_. L) . i = (0_. L) . i by FUNCT_7:32
.= 0. L by A1, FUNCOP_1:7 ;
::_thesis: verum
end;
end;
theorem Th30: :: POLYNOM3:30
for L being non empty multLoopStr_0 holds
( (1_. L) . 0 = 1. L & ( for n being Nat st n <> 0 holds
(1_. L) . n = 0. L ) )
proof
let L be non empty multLoopStr_0 ; ::_thesis: ( (1_. L) . 0 = 1. L & ( for n being Nat st n <> 0 holds
(1_. L) . n = 0. L ) )
0 in NAT ;
then 0 in dom (0_. L) by FUNCT_2:def_1;
hence (1_. L) . 0 = 1. L by FUNCT_7:31; ::_thesis: for n being Nat st n <> 0 holds
(1_. L) . n = 0. L
let n be Nat; ::_thesis: ( n <> 0 implies (1_. L) . n = 0. L )
A1: n in NAT by ORDINAL1:def_12;
assume n <> 0 ; ::_thesis: (1_. L) . n = 0. L
hence (1_. L) . n = (0_. L) . n by FUNCT_7:32
.= 0. L by A1, FUNCOP_1:7 ;
::_thesis: verum
end;
definition
let L be non empty doubleLoopStr ;
let p, q be sequence of L;
funcp *' q -> sequence of L means :Def9: :: POLYNOM3:def 9
for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & it . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) );
existence
ex b1 being sequence of L st
for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & b1 . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) )
proof
defpred S1[ Element of NAT , Element of L] means ex r being FinSequence of the carrier of L st
( len r = $1 + 1 & $2 = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . (($1 + 1) -' k)) ) );
A1: for i being Element of NAT ex v being Element of L st S1[i,v]
proof
let i be Element of NAT ; ::_thesis: ex v being Element of L st S1[i,v]
deffunc H1( Nat) -> Element of the carrier of L = (p . ($1 -' 1)) * (q . ((i + 1) -' $1));
consider r being FinSequence of the carrier of L such that
A2: len r = i + 1 and
A3: for k being Nat st k in dom r holds
r . k = H1(k) from FINSEQ_2:sch_1();
take v = Sum r; ::_thesis: S1[i,v]
take r ; ::_thesis: ( len r = i + 1 & v = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) )
thus len r = i + 1 by A2; ::_thesis: ( v = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) )
thus v = Sum r ; ::_thesis: for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k))
let k be Element of NAT ; ::_thesis: ( k in dom r implies r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) )
assume k in dom r ; ::_thesis: r . k = (p . (k -' 1)) * (q . ((i + 1) -' k))
hence r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A3; ::_thesis: verum
end;
consider f being Function of NAT, the carrier of L such that
A4: for i being Element of NAT holds S1[i,f . i] from FUNCT_2:sch_3(A1);
take f ; ::_thesis: for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & f . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) )
thus for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & f . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) by A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being sequence of L st ( for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & b1 . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) & ( for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & b2 . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) holds
b1 = b2
proof
let p1, p2 be sequence of L; ::_thesis: ( ( for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & p1 . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) & ( for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & p2 . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) implies p1 = p2 )
assume that
A5: for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & p1 . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) and
A6: for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & p2 . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ; ::_thesis: p1 = p2
now__::_thesis:_for_i_being_Element_of_NAT_holds_p1_._i_=_p2_._i
let i be Element of NAT ; ::_thesis: p1 . i = p2 . i
consider r1 being FinSequence of the carrier of L such that
A7: len r1 = i + 1 and
A8: p1 . i = Sum r1 and
A9: for k being Element of NAT st k in dom r1 holds
r1 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A5;
consider r2 being FinSequence of the carrier of L such that
A10: len r2 = i + 1 and
A11: p2 . i = Sum r2 and
A12: for k being Element of NAT st k in dom r2 holds
r2 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A6;
A13: dom r1 = Seg (len r2) by A7, A10, FINSEQ_1:def_3
.= dom r2 by FINSEQ_1:def_3 ;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_r1_holds_
r1_._k_=_r2_._k
let k be Nat; ::_thesis: ( k in dom r1 implies r1 . k = r2 . k )
assume A14: k in dom r1 ; ::_thesis: r1 . k = r2 . k
hence r1 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A9
.= r2 . k by A12, A13, A14 ;
::_thesis: verum
end;
hence p1 . i = p2 . i by A8, A11, A13, FINSEQ_1:13; ::_thesis: verum
end;
hence p1 = p2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines *' POLYNOM3:def_9_:_
for L being non empty doubleLoopStr
for p, q, b4 being sequence of L holds
( b4 = p *' q iff for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & b4 . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) );
registration
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
let p, q be Polynomial of L;
clusterp *' q -> finite-Support ;
coherence
p *' q is finite-Support
proof
take s = (len p) + (len q); :: according to ALGSEQ_1:def_1 ::_thesis: for b1 being set holds
( not s <= b1 or (p *' q) . b1 = 0. L )
let i be Nat; ::_thesis: ( not s <= i or (p *' q) . i = 0. L )
i in NAT by ORDINAL1:def_12;
then consider r being FinSequence of the carrier of L such that
A1: len r = i + 1 and
A2: (p *' q) . i = Sum r and
A3: for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by Def9;
assume i >= s ; ::_thesis: (p *' q) . i = 0. L
then len p <= i - (len q) by XREAL_1:19;
then A4: - (len p) >= - (i - (len q)) by XREAL_1:24;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_r_holds_
r_._k_=_0._L
let k be Element of NAT ; ::_thesis: ( k in dom r implies r . b1 = 0. L )
assume A5: k in dom r ; ::_thesis: r . b1 = 0. L
then A6: r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A3;
k <= i + 1 by A1, A5, FINSEQ_3:25;
then A7: (i + 1) - k >= 0 by XREAL_1:48;
percases ( k -' 1 < len p or k -' 1 >= len p ) ;
suppose k -' 1 < len p ; ::_thesis: r . b1 = 0. L
then k - 1 < len p by XREAL_0:def_2;
then - (k - 1) > - (len p) by XREAL_1:24;
then 1 - k > (len q) - i by A4, XXREAL_0:2;
then i + (1 - k) > len q by XREAL_1:19;
then (i + 1) -' k >= len q by A7, XREAL_0:def_2;
then q . ((i + 1) -' k) = 0. L by ALGSEQ_1:8;
hence r . k = 0. L by A6, VECTSP_1:6; ::_thesis: verum
end;
suppose k -' 1 >= len p ; ::_thesis: r . b1 = 0. L
then p . (k -' 1) = 0. L by ALGSEQ_1:8;
hence r . k = 0. L by A6, VECTSP_1:7; ::_thesis: verum
end;
end;
end;
hence (p *' q) . i = 0. L by A2, Th1; ::_thesis: verum
end;
end;
theorem Th31: :: POLYNOM3:31
for L being non empty right_complementable right-distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being sequence of L holds p *' (q + r) = (p *' q) + (p *' r)
proof
let L be non empty right_complementable right-distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q, r being sequence of L holds p *' (q + r) = (p *' q) + (p *' r)
let p, q, r be sequence of L; ::_thesis: p *' (q + r) = (p *' q) + (p *' r)
now__::_thesis:_for_i_being_Element_of_NAT_holds_(p_*'_(q_+_r))_._i_=_((p_*'_q)_+_(p_*'_r))_._i
let i be Element of NAT ; ::_thesis: (p *' (q + r)) . i = ((p *' q) + (p *' r)) . i
consider r1 being FinSequence of the carrier of L such that
A1: len r1 = i + 1 and
A2: (p *' (q + r)) . i = Sum r1 and
A3: for k being Element of NAT st k in dom r1 holds
r1 . k = (p . (k -' 1)) * ((q + r) . ((i + 1) -' k)) by Def9;
A4: dom r1 = Seg (i + 1) by A1, FINSEQ_1:def_3;
consider r3 being FinSequence of the carrier of L such that
A5: len r3 = i + 1 and
A6: (p *' r) . i = Sum r3 and
A7: for k being Element of NAT st k in dom r3 holds
r3 . k = (p . (k -' 1)) * (r . ((i + 1) -' k)) by Def9;
consider r2 being FinSequence of the carrier of L such that
A8: len r2 = i + 1 and
A9: (p *' q) . i = Sum r2 and
A10: for k being Element of NAT st k in dom r2 holds
r2 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by Def9;
reconsider r29 = r2, r39 = r3 as Element of (i + 1) -tuples_on the carrier of L by A8, A5, FINSEQ_2:92;
A11: len (r29 + r39) = i + 1 by CARD_1:def_7;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_r1_holds_
r1_._k_=_(r2_+_r3)_._k
let k be Nat; ::_thesis: ( k in dom r1 implies r1 . k = (r2 + r3) . k )
assume A12: k in dom r1 ; ::_thesis: r1 . k = (r2 + r3) . k
then A13: k in dom (r2 + r3) by A11, A4, FINSEQ_1:def_3;
k in dom r3 by A5, A4, A12, FINSEQ_1:def_3;
then A14: r3 . k = (p . (k -' 1)) * (r . ((i + 1) -' k)) by A7;
k in dom r2 by A8, A4, A12, FINSEQ_1:def_3;
then A15: r2 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A10;
thus r1 . k = (p . (k -' 1)) * ((q + r) . ((i + 1) -' k)) by A3, A12
.= (p . (k -' 1)) * ((q . ((i + 1) -' k)) + (r . ((i + 1) -' k))) by NORMSP_1:def_2
.= ((p . (k -' 1)) * (q . ((i + 1) -' k))) + ((p . (k -' 1)) * (r . ((i + 1) -' k))) by VECTSP_1:def_2
.= (r2 + r3) . k by A13, A15, A14, FVSUM_1:17 ; ::_thesis: verum
end;
then Sum r1 = Sum (r29 + r39) by A1, A11, FINSEQ_2:9
.= (Sum r2) + (Sum r3) by FVSUM_1:76 ;
hence (p *' (q + r)) . i = ((p *' q) + (p *' r)) . i by A2, A9, A6, NORMSP_1:def_2; ::_thesis: verum
end;
hence p *' (q + r) = (p *' q) + (p *' r) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th32: :: POLYNOM3:32
for L being non empty right_complementable left-distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being sequence of L holds (p + q) *' r = (p *' r) + (q *' r)
proof
let L be non empty right_complementable left-distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q, r being sequence of L holds (p + q) *' r = (p *' r) + (q *' r)
let p, q, r be sequence of L; ::_thesis: (p + q) *' r = (p *' r) + (q *' r)
now__::_thesis:_for_i_being_Element_of_NAT_holds_((p_+_q)_*'_r)_._i_=_((p_*'_r)_+_(q_*'_r))_._i
let i be Element of NAT ; ::_thesis: ((p + q) *' r) . i = ((p *' r) + (q *' r)) . i
consider r1 being FinSequence of the carrier of L such that
A1: len r1 = i + 1 and
A2: ((p + q) *' r) . i = Sum r1 and
A3: for k being Element of NAT st k in dom r1 holds
r1 . k = ((p + q) . (k -' 1)) * (r . ((i + 1) -' k)) by Def9;
A4: dom r1 = Seg (i + 1) by A1, FINSEQ_1:def_3;
consider r3 being FinSequence of the carrier of L such that
A5: len r3 = i + 1 and
A6: (q *' r) . i = Sum r3 and
A7: for k being Element of NAT st k in dom r3 holds
r3 . k = (q . (k -' 1)) * (r . ((i + 1) -' k)) by Def9;
consider r2 being FinSequence of the carrier of L such that
A8: len r2 = i + 1 and
A9: (p *' r) . i = Sum r2 and
A10: for k being Element of NAT st k in dom r2 holds
r2 . k = (p . (k -' 1)) * (r . ((i + 1) -' k)) by Def9;
reconsider r29 = r2, r39 = r3 as Element of (i + 1) -tuples_on the carrier of L by A8, A5, FINSEQ_2:92;
A11: len (r29 + r39) = i + 1 by CARD_1:def_7;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_r1_holds_
r1_._k_=_(r2_+_r3)_._k
let k be Nat; ::_thesis: ( k in dom r1 implies r1 . k = (r2 + r3) . k )
assume A12: k in dom r1 ; ::_thesis: r1 . k = (r2 + r3) . k
then A13: k in dom (r2 + r3) by A11, A4, FINSEQ_1:def_3;
k in dom r3 by A5, A4, A12, FINSEQ_1:def_3;
then A14: r3 . k = (q . (k -' 1)) * (r . ((i + 1) -' k)) by A7;
k in dom r2 by A8, A4, A12, FINSEQ_1:def_3;
then A15: r2 . k = (p . (k -' 1)) * (r . ((i + 1) -' k)) by A10;
thus r1 . k = ((p + q) . (k -' 1)) * (r . ((i + 1) -' k)) by A3, A12
.= ((p . (k -' 1)) + (q . (k -' 1))) * (r . ((i + 1) -' k)) by NORMSP_1:def_2
.= ((p . (k -' 1)) * (r . ((i + 1) -' k))) + ((q . (k -' 1)) * (r . ((i + 1) -' k))) by VECTSP_1:def_3
.= (r2 + r3) . k by A13, A15, A14, FVSUM_1:17 ; ::_thesis: verum
end;
then Sum r1 = Sum (r29 + r39) by A1, A11, FINSEQ_2:9
.= (Sum r2) + (Sum r3) by FVSUM_1:76 ;
hence ((p + q) *' r) . i = ((p *' r) + (q *' r)) . i by A2, A9, A6, NORMSP_1:def_2; ::_thesis: verum
end;
hence (p + q) *' r = (p *' r) + (q *' r) by FUNCT_2:63; ::_thesis: verum
end;
definition
let n be Element of NAT ;
:: original: <*
redefine func<*n*> -> Element of 1 -tuples_on NAT;
coherence
<*n*> is Element of 1 -tuples_on NAT
proof
thus <*n*> is Element of 1 -tuples_on NAT by FINSEQ_2:131; ::_thesis: verum
end;
end;
theorem Th33: :: POLYNOM3:33
for L being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being sequence of L holds (p *' q) *' r = p *' (q *' r)
proof
let L be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q, r being sequence of L holds (p *' q) *' r = p *' (q *' r)
let p, q, r be sequence of L; ::_thesis: (p *' q) *' r = p *' (q *' r)
now__::_thesis:_for_i_being_Element_of_NAT_holds_((p_*'_q)_*'_r)_._i_=_(p_*'_(q_*'_r))_._i
let i be Element of NAT ; ::_thesis: ((p *' q) *' r) . i = (p *' (q *' r)) . i
deffunc H1( Nat) -> Element of ((2 + 1) -tuples_on NAT) * = (Decomp (($1 -' 1),2)) ^^ ($1 |-> <*((i + 1) -' $1)*>);
consider f2 being FinSequence of ((2 + 1) -tuples_on NAT) * such that
A1: len f2 = i + 1 and
A2: for k being Nat st k in dom f2 holds
f2 . k = H1(k) from FINSEQ_2:sch_1();
A3: dom f2 = Seg (i + 1) by A1, FINSEQ_1:def_3;
reconsider f2 = f2 as FinSequence of (3 -tuples_on NAT) * ;
deffunc H2( Nat) -> Element of ((1 + 2) -tuples_on NAT) * = (((i + 2) -' $1) |-> <*($1 -' 1)*>) ^^ (Decomp (((i + 1) -' $1),2));
consider g2 being FinSequence of ((1 + 2) -tuples_on NAT) * such that
A4: len g2 = i + 1 and
A5: for k being Nat st k in dom g2 holds
g2 . k = H2(k) from FINSEQ_2:sch_1();
A6: dom g2 = Seg (i + 1) by A4, FINSEQ_1:def_3;
reconsider g2 = g2 as FinSequence of (3 -tuples_on NAT) * ;
consider r2 being FinSequence of the carrier of L such that
A7: len r2 = i + 1 and
A8: (p *' (q *' r)) . i = Sum r2 and
A9: for k being Element of NAT st k in dom r2 holds
r2 . k = (p . (k -' 1)) * ((q *' r) . ((i + 1) -' k)) by Def9;
A10: dom r2 = Seg (i + 1) by A7, FINSEQ_1:def_3;
A11: dom (Card f2) = dom f2 by CARD_3:def_2
.= Seg (len g2) by A1, A4, FINSEQ_1:def_3
.= dom g2 by FINSEQ_1:def_3
.= dom (Card g2) by CARD_3:def_2
.= dom (Rev (Card g2)) by FINSEQ_5:57 ;
A12: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(Card_f2)_holds_
(Card_f2)_._j_=_(Rev_(Card_g2))_._j
let j be Nat; ::_thesis: ( j in dom (Card f2) implies (Card f2) . j = (Rev (Card g2)) . j )
A13: dom (j |-> <*((i + 1) -' j)*>) = Seg j by FUNCOP_1:13;
assume A14: j in dom (Card f2) ; ::_thesis: (Card f2) . j = (Rev (Card g2)) . j
then A15: j in Seg (len (Rev (Card g2))) by A11, FINSEQ_1:def_3;
then A16: j >= 1 by FINSEQ_1:1;
then j - 1 >= 0 by XREAL_1:48;
then A17: (i + 1) - (j - 1) <= i + 1 by XREAL_1:43;
A18: dom (Card g2) = dom g2 by CARD_3:def_2;
then A19: len (Card g2) = len g2 by FINSEQ_3:29;
then A20: j in Seg (len g2) by A15, FINSEQ_5:def_3;
then A21: f2 . j = (Decomp ((j -' 1),2)) ^^ (j |-> <*((i + 1) -' j)*>) by A2, A3, A4;
i + 1 >= j by A4, A20, FINSEQ_1:1;
then A22: (i + 1) - j >= 0 by XREAL_1:48;
then ((i + 1) - j) + 1 = ((i + 1) -' j) + 1 by XREAL_0:def_2;
then reconsider lj = ((len (Card g2)) - j) + 1 as Element of NAT by A4, A18, FINSEQ_3:29;
(i + 1) - (((i + 1) - j) + 1) = 0 + (j - 1) ;
then A23: (i + 1) - (((i + 1) - j) + 1) >= 0 by A16, XREAL_1:48;
then A24: ((i + 1) -' lj) + 1 = (0 + (j - 1)) + 1 by A4, A19, XREAL_0:def_2
.= j ;
((i + 1) - j) + 1 >= 0 + 1 by A22, XREAL_1:6;
then lj in Seg (i + 1) by A4, A19, A17, FINSEQ_1:1;
then A25: g2 . lj = (((i + 2) -' lj) |-> <*(lj -' 1)*>) ^^ (Decomp (((i + 1) -' lj),2)) by A5, A6;
A26: ((i + 1) -' lj) + 1 = ((i + 1) - lj) + 1 by A4, A19, A23, XREAL_0:def_2
.= (i + (1 + 1)) - lj ;
A27: dom (((i + 2) -' lj) |-> <*(lj -' 1)*>) = Seg ((i + 2) -' lj) by FUNCOP_1:13
.= Seg j by A24, A26, XREAL_0:def_2 ;
A28: dom (Decomp (((i + 1) -' lj),2)) = Seg (len (Decomp (((i + 1) -' lj),2))) by FINSEQ_1:def_3
.= Seg j by A24, Th9 ;
Seg (len (g2 . lj)) = dom (g2 . lj) by FINSEQ_1:def_3
.= (Seg j) /\ (Seg j) by A25, A28, A27, PRE_POLY:def_4
.= Seg j ;
then A29: len (g2 . lj) = j by FINSEQ_1:6;
A30: dom (Decomp ((j -' 1),2)) = Seg (len (Decomp ((j -' 1),2))) by FINSEQ_1:def_3
.= Seg ((j -' 1) + 1) by Th9
.= Seg j by A16, XREAL_1:235 ;
Seg (len (f2 . j)) = dom (f2 . j) by FINSEQ_1:def_3
.= (Seg j) /\ (Seg j) by A21, A30, A13, PRE_POLY:def_4
.= Seg j ;
then A31: len (f2 . j) = j by FINSEQ_1:6;
((len (Card g2)) - j) + 1 in Seg (len g2) by A19, A20, FINSEQ_5:2;
then A32: ((len (Card g2)) - j) + 1 in dom g2 by FINSEQ_1:def_3;
j in dom f2 by A14, CARD_3:def_2;
hence (Card f2) . j = j by A31, CARD_3:def_2
.= (Card g2) . (((len (Card g2)) - j) + 1) by A32, A29, CARD_3:def_2
.= (Rev (Card g2)) . j by A11, A14, FINSEQ_5:def_3 ;
::_thesis: verum
end;
len (Card f2) = len (Rev (Card g2)) by A11, FINSEQ_3:29;
then A33: Card f2 = Rev (Card g2) by A12, FINSEQ_2:9;
reconsider w = Card g2 as FinSequence of NAT ;
A34: Seg (len (FlattenSeq f2)) = dom (FlattenSeq f2) by FINSEQ_1:def_3;
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_rng_(FlattenSeq_f2)_implies_y_in_rng_(FlattenSeq_g2)_)_&_(_y_in_rng_(FlattenSeq_g2)_implies_y_in_rng_(FlattenSeq_f2)_)_)
let y be set ; ::_thesis: ( ( y in rng (FlattenSeq f2) implies y in rng (FlattenSeq g2) ) & ( y in rng (FlattenSeq g2) implies y in rng (FlattenSeq f2) ) )
thus ( y in rng (FlattenSeq f2) implies y in rng (FlattenSeq g2) ) ::_thesis: ( y in rng (FlattenSeq g2) implies y in rng (FlattenSeq f2) )
proof
assume y in rng (FlattenSeq f2) ; ::_thesis: y in rng (FlattenSeq g2)
then consider x being Nat such that
A35: x in dom (FlattenSeq f2) and
A36: (FlattenSeq f2) . x = y by FINSEQ_2:10;
consider i1, j1 being Element of NAT such that
A37: i1 in dom f2 and
A38: j1 in dom (f2 . i1) and
x = (Sum (Card (f2 | (i1 -' 1)))) + j1 and
A39: (f2 . i1) . j1 = (FlattenSeq f2) . x by A35, PRE_POLY:29;
A40: f2 . i1 = (Decomp ((i1 -' 1),2)) ^^ (i1 |-> <*((i + 1) -' i1)*>) by A2, A37;
then j1 in (dom (Decomp ((i1 -' 1),2))) /\ (dom (i1 |-> <*((i + 1) -' i1)*>)) by A38, PRE_POLY:def_4;
then j1 in dom (i1 |-> <*((i + 1) -' i1)*>) by XBOOLE_0:def_4;
then A41: j1 in Seg i1 by FUNCOP_1:13;
then A42: j1 <= i1 by FINSEQ_1:1;
then A43: i1 - j1 >= 0 by XREAL_1:48;
set j2 = (i1 -' j1) + 1;
set i2 = j1;
A44: dom (((i + 2) -' j1) |-> <*(j1 -' 1)*>) = Seg ((i + 2) -' j1) by FUNCOP_1:13;
A45: i1 in Seg (i + 1) by A1, A37, FINSEQ_1:def_3;
then A46: 1 <= i1 by FINSEQ_1:1;
then A47: j1 in Seg ((i1 -' 1) + 1) by A41, XREAL_1:235;
A48: i1 <= i + 1 by A45, FINSEQ_1:1;
then A49: (i + 1) - i1 >= 0 by XREAL_1:48;
A50: i + 1 >= j1 by A48, A42, XXREAL_0:2;
then A51: (i + 1) - j1 >= 0 by XREAL_1:48;
then A52: ((i + 1) -' j1) + 1 = ((i + 1) - j1) + 1 by XREAL_0:def_2
.= (i + (1 + 1)) - j1 ;
(i + 1) -' j1 >= i1 -' j1 by A48, NAT_D:42;
then ((i + 1) -' j1) + 1 >= (i1 -' j1) + 1 by XREAL_1:6;
then (((i + 1) -' j1) + 1) - ((i1 -' j1) + 1) >= 0 by XREAL_1:48;
then A53: (((i + 1) -' j1) + 1) -' ((i1 -' j1) + 1) = (((i + 1) -' j1) + 1) - ((i1 -' j1) + 1) by XREAL_0:def_2
.= (((i + 1) -' j1) + 1) - ((i1 - j1) + 1) by A43, XREAL_0:def_2
.= (((i + 1) - j1) + 1) - ((1 - j1) + i1) by A51, XREAL_0:def_2
.= (i + 1) -' i1 by A49, XREAL_0:def_2 ;
1 <= j1 by A41, FINSEQ_1:1;
then A54: j1 in Seg (i + 1) by A50, FINSEQ_1:1;
then A55: g2 . j1 = (((i + 2) -' j1) |-> <*(j1 -' 1)*>) ^^ (Decomp (((i + 1) -' j1),2)) by A5, A6;
i1 -' j1 <= (i + 1) -' j1 by A48, NAT_D:42;
then ( 1 <= (i1 -' j1) + 1 & (i1 -' j1) + 1 <= ((i + 1) -' j1) + 1 ) by NAT_1:11, XREAL_1:6;
then A56: (i1 -' j1) + 1 in Seg (((i + 1) -' j1) + 1) by FINSEQ_1:1;
then A57: (i1 -' j1) + 1 in Seg ((i + 2) -' j1) by A52, XREAL_0:def_2;
dom (Decomp (((i + 1) -' j1),2)) = Seg (len (Decomp (((i + 1) -' j1),2))) by FINSEQ_1:def_3
.= Seg (((i + 1) -' j1) + 1) by Th9
.= Seg ((i + 2) -' j1) by A52, XREAL_0:def_2 ;
then dom (g2 . j1) = (Seg ((i + 2) -' j1)) /\ (Seg ((i + 2) -' j1)) by A55, A44, PRE_POLY:def_4;
then A58: (i1 -' j1) + 1 in dom (g2 . j1) by A56, A52, XREAL_0:def_2;
then A59: (g2 . j1) . ((i1 -' j1) + 1) = ((((i + 2) -' j1) |-> <*(j1 -' 1)*>) . ((i1 -' j1) + 1)) ^ ((Decomp (((i + 1) -' j1),2)) . ((i1 -' j1) + 1)) by A55, PRE_POLY:def_4
.= <*(j1 -' 1)*> ^ ((Decomp (((i + 1) -' j1),2)) . ((i1 -' j1) + 1)) by A57, FUNCOP_1:7
.= <*(j1 -' 1)*> ^ <*(((i1 -' j1) + 1) -' 1),((((i + 1) -' j1) + 1) -' ((i1 -' j1) + 1))*> by A56, Th14
.= <*(j1 -' 1),(((i1 -' j1) + 1) -' 1),((((i + 1) -' j1) + 1) -' ((i1 -' j1) + 1))*> by FINSEQ_1:43
.= <*(j1 -' 1),(i1 -' j1),((i + 1) -' i1)*> by A53, NAT_D:34 ;
j1 in dom g2 by A4, A54, FINSEQ_1:def_3;
then A60: ( (Sum (Card (g2 | (j1 -' 1)))) + ((i1 -' j1) + 1) in dom (FlattenSeq g2) & (g2 . j1) . ((i1 -' j1) + 1) = (FlattenSeq g2) . ((Sum (Card (g2 | (j1 -' 1)))) + ((i1 -' j1) + 1)) ) by A58, PRE_POLY:30;
y = ((Decomp ((i1 -' 1),2)) . j1) ^ ((i1 |-> <*((i + 1) -' i1)*>) . j1) by A36, A38, A39, A40, PRE_POLY:def_4
.= ((Decomp ((i1 -' 1),2)) . j1) ^ <*((i + 1) -' i1)*> by A41, FUNCOP_1:7
.= <*(j1 -' 1),(((i1 -' 1) + 1) -' j1)*> ^ <*((i + 1) -' i1)*> by A47, Th14
.= <*(j1 -' 1),(i1 -' j1)*> ^ <*((i + 1) -' i1)*> by A46, XREAL_1:235
.= <*(j1 -' 1),(i1 -' j1),((i + 1) -' i1)*> by FINSEQ_1:43 ;
hence y in rng (FlattenSeq g2) by A59, A60, FUNCT_1:def_3; ::_thesis: verum
end;
assume y in rng (FlattenSeq g2) ; ::_thesis: y in rng (FlattenSeq f2)
then consider x being Nat such that
A61: x in dom (FlattenSeq g2) and
A62: (FlattenSeq g2) . x = y by FINSEQ_2:10;
consider i1, j1 being Element of NAT such that
A63: i1 in dom g2 and
A64: j1 in dom (g2 . i1) and
x = (Sum (Card (g2 | (i1 -' 1)))) + j1 and
A65: (g2 . i1) . j1 = (FlattenSeq g2) . x by A61, PRE_POLY:29;
A66: g2 . i1 = (((i + 2) -' i1) |-> <*(i1 -' 1)*>) ^^ (Decomp (((i + 1) -' i1),2)) by A5, A63;
then j1 in (dom (((i + 2) -' i1) |-> <*(i1 -' 1)*>)) /\ (dom (Decomp (((i + 1) -' i1),2))) by A64, PRE_POLY:def_4;
then j1 in dom (((i + 2) -' i1) |-> <*(i1 -' 1)*>) by XBOOLE_0:def_4;
then A67: j1 in Seg ((i + 2) -' i1) by FUNCOP_1:13;
then j1 >= 1 by FINSEQ_1:1;
then A68: j1 - 1 >= 0 by XREAL_1:48;
A69: i1 in Seg (i + 1) by A4, A63, FINSEQ_1:def_3;
then i1 <= i + 1 by FINSEQ_1:1;
then A70: (i + 1) - i1 >= 0 by XREAL_1:48;
then ((i + 1) -' i1) + 1 = ((i + 1) - i1) + 1 by XREAL_0:def_2
.= (i + (1 + 1)) - i1 ;
then A71: j1 in Seg (((i + 1) -' i1) + 1) by A67, XREAL_0:def_2;
then A72: j1 <= ((i + 1) -' i1) + 1 by FINSEQ_1:1;
then A73: (((i + 1) -' i1) + 1) - j1 >= 0 by XREAL_1:48;
j1 <= ((i + 1) - i1) + 1 by A70, A72, XREAL_0:def_2;
then j1 - 1 <= (i + 1) - i1 by XREAL_1:20;
then A74: (j1 - 1) + i1 <= i + 1 by XREAL_1:19;
then A75: (j1 -' 1) + i1 <= i + 1 by A68, XREAL_0:def_2;
(i + 1) - ((j1 - 1) + i1) >= 0 by A74, XREAL_1:48;
then (i + 1) - ((j1 -' 1) + i1) >= 0 by A68, XREAL_0:def_2;
then A76: (i + 1) -' ((j1 -' 1) + i1) = (i + 1) - ((j1 -' 1) + i1) by XREAL_0:def_2
.= (i + 1) - ((j1 - 1) + i1) by A68, XREAL_0:def_2
.= (((i + 1) - i1) + 1) - j1
.= (((i + 1) -' i1) + 1) - j1 by A70, XREAL_0:def_2
.= (((i + 1) -' i1) + 1) -' j1 by A73, XREAL_0:def_2 ;
A77: y = ((((i + 2) -' i1) |-> <*(i1 -' 1)*>) . j1) ^ ((Decomp (((i + 1) -' i1),2)) . j1) by A62, A64, A65, A66, PRE_POLY:def_4
.= <*(i1 -' 1)*> ^ ((Decomp (((i + 1) -' i1),2)) . j1) by A67, FUNCOP_1:7
.= <*(i1 -' 1)*> ^ <*(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*> by A71, Th14
.= <*(i1 -' 1),(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*> by FINSEQ_1:43 ;
set j2 = i1;
set i2 = (j1 -' 1) + i1;
A78: (j1 -' 1) + i1 >= i1 by NAT_1:11;
A79: dom (((j1 -' 1) + i1) |-> <*((i + 1) -' ((j1 -' 1) + i1))*>) = Seg ((j1 -' 1) + i1) by FUNCOP_1:13;
A80: 1 <= i1 by A69, FINSEQ_1:1;
then A81: i1 in Seg ((j1 -' 1) + i1) by A78, FINSEQ_1:1;
then A82: i1 in Seg ((((j1 -' 1) + i1) -' 1) + 1) by A80, A78, XREAL_1:235, XXREAL_0:2;
(j1 -' 1) + i1 >= 1 by A80, A78, XXREAL_0:2;
then A83: (j1 -' 1) + i1 in Seg (i + 1) by A75, FINSEQ_1:1;
then A84: f2 . ((j1 -' 1) + i1) = (Decomp ((((j1 -' 1) + i1) -' 1),2)) ^^ (((j1 -' 1) + i1) |-> <*((i + 1) -' ((j1 -' 1) + i1))*>) by A2, A3;
dom (Decomp ((((j1 -' 1) + i1) -' 1),2)) = Seg (len (Decomp ((((j1 -' 1) + i1) -' 1),2))) by FINSEQ_1:def_3
.= Seg ((((j1 -' 1) + i1) -' 1) + 1) by Th9
.= Seg ((j1 -' 1) + i1) by A80, A78, XREAL_1:235, XXREAL_0:2 ;
then dom (f2 . ((j1 -' 1) + i1)) = (Seg ((j1 -' 1) + i1)) /\ (Seg ((j1 -' 1) + i1)) by A84, A79, PRE_POLY:def_4;
then A85: i1 in dom (f2 . ((j1 -' 1) + i1)) by A80, A78, FINSEQ_1:1;
(j1 -' 1) + i1 in dom f2 by A1, A83, FINSEQ_1:def_3;
then A86: ( (Sum (Card (f2 | (((j1 -' 1) + i1) -' 1)))) + i1 in dom (FlattenSeq f2) & (f2 . ((j1 -' 1) + i1)) . i1 = (FlattenSeq f2) . ((Sum (Card (f2 | (((j1 -' 1) + i1) -' 1)))) + i1) ) by A85, PRE_POLY:30;
(f2 . ((j1 -' 1) + i1)) . i1 = ((Decomp ((((j1 -' 1) + i1) -' 1),2)) . i1) ^ ((((j1 -' 1) + i1) |-> <*((i + 1) -' ((j1 -' 1) + i1))*>) . i1) by A84, A85, PRE_POLY:def_4
.= ((Decomp ((((j1 -' 1) + i1) -' 1),2)) . i1) ^ <*((i + 1) -' ((j1 -' 1) + i1))*> by A81, FUNCOP_1:7
.= <*(i1 -' 1),(((((j1 -' 1) + i1) -' 1) + 1) -' i1)*> ^ <*((i + 1) -' ((j1 -' 1) + i1))*> by A82, Th14
.= <*(i1 -' 1),(((((j1 -' 1) + i1) -' 1) + 1) -' i1),((i + 1) -' ((j1 -' 1) + i1))*> by FINSEQ_1:43
.= <*(i1 -' 1),(((j1 -' 1) + i1) -' i1),((i + 1) -' ((j1 -' 1) + i1))*> by A80, A78, XREAL_1:235, XXREAL_0:2
.= <*(i1 -' 1),(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*> by A76, NAT_D:34 ;
hence y in rng (FlattenSeq f2) by A77, A86, FUNCT_1:def_3; ::_thesis: verum
end;
then A87: rng (FlattenSeq f2) = rng (FlattenSeq g2) by TARSKI:1;
now__::_thesis:_for_x,_y_being_set_st_x_in_dom_(FlattenSeq_g2)_&_y_in_dom_(FlattenSeq_g2)_&_(FlattenSeq_g2)_._x_=_(FlattenSeq_g2)_._y_holds_
x_=_y
A88: (i + 1) + 1 >= i + 1 by NAT_1:11;
let x, y be set ; ::_thesis: ( x in dom (FlattenSeq g2) & y in dom (FlattenSeq g2) & (FlattenSeq g2) . x = (FlattenSeq g2) . y implies x = y )
assume that
A89: x in dom (FlattenSeq g2) and
A90: y in dom (FlattenSeq g2) and
A91: (FlattenSeq g2) . x = (FlattenSeq g2) . y ; ::_thesis: x = y
consider i1, j1 being Element of NAT such that
A92: i1 in dom g2 and
A93: j1 in dom (g2 . i1) and
A94: x = (Sum (Card (g2 | (i1 -' 1)))) + j1 and
A95: (g2 . i1) . j1 = (FlattenSeq g2) . x by A89, PRE_POLY:29;
A96: g2 . i1 = (((i + 2) -' i1) |-> <*(i1 -' 1)*>) ^^ (Decomp (((i + 1) -' i1),2)) by A5, A92;
i1 in Seg (i + 1) by A4, A92, FINSEQ_1:def_3;
then A97: i1 <= i + 1 by FINSEQ_1:1;
then (i + 1) + 1 >= i1 by A88, XXREAL_0:2;
then A98: (i + 2) - i1 >= 0 by XREAL_1:48;
(i + 1) - i1 >= 0 by A97, XREAL_1:48;
then A99: ((i + 1) -' i1) + 1 = ((i + 1) - i1) + 1 by XREAL_0:def_2
.= (i + 2) -' i1 by A98, XREAL_0:def_2 ;
A100: dom (((i + 2) -' i1) |-> <*(i1 -' 1)*>) = Seg ((i + 2) -' i1) by FUNCOP_1:13;
dom (Decomp (((i + 1) -' i1),2)) = Seg (len (Decomp (((i + 1) -' i1),2))) by FINSEQ_1:def_3
.= Seg ((i + 2) -' i1) by A99, Th9 ;
then A101: dom (g2 . i1) = (Seg ((i + 2) -' i1)) /\ (Seg ((i + 2) -' i1)) by A96, A100, PRE_POLY:def_4
.= Seg ((i + 2) -' i1) ;
j1 in Seg (len (g2 . i1)) by A93, FINSEQ_1:def_3;
then A102: j1 >= 1 by FINSEQ_1:1;
consider i2, j2 being Element of NAT such that
A103: i2 in dom g2 and
A104: j2 in dom (g2 . i2) and
A105: y = (Sum (Card (g2 | (i2 -' 1)))) + j2 and
A106: (g2 . i2) . j2 = (FlattenSeq g2) . y by A90, PRE_POLY:29;
A107: g2 . i2 = (((i + 2) -' i2) |-> <*(i2 -' 1)*>) ^^ (Decomp (((i + 1) -' i2),2)) by A5, A103;
i2 in Seg (i + 1) by A4, A103, FINSEQ_1:def_3;
then A108: i2 <= i + 1 by FINSEQ_1:1;
then (i + 1) + 1 >= i2 by A88, XXREAL_0:2;
then A109: (i + 2) - i2 >= 0 by XREAL_1:48;
(i + 1) - i2 >= 0 by A108, XREAL_1:48;
then A110: ((i + 1) -' i2) + 1 = ((i + 1) - i2) + 1 by XREAL_0:def_2
.= (i + 2) -' i2 by A109, XREAL_0:def_2 ;
A111: dom (((i + 2) -' i2) |-> <*(i2 -' 1)*>) = Seg ((i + 2) -' i2) by FUNCOP_1:13;
dom (Decomp (((i + 1) -' i2),2)) = Seg (len (Decomp (((i + 1) -' i2),2))) by FINSEQ_1:def_3
.= Seg ((i + 2) -' i2) by A110, Th9 ;
then A112: dom (g2 . i2) = (Seg ((i + 2) -' i2)) /\ (Seg ((i + 2) -' i2)) by A107, A111, PRE_POLY:def_4
.= Seg ((i + 2) -' i2) ;
A113: (g2 . i2) . j2 = ((((i + 2) -' i2) |-> <*(i2 -' 1)*>) . j2) ^ ((Decomp (((i + 1) -' i2),2)) . j2) by A104, A107, PRE_POLY:def_4
.= <*(i2 -' 1)*> ^ ((Decomp (((i + 1) -' i2),2)) . j2) by A104, A112, FUNCOP_1:7
.= <*(i2 -' 1)*> ^ <*(j2 -' 1),((((i + 1) -' i2) + 1) -' j2)*> by A104, A110, A112, Th14
.= <*(i2 -' 1),(j2 -' 1),((((i + 1) -' i2) + 1) -' j2)*> by FINSEQ_1:43 ;
j2 in Seg (len (g2 . i2)) by A104, FINSEQ_1:def_3;
then A114: j2 >= 1 by FINSEQ_1:1;
(g2 . i1) . j1 = ((((i + 2) -' i1) |-> <*(i1 -' 1)*>) . j1) ^ ((Decomp (((i + 1) -' i1),2)) . j1) by A93, A96, PRE_POLY:def_4
.= <*(i1 -' 1)*> ^ ((Decomp (((i + 1) -' i1),2)) . j1) by A93, A101, FUNCOP_1:7
.= <*(i1 -' 1)*> ^ <*(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*> by A93, A99, A101, Th14
.= <*(i1 -' 1),(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*> by FINSEQ_1:43 ;
then ( i1 -' 1 = i2 -' 1 & j1 -' 1 = j2 -' 1 ) by A91, A95, A106, A113, FINSEQ_1:78;
hence x = y by A94, A105, A102, A114, XREAL_1:234; ::_thesis: verum
end;
then A115: FlattenSeq g2 is one-to-one by FUNCT_1:def_4;
len (FlattenSeq f2) = Sum (Card f2) by PRE_POLY:27
.= Sum w by A33, Th3
.= len (FlattenSeq g2) by PRE_POLY:27 ;
then FlattenSeq f2 is one-to-one by A87, A115, FINSEQ_4:61;
then FlattenSeq f2, FlattenSeq g2 are_fiberwise_equipotent by A87, A115, RFINSEQ:26;
then consider P being Permutation of (dom (FlattenSeq g2)) such that
A116: FlattenSeq f2 = (FlattenSeq g2) * P by RFINSEQ:4;
A117: dom (Card g2) = dom g2 by CARD_3:def_2;
then A118: len (Card g2) = len g2 by FINSEQ_3:29;
consider r1 being FinSequence of the carrier of L such that
A119: len r1 = i + 1 and
A120: ((p *' q) *' r) . i = Sum r1 and
A121: for k being Element of NAT st k in dom r1 holds
r1 . k = ((p *' q) . (k -' 1)) * (r . ((i + 1) -' k)) by Def9;
A122: dom r1 = Seg (i + 1) by A119, FINSEQ_1:def_3;
deffunc H3( Nat) -> Element of the carrier of L * = prodTuples (p,q,r,(f2 /. $1));
consider f1 being FinSequence of the carrier of L * such that
A123: len f1 = len f2 and
A124: for k being Nat st k in dom f1 holds
f1 . k = H3(k) from FINSEQ_2:sch_1();
A125: dom f1 = Seg (len f2) by A123, FINSEQ_1:def_3;
A126: now__::_thesis:_for_j_being_Nat_st_j_in_dom_r1_holds_
r1_._j_=_(Sum_f1)_._j
let j be Nat; ::_thesis: ( j in dom r1 implies r1 . j = (Sum f1) . j )
A127: dom (j |-> <*((i + 1) -' j)*>) = Seg j by FUNCOP_1:13;
consider r3 being FinSequence of the carrier of L such that
A128: len r3 = (j -' 1) + 1 and
A129: (p *' q) . (j -' 1) = Sum r3 and
A130: for k being Element of NAT st k in dom r3 holds
r3 . k = (p . (k -' 1)) * (q . (((j -' 1) + 1) -' k)) by Def9;
assume A131: j in dom r1 ; ::_thesis: r1 . j = (Sum f1) . j
then A132: 1 <= j by A122, FINSEQ_1:1;
then A133: len r3 = j by A128, XREAL_1:235;
len (Decomp ((j -' 1),2)) = (j -' 1) + 1 by Th9
.= j by A132, XREAL_1:235 ;
then A134: dom (Decomp ((j -' 1),2)) = Seg j by FINSEQ_1:def_3;
A135: dom r1 = dom f1 by A119, A1, A123, FINSEQ_3:29;
then A136: f1 /. j = f1 . j by A131, PARTFUN1:def_6
.= prodTuples (p,q,r,(f2 /. j)) by A1, A124, A125, A122, A131 ;
dom f1 = dom f2 by A123, FINSEQ_3:29;
then A137: f2 /. j = f2 . j by A131, A135, PARTFUN1:def_6
.= (Decomp ((j -' 1),2)) ^^ (j |-> <*((i + 1) -' j)*>) by A2, A3, A122, A131 ;
then A138: dom (f2 /. j) = (dom (Decomp ((j -' 1),2))) /\ (dom (j |-> <*((i + 1) -' j)*>)) by PRE_POLY:def_4
.= Seg j by A134, A127 ;
A139: len (prodTuples (p,q,r,(f2 /. j))) = len (f2 /. j) by Def5
.= j by A131, A138, FINSEQ_1:def_3 ;
then A140: dom (prodTuples (p,q,r,(f2 /. j))) = Seg j by FINSEQ_1:def_3;
A141: dom (r3 * (r . ((i + 1) -' j))) = dom r3 by POLYNOM1:def_2;
A142: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(prodTuples_(p,q,r,(f2_/._j)))_holds_
(prodTuples_(p,q,r,(f2_/._j)))_._k_=_(r3_*_(r_._((i_+_1)_-'_j)))_._k
let k be Nat; ::_thesis: ( k in dom (prodTuples (p,q,r,(f2 /. j))) implies (prodTuples (p,q,r,(f2 /. j))) . k = (r3 * (r . ((i + 1) -' j))) . k )
assume A143: k in dom (prodTuples (p,q,r,(f2 /. j))) ; ::_thesis: (prodTuples (p,q,r,(f2 /. j))) . k = (r3 * (r . ((i + 1) -' j))) . k
then A144: (f2 /. j) /. k = (f2 /. j) . k by A138, A140, PARTFUN1:def_6
.= ((Decomp ((j -' 1),2)) . k) ^ ((j |-> <*((i + 1) -' j)*>) . k) by A137, A138, A140, A143, PRE_POLY:def_4
.= <*(k -' 1),(((j -' 1) + 1) -' k)*> ^ ((j |-> <*((i + 1) -' j)*>) . k) by A128, A133, A140, A143, Th14
.= <*(k -' 1),(((j -' 1) + 1) -' k)*> ^ <*((i + 1) -' j)*> by A140, A143, FUNCOP_1:7
.= <*(k -' 1),(((j -' 1) + 1) -' k),((i + 1) -' j)*> by FINSEQ_1:43 ;
1 in Seg 3 by ENUMSET1:def_1, FINSEQ_3:1;
then 1 in Seg (len ((f2 /. j) /. k)) by A144, FINSEQ_1:45;
then 1 in dom ((f2 /. j) /. k) by FINSEQ_1:def_3;
then A145: ((f2 /. j) /. k) /. 1 = ((f2 /. j) /. k) . 1 by PARTFUN1:def_6
.= k -' 1 by A144, FINSEQ_1:45 ;
A146: k in dom r3 by A133, A140, A143, FINSEQ_1:def_3;
then A147: r3 /. k = r3 . k by PARTFUN1:def_6
.= (p . (k -' 1)) * (q . (((j -' 1) + 1) -' k)) by A130, A146 ;
3 in Seg 3 by ENUMSET1:def_1, FINSEQ_3:1;
then 3 in Seg (len ((f2 /. j) /. k)) by A144, FINSEQ_1:45;
then 3 in dom ((f2 /. j) /. k) by FINSEQ_1:def_3;
then A148: ((f2 /. j) /. k) /. 3 = ((f2 /. j) /. k) . 3 by PARTFUN1:def_6
.= (i + 1) -' j by A144, FINSEQ_1:45 ;
2 in Seg 3 by ENUMSET1:def_1, FINSEQ_3:1;
then 2 in Seg (len ((f2 /. j) /. k)) by A144, FINSEQ_1:45;
then 2 in dom ((f2 /. j) /. k) by FINSEQ_1:def_3;
then A149: ((f2 /. j) /. k) /. 2 = ((f2 /. j) /. k) . 2 by PARTFUN1:def_6
.= ((j -' 1) + 1) -' k by A144, FINSEQ_1:45 ;
thus (prodTuples (p,q,r,(f2 /. j))) . k = ((p . (((f2 /. j) /. k) /. 1)) * (q . (((f2 /. j) /. k) /. 2))) * (r . (((f2 /. j) /. k) /. 3)) by A138, A140, A143, Def5
.= (r3 * (r . ((i + 1) -' j))) /. k by A146, A147, A145, A149, A148, POLYNOM1:def_2
.= (r3 * (r . ((i + 1) -' j))) . k by A141, A146, PARTFUN1:def_6 ; ::_thesis: verum
end;
len f1 = len (Sum f1) by MATRLIN:def_6;
then A150: dom f1 = dom (Sum f1) by FINSEQ_3:29;
len (r3 * (r . ((i + 1) -' j))) = len r3 by A141, FINSEQ_3:29;
then A151: prodTuples (p,q,r,(f2 /. j)) = r3 * (r . ((i + 1) -' j)) by A139, A133, A142, FINSEQ_2:9;
((p *' q) . (j -' 1)) * (r . ((i + 1) -' j)) = Sum (r3 * (r . ((i + 1) -' j))) by A129, POLYNOM1:13;
hence r1 . j = Sum (r3 * (r . ((i + 1) -' j))) by A121, A131
.= (Sum f1) /. j by A131, A150, A135, A136, A151, MATRLIN:def_6
.= (Sum f1) . j by A131, A150, A135, PARTFUN1:def_6 ;
::_thesis: verum
end;
deffunc H4( Nat) -> Element of the carrier of L * = prodTuples (p,q,r,(g2 /. $1));
consider g1 being FinSequence of the carrier of L * such that
A152: len g1 = len g2 and
A153: for k being Nat st k in dom g1 holds
g1 . k = H4(k) from FINSEQ_2:sch_1();
A154: dom g1 = Seg (len g2) by A152, FINSEQ_1:def_3;
A155: now__::_thesis:_for_j_being_Nat_st_j_in_dom_r2_holds_
r2_._j_=_(Sum_g1)_._j
let j be Nat; ::_thesis: ( j in dom r2 implies r2 . j = (Sum g1) . j )
A156: dom (((i + 2) -' j) |-> <*(j -' 1)*>) = Seg ((i + 2) -' j) by FUNCOP_1:13;
consider r3 being FinSequence of the carrier of L such that
A157: len r3 = ((i + 1) -' j) + 1 and
A158: (q *' r) . ((i + 1) -' j) = Sum r3 and
A159: for k being Element of NAT st k in dom r3 holds
r3 . k = (q . (k -' 1)) * (r . ((((i + 1) -' j) + 1) -' k)) by Def9;
assume A160: j in dom r2 ; ::_thesis: r2 . j = (Sum g1) . j
then A161: j <= i + 1 by A10, FINSEQ_1:1;
(i + 1) + 1 >= i + 1 by NAT_1:11;
then (i + 1) + 1 >= j by A161, XXREAL_0:2;
then A162: (i + 2) - j >= 0 by XREAL_1:48;
(i + 1) - j >= 0 by A161, XREAL_1:48;
then A163: ((i + 1) -' j) + 1 = ((i + 1) - j) + 1 by XREAL_0:def_2
.= (i + 2) -' j by A162, XREAL_0:def_2 ;
then len (Decomp (((i + 1) -' j),2)) = (i + 2) -' j by Th9;
then A164: dom (Decomp (((i + 1) -' j),2)) = Seg ((i + 2) -' j) by FINSEQ_1:def_3;
A165: dom r2 = dom g1 by A7, A4, A152, FINSEQ_3:29;
then A166: g1 /. j = g1 . j by A160, PARTFUN1:def_6
.= prodTuples (p,q,r,(g2 /. j)) by A4, A153, A154, A10, A160 ;
dom g1 = dom g2 by A152, FINSEQ_3:29;
then A167: g2 /. j = g2 . j by A160, A165, PARTFUN1:def_6
.= (((i + 2) -' j) |-> <*(j -' 1)*>) ^^ (Decomp (((i + 1) -' j),2)) by A5, A6, A10, A160 ;
then A168: dom (g2 /. j) = (dom (((i + 2) -' j) |-> <*(j -' 1)*>)) /\ (dom (Decomp (((i + 1) -' j),2))) by PRE_POLY:def_4
.= Seg ((i + 2) -' j) by A164, A156 ;
A169: len (prodTuples (p,q,r,(g2 /. j))) = len (g2 /. j) by Def5
.= (i + 2) -' j by A168, FINSEQ_1:def_3 ;
then A170: dom (prodTuples (p,q,r,(g2 /. j))) = Seg ((i + 2) -' j) by FINSEQ_1:def_3;
A171: dom ((p . (j -' 1)) * r3) = dom r3 by POLYNOM1:def_1;
A172: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(prodTuples_(p,q,r,(g2_/._j)))_holds_
(prodTuples_(p,q,r,(g2_/._j)))_._k_=_((p_._(j_-'_1))_*_r3)_._k
let k be Nat; ::_thesis: ( k in dom (prodTuples (p,q,r,(g2 /. j))) implies (prodTuples (p,q,r,(g2 /. j))) . k = ((p . (j -' 1)) * r3) . k )
assume A173: k in dom (prodTuples (p,q,r,(g2 /. j))) ; ::_thesis: (prodTuples (p,q,r,(g2 /. j))) . k = ((p . (j -' 1)) * r3) . k
then A174: (g2 /. j) /. k = (g2 /. j) . k by A168, A170, PARTFUN1:def_6
.= ((((i + 2) -' j) |-> <*(j -' 1)*>) . k) ^ ((Decomp (((i + 1) -' j),2)) . k) by A167, A168, A170, A173, PRE_POLY:def_4
.= ((((i + 2) -' j) |-> <*(j -' 1)*>) . k) ^ <*(k -' 1),((((i + 1) -' j) + 1) -' k)*> by A163, A170, A173, Th14
.= <*(j -' 1)*> ^ <*(k -' 1),((((i + 1) -' j) + 1) -' k)*> by A170, A173, FUNCOP_1:7
.= <*(j -' 1),(k -' 1),((((i + 1) -' j) + 1) -' k)*> by FINSEQ_1:43 ;
1 in Seg 3 by ENUMSET1:def_1, FINSEQ_3:1;
then 1 in Seg (len ((g2 /. j) /. k)) by A174, FINSEQ_1:45;
then 1 in dom ((g2 /. j) /. k) by FINSEQ_1:def_3;
then A175: ((g2 /. j) /. k) /. 1 = ((g2 /. j) /. k) . 1 by PARTFUN1:def_6
.= j -' 1 by A174, FINSEQ_1:45 ;
A176: k in dom r3 by A157, A163, A170, A173, FINSEQ_1:def_3;
then A177: r3 /. k = r3 . k by PARTFUN1:def_6
.= (q . (k -' 1)) * (r . ((((i + 1) -' j) + 1) -' k)) by A159, A176 ;
3 in Seg 3 by ENUMSET1:def_1, FINSEQ_3:1;
then 3 in Seg (len ((g2 /. j) /. k)) by A174, FINSEQ_1:45;
then 3 in dom ((g2 /. j) /. k) by FINSEQ_1:def_3;
then A178: ((g2 /. j) /. k) /. 3 = ((g2 /. j) /. k) . 3 by PARTFUN1:def_6
.= (((i + 1) -' j) + 1) -' k by A174, FINSEQ_1:45 ;
2 in Seg 3 by ENUMSET1:def_1, FINSEQ_3:1;
then 2 in Seg (len ((g2 /. j) /. k)) by A174, FINSEQ_1:45;
then 2 in dom ((g2 /. j) /. k) by FINSEQ_1:def_3;
then A179: ((g2 /. j) /. k) /. 2 = ((g2 /. j) /. k) . 2 by PARTFUN1:def_6
.= k -' 1 by A174, FINSEQ_1:45 ;
thus (prodTuples (p,q,r,(g2 /. j))) . k = ((p . (((g2 /. j) /. k) /. 1)) * (q . (((g2 /. j) /. k) /. 2))) * (r . (((g2 /. j) /. k) /. 3)) by A168, A170, A173, Def5
.= (p . (((g2 /. j) /. k) /. 1)) * ((q . (((g2 /. j) /. k) /. 2)) * (r . (((g2 /. j) /. k) /. 3))) by GROUP_1:def_3
.= ((p . (j -' 1)) * r3) /. k by A176, A177, A175, A179, A178, POLYNOM1:def_1
.= ((p . (j -' 1)) * r3) . k by A171, A176, PARTFUN1:def_6 ; ::_thesis: verum
end;
len g1 = len (Sum g1) by MATRLIN:def_6;
then A180: dom g1 = dom (Sum g1) by FINSEQ_3:29;
len ((p . (j -' 1)) * r3) = len r3 by A171, FINSEQ_3:29;
then A181: prodTuples (p,q,r,(g2 /. j)) = (p . (j -' 1)) * r3 by A157, A163, A169, A172, FINSEQ_2:9;
(p . (j -' 1)) * ((q *' r) . ((i + 1) -' j)) = Sum ((p . (j -' 1)) * r3) by A158, POLYNOM1:12;
hence r2 . j = Sum ((p . (j -' 1)) * r3) by A9, A160
.= (Sum g1) /. j by A160, A180, A165, A166, A181, MATRLIN:def_6
.= (Sum g1) . j by A160, A180, A165, PARTFUN1:def_6 ;
::_thesis: verum
end;
A182: dom (Card g2) = Seg (i + 1) by A4, A117, FINSEQ_1:def_3;
A183: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(Card_g2)_holds_
(Card_g2)_._j_=_(Card_g1)_._j
let j be Nat; ::_thesis: ( j in dom (Card g2) implies (Card g2) . j = (Card g1) . j )
assume A184: j in dom (Card g2) ; ::_thesis: (Card g2) . j = (Card g1) . j
then A185: j in dom g1 by A4, A152, A182, FINSEQ_1:def_3;
g1 . j = prodTuples (p,q,r,(g2 /. j)) by A4, A153, A154, A182, A184;
then A186: len (g1 . j) = len (g2 /. j) by Def5
.= len (g2 . j) by A117, A184, PARTFUN1:def_6 ;
thus (Card g2) . j = len (g2 . j) by A117, A184, CARD_3:def_2
.= (Card g1) . j by A185, A186, CARD_3:def_2 ; ::_thesis: verum
end;
A187: dom (Card g1) = dom g1 by CARD_3:def_2;
then len (Card g1) = len g1 by FINSEQ_3:29;
then A188: Card g2 = Card g1 by A152, A118, A183, FINSEQ_2:9;
then A189: len (FlattenSeq g2) = len (FlattenSeq g1) by PRE_POLY:28;
then A190: dom (FlattenSeq g2) = dom (FlattenSeq g1) by FINSEQ_3:29;
then reconsider P = P as Permutation of (dom (FlattenSeq g1)) ;
A191: dom (FlattenSeq g1) = Seg (len (FlattenSeq g1)) by FINSEQ_1:def_3;
A192: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(FlattenSeq_g1)_holds_
(FlattenSeq_g1)_._j_=_(prodTuples_(p,q,r,(FlattenSeq_g2)))_._j
let j be Nat; ::_thesis: ( j in dom (FlattenSeq g1) implies (FlattenSeq g1) . j = (prodTuples (p,q,r,(FlattenSeq g2))) . j )
assume A193: j in dom (FlattenSeq g1) ; ::_thesis: (FlattenSeq g1) . j = (prodTuples (p,q,r,(FlattenSeq g2))) . j
then consider i1, j1 being Element of NAT such that
A194: i1 in dom g1 and
A195: j1 in dom (g1 . i1) and
A196: j = (Sum (Card (g1 | (i1 -' 1)))) + j1 and
A197: (g1 . i1) . j1 = (FlattenSeq g1) . j by PRE_POLY:29;
A198: j in dom (FlattenSeq g2) by A189, A191, A193, FINSEQ_1:def_3;
then consider i2, j2 being Element of NAT such that
A199: ( i2 in dom g2 & j2 in dom (g2 . i2) ) and
A200: j = (Sum (Card (g2 | (i2 -' 1)))) + j2 and
A201: (g2 . i2) . j2 = (FlattenSeq g2) . j by PRE_POLY:29;
(Sum ((Card g1) | (i1 -' 1))) + j1 = (Sum (Card (g1 | (i1 -' 1)))) + j1 by Th16
.= (Sum ((Card g2) | (i2 -' 1))) + j2 by A196, A200, Th16 ;
then A202: ( i1 = i2 & j1 = j2 ) by A188, A194, A195, A199, Th22;
i1 in Seg (len g2) by A152, A194, FINSEQ_1:def_3;
then A203: i1 in dom g2 by FINSEQ_1:def_3;
A204: g1 . i1 = prodTuples (p,q,r,(g2 /. i1)) by A153, A194;
then len (g1 . i1) = len (g2 /. i1) by Def5
.= len (g2 . i1) by A187, A117, A188, A194, PARTFUN1:def_6 ;
then j1 in Seg (len (g2 . i1)) by A195, FINSEQ_1:def_3;
then A205: j1 in Seg (len (g2 /. i1)) by A203, PARTFUN1:def_6;
then j1 in dom (g2 /. i1) by FINSEQ_1:def_3;
then A206: (g2 /. i1) /. j1 = (g2 /. i1) . j1 by PARTFUN1:def_6
.= (g2 . i1) . j1 by A203, PARTFUN1:def_6
.= (FlattenSeq g2) /. j by A198, A201, A202, PARTFUN1:def_6 ;
Seg (len (g2 /. i1)) = dom (g2 /. i1) by FINSEQ_1:def_3;
hence (FlattenSeq g1) . j = ((p . (((g2 /. i1) /. j1) /. 1)) * (q . (((g2 /. i1) /. j1) /. 2))) * (r . (((g2 /. i1) /. j1) /. 3)) by A197, A204, A205, Def5
.= (prodTuples (p,q,r,(FlattenSeq g2))) . j by A190, A193, A206, Def5 ;
::_thesis: verum
end;
A207: dom (Card f2) = dom f2 by CARD_3:def_2;
then A208: len (Card f2) = len f2 by FINSEQ_3:29;
A209: dom (Card f2) = Seg (i + 1) by A1, A207, FINSEQ_1:def_3;
A210: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(Card_f2)_holds_
(Card_f2)_._j_=_(Card_f1)_._j
let j be Nat; ::_thesis: ( j in dom (Card f2) implies (Card f2) . j = (Card f1) . j )
assume A211: j in dom (Card f2) ; ::_thesis: (Card f2) . j = (Card f1) . j
then A212: j in dom f1 by A1, A123, A209, FINSEQ_1:def_3;
f1 . j = prodTuples (p,q,r,(f2 /. j)) by A1, A124, A125, A209, A211;
then A213: len (f1 . j) = len (f2 /. j) by Def5
.= len (f2 . j) by A207, A211, PARTFUN1:def_6 ;
thus (Card f2) . j = len (f2 . j) by A207, A211, CARD_3:def_2
.= (Card f1) . j by A212, A213, CARD_3:def_2 ; ::_thesis: verum
end;
A214: dom (Card f1) = dom f1 by CARD_3:def_2;
then len (Card f1) = len f1 by FINSEQ_3:29;
then A215: Card f2 = Card f1 by A123, A208, A210, FINSEQ_2:9;
then A216: len (FlattenSeq f1) = len (FlattenSeq f2) by PRE_POLY:28;
A217: Seg (len (FlattenSeq f1)) = dom (FlattenSeq f1) by FINSEQ_1:def_3;
A218: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(FlattenSeq_f1)_holds_
(FlattenSeq_f1)_._j_=_(prodTuples_(p,q,r,(FlattenSeq_f2)))_._j
let j be Nat; ::_thesis: ( j in dom (FlattenSeq f1) implies (FlattenSeq f1) . j = (prodTuples (p,q,r,(FlattenSeq f2))) . j )
assume A219: j in dom (FlattenSeq f1) ; ::_thesis: (FlattenSeq f1) . j = (prodTuples (p,q,r,(FlattenSeq f2))) . j
then consider i1, j1 being Element of NAT such that
A220: i1 in dom f1 and
A221: j1 in dom (f1 . i1) and
A222: j = (Sum (Card (f1 | (i1 -' 1)))) + j1 and
A223: (f1 . i1) . j1 = (FlattenSeq f1) . j by PRE_POLY:29;
A224: j in dom (FlattenSeq f2) by A216, A34, A219, FINSEQ_1:def_3;
then consider i2, j2 being Element of NAT such that
A225: ( i2 in dom f2 & j2 in dom (f2 . i2) ) and
A226: j = (Sum (Card (f2 | (i2 -' 1)))) + j2 and
A227: (f2 . i2) . j2 = (FlattenSeq f2) . j by PRE_POLY:29;
(Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum (Card (f1 | (i1 -' 1)))) + j1 by Th16
.= (Sum ((Card f2) | (i2 -' 1))) + j2 by A222, A226, Th16 ;
then A228: ( i1 = i2 & j1 = j2 ) by A215, A220, A221, A225, Th22;
i1 in Seg (len f2) by A123, A220, FINSEQ_1:def_3;
then A229: i1 in dom f2 by FINSEQ_1:def_3;
A230: f1 . i1 = prodTuples (p,q,r,(f2 /. i1)) by A124, A220;
then len (f1 . i1) = len (f2 /. i1) by Def5
.= len (f2 . i1) by A214, A207, A215, A220, PARTFUN1:def_6 ;
then j1 in Seg (len (f2 . i1)) by A221, FINSEQ_1:def_3;
then A231: j1 in Seg (len (f2 /. i1)) by A229, PARTFUN1:def_6;
then j1 in dom (f2 /. i1) by FINSEQ_1:def_3;
then A232: (f2 /. i1) /. j1 = (f2 /. i1) . j1 by PARTFUN1:def_6
.= (f2 . i1) . j1 by A229, PARTFUN1:def_6
.= (FlattenSeq f2) /. j by A224, A227, A228, PARTFUN1:def_6 ;
Seg (len (f2 /. i1)) = dom (f2 /. i1) by FINSEQ_1:def_3;
hence (FlattenSeq f1) . j = ((p . (((f2 /. i1) /. j1) /. 1)) * (q . (((f2 /. i1) /. j1) /. 2))) * (r . (((f2 /. i1) /. j1) /. 3)) by A223, A230, A231, Def5
.= ((p . (((FlattenSeq f2) /. j) /. 1)) * (q . (((FlattenSeq f2) /. j) /. 2))) * (r . (((FlattenSeq f2) /. j) /. 3)) by A232
.= (prodTuples (p,q,r,(FlattenSeq f2))) . j by A216, A34, A217, A219, Def5 ;
::_thesis: verum
end;
len (Sum g1) = i + 1 by A4, A152, MATRLIN:def_6;
then r2 = Sum g1 by A7, A155, FINSEQ_2:9;
then A233: Sum r2 = Sum (FlattenSeq g1) by POLYNOM1:14;
len (FlattenSeq g1) = len (prodTuples (p,q,r,(FlattenSeq g2))) by A189, Def5;
then A234: FlattenSeq g1 = prodTuples (p,q,r,(FlattenSeq g2)) by A192, FINSEQ_2:9;
len (FlattenSeq f1) = len (prodTuples (p,q,r,(FlattenSeq f2))) by A216, Def5;
then FlattenSeq f1 = prodTuples (p,q,r,(FlattenSeq f2)) by A218, FINSEQ_2:9;
then A235: FlattenSeq f1 = (FlattenSeq g1) * P by A234, A116, Th15;
len (Sum f1) = i + 1 by A1, A123, MATRLIN:def_6;
then r1 = Sum f1 by A119, A126, FINSEQ_2:9;
then Sum r1 = Sum (FlattenSeq f1) by POLYNOM1:14;
hence ((p *' q) *' r) . i = (p *' (q *' r)) . i by A120, A8, A233, A235, RLVECT_2:7; ::_thesis: verum
end;
hence (p *' q) *' r = p *' (q *' r) by FUNCT_2:63; ::_thesis: verum
end;
definition
let L be non empty commutative Abelian add-associative right_zeroed doubleLoopStr ;
let p, q be sequence of L;
:: original: *'
redefine funcp *' q -> sequence of L;
commutativity
for p, q being sequence of L holds p *' q = q *' p
proof
let p, q be sequence of L; ::_thesis: p *' q = q *' p
now__::_thesis:_for_i_being_Element_of_NAT_holds_(p_*'_q)_._i_=_(q_*'_p)_._i
let i be Element of NAT ; ::_thesis: (p *' q) . i = (q *' p) . i
consider r1 being FinSequence of the carrier of L such that
A1: len r1 = i + 1 and
A2: (p *' q) . i = Sum r1 and
A3: for k being Element of NAT st k in dom r1 holds
r1 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by Def9;
consider r2 being FinSequence of the carrier of L such that
A4: len r2 = i + 1 and
A5: (q *' p) . i = Sum r2 and
A6: for k being Element of NAT st k in dom r2 holds
r2 . k = (q . (k -' 1)) * (p . ((i + 1) -' k)) by Def9;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_r1_holds_
r1_._k_=_r2_._(((len_r2)_-_k)_+_1)
let k be Nat; ::_thesis: ( k in dom r1 implies r1 . k = r2 . (((len r2) - k) + 1) )
assume A7: k in dom r1 ; ::_thesis: r1 . k = r2 . (((len r2) - k) + 1)
then A8: 1 <= k by FINSEQ_3:25;
then A9: k - 1 >= 0 by XREAL_1:48;
k <= i + 1 by A1, A7, FINSEQ_3:25;
then A10: (i + 1) - k >= 0 by XREAL_1:48;
then reconsider k1 = ((len r2) - k) + 1 as Element of NAT by A4, INT_1:3;
A11: (i + 1) -' k = (((i + 1) - k) + 1) - 1 by A10, XREAL_0:def_2
.= k1 -' 1 by A4, A10, XREAL_0:def_2 ;
1 - k <= 0 by A8, XREAL_1:47;
then i + (1 - k) <= i + 0 by XREAL_1:6;
then A12: k1 <= i + 1 by A4, XREAL_1:6;
then (i + 1) - k1 >= 0 by XREAL_1:48;
then A13: (i + 1) -' k1 = (i + 1) - ((i + 1) - (k - 1)) by A4, XREAL_0:def_2
.= k -' 1 by A9, XREAL_0:def_2 ;
((i + 1) - k) + 1 >= 0 + 1 by A10, XREAL_1:6;
then A14: k1 in dom r2 by A4, A12, FINSEQ_3:25;
thus r1 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A3, A7
.= r2 . (((len r2) - k) + 1) by A6, A14, A13, A11 ; ::_thesis: verum
end;
then r1 = Rev r2 by A1, A4, FINSEQ_5:def_3;
hence (p *' q) . i = (q *' p) . i by A2, A5, Th2; ::_thesis: verum
end;
hence p *' q = q *' p by FUNCT_2:63; ::_thesis: verum
end;
end;
theorem :: POLYNOM3:34
for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for p being sequence of L holds p *' (0_. L) = 0_. L
proof
let L be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being sequence of L holds p *' (0_. L) = 0_. L
let p be sequence of L; ::_thesis: p *' (0_. L) = 0_. L
now__::_thesis:_for_i_being_Element_of_NAT_holds_(p_*'_(0_._L))_._i_=_(0_._L)_._i
let i be Element of NAT ; ::_thesis: (p *' (0_. L)) . i = (0_. L) . i
consider r being FinSequence of the carrier of L such that
len r = i + 1 and
A1: (p *' (0_. L)) . i = Sum r and
A2: for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * ((0_. L) . ((i + 1) -' k)) by Def9;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_r_holds_
r_._k_=_0._L
let k be Element of NAT ; ::_thesis: ( k in dom r implies r . k = 0. L )
assume k in dom r ; ::_thesis: r . k = 0. L
hence r . k = (p . (k -' 1)) * ((0_. L) . ((i + 1) -' k)) by A2
.= (p . (k -' 1)) * (0. L) by FUNCOP_1:7
.= 0. L by VECTSP_1:6 ;
::_thesis: verum
end;
hence (p *' (0_. L)) . i = 0. L by A1, Th1
.= (0_. L) . i by FUNCOP_1:7 ;
::_thesis: verum
end;
hence p *' (0_. L) = 0_. L by FUNCT_2:63; ::_thesis: verum
end;
theorem Th35: :: POLYNOM3:35
for L being non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr
for p being sequence of L holds p *' (1_. L) = p
proof
let L be non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being sequence of L holds p *' (1_. L) = p
let p be sequence of L; ::_thesis: p *' (1_. L) = p
now__::_thesis:_for_i_being_Element_of_NAT_holds_(p_*'_(1_._L))_._i_=_p_._i
let i be Element of NAT ; ::_thesis: (p *' (1_. L)) . i = p . i
consider r being FinSequence of the carrier of L such that
A1: len r = i + 1 and
A2: (p *' (1_. L)) . i = Sum r and
A3: for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * ((1_. L) . ((i + 1) -' k)) by Def9;
i + 1 in Seg (len r) by A1, FINSEQ_1:4;
then A4: i + 1 in dom r by FINSEQ_1:def_3;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_(Del_(r,(i_+_1)))_holds_
(Del_(r,(i_+_1)))_._k_=_0._L
let k be Element of NAT ; ::_thesis: ( k in dom (Del (r,(i + 1))) implies (Del (r,(i + 1))) . k = 0. L )
assume k in dom (Del (r,(i + 1))) ; ::_thesis: (Del (r,(i + 1))) . k = 0. L
then A5: k in Seg (len (Del (r,(i + 1)))) by FINSEQ_1:def_3;
then k in Seg i by A1, PRE_POLY:12;
then A6: k <= i by FINSEQ_1:1;
then A7: k < i + 1 by NAT_1:13;
A8: (i + 1) - k <> 0 by A6, NAT_1:13;
(i + 1) - k >= 0 by A7, XREAL_1:48;
then A9: (i + 1) -' k <> 0 by A8, XREAL_0:def_2;
1 <= k by A5, FINSEQ_1:1;
then k in Seg (i + 1) by A7, FINSEQ_1:1;
then A10: k in dom r by A1, FINSEQ_1:def_3;
thus (Del (r,(i + 1))) . k = r . k by A7, FINSEQ_3:110
.= (p . (k -' 1)) * ((1_. L) . ((i + 1) -' k)) by A3, A10
.= (p . (k -' 1)) * (0. L) by A9, Th30
.= 0. L by VECTSP_1:6 ; ::_thesis: verum
end;
then A11: Sum (Del (r,(i + 1))) = 0. L by Th1;
r = (Del (r,(i + 1))) ^ <*(r . (i + 1))*> by A1, PRE_POLY:13
.= (Del (r,(i + 1))) ^ <*(r /. (i + 1))*> by A4, PARTFUN1:def_6 ;
then A12: Sum r = (Sum (Del (r,(i + 1)))) + (Sum <*(r /. (i + 1))*>) by RLVECT_1:41
.= (Sum (Del (r,(i + 1)))) + (r /. (i + 1)) by RLVECT_1:44 ;
r /. (i + 1) = r . (i + 1) by A4, PARTFUN1:def_6
.= (p . ((i + 1) -' 1)) * ((1_. L) . ((i + 1) -' (i + 1))) by A3, A4
.= (p . i) * ((1_. L) . ((i + 1) -' (i + 1))) by NAT_D:34
.= (p . i) * ((1_. L) . 0) by XREAL_1:232
.= (p . i) * (1_ L) by Th30
.= p . i by VECTSP_1:def_4 ;
hence (p *' (1_. L)) . i = p . i by A2, A12, A11, RLVECT_1:4; ::_thesis: verum
end;
hence p *' (1_. L) = p by FUNCT_2:63; ::_thesis: verum
end;
begin
definition
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
func Polynom-Ring L -> non empty strict doubleLoopStr means :Def10: :: POLYNOM3:def 10
( ( for x being set holds
( x in the carrier of it iff x is Polynomial of L ) ) & ( for x, y being Element of it
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of it
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. it = 0_. L & 1. it = 1_. L );
existence
ex b1 being non empty strict doubleLoopStr st
( ( for x being set holds
( x in the carrier of b1 iff x is Polynomial of L ) ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b1 = 0_. L & 1. b1 = 1_. L )
proof
A1: 0_. L in { x where x is Polynomial of L : verum } ;
then reconsider Ca = { x where x is Polynomial of L : verum } as non empty set ;
reconsider Ze = 0_. L as Element of Ca by A1;
defpred S1[ set , set , set ] means ex p, q being Polynomial of L st
( p = $1 & q = $2 & $3 = p + q );
A2: for x, y being Element of Ca ex u being Element of Ca st S1[x,y,u]
proof
let x, y be Element of Ca; ::_thesis: ex u being Element of Ca st S1[x,y,u]
x in Ca ;
then consider p being Polynomial of L such that
A3: x = p ;
y in Ca ;
then consider q being Polynomial of L such that
A4: y = q ;
p + q in Ca ;
then reconsider u = p + q as Element of Ca ;
take u ; ::_thesis: S1[x,y,u]
take p ; ::_thesis: ex q being Polynomial of L st
( p = x & q = y & u = p + q )
take q ; ::_thesis: ( p = x & q = y & u = p + q )
thus ( p = x & q = y & u = p + q ) by A3, A4; ::_thesis: verum
end;
consider Ad being Function of [:Ca,Ca:],Ca such that
A5: for x, y being Element of Ca holds S1[x,y,Ad . (x,y)] from BINOP_1:sch_3(A2);
1_. L in { x where x is Polynomial of L : verum } ;
then reconsider Un = 1_. L as Element of Ca ;
defpred S2[ set , set , set ] means ex p, q being Polynomial of L st
( p = $1 & q = $2 & $3 = p *' q );
A6: for x, y being Element of Ca ex u being Element of Ca st S2[x,y,u]
proof
let x, y be Element of Ca; ::_thesis: ex u being Element of Ca st S2[x,y,u]
x in Ca ;
then consider p being Polynomial of L such that
A7: x = p ;
y in Ca ;
then consider q being Polynomial of L such that
A8: y = q ;
p *' q in Ca ;
then reconsider u = p *' q as Element of Ca ;
take u ; ::_thesis: S2[x,y,u]
take p ; ::_thesis: ex q being Polynomial of L st
( p = x & q = y & u = p *' q )
take q ; ::_thesis: ( p = x & q = y & u = p *' q )
thus ( p = x & q = y & u = p *' q ) by A7, A8; ::_thesis: verum
end;
consider Mu being Function of [:Ca,Ca:],Ca such that
A9: for x, y being Element of Ca holds S2[x,y,Mu . (x,y)] from BINOP_1:sch_3(A6);
reconsider P = doubleLoopStr(# Ca,Ad,Mu,Un,Ze #) as non empty strict doubleLoopStr ;
take P ; ::_thesis: ( ( for x being set holds
( x in the carrier of P iff x is Polynomial of L ) ) & ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. P = 0_. L & 1. P = 1_. L )
thus for x being set holds
( x in the carrier of P iff x is Polynomial of L ) ::_thesis: ( ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. P = 0_. L & 1. P = 1_. L )
proof
let x be set ; ::_thesis: ( x in the carrier of P iff x is Polynomial of L )
thus ( x in the carrier of P implies x is Polynomial of L ) ::_thesis: ( x is Polynomial of L implies x in the carrier of P )
proof
assume x in the carrier of P ; ::_thesis: x is Polynomial of L
then ex p being Polynomial of L st x = p ;
hence x is Polynomial of L ; ::_thesis: verum
end;
thus ( x is Polynomial of L implies x in the carrier of P ) ; ::_thesis: verum
end;
thus for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ::_thesis: ( ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. P = 0_. L & 1. P = 1_. L )
proof
let x, y be Element of P; ::_thesis: for p, q being sequence of L st x = p & y = q holds
x + y = p + q
let p, q be sequence of L; ::_thesis: ( x = p & y = q implies x + y = p + q )
assume A10: ( x = p & y = q ) ; ::_thesis: x + y = p + q
ex p1, q1 being Polynomial of L st
( p1 = x & q1 = y & Ad . (x,y) = p1 + q1 ) by A5;
hence x + y = p + q by A10; ::_thesis: verum
end;
thus for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ::_thesis: ( 0. P = 0_. L & 1. P = 1_. L )
proof
let x, y be Element of P; ::_thesis: for p, q being sequence of L st x = p & y = q holds
x * y = p *' q
let p, q be sequence of L; ::_thesis: ( x = p & y = q implies x * y = p *' q )
assume A11: ( x = p & y = q ) ; ::_thesis: x * y = p *' q
ex p1, q1 being Polynomial of L st
( p1 = x & q1 = y & Mu . (x,y) = p1 *' q1 ) by A9;
hence x * y = p *' q by A11; ::_thesis: verum
end;
thus 0. P = 0_. L ; ::_thesis: 1. P = 1_. L
thus 1. P = 1_. L ; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty strict doubleLoopStr st ( for x being set holds
( x in the carrier of b1 iff x is Polynomial of L ) ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b1 = 0_. L & 1. b1 = 1_. L & ( for x being set holds
( x in the carrier of b2 iff x is Polynomial of L ) ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b2 = 0_. L & 1. b2 = 1_. L holds
b1 = b2
proof
let P1, P2 be non empty strict doubleLoopStr ; ::_thesis: ( ( for x being set holds
( x in the carrier of P1 iff x is Polynomial of L ) ) & ( for x, y being Element of P1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of P1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. P1 = 0_. L & 1. P1 = 1_. L & ( for x being set holds
( x in the carrier of P2 iff x is Polynomial of L ) ) & ( for x, y being Element of P2
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of P2
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. P2 = 0_. L & 1. P2 = 1_. L implies P1 = P2 )
assume that
A12: for x being set holds
( x in the carrier of P1 iff x is Polynomial of L ) and
A13: for x, y being Element of P1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q and
A14: for x, y being Element of P1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q and
A15: ( 0. P1 = 0_. L & 1. P1 = 1_. L ) and
A16: for x being set holds
( x in the carrier of P2 iff x is Polynomial of L ) and
A17: for x, y being Element of P2
for p, q being sequence of L st x = p & y = q holds
x + y = p + q and
A18: for x, y being Element of P2
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q and
A19: ( 0. P2 = 0_. L & 1. P2 = 1_. L ) ; ::_thesis: P1 = P2
A20: now__::_thesis:_for_x_being_set_holds_
(_x_in_the_carrier_of_P1_iff_x_in_the_carrier_of_P2_)
let x be set ; ::_thesis: ( x in the carrier of P1 iff x in the carrier of P2 )
( x in the carrier of P1 iff x is Polynomial of L ) by A12;
hence ( x in the carrier of P1 iff x in the carrier of P2 ) by A16; ::_thesis: verum
end;
then A21: the carrier of P1 = the carrier of P2 by TARSKI:1;
A22: now__::_thesis:_for_x_being_Element_of_P1
for_y_being_Element_of_P2_holds_the_multF_of_P1_._(x,y)_=_the_multF_of_P2_._(x,y)
let x be Element of P1; ::_thesis: for y being Element of P2 holds the multF of P1 . (x,y) = the multF of P2 . (x,y)
let y be Element of P2; ::_thesis: the multF of P1 . (x,y) = the multF of P2 . (x,y)
reconsider y1 = y as Element of P1 by A20;
reconsider x1 = x as Element of P2 by A20;
reconsider p = x as sequence of L by A12;
reconsider q = y as sequence of L by A16;
thus the multF of P1 . (x,y) = x * y1
.= p *' q by A14
.= x1 * y by A18
.= the multF of P2 . (x,y) ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Element_of_P1
for_y_being_Element_of_P2_holds_the_addF_of_P1_._(x,y)_=_the_addF_of_P2_._(x,y)
let x be Element of P1; ::_thesis: for y being Element of P2 holds the addF of P1 . (x,y) = the addF of P2 . (x,y)
let y be Element of P2; ::_thesis: the addF of P1 . (x,y) = the addF of P2 . (x,y)
reconsider y1 = y as Element of P1 by A20;
reconsider x1 = x as Element of P2 by A20;
reconsider p = x as sequence of L by A12;
reconsider q = y as sequence of L by A16;
thus the addF of P1 . (x,y) = x + y1
.= p + q by A13
.= x1 + y by A17
.= the addF of P2 . (x,y) ; ::_thesis: verum
end;
then the addF of P1 = the addF of P2 by A21, BINOP_1:2;
hence P1 = P2 by A15, A19, A21, A22, BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines Polynom-Ring POLYNOM3:def_10_:_
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for b2 being non empty strict doubleLoopStr holds
( b2 = Polynom-Ring L iff ( ( for x being set holds
( x in the carrier of b2 iff x is Polynomial of L ) ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b2 = 0_. L & 1. b2 = 1_. L ) );
registration
let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring L -> non empty strict Abelian ;
coherence
Polynom-Ring L is Abelian
proof
let p, q be Element of (Polynom-Ring L); :: according to RLVECT_1:def_2 ::_thesis: p + q = q + p
reconsider p1 = p, q1 = q as sequence of L by Def10;
thus p + q = p1 + q1 by Def10
.= q + p by Def10 ; ::_thesis: verum
end;
end;
registration
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring L -> non empty strict add-associative ;
coherence
Polynom-Ring L is add-associative
proof
let p, q, r be Element of (Polynom-Ring L); :: according to RLVECT_1:def_3 ::_thesis: (p + q) + r = p + (q + r)
reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def10;
A1: q + r = q1 + r1 by Def10;
p + q = p1 + q1 by Def10;
hence (p + q) + r = (p1 + q1) + r1 by Def10
.= p1 + (q1 + r1) by Th26
.= p + (q + r) by A1, Def10 ;
::_thesis: verum
end;
cluster Polynom-Ring L -> non empty strict right_zeroed ;
coherence
Polynom-Ring L is right_zeroed
proof
let p be Element of (Polynom-Ring L); :: according to RLVECT_1:def_4 ::_thesis: p + (0. (Polynom-Ring L)) = p
reconsider p1 = p as sequence of L by Def10;
0. (Polynom-Ring L) = 0_. L by Def10;
hence p + (0. (Polynom-Ring L)) = p1 + (0_. L) by Def10
.= p by Th28 ;
::_thesis: verum
end;
cluster Polynom-Ring L -> non empty right_complementable strict ;
coherence
Polynom-Ring L is right_complementable
proof
let p be Element of (Polynom-Ring L); :: according to ALGSTR_0:def_16 ::_thesis: p is right_complementable
reconsider p1 = p as Polynomial of L by Def10;
reconsider q = - p1 as Element of (Polynom-Ring L) by Def10;
take q ; :: according to ALGSTR_0:def_11 ::_thesis: p + q = 0. (Polynom-Ring L)
thus p + q = p1 - p1 by Def10
.= 0_. L by Th29
.= 0. (Polynom-Ring L) by Def10 ; ::_thesis: verum
end;
end;
registration
let L be non empty right_complementable commutative distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring L -> non empty strict commutative ;
coherence
Polynom-Ring L is commutative
proof
let p, q be Element of (Polynom-Ring L); :: according to GROUP_1:def_12 ::_thesis: p * q = q * p
reconsider p1 = p, q1 = q as sequence of L by Def10;
thus p * q = p1 *' q1 by Def10
.= q * p by Def10 ; ::_thesis: verum
end;
end;
registration
let L be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring L -> non empty strict associative ;
coherence
Polynom-Ring L is associative
proof
let p, q, r be Element of (Polynom-Ring L); :: according to GROUP_1:def_3 ::_thesis: (p * q) * r = p * (q * r)
reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def10;
A1: q * r = q1 *' r1 by Def10;
p * q = p1 *' q1 by Def10;
hence (p * q) * r = (p1 *' q1) *' r1 by Def10
.= p1 *' (q1 *' r1) by Th33
.= p * (q * r) by A1, Def10 ;
::_thesis: verum
end;
end;
Lm2: now__::_thesis:_for_L_being_non_empty_right_complementable_commutative_well-unital_distributive_Abelian_add-associative_right_zeroed_doubleLoopStr_
for_x,_e_being_Element_of_(Polynom-Ring_L)_st_e_=_1._(Polynom-Ring_L)_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let L be non empty right_complementable commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for x, e being Element of (Polynom-Ring L) st e = 1. (Polynom-Ring L) holds
( x * e = x & e * x = x )
set Pm = Polynom-Ring L;
let x, e be Element of (Polynom-Ring L); ::_thesis: ( e = 1. (Polynom-Ring L) implies ( x * e = x & e * x = x ) )
reconsider p = x as Polynomial of L by Def10;
assume A1: e = 1. (Polynom-Ring L) ; ::_thesis: ( x * e = x & e * x = x )
A2: 1. (Polynom-Ring L) = 1_. L by Def10;
hence x * e = p *' (1_. L) by A1, Def10
.= x by Th35 ;
::_thesis: e * x = x
thus e * x = p *' (1_. L) by A1, A2, Def10
.= x by Th35 ; ::_thesis: verum
end;
registration
let L be non empty right_complementable commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring L -> non empty strict well-unital ;
coherence
Polynom-Ring L is well-unital
proof
let x be Element of (Polynom-Ring L); :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. (Polynom-Ring L)) = x & (1. (Polynom-Ring L)) * x = x )
thus ( x * (1. (Polynom-Ring L)) = x & (1. (Polynom-Ring L)) * x = x ) by Lm2; ::_thesis: verum
end;
end;
registration
let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring L -> non empty strict distributive ;
coherence
Polynom-Ring L is distributive
proof
let p, q, r be Element of (Polynom-Ring L); :: according to VECTSP_1:def_7 ::_thesis: ( p * (q + r) = (p * q) + (p * r) & (q + r) * p = (q * p) + (r * p) )
reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def10;
A1: ( p * q = p1 *' q1 & p * r = p1 *' r1 ) by Def10;
q + r = q1 + r1 by Def10;
hence p * (q + r) = p1 *' (q1 + r1) by Def10
.= (p1 *' q1) + (p1 *' r1) by Th31
.= (p * q) + (p * r) by A1, Def10 ;
::_thesis: (q + r) * p = (q * p) + (r * p)
A2: ( q * p = q1 *' p1 & r * p = r1 *' p1 ) by Def10;
q + r = q1 + r1 by Def10;
hence (q + r) * p = (q1 + r1) *' p1 by Def10
.= (q1 *' p1) + (r1 *' p1) by Th32
.= (q * p) + (r * p) by A2, Def10 ;
::_thesis: verum
end;
end;
theorem :: POLYNOM3:36
for L being non empty right_complementable commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr holds 1. (Polynom-Ring L) = 1_. L by Def10;