:: Derivation of Commutative Rings \& {L}eibnitz Formula for Power of
:: Derivation
:: by Yasushige Watase
::
:: Received March 30, 2021
:: Copyright (c) 2021-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_3, VECTSP_1, ALGSTR_0, TARSKI, NAT_1, MESFUNC1, VECTSP_2,
STRUCT_0, SUBSET_1, SUPINF_2, GROUP_1, POLYNOM1, POLYNOM3, FUNCSDOM,
HURWITZ, FINSEQ_1, ALGSEQ_1, FUNCT_1, RELAT_1, CARD_1, XBOOLE_0, NUMBERS,
MSSUBFAM, CARD_3, RLVECT_1, AFINSQ_1, PARTFUN1, XXREAL_0, XCMPLX_0,
ORDINAL4, RATFUNC1, NEWTON, ARYTM_1, FIELD_1, FUNCOP_1, ALGSTR_1,
BINOP_1, LATTICES, RFINSEQ, FINSEQ_3, FINSEQ_5, POLYDIFF, POLYNOM5,
FUNCT_2, RINGDER1, TOPGEN_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, NAT_D,
FINSEQ_1, NEWTON, RFINSEQ, FINSEQ_5, FINSEQ_7,
WSIERP_1, STRUCT_0, ALGSTR_0,
GROUP_1, VECTSP_1, ALGSTR_1, VECTSP_2, GROUP_4, POLYNOM1, ALGSEQ_1,
BINOM, POLYNOM3, RLVECT_1, POLYNOM5, HURWITZ, VECTSP11, RATFUNC1, RING_4,
POLYDIFF, FIELD_1;
constructors RELSET_1, NAT_D, FINSEQOP, NEWTON, RFINSEQ, FINSEQ_5, FINSEQ_7,
GROUP_4, FVSUM_1, ALGSEQ_1, GCD_1, BINOM, POLYNOM3, POLYNOM4, VECTSP11,
RATFUNC1, POLYDIFF, FIELD_1, WSIERP_1;
registrations XBOOLE_0, XXREAL_0, XREAL_0, CARD_1, ORDINAL1, RELSET_1, MOD_4,
FUNCT_1, NAT_1, INT_1, POLYDIFF, FINSEQ_1, STRUCT_0, RLVECT_1, VECTSP_1,
ALGSTR_1, RING_3, RING_4, RING_5, POLYNOM3, POLYNOM4, POLYNOM5, RATFUNC1,
FUNCOP_1, RELAT_1, FDIFF_1, FUNCT_2, GR_CY_1, ALGSEQ_1;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions TARSKI, GROUP_1, FINSEQ_1, FUNCT_1, FUNCT_2, POLYDIFF, ALGSTR_0,
VECTSP_1;
equalities FINSEQ_1, XCMPLX_0, POLYNOM3, RING_4, POLYDIFF, HURWITZ, RLVECT_1,
STRUCT_0, SUBSET_1, ALGSTR_0, VECTSP_1, RATFUNC1, POLYNOM5, FUNCSDOM,
VALUED_1;
expansions STRUCT_0, VECTSP_1, TARSKI, FUNCT_2, FINSEQ_1, FUNCT_1, RING_4,
RATFUNC1, POLYDIFF, RLVECT_1;
theorems GROUP_1, VECTSP_1, RLVECT_1, POLYDIFF, PARTFUN1, FUNCT_2, FUNCT_1,
POLYNOM4, RING_5, ALGSEQ_1, POLYNOM3, NAT_1, INT_1, FINSEQ_1, NORMSP_1,
RING_4, XREAL_1, UPROOTS, XXREAL_0, POLYNOM5, FINSEQ_2, GROUP_4, BINOM,
FINSEQ_3, FINSEQ_5, VECTSP11, RELAT_1, FINSEQ_4, FINSEQOP, FINSEQ_7,
RFINSEQ, POLYNOM1, GENEALG1, MATRIXR1, FVSUM_1, NAT_D, NEWTON, PRE_POLY,
VECTSP_2, FIELD_1, RING_2, TARSKI, ORDINAL1;
schemes ALGSEQ_1, NAT_1, FUNCT_2, FINSEQ_1;
begin :: Preliminaries
reserve L for Abelian left_zeroed add-associative associative right_zeroed
right_complementable distributive non empty doubleLoopStr;
reserve a,b,c for Element of L;
reserve R for non degenerated comRing;
reserve n,m,i,j,k for Nat;
:: <section0>Preliminaries</section0>
theorem Th1:
n*a + n*b = n*(a+b)
proof
defpred P[Nat] means $1*a + $1*b = $1*(a+b);
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
(n+1)*a + (n+1)*b = (n*a + 1*a) + (n+1)*b by BINOM:15
.= n*a + a + (n+1)*b by BINOM:13
.= n*a + ((n+1)*b + a) by RLVECT_1:def 3
.= n*a + ((n*b +1*b) + a) by BINOM:15
.= n*a + ((n*b +b) + a) by BINOM:13
.= n*a + (n*b + (a + b)) by RLVECT_1:def 3
.= n*(a+b) + (a+b) by A2,RLVECT_1:def 3
.= n*(a+b) + 1*(a+b) by BINOM:13
.= (n+1)*(a+b) by BINOM:15;
hence thesis;
end;
0*a + 0*b = 0.L + 0*b by BINOM:12
.= 0.L*(a+b) by BINOM:12
.= 0*(a+b) by BINOM:12; then
A3: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem
(n*a)*b = a*(n*b)
proof
defpred P[Nat] means ($1*a)*b = a*($1*b);
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
((n+1)*a)*b = ((n*a) + (1*a))*b by BINOM:15
.= (n*a)*b + (1*a)*b by VECTSP_1:def 3
.= (n*a)*b + a*b by BINOM:13
.= a*(n*b) + a*(1*b) by A2,BINOM:13
.= a*(n*b+ 1*b) by VECTSP_1:def 2
.= a*((n+1)*b) by BINOM:15;
hence thesis;
end;
(0*a)*b = 0.L* b by BINOM:12
.= a*0.L
.= a*(0*b) by BINOM:12; then
A3: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th3:
n*0.L = 0.L
proof
defpred P[Nat] means $1*0.L = 0.L;
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
(n+1)*0.L = n*0.L + 1*0.L by BINOM:15
.= 0.L by A2,BINOM:13;
hence thesis;
end;
A3: P[0] by BINOM:12;
for n be Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem
0.L*n = 0.L
proof
defpred P[Nat] means 0.L * $1= 0.L;
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume P[n];
0.L*(n+1) = (n+1)*0.L by BINOM:17
.= n*0.L + 1*0.L by BINOM:15
.= n*0.L + 0.L by BINOM:13
.= 0.L by Th3;
hence thesis;
end;
A2: P[0] by BINOM:12;
for n be Nat holds P[n] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
begin :: Definition of Derivation of Rings and Its Properties
:: <section1>Definition of Derivation of Rings and Its Properties</section1>
:::::::::::::::::::::::::::::::::::::
::: Derivation Hideyuki Matsumura "Commutative_Ring_Theory" Ch.9 p.190
::: Derivation D: R -> R
:::::::::::::::::::::::::::::::::::::::::::::::
reserve D for Function of R, R;
reserve x,y,z for Element of R;
definition
let R;
let IT be Function of R, R;
attr IT is derivation means :Def1:
for x,y be Element of R holds
IT.(x + y) = IT.x + IT.y &
IT.(x*y) = x*IT.y + y*IT.x;
end;
registration let R;
cluster derivation -> additive for Function of R,R;
coherence;
end;
registration
let R;
cluster derivation for Function of R,R;
existence
proof
take f = (the carrier of R) --> 0.R;
thus thesis;
end;
end;
definition
let R;
mode Derivation of R is derivation Function of R,R;
end;
definition
let R;
func Der(R) -> Subset of Funcs([#]R,[#]R) equals
{f where f is Function of R,R : f is derivation };
coherence
proof
set E = {f where f is Function of R,R : f is derivation };
for o be object holds o in E implies o in Funcs([#]R,[#]R)
proof
let o be object;
assume o in E; then
consider f be Function of R,R such that
A2: f = o & f is derivation;
A3: dom f = [#]R by FUNCT_2:def 1;
rng f c= [#]R;
hence thesis by A2,A3,FUNCT_2:def 2;
end;
hence thesis by TARSKI:def 3;
end;
end;
registration
let R;
cluster Der(R) -> non empty;
correctness
proof
set f = (the carrier of R) --> 0.R;
f is derivation; then
f in Der(R);
hence thesis;
end;
end;
reserve D for Derivation of R;
theorem Th5:
D.(1.R) = 0.R & D.(0.R) = 0.R
proof
A1: D.(0.R) = D.(0.R + 0.R) .= D.(0.R) + D.(0.R) by Def1;
D.(1.R) = D.((1.R)*(1.R))
.= (1.R)*D.(1.R) + (1.R)*D.(1.R) by Def1 .= D.(1.R) + D.(1.R);
hence thesis by A1,RLVECT_1:9;
end;
theorem Th6:
for n,x holds D.(n*x) = n*D.x
proof
let n,x;
defpred P[Nat] means D.($1*x) = $1*D.x;
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
D.((n+1)*x) = D.(n*x + 1*x) by BINOM:15
.= D.(n*x) + D.(1*x) by Def1
.= D.(n*x) + D.x by BINOM:13
.= n*D.x + 1*D.x by A2,BINOM:13
.= (n+1)*D.x by BINOM:15;
hence thesis;
end;
0*D.x = 0.R by BINOM:12 .= D.(0.R) by Th5 .= D.(0*x) by BINOM:12;
then
A3: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th7:
D.(x|^(m+1)) = (m+1)*((x|^m)*D.x)
proof
defpred P[Nat] means D.(x|^($1+1)) = ($1+1)*((x|^$1)*D.x);
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
set t = n+1;
A3: x|^((n+1)+1) = (x|^1)*(x|^t) by BINOM:10
.= x*x|^(n+1) by BINOM:8;
D.(x|^((n+1)+1))
= x*((n+1)*((x|^n)*D.x)) + (x|^(n+1))*D.x by A2, Def1,A3
.= (n+1)*(x*((x|^n)*D.x)) + (x|^(n+1))*D.x by BINOM:19
.= (n+1)*((x*(x|^n))*D.x) + (x|^(n+1))*D.x by GROUP_1:def 3
.= (n+1)*(((x|^1)*(x|^n))*D.x) + (x|^(n+1))*D.x by BINOM:8
.= (n+1)*((x|^(n+1))*D.x) + (x|^(n+1))*D.x by BINOM:10
.= (n+1)*((x|^(n+1))*D.x) + 1*((x|^(n+1))*D.x) by BINOM:13
.= (n+1+1)*((x|^(n+1))*D.x) by BINOM:15;
hence thesis;
end;
(0+1)*((x|^0)*D.x) = 1*((1_R)*D.x) by BINOM:8
.= D.x by BINOM:13
.= D.(x|^(0+1)) by BINOM:8; then
A4: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Power of Derivation D|^(n+1).f = D.(D|^n.f)
::::::::::::::::::::::::::::::::::::::::::::::::::::
:: D|^2 is Function of the carrier of R,the carrier of R;
:: D|^3 is Function of the carrier of R,the carrier of R;
:: D|^0 = id R by VECTSP11:18;
:: R is non empty & D is Function of R,R;
:: dom D = the carrier of R by FUNCT_2:def 1;
:::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem Th8:
(D|^(n+1)) = (D*D|^n) & dom D = the carrier of R &
dom (D|^n) = the carrier of R & D|^n is (the carrier of R)-valued Function
proof
D|^1 = D by VECTSP11:19;
hence thesis by FUNCT_2:def 1,VECTSP11:20;
end;
theorem Th9:
for n,x holds (D|^(n+1)).x = D.((D|^n).x)
proof
let n,x;
A1: dom (D|^n) = the carrier of R by Th8;
(D|^(n+1)).x = ((D*D|^n)).x by Th8
.= D.((D|^n).x) by A1,FUNCT_1:13;
hence thesis;
end;
::::::::::::::::::::::::::::::::::::::::
::: D.(a/b) = (b*D.a - a*F.b)/b^2
::::::::::::::::::::::::::::::::::::::::
theorem
for x,y,z st z*y=1.R holds y|^2*D.(x*z) = (y*D.x -x*D.y)
proof
let x,y,z;
assume
A1: z*y=1.R;
reconsider c = x*z as Element of R;
reconsider d = c*D.y as Element of R;
c*y = x*1.R by A1,GROUP_1:def 3
.= x; then
D.x = c*D.y + y*D.c by Def1; then
A2: y*D.c = D.x - c*D.y by VECTSP_2:2 .= D.x + - d;
A3: y*(c*D.y) = (y*(z*x))*D.y by GROUP_1:def 3
.= ((1.R)*x)*D.y by A1,GROUP_1:def 3
.= x*D.y;
y|^2 = y|^(1+1) .= (y|^1)*(y|^1) by BINOM:10 .= y*y|^1 by BINOM:8
.= y*y by BINOM:8; then
y|^2*D.c = y*(D.x + (- d)) by A2,GROUP_1:def 3
.= y*(D.x) + y*(-d) by VECTSP_1:def 2
.= y*D.x - x*D.y by A3,VECTSP_1:8;
hence thesis;
end;
reserve s for FinSequence of the carrier of R;
reserve h for Function of R,R;
definition
let R,s,h;
redefine func h*s -> FinSequence of the carrier of R; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence by FINSEQ_2:32;
end;
theorem Th11:
for h,s st h is additive holds h.(Sum s) = Sum(h*s)
proof
let h,s;
assume
A1: h is additive;
defpred P[Nat] means
for h,s holds
len s = $1 & h is additive implies h.(Sum s) = Sum (h*s);
A2: P[0]
proof
let h,s;
assume that
A3: len s = 0 and
A4: h is additive;
Sum s = 0.R by A3,RLVECT_1:75; then
A6: h.(Sum s) = 0.R by A4,RING_2:6;
dom h = the carrier of R by FUNCT_2:def 1; then
rng s c= dom h; then
dom(h*s) = dom s by RELAT_1:27 .= Seg len s by FINSEQ_1:def 3; then
h*s = <*>the carrier of R by A3;
hence thesis by A6,RLVECT_1:43;
end;
A9: for n be Nat st P[n] holds P[n+1]
proof
let n;
assume
A10: P[n];
for h,s holds
len s = n+1 & h is additive implies h.(Sum s) = Sum (h*s)
proof
let h,s;
assume that
A11: len s = n+1 and
A12: h is additive;
set s0=s|n;
dom s = Seg(n+1) by A11,FINSEQ_1:def 3; then
s.(n+1) in rng s by FUNCT_1:3,FINSEQ_1:4; then
reconsider v=s.(n+1) as Element of R;
A13: n = len s0 by A11,FINSEQ_1:59,NAT_1:11;
1 <= n+1 <= len s by A11,NAT_1:11; then
A15: s/.len s = s.(n+1) by A11,FINSEQ_4:15; then
A16: s = (s|n)^<*v*> by A11,FINSEQ_5:21;
A17: h*s = h*((s|n)^<*v*>) by A15,A11,FINSEQ_5:21
.= (h*s0)^<*h.v*> by FINSEQOP:8;
h.(Sum s) = h.(Sum s0 + Sum<*v*>) by A16,RLVECT_1:41
.= h.(Sum s0 + v) by RLVECT_1:44
.= h.(Sum s0) + h.v by A12
.= Sum(h*s0) + h.v by A10,A12,A13
.= Sum(h*s0) + Sum <*h.v*> by RLVECT_1:44
.= Sum(h*s) by A17,RLVECT_1:41;
hence thesis;
end;
hence thesis;
end;
A18: for n be Nat holds P[n] from NAT_1:sch 2(A2,A9);
len s is Nat;
hence thesis by A1,A18;
end;
::::::::::::::::::::::::::::::::::::::::::::::::
::: Formula
::: (f1 + f2 +...+fn)' = f1' + f2' +...+ fn'
::::::::::::::::::::::::::::::::::::::::::::::::
theorem
for D,s holds D.(Sum s) = Sum(D*s) by Th11;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Formula
:: (f1*f2*...*fn)' = f1'*f2...*fn + f1*f2'*..*fn +....+ f1*f2*f3*..*fn'
:: D.(Product s) = (f1*f2*...*fn)'
:: Sum DProd(D,s) = f1'*f2...fn + f1*f2'*....fn + f1*f2*f3'..
:: here DProd(D,s) = f1*..*D.fi*...*fn = Product( replace(s,i,D.fi))
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let R,D,s;
func DProd(D,s) -> FinSequence of the carrier of R means :Def3:
len it = len s & for i st i in dom it holds
it.i = Product (Replace(s,i,D.(s/.i)));
existence
proof
deffunc F(Nat) = Product (Replace(s,$1,D.(s/.$1)));
consider z being FinSequence such that
A1: len z = len s & for k being Nat st k in dom z holds z.k = F(k)
from FINSEQ_1:sch 2;
take z;
z is FinSequence of the carrier of R
proof
A2: for p be object st p in rng z holds p in the carrier of R
proof
let p be object;
assume p in rng z; then
consider i be object such that
A3: i in dom z and
A4: p = z.i by FUNCT_1:def 3;
reconsider i as Nat by A3;
z.i = Product (Replace(s,i,D.(s/.i))) by A1,A3;
hence thesis by A4;
end;
rng z c= the carrier of R by A2;
hence thesis by FINSEQ_1:def 4;
end;
hence thesis by A1;
end;
uniqueness
proof
let z1,z2 be FinSequence of the carrier of R such that
A7: len z1 = len s and
A8: for i be Nat st i in dom z1 holds
z1.i = Product (Replace(s,i,D.(s/.i))) and
A9: len z2 = len s and
A10: for j be Nat st j in dom z2 holds
z2.j = Product (Replace(s,j,D.(s/.j)));
A11: dom z1 = Seg len s by A7,FINSEQ_1:def 3.= dom z2 by A9,FINSEQ_1:def 3;
for q be Nat st q in dom z1 holds z1.q = z2.q
proof
let q be Nat;
assume
A12: q in dom z1; then
reconsider q9 = q as Element of NAT;
z1.q9 =Product (Replace(s,q9,D.(s/.q9))) by A8,A12
.= z2.q9 by A10,A11,A12;
hence thesis;
end;
hence thesis by A11;
end;
end;
theorem Th13:
for s holds len s = 1 implies Sum DProd(D,s)= D.(Product s)
proof
let s;
assume
A1: len s = 1;
reconsider Ds1 = D.(s/.1) as Element of R;
dom s = Seg 1 by A1,FINSEQ_1:def 3; then
A2: 1 in dom s;
A3: s = <* s.1 *> by A1, FINSEQ_1:40 .= <* s/.1 *> by A2,PARTFUN1:def 6;
reconsider s1 = s/.1 as Element of R;
A4: len DProd(D,s) = 1 by A1,Def3;
dom DProd(D,s) = Seg 1 by A4,FINSEQ_1:def 3; then
A5: 1 in dom DProd(D,s);
A6: Replace(s,1,Ds1) = <* Ds1 *> by A3,FINSEQ_7:12;
Sum DProd(D,s) = DProd(D,s).1 by A4, RLVECT_1:76
.= Product <* D.(s/.1) *> by A6,A5,Def3
.= D.(s/.1) by GROUP_4:9
.= D.(Product s) by A3,GROUP_4:9;
hence thesis;
end;
theorem
for t be FinSequence of the carrier of R st len t >= 1 holds
Sum DProd(D,t) = D.(Product t)
proof
let t be FinSequence of the carrier of R;
assume
A1: len t >= 1;
defpred P[non zero Nat] means
for s holds len s = $1 implies Sum DProd(D,s)= D.(Product s);
A2: P[1] by Th13;
A3: for k be non zero Nat holds P[k] implies P[k+1]
proof
let k be non zero Nat;
assume
A4: P[k];
for s holds len s = k+1 implies Sum DProd(D,s)= D.(Product s)
proof
let s;
assume
A5: len s = k+1; then
A6: dom s = Seg (k+1) by FINSEQ_1:def 3;
A7: dom DProd(D,s) = Seg len DProd(D,s) by FINSEQ_1:def 3
.= Seg (k+1) by A5,Def3;
A8: 1 <= k+1 & k+1 <= k+1 by NAT_1:11; then
A9: k+1 in dom s by A6;
A10: k+1 in dom DProd(D,s) by A7,A8;
reconsider sk1 = s/.(k+1) as Element of R;
A11: k < len s by A5,XREAL_1:29; then
A12: len (s|k) = k by FINSEQ_1:59;
A13: (s|k)^<* s/.(k+1) *> = (s|k)^<* s.(k+1) *> by A9,PARTFUN1:def 6
.= s|(k+1) by A5,XREAL_1:29,FINSEQ_5:83;
A14: (Product (s|k))*D.(s/.(k+1)) = DProd(D,s)/.(k+1)
proof
A15: Replace(s,k+1,D.(s/.(k+1)))
= (s|((k+1)-'1))^<*D.(s/.(k+1))*>^(s/^(k+1))
by A5,A8,FINSEQ_7:def 1
.= (s|k)^<*D.(s/.(k+1))*>^(s/^(k+1)) by NAT_D:34
.= (s|k)^<*D.(s/.(k+1))*>^{} by A5,RFINSEQ:27
.= (s|k)^<*D.(s/.(k+1))*> by FINSEQ_1:34;
(Product (s|k))*D.(s/.(k+1))
= Product (Replace(s,k+1,D.(s/.(k+1)))) by A15,GROUP_4:6
.= DProd(D,s).(k+1) by A10,Def3
.= DProd(D,s)/.(k+1) by A10,PARTFUN1:def 6;
hence thesis;
end;
A16: dom DProd(D,s|k) = Seg len DProd(D,s|k) by FINSEQ_1:def 3
.= Seg len (s|k) by Def3 .= Seg k by FINSEQ_1:59,A11;
reconsider sk1 = s/.(k+1) as Element of R;
A17: for i be Nat st i in dom DProd(D,s|k) holds
(sk1*(DProd(D,(s|k))))/.i = DProd(D,s).i
proof
let i be Nat;
assume
A18: i in dom DProd(D,s|k); then
A19: DProd(D,s|k)/.i = DProd(D,s|k).i by PARTFUN1:def 6
.= Product (Replace(s|k,i,D.((s|k)/.i))) by A18,Def3;
A20: 1 <= i & i <= k by FINSEQ_1:1,A18,A16; then
A21: 1 <= i & i <= len (s|k) by FINSEQ_1:59,A11;
1 <= k & k <= k +1 by A20,XXREAL_0:2,NAT_1:11; then
A23: k in dom s by A6;
reconsider i1 = i-'1 as Nat;
i - 1 <= k - 0 by A20,XREAL_1:13; then
i -' 1 <= k by A20,XREAL_1:233; then
A26: Seg (i -' 1) c= Seg k by FINSEQ_1:5;
A27: ((s|k)/^i)^<*s/.(k+1)*>
= ((s|k)^<*s/.(k+1)*>)/^i by A21,GENEALG1:1
.= ((s|k)^<*s.(k+1)*>)/^i by A9,PARTFUN1:def 6
.= s/^i by A5,RFINSEQ:7;
A28: i <= len s by A5,A20,NAT_1:13;
i <= k+1 by A20,NAT_1:13; then
A30: i in dom DProd(D,s) by A7,A20;
A31: Replace(s|k,i,D.((s|k)/.i))^<* s/.(k+1) *>
= ((s|k)|(i-'1))^<*D.((s|k)/.i)*>^((s|k)/^i)^<*s/.(k+1)*>
by A21,FINSEQ_7:def 1
.= (s|(i-'1))^<*D.((s|k)/.i)*>^((s|k)/^i)^<*s/.(k+1)*>
by A26,FUNCT_1:51
.= s|(i-'1)^<*D.((s|k)/.i)*>^(s/^i) by A27,FINSEQ_1:32
.= Replace(s,i,D.((s|k)/.i)) by A20,A28,FINSEQ_7:def 1
.= Replace(s,i,D.(s/.i)) by A23,A18,A16,FINSEQ_4:71;
(s/.(k+1)*DProd(D,(s|k)))/.i
= (Product (Replace(s|k,i,D.((s|k)/.i))))* (s/.(k+1))
by A19,A18,POLYNOM1:def 1
.= Product (Replace(s,i,D.(s/.i))) by A31,GROUP_4:6
.= DProd(D,s).i by Def3,A30;
hence thesis;
end;
A32: (Product (s|k))*s/.(k+1) = Product( s|(k+1)) by A13,GROUP_4:6
.= Product s by A5,FINSEQ_1:58;
A33: ((s/.(k+1))*DProd(D,(s|k)))^<* DProd(D,s)/.(k+1)*> = DProd(D,s)
proof
set F = (s/.(k+1))*DProd(D,(s|k));
A34: len F = len DProd(D,(s|k)) by MATRIXR1:16 .= len (s|k) by Def3
.= k by FINSEQ_1:59,A11; then
A35: dom F = Seg k by FINSEQ_1:def 3;
A36: len (F^<* DProd(D,s)/.(k+1)*>) = k+1 by A34,FINSEQ_2:16;
for i st 1 <= i & i <= len (F^<* DProd(D,s)/.(k+1)*>)
holds (F^<* DProd(D,s)/.(k+1)*>).i = DProd(D,s).i
proof
let i;
assume 1 <= i & i <= len (F^<* DProd(D,s)/.(k+1)*>); then
i in Seg (k+1) by A36; then
per cases by FINSEQ_2:7;
suppose
A39: i in Seg k; then
(F^<* DProd(D,s)/.(k+1)*>).i = F.i by A35,FINSEQ_1:def 7
.= ((s/.(k+1))*DProd(D,(s|k)))/.i by PARTFUN1:def 6,A39,A35
.= DProd(D,s).i by A17,A16,A39;
hence thesis;
end;
suppose
A40: i = k+1; then
(F^<* DProd(D,s)/.(k+1)*>).i
= DProd(D,s)/.(k+1) by A34,FINSEQ_1:42
.= DProd(D,s).(k+1) by PARTFUN1:def 6,A7,FINSEQ_1:4;
hence thesis by A40;
end;
end;
hence thesis by A36,A5,Def3;
end;
D.(Product s)
= s/.(k+1)*D.(Product (s|k))+(Product (s|k))*D.(s/.(k+1))
by Def1,A32
.= (s/.(k+1))*Sum DProd(D,(s|k)) + (Product (s|k))*D.(s/.(k+1))
by A4,A12
.= Sum((s/.(k+1))*DProd(D,(s|k))) + DProd(D,s)/.(k+1)
by A14,POLYNOM1:12
.= Sum( DProd(D,s)) by A33,FVSUM_1:71;
hence thesis;
end;
hence thesis;
end;
for k be non zero Nat holds P[k] from NAT_1:sch 10(A2,A3);
hence thesis by A1;
end;
begin
:: <section2>Proof of Leibnitz Formula for Power of Derivations</section2>
:::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Leibniz Formula for power of a derivation of a commutative ring
:: LBZ(D,n,x,y) = <* nC0*(D^n.x), nC1*(D^(n-1).x)*(D.y),......*>
:: D^n(x+y) = nC0*(D^n.x) + nC1*(D^(n-1).x)*(D.y) +
:: D^n(x+y) = Sum LBZ(D,n,x,y)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let R,D,n;
let x,y be Element of R;
func LBZ(D,n,x,y) -> FinSequence of the carrier of R means :Def4:
len it = n+1 & for i st i in dom it holds
it.i = (n choose (i-'1))*((D|^(n+1-'i)).x)*((D|^(i -' 1)).y);
existence
proof
deffunc F(Nat) = (n choose ($1-'1))*((D|^(n+1-'$1)).x)*((D|^($1 -' 1)).y);
consider z being FinSequence such that
A1: len z = n+1 & for k being Nat st k in dom z holds z.k = F(k)
from FINSEQ_1:sch 2;
take z;
z is FinSequence of R
proof
A2: for p be object st p in rng z holds
p in the carrier of R
proof
let p be object;
assume p in rng z; then
consider i be object such that
A3: i in dom z and
A4: p = z.i by FUNCT_1:def 3;
reconsider i as Nat by A3;
z.i = (n choose (i-'1))*((D|^(n+1-'i)).x)*((D|^(i -' 1)).y) by A1,A3;
hence thesis by A4;
end;
rng z c= the carrier of R by A2;
hence thesis by FINSEQ_1:def 4;
end;
hence thesis by A1;
end;
uniqueness
proof
let z1,z2 be FinSequence of the carrier of R such that
A7: len z1 = n+1 and
A8: for i be Nat st i in dom z1 holds
z1.i = (n choose (i-'1))*((D|^(n+1-'i)).x)*((D|^(i -' 1)).y) and
A9: len z2 = n+1 and
A10: for j be Nat st j in dom z2 holds
z2.j = (n choose (j-'1))*((D|^(n+1-'j)).x)*((D|^(j -' 1)).y);
A11: dom z1 = Seg (n+1) by A7,FINSEQ_1:def 3.= dom z2 by A9,FINSEQ_1:def 3;
for q be Nat st q in dom z1 holds z1.q = z2.q
proof
let q be Nat;
assume
A12: q in dom z1; then
reconsider q9 = q as Element of NAT;
z1.q
= (n choose (q9-'1))*((D|^(n+1-'q9)).x)*((D|^(q9 -' 1)).y) by A8,A12
.= z2.q9 by A10,A11,A12;
hence thesis;
end;
hence thesis by A11;
end;
end;
theorem Th15:
LBZ(D,0,x,y) = <* x*y *>
proof
A1: len LBZ(D,0,x,y) = 0+1 by Def4; then
dom(LBZ(D,0,x,y)) = Seg 1 by FINSEQ_1:def 3; then
A2: 1 in dom(LBZ(D,0,x,y));
A3: 0 choose (1-'1) = 0 choose 0 by XREAL_1:232 .= 1 by NEWTON:19;
A4: 1-'1 = 0 by XREAL_1:232;
LBZ(D,0,x,y).1 = 1*((D|^(0+1-'1)).x)*((D|^(1 -' 1)).y) by A3,A2,Def4
.= ((D|^(0+0)).x)*((D|^0).y) by A4,BINOM:13
.= ((D|^0).x)*((id R).y) by VECTSP11:18
.= ((id R).x)*((id R).y) by VECTSP11:18
.= x*y;
hence thesis by A1,FINSEQ_1:40;
end;
theorem Th16:
LBZ(D,1,x,y) = <* y*D.x, x*D.y *>
proof
len LBZ(D,1,x,y) = 1+1 by Def4; then
dom(LBZ(D,1,x,y)) = Seg 2 by FINSEQ_1:def 3; then
A2: 1 in dom(LBZ(D,1,x,y)) & 2 in dom(LBZ(D,1,x,y));
A3: 1 choose (1-'1) = 1 choose 0 by XREAL_1:232 .= 1 by NEWTON:19;
A4: 2-'1 = 2-1 by XREAL_1:233; then
A5: 1 choose (2-'1) = 1 by NEWTON:21;
A6: LBZ(D,1,x,y).1 = 1*((D|^(1+1-'1)).x)*((D|^(1 -' 1)).y) by A3,A2,Def4
.= ((D|^(2-'1)).x)*((D|^(1 -' 1)).y) by BINOM:13
.= ((D|^1).x)*((D|^0).y) by XREAL_1:232,A4
.= ((D|^1).x)*((id R).y) by VECTSP11:18
.= y*D.x by VECTSP11:19;
LBZ(D,1,x,y).2 = 1*((D|^(1+1-'2)).x)*((D|^(2 -' 1)).y) by A5,A2,Def4
.= ((D|^(2-'2)).x)*((D|^(2 -' 1)).y) by BINOM:13
.= ((D|^0).x)*((D|^1).y) by XREAL_1:232,A4
.= ((id R).x)*((D|^1).y) by VECTSP11:18
.= x*D.y by VECTSP11:19;
hence thesis by Def4,A6,FINSEQ_1:44;
end;
definition
let R,D,m;
let x,y be Element of R;
func LBZ0(D,m,x,y) -> FinSequence of the carrier of R means :Def5:
len it = m & for i st i in dom it holds
it.i = ((m choose (i-'1))+(m choose i))*((D|^(m+1 -'i)).x)*((D|^i).y);
existence
proof
deffunc F(Nat)
= ((m choose ($1-'1))+(m choose $1))*((D|^(m+1 -'$1)).x)*((D|^$1).y);
consider z being FinSequence such that
A1: len z = m & for k being Nat st k in dom z holds z.k = F(k)
from FINSEQ_1:sch 2;
take z;
z is FinSequence of R
proof
A2: for p be object st p in rng z holds
p in the carrier of R
proof
let p be object;
assume p in rng z; then
consider i be object such that
A3: i in dom z and
A4: p = z.i by FUNCT_1:def 3;
reconsider i as Nat by A3;
z.i = ((m choose (i-'1))+(m choose i))*((D|^(m+1 -'i)).x)*((D|^i).y)
by A1,A3;
hence thesis by A4;
end;
rng z c= the carrier of R by A2;
hence thesis by FINSEQ_1:def 4;
end;
hence thesis by A1;
end;
uniqueness
proof
let z1,z2 be FinSequence of the carrier of R such that
A7: len z1 = m and
A8: for i be Nat st i in dom z1 holds
z1.i = ((m choose (i-'1))+(m choose i))*((D|^(m+1 -'i)).x)*((D|^i).y) and
A9: len z2 = m and
A10: for j be Nat st j in dom z2 holds
z2.j = ((m choose (j-'1))+(m choose j))*((D|^(m+1 -'j)).x)*((D|^j).y);
A11: dom z1 = Seg m by A7,FINSEQ_1:def 3.= dom z2 by A9,FINSEQ_1:def 3;
for q be Nat st q in dom z1 holds z1.q = z2.q
proof
let q be Nat;
assume
A12: q in dom z1; then
reconsider q9 = q as Element of NAT;
z1.q9
=((m choose (q9-'1))+(m choose q9))*((D|^(m+1 -'q9)).x)*((D|^q9).y)
by A8,A12
.= z2.q9 by A10,A11,A12;
hence thesis;
end;
hence thesis by A11;
end;
end;
definition
let R,D,m;
let x,y be Element of R;
func LBZ1(D,m,x,y) -> FinSequence of the carrier of R means :Def6:
len it = m &
for i st i in dom it holds
it.i = (m choose (i-'1))*((D|^(m+1 -'i)).x)*((D|^i).y);
existence
proof
deffunc F(Nat) = (m choose ($1-'1))*((D|^(m+1 -'$1)).x)*((D|^$1).y);
consider z being FinSequence such that
A1: len z = m & for k being Nat st k in dom z holds z.k = F(k)
from FINSEQ_1:sch 2;
take z;
z is FinSequence of the carrier of R
proof
A2: for p be object st p in rng z holds
p in the carrier of R
proof
let p be object;
assume p in rng z; then
consider i be object such that
A3: i in dom z and
A4: p = z.i by FUNCT_1:def 3;
reconsider i as Nat by A3;
z.i = (m choose (i-'1))*((D|^(m+1 -'i)).x)*((D|^i).y) by A1,A3;
hence thesis by A4;
end;
rng z c= the carrier of R by A2;
hence thesis by FINSEQ_1:def 4;
end;
hence thesis by A1;
end;
uniqueness
proof
let z1,z2 be FinSequence of the carrier of R such that
A7: len z1 = m and
A8: for i be Nat st i in dom z1 holds
z1.i = (m choose (i-'1))*((D|^(m+1 -'i)).x)*((D|^i).y) and
A9: len z2 = m and
A10: for j be Nat st j in dom z2 holds
z2.j = (m choose (j-'1))*((D|^(m+1 -'j)).x)*((D|^j).y);
A11: dom z1 = Seg m by A7,FINSEQ_1:def 3.= dom z2 by A9,FINSEQ_1:def 3;
for q be Nat st q in dom z1 holds z1.q = z2.q
proof
let q be Nat;
assume
A12: q in dom z1; then
reconsider q9 = q as Element of NAT;
z1.q9 = (m choose (q9-'1))*((D|^(m+1 -'q9)).x)*((D|^q9).y) by A8,A12
.= z2.q9 by A10,A11,A12;
hence thesis;
end;
hence thesis by A11;
end;
end;
definition
let R,D,m;
let x,y be Element of R;
func LBZ2(D,m,x,y) -> FinSequence of the carrier of R means :Def7:
len it = m &
for i st i in dom it holds
it.i = (m choose i)*((D|^(m +1 -'i)).x)*((D|^i).y);
existence
proof
deffunc F(Nat) = (m choose $1)*((D|^(m+1 -'$1)).x)*((D|^$1).y);
consider z being FinSequence such that
A1: len z =m & for k being Nat st k in dom z holds z.k = F(k)
from FINSEQ_1:sch 2;
take z;
z is FinSequence of the carrier of R
proof
A2: for p be object st p in rng z holds
p in the carrier of R
proof
let p be object;
assume p in rng z; then
consider i be object such that
A3: i in dom z and
A4: p = z.i by FUNCT_1:def 3;
reconsider i as Nat by A3;
z.i = (m choose i)*((D|^(m+1 -'i)).x)*((D|^i).y) by A1,A3;
hence thesis by A4;
end;
rng z c= the carrier of R by A2;
hence thesis by FINSEQ_1:def 4;
end;
hence thesis by A1;
end;
uniqueness
proof
let z1,z2 be FinSequence of the carrier of R such that
A7: len z1 = m and
A8: for i be Nat st i in dom z1 holds
z1.i = (m choose i)*((D|^(m+1 -'i)).x)*((D|^i).y) and
A9: len z2 = m and
A10: for j be Nat st j in dom z2 holds
z2.j = (m choose j)*((D|^(m+1 -'j)).x)*((D|^j).y);
A11: dom z1 = Seg m by A7,FINSEQ_1:def 3.= dom z2 by A9,FINSEQ_1:def 3;
for q be Nat st q in dom z1 holds z1.q = z2.q
proof
let q be Nat;
assume
A12: q in dom z1; then
reconsider q9 = q as Element of NAT;
z1.q9 = (m choose q9)*((D|^(m+1 -'q9)).x)*((D|^q9).y) by A8,A12
.= z2.q9 by A10,A11,A12;
hence thesis;
end;
hence thesis by A11;
end;
end;
theorem
D.(Sum(LBZ0(D,n,x,y))) = Sum(D*(LBZ0(D,n,x,y))) by Th11;
theorem Th18:
LBZ0(D,m,x,y) = LBZ1(D,m,x,y) + LBZ2(D,m,x,y)
proof
set p = LBZ1(D,m,x,y);
set q = LBZ2(D,m,x,y);
set r = LBZ0(D,m,x,y);
A1: dom p = Seg len p by FINSEQ_1:def 3 .= Seg m by Def6;
A2: dom q = Seg len q by FINSEQ_1:def 3 .= Seg m by Def7;
A3: dom r = Seg len r by FINSEQ_1:def 3 .= Seg m by Def5;
A4: dom (p + q) = Seg m by A1,BINOM:def 1;
A5: Seg len (p+q) = dom (p + q) by FINSEQ_1:def 3 .= dom p by BINOM:def 1
.= Seg len p by FINSEQ_1:def 3 .= Seg m by Def6;
A6: len r = m by Def5 .= len (p+q) by A5,FINSEQ_1:6;
for k st 1 <= k & k <= len (p+q) holds (p+q).k = r.k
proof
let k be Nat;
assume
A7: 1 <= k & k <= len (p+q); then
A8: k in dom p by A1,A5; then
A9: p/.k = p.k by PARTFUN1:def 6
.= (m choose (k-'1))*((D|^(m+1 -'k)).x)*((D|^k).y) by A8,Def6;
A10: k in dom q by A2,A5,A7; then
A11: q/.k = q.k by PARTFUN1:def 6
.= (m choose k)*((D|^(m +1 -'k)).x)*((D|^k).y) by A10,Def7;
A12: k in dom r by A3,A5,A7;
k in dom (p+q) by A4,A5,A7; then
(p+q).k = (p+q)/.k by PARTFUN1:def 6
.= (m choose (k-'1))*((D|^(m+1 -'k)).x)*((D|^k).y)
+ (m choose k)*((D|^(m+1 -'k)).x)*((D|^k).y) by A11,A9,A7,BINOM:def 1
.= (m choose (k-'1))*(((D|^(m+1 -'k)).x)*((D|^k).y))
+ (m choose k)*((D|^(m+1 -'k)).x)*((D|^k).y) by BINOM:19
.= (m choose (k-'1))*(((D|^(m+1 -'k)).x)*((D|^k).y))
+ (m choose k)*(((D|^(m+1 -'k)).x)*((D|^k).y)) by BINOM:19
.= ((m choose (k-'1))+(m choose k))*(((D|^(m+1 -'k)).x)*((D|^k).y))
by BINOM:15
.= ((m choose (k-'1))+(m choose k))*((D|^(m+1 -'k)).x)*((D|^k).y)
by BINOM:19
.= r.k by A12,Def5;
hence thesis;
end;
hence thesis by A6;
end;
theorem Th19:
Sum LBZ0(D,n,x,y) = Sum LBZ1(D,n,x,y) + Sum LBZ2(D,n,x,y)
proof
set p= LBZ1(D,n,x,y);
set q= LBZ2(D,n,x,y);
set r= LBZ0(D,n,x,y);
A1: dom p = Seg len p by FINSEQ_1:def 3 .= Seg n by Def6;
A2: dom q = Seg len q by FINSEQ_1:def 3 .= Seg n by Def7;
Sum r = Sum(p + q) by Th18 .= Sum p + Sum q by A1,A2,BINOM:7;
hence thesis;
end;
theorem Th20:
D*LBZ0(D,n,x,y) = Del(LBZ2(D,n+1,x,y),n+1) + Del(LBZ1(D,n+1,x,y),1)
proof
set p= LBZ2(D,n+1,x,y);
set q= LBZ1(D,n+1,x,y);
set r= LBZ0(D,n,x,y);
A1: len p = n+1 by Def7;
A2: len q = n+1 by Def6;
A3: dom p = Seg len p by FINSEQ_1:def 3 .= Seg (n+1) by Def7;
A4: dom q = Seg len q by FINSEQ_1:def 3 .= Seg (n+1) by Def6;
A5: dom r = Seg len r by FINSEQ_1:def 3 .= Seg n by Def5;
A6: 1 <= n+1 by NAT_1:12; then
A7: n+1 in dom p by A1,FINSEQ_3:25;
A8: 1 in dom q by A2,A6,FINSEQ_3:25;
reconsider p1 = Del(p,n+1) as FinSequence of the carrier of R;
reconsider q1 = Del(q,1) as FinSequence of the carrier of R;
A9: dom Del(p,n+1) = Seg len p1 by FINSEQ_1:def 3
.= Seg n by A1,FINSEQ_3:109,A7;
A10: dom Del(q,1) = Seg len q1 by FINSEQ_1:def 3
.= Seg n by A2,FINSEQ_3:109,A8;
A11: dom (p1+q1) = Seg n by A9,BINOM:def 1;
A12: Seg len(p1+q1) = dom (p1+q1) by FINSEQ_1:def 3
.= Seg n by A9,BINOM:def 1;
A14: len (D*r) = len r by FINSEQ_2:33 .= n by Def5;
for i st 1 <= i & i <= len (D*r) holds (D*r).i = (p1 + q1).i
proof
let i;
assume
A16: 1 <= i & i <= len (D*r); then
A17: i in dom r by A5,A14;
A18: i in dom (D*r) by A16,FINSEQ_3:25;
A19: i in dom (p1+q1) by A14,A16,A11;
A20: 1 <= i & i <= len (p1+q1) by A12,FINSEQ_1:6,A14,A16;
A21: i < n+1 by A14,A16,XREAL_1:39;
A22: 1 <=i<=n+1 by A14,A16,XREAL_1:39; then
A23: i in dom p by A3;
i in dom p1 by A14,A16,A9; then
A24: p1/.i = p1.i by PARTFUN1:def 6 .= p.i by A21,FINSEQ_3:110
.= ((n+1) choose i)*((D|^((n+1) +1 -'i)).x)*((D|^i).y) by A23,Def7
.= ((n+1) choose i)*((D|^((n+2)-'i)).x)*((D|^i).y);
A25: 1 <= i+1 by NAT_1:12;
A26: i+1 <= n+1 by A21,INT_1:7; then
A28: (n+1)+1 -'(i+1) = (n+2) -(i+1) by XREAL_1:38,233
.= n+1-i
.= n+1-'i by A22,XREAL_1:233;
A27: (i+1) in dom q by A25,A26,A4;
A29: i in dom q1 by A14,A16,A10;
A30: 1 in dom q by A4,A6;
reconsider qq1 = q1 as (the carrier of R)-valued Function;
reconsider ii = i as object;
A31: q1/.i = qq1.ii by A29,PARTFUN1:def 6
.= q.(i+1) by A14,A16,A2,A30,FINSEQ_3:111;
A32: q1/.i
= ((n+1) choose ((i+1)-'1))*((D|^((n+1)+1 -'(i+1))).x)*((D|^(i+1)).y)
by A27,A31,Def6
.=((n+1) choose i)*((D|^(n+1-'i)).x)*((D|^(i+1)).y) by A28,NAT_D:34;
A33: i<=n+2 by A14,A16,XREAL_1:39;
A34: n+1 -'i+1 = (n+1) -i +1 by A22,XREAL_1:233 .= n+2 - i
.= (n+2) -'i by A33,XREAL_1:233;
i in dom r by A14,A16,A5; then
A35: r.i = ((n choose i)+(n choose (i-'1)))*((D|^(n+1 -'i)).x)*((D|^i).y)
by Def5
.= ((n choose ((i-'1)+1))+(n choose (i-'1)))*((D|^(n+1 -'i)).x)
*((D|^i).y) by A16,XREAL_1:235
.= ((n+1) choose ((i-'1)+1))*((D|^(n+1 -'i)).x)*((D|^i).y) by NEWTON:22
.= ((n+1) choose i)*((D|^(n+1 -'i)).x)*((D|^i).y)
by A16,XREAL_1:235;
(D*r)/.i = (D*r).i by A18,PARTFUN1:def 6
.= D.((((n+1) choose i)*((D|^(n+1 -'i)).x))*((D|^i).y) )
by A35, A17,FUNCT_1:13
.= D.((((n+1) choose i)*((D|^(n+1 -'i)).x)))*((D|^i).y)
+ (((n+1) choose i)*((D|^(n+1 -'i)).x))*D.((D|^i).y) by Def1
.= ((n+1) choose i)*(D.((D|^(n+1 -'i)).x))*((D|^i).y)
+ (((n+1) choose i)*((D|^(n+1 -'i)).x))*D.((D|^i).y) by Th6
.= ((n+1) choose i)*(((D|^(n+1 -'i+1)).x))*((D|^i).y)
+ (((n+1) choose i)*((D|^(n+1 -'i)).x))*D.((D|^i).y) by Th9
.= p1/.i + q1/.i by A32,A24,A34,Th9
.= (p1+q1)/.i by A20,BINOM:def 1; then
(D*r).i = (p1+q1)/.i by A18,PARTFUN1:def 6
.= (p1+q1).i by A19,PARTFUN1:def 6;
hence thesis;
end;
hence thesis by A14,A12,FINSEQ_1:6;
end;
Lm1:
for n st 1 <= n holds (LBZ1(D,n,x,y))/.1 = ((D|^n).x)*D.y
proof
let n;
assume
A1: n >= 1;
set p= LBZ(D,n,x,y);
set q= LBZ1(D,n,x,y);
dom q = Seg len q by FINSEQ_1:def 3 .= Seg n by Def6; then
A2: 1 in dom q by A1; then
q/.1 = q.1 by PARTFUN1:def 6
.=(n choose (1-'1))*((D|^(n+1 -'1)).x)*((D|^1).y) by A2,Def6
.= (n choose 0)*((D|^(n+1-'1)).x)*((D|^1).y) by XREAL_1:232
.= 1*((D|^(n+1-'1)).x)*((D|^1).y) by NEWTON:19
.= ((D|^(n+1-'1)).x)*((D|^1).y) by BINOM:13
.= ((D|^n).x)*((D|^1).y) by NAT_D:34
.= ((D|^n).x)*D.y by VECTSP11:19;
hence thesis;
end;
Lm2:
for n st 1 <= n holds (LBZ2(D,n,x,y))/.n = (D.x)*((D|^n).y)
proof
let n;
assume
A1: n >= 1;
set p= LBZ(D,n,x,y);
set q= LBZ2(D,n,x,y);
dom q = Seg len q by FINSEQ_1:def 3 .= Seg n by Def7; then
A2: n in dom q by A1;
A3: n +1 -'n = n+1-n by XREAL_1:233,NAT_1:12 .= 1;
q/.n = q.n by A2,PARTFUN1:def 6
.=(n choose n)*((D|^(n +1 -'n)).x)*((D|^n).y) by A2,Def7
.= 1*((D|^(n +1 -'n)).x)*((D|^n).y) by NEWTON:21
.= ((D|^1).x)*((D|^n).y) by A3,BINOM:13
.= (D.x)*((D|^n).y) by VECTSP11:19;
hence thesis;
end;
theorem Th21:
Sum(D*LBZ0(D,n,x,y)) =
- (LBZ1(D,n+1,x,y)/.1) + Sum LBZ0(D,n+1,x,y) - (LBZ2(D,n+1,x,y)/.(n+1))
proof
set p= LBZ2(D,n+1,x,y);
set q= LBZ1(D,n+1,x,y);
set r= LBZ0(D,n,x,y);
A1: len p = n+1 by Def7;
A2: len q = n+1 by Def6;
A3: 1 <= n+1 by NAT_1:12; then
A4: n+1 in dom p by A1,FINSEQ_3:25;
A5: 1 in dom q by A2,A3,FINSEQ_3:25;
set p1 = Del(p,n+1);
set q1 = Del(q,1);
set r1 = D*r;
A6: dom p1 = Seg len p1 by FINSEQ_1:def 3 .= Seg n by A1,A4,FINSEQ_3:109;
A7: dom q1 = Seg len q1 by FINSEQ_1:def 3 .= Seg n by A2,A5,FINSEQ_3:109;
reconsider p1,p,q1,q as FinSequence of R;
len p >= 1 by NAT_1:12,A1; then
A8: len p in dom p by FINSEQ_3:25;
reconsider a = p.(len p) as Element of R by A8,FINSEQ_2:11;
A9: a = (LBZ2(D,n+1,x,y)/.(n+1)) by A1,A8,PARTFUN1:def 6;
len q >= 1 by NAT_1:12,A2; then
A10: 1 in dom q by FINSEQ_3:25; then
reconsider b = q.1 as Element of R by FINSEQ_2:11;
A11: b = (LBZ1(D,n+1,x,y)/.1) by A10,PARTFUN1:def 6;
p <> {} by Def7; then
A13: Sum p = Sum( p1^<*a*> ) by A1,PRE_POLY:13
.= Sum p1 + Sum <*a*> by RLVECT_1:41
.= Sum p1 + a by BINOM:3;
q <> {} by Def6; then
A15: Sum q = Sum( <*b*>^q1 ) by FINSEQ_5:86
.= Sum <*b*> + Sum q1 by RLVECT_1:41
.= b + Sum q1 by BINOM:3;
Sum(D*LBZ0(D,n,x,y)) = Sum( p1 + q1) by Th20
.= Sum p1 + Sum q1 by A6,A7,BINOM:7
.= (Sum p - a) + Sum q1 by A13,VECTSP_2:2
.= (Sum p + (-a) + (Sum q - b)) by A15,VECTSP_2:2
.= (Sum p + (-a) + Sum q - b) by RLVECT_1:def 3
.= -b + ((Sum p + Sum q) -a) by RLVECT_1:def 3
.= -LBZ1(D,n+1,x,y)/.1 +(Sum p + Sum q) -LBZ2(D,n+1,x,y)/.(n+1)
by A9,A11,RLVECT_1:def 3;
hence thesis by Th19;
end;
theorem Th22:
LBZ(D,n+1,x,y) = <*((D|^(n+1)).x)*y *>^(LBZ0(D,n,x,y))^<* x*((D|^(n+1)).y)*>
proof
set p= LBZ(D,n+1,x,y);
set q= LBZ0(D,n,x,y);
set r = <* ((D|^(n+1)).x)*y *>^q^<* x*((D|^(n+1)).y) *>;
set r1 = <* ((D|^(n+1)).x)*y *>^q;
set r2 = r1^<* x*((D|^(n+1)).y) *>;
set r3 = q^<* x*((D|^(n+1)).y) *>;
r1 = Ins(q,0,((D|^(n+1)).x)*y) by FINSEQ_5:67; then
A2: len r1 = len q + 1 by FINSEQ_5:69 .= n + 1 by Def5;
A3: len p = (n+1)+1 by Def4 .= n + 2;
r = Ins(r1,n+1,x*((D|^(n+1)).y)) by A2,FINSEQ_5:68; then
A4: len r = n + 1 +1 by A2,FINSEQ_5:69 .= len p by A3;
for k st 1 <= k & k <= len p holds p.k = r.k
proof
let k;
assume
A5: 1 <= k & k <= len p;
A6: k in dom p by A5,FINSEQ_3:25;
n+1+1 > 0+1 by XREAL_1:8; then
A7: n+2 -'1 = n+2 - 1 by XREAL_1:233 .= n+1;
1 < k+1 & k < n+2 +1 by A5,A3,NAT_1:13; then
per cases by NAT_1:22;
suppose
A9: k = 1;
n+1+1 > 0+1 by XREAL_1:8; then
A10: n+2 -'1 = n+2 - 1 by XREAL_1:233 .= n+1;
A11: p.k = ((n+1) choose (k-'1))*((D|^((n+1)+1-'k)).x)*((D|^(k -' 1)).y)
by A6,Def4
.= ((n+1) choose 0)*((D|^(n+2-'1)).x)*((D|^(1-'1)).y)
by A9,XREAL_1:232
.= (1*((D|^(n+2-'1)).x))*((D|^(1-'1)).y) by NEWTON:19
.= ((D|^(n+2-'1)).x)*((D|^(1-'1)).y) by BINOM:13
.= ((D|^(n+1)).x)*((D|^0).y) by A10,XREAL_1:232
.= ((D|^(n+1)).x)*((id R).y) by VECTSP11:18
.= ((D|^(n+1)).x)*y;
r.k = (Ins(r1,n+1,x*((D|^(n+1)).y))).1 by A9,A2,FINSEQ_5:68
.= (<* ((D|^(n+1)).x)*y *>^q).1 by NAT_1:11,FINSEQ_5:75
.= p.k by A11,FINSEQ_1:41;
hence thesis;
end;
suppose
A12: 1 < k & k < n+2;
A13: dom r1 = Seg (n + 1) by A2,FINSEQ_1:def 3;
1+1 <= k by A12,INT_1:7; then
A15: 2 -1 <= k -1 by XREAL_1:9;
k + 1 <= n+2 by A12,INT_1:7; then
A17: k+1-1 <= n+2-1 by XREAL_1:9; then
A18: k in dom r1 by A13,A12;
reconsider s = k - 1 as Nat by A12;
reconsider q1 = <* ((D|^(n+1)).x)*y *> as FinSequence of R;
A19: dom q = Seg len q by FINSEQ_1:def 3 .= Seg n by Def5;
k - 1 <= n + 1 -1 by A17,XREAL_1:9; then
A21: s in dom q by A19,A15;
reconsider t = s -1 as Nat by A15;
A22: k-'1 = s by A12,XREAL_1:233;
A23: (n+1)+1-'k = (n+1)+1-k by A12,XREAL_1:233 .= (n+1) - s
.= (n+1) -'s by A12,A17,XREAL_1:9,233;
r.k = (q1^q ).(s+1) by A18, FINSEQ_1:def 7
.= (q1^q ).(len q1 + s) by FINSEQ_1:39
.= (LBZ0(D,n,x,y)).s by A21,FINSEQ_1:def 7
.= ((n choose (s-'1))+(n choose s))*((D|^(n+1 -'s)).x)*((D|^s).y)
by A21,Def5
.= ((n choose t)+(n choose (t+1)))*((D|^(n+1 -'s)).x)*((D|^s).y)
by A15,XREAL_1:233
.= ((n+1) choose (k-'1))*((D|^((n+1)+1-'k)).x)*((D|^(k-'1)).y)
by A23,A22,NEWTON:22
.= p.k by A6,Def4;
hence thesis;
end;
suppose
A24: k = n+2; then
A25: r.k = (Ins(r1,n+1,x*((D|^(n+1)).y))).(n+1+1) by A2,FINSEQ_5:68
.= x*((D|^(n+1)).y) by FINSEQ_5:73,A2;
p.k = ((n+1) choose (n+1))*
((D|^((n+1)+1-'(n+2))).x)*((D|^(n+2 -' 1)).y) by A7,A24,A6,Def4
.= 1*((D|^((n+1)+1-'(n+2))).x)*((D|^(n+2 -' 1)).y) by NEWTON:21
.= ((D|^((n+2 -'(n+2)))).x)*((D|^(n+2 -' 1)).y) by BINOM:13
.= ((D|^0).x)*((D|^(n+1)).y) by A7,XREAL_1:232
.= ((id R).x)*((D|^(n+1)).y) by VECTSP11:18
.= r.k by A25;
hence thesis;
end;
end;
hence thesis by A4;
end;
theorem Th23:
Sum(<* ((D|^(n+1)).x)*y *>^(LBZ0(D,n,x,y))^<* x*((D|^(n+1)).y) *>)
= ((D|^(n+1)).x)*y + Sum(LBZ0(D,n,x,y))+ x*((D|^(n+1)).y)
proof
set p1 = <* ((D|^(n+1)).x)*y *>;
set p2 = <* x*((D|^(n+1)).y) *>;
set q = (LBZ0(D,n,x,y));
set r = <*((D|^(n+1)).x)*y *>^(LBZ0(D,n,x,y))^<* x*((D|^(n+1)).y)*>;
set r1 = p1^q;
set r2 = r1^p2;
set r3 = q^p2;
A1: Sum(p1) = ((D|^(n+1)).x)*y by RLVECT_1:44;
r = p1^r3 by FINSEQ_1:32; then
Sum(r) = Sum(p1)+ Sum(q^p2) by RLVECT_1:41
.= ((D|^(n+1)).x)*y + (Sum(q)+Sum(p2)) by A1,RLVECT_1:41
.= ((D|^(n+1)).x)*y + (Sum(q)+ x*((D|^(n+1)).y) ) by RLVECT_1:44
.= ((D|^(n+1)).x)*y + Sum(q)+ x*((D|^(n+1)).y) by RLVECT_1:def 3;
hence thesis;
end;
theorem Th24:
D.(Sum(LBZ(D,n+1,x,y))) = Sum(LBZ(D,n+2,x,y))
proof
set p1 = <*((D|^(n+1)).x)*y*>;
set p2 = LBZ0(D,n,x,y);
set p3 = <*x*((D|^(n+1)).y)*>;
set q = LBZ(D,n+1,x,y);
A1: D.(((D|^(n+1)).x)*y) = D.((D|^(n+1)).x)*y +((D|^(n+1)).x)*D.y by Def1
.= ((D|^(n+1+1)).x)*y + ((D|^(n+1)).x)*D.y by Th9;
A2: D.(x*((D|^(n+1)).y)) = (D.x)*((D|^(n+1)).y) + x*D.((D|^(n+1)).y) by Def1
.= (D.x)*((D|^(n+1)).y) + x*((D|^(n+1+1)).y) by Th9;
A3: Sum(D*p2)
= -(LBZ1(D,n+1,x,y)/.1)+Sum LBZ0(D,n+1,x,y)-(LBZ2(D,n+1,x,y)/.(n+1))
by Th21
.= -(((D|^(n+1)).x)*D.y) +Sum LBZ0(D,n+1,x,y)-(LBZ2(D,n+1,x,y)/.(n+1))
by NAT_1:12,Lm1
.= -(((D|^(n+1)).x)*D.y) +Sum LBZ0(D,n+1,x,y)-((D.x)*((D|^(n+1)).y))
by NAT_1:12,Lm2;
D.(Sum(LBZ(D,n+1,x,y))) = Sum(D*(LBZ(D,n+1,x,y))) by Th11
.= Sum(D*(p1^p2^p3)) by Th22
.= Sum( (D*(p1^p2))^(D*p3)) by FINSEQOP:9
.= Sum(D*(p1^p2))+ Sum(D*p3) by RLVECT_1:41
.= Sum((D*p1)^(D*p2)) + Sum(D*p3) by FINSEQOP:9
.= Sum(D*p1)+ Sum(D*p2)+ Sum(D*p3) by RLVECT_1:41
.= Sum(<*D.(((D|^(n+1)).x)*y)*>)+ Sum(D*p2)+ Sum(D*p3) by FINSEQ_2:35
.= D.(((D|^(n+1)).x)*y)+ Sum(D*p2)+ Sum(D*p3) by BINOM:3
.= D.(((D|^(n+1)).x)*y)+ Sum(D*p2)+ Sum(<* D.(x*((D|^(n+1)).y))*>)
by FINSEQ_2:35
.= ((D|^(n+1+1)).x)*y + ((D|^(n+1)).x)*D.y
+ (-((D|^(n+1)).x)*D.y + Sum(LBZ0(D,n+1,x,y))-(D.x)*((D|^(n+1)).y))
+ D.(x*((D|^(n+1)).y)) by A3,A1,BINOM:3
.= ((D|^(n+1+1)).x)*y + ((D|^(n+1)).x)*D.y
+ (-((D|^(n+1)).x)*D.y +(Sum( LBZ0(D,n+1,x,y)) -(D.x)*((D|^(n+1)).y)))
+ D.(x*((D|^(n+1)).y)) by RLVECT_1:def 3
.= ((D|^(n+1+1)).x)*y + ((D|^(n+1)).x)*D.y
-((D|^(n+1)).x)*D.y +((Sum( LBZ0(D,n+1,x,y)) -(D.x)*((D|^(n+1)).y)))
+ D.(x*((D|^(n+1)).y)) by RLVECT_1:def 3
.= ((D|^(n+1+1)).x)*y + (((D|^(n+1)).x)*D.y
-((D|^(n+1)).x)*D.y) +((Sum( LBZ0(D,n+1,x,y)) -(D.x)*((D|^(n+1)).y)))
+ D.(x*((D|^(n+1)).y)) by RLVECT_1:def 3
.= ((D|^(n+1+1)).x)*y + (0.R)
+((Sum( LBZ0(D,n+1,x,y)) -(D.x)*((D|^(n+1)).y)))
+ D.(x*((D|^(n+1)).y)) by RLVECT_1:15
.= ((D|^(n+1+1)).x)*y
+ Sum( LBZ0(D,n+1,x,y))+(-(D.x)*((D|^(n+1)).y))
+ ((D.x)*((D|^(n+1)).y) + x*((D|^(n+1+1)).y)) by A2,RLVECT_1:def 3
.= ((D|^(n+1+1)).x)*y
+ Sum( LBZ0(D,n+1,x,y))+((-(D.x)*((D|^(n+1)).y))
+ ((D.x)*((D|^(n+1)).y) + x*((D|^(n+1+1)).y))) by RLVECT_1:def 3
.= ((D|^(n+1+1)).x)*y
+ Sum( LBZ0(D,n+1,x,y))+(( -(D.x)*((D|^(n+1)).y)
+ (D.x)*((D|^(n+1)).y)) + x*((D|^(n+1+1)).y)) by RLVECT_1:def 3
.= ((D|^(n+1+1)).x)*y
+ Sum( LBZ0(D,n+1,x,y))+((0.R) + x*((D|^(n+1+1)).y)) by RLVECT_1:5
.= Sum(<*((D|^(n+1+1)).x)*y*>^(LBZ0(D,n+1,x,y))^<*x*((D|^(n+1+1)).y)*>)
by Th23
.= Sum LBZ(D,n+1+1,x,y) by Th22;
hence thesis;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::
:: Leibniz Formula for Power of Derivation.
:::::::::::::::::::::::::::::::::::::::::::::::::
theorem
(D|^n).(x*y) = Sum(LBZ(D,n,x,y))
proof
per cases;
suppose
A1: n <> 0;
defpred P[Nat] means (D|^$1).(x*y) = Sum(LBZ(D,$1,x,y));
Sum(LBZ(D,1,x,y)) = Sum <* y*D.x, x*D.y *> by Th16
.= Sum(<* y*D.x *>) + x*D.y by FVSUM_1:71
.= y*D.x + x*D.y by BINOM:3
.= D.(x*y) by Def1; then
A2: P[1] by VECTSP11:19;
A3: for n being non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A4: P[n];
reconsider k = n-1 as Nat;
(D|^(n+1)).(x*y) = D.(Sum(LBZ(D,k+1,x,y))) by A4,Th9
.= Sum(LBZ(D,k+2,x,y)) by Th24
.= Sum(LBZ(D,n+1,x,y));
hence thesis;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A2,A3);
hence thesis by A1;
end;
suppose
A5: n = 0;
Sum(LBZ(D,0,x,y)) = Sum<* x*y *> by Th15
.= (id R).(x*y) by BINOM:3
.= (D|^0).(x*y) by VECTSP11:18;
hence thesis by A5;
end;
end;
begin
::<section3>Example of Derivation of Polynomial Ring over a Commutative Ring</section3>
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:::: formalize derivation of Polynom-Ring R.
:::: start with same fashion of poly_diff of POLYDIFF1:
:::: However resource of Def of poly_diff of POLYDIFF1 cannot be imported
:::: with the environment of this article technically.
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::: Relations between
::: Element of the carrier of Polynom-Ring R and Polynomial of R
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let R;
let f be Function of Polynom-Ring R, Polynom-Ring R;
let p be Element of the carrier of Polynom-Ring R;
redefine func f.p -> Element of the carrier of Polynom-Ring R; :: redefines . (FUNCT_1, definition)
coherence
proof
f.p is Element of Polynom-Ring R;
hence thesis;
end;
end;
definition
let R be Ring;
func Der1(R) -> Function of Polynom-Ring R, Polynom-Ring R means :Def8:
for f being Element of the carrier of Polynom-Ring R
for i being Nat holds (it.f).i = (i+1)*f.(i+1);
existence
proof
A1: for f being Polynomial of R ex g being Polynomial of R
st for i being Nat holds g.i = (i+1)*f.(i+1)
proof
let f be Polynomial of R;
deffunc F(Nat) = ($1+1)*f.($1+1);
consider q being AlgSequence of R such that
A2: len q <= len f & for k being Nat st k < len f holds q.k = F(k)
from ALGSEQ_1:sch 1;
take q;
now let i be Nat;
per cases;
suppose
A3: i +1 <= len f;
i < i + 1 by XREAL_1:29; then
i < len f by A3, XXREAL_0:2;
hence q.i = (i+1)*f.(i+1) by A2;
end;
suppose
A4: i+1 > len f; then
A5: len q < i+1 by A2,XXREAL_0:2;
thus (i+1)*f.(i+1) = (i+1)*0.R by ALGSEQ_1:8,A4
.= 0.R by Th3 .= q.i by A5,NAT_1:13,ALGSEQ_1:8;
end;
end;
hence thesis;
end;
defpred P[object,object] means
ex f,g being Polynomial of R
st $1 = f & $2 = g & for i being Nat holds g.i = (i+1)*f.(i+1);
A6: for x being object st x in the carrier of Polynom-Ring R
ex y being object st y in the carrier of Polynom-Ring R & P[x,y]
proof
let x be object;
assume x in the carrier of Polynom-Ring R; then
reconsider y = x as Polynomial of R by POLYNOM3:def 10;
consider z being Polynomial of R such that
A7: for i being Nat holds z.i = (i+1)*y.(i+1) by A1;
take z;
thus thesis by A7,POLYNOM3:def 10;
end;
consider F being Function of
the carrier of Polynom-Ring R, the carrier of Polynom-Ring R such that
A8: for x being object st x in the carrier of Polynom-Ring R holds P[x,F.x]
from FUNCT_2:sch 1(A6);
take F;
now let f,g be Polynomial of R;
assume
A9: g = F.f;
let i be Nat;
f in the carrier of Polynom-Ring R by POLYNOM3:def 10; then
P[f,F.f] by A8;
hence g.i = (i+1)*f.(i+1) by A9;
end;
hence thesis;
end;
uniqueness
proof
let F,G be Function of Polynom-Ring R, Polynom-Ring R;
assume that
A10: for f being Element of the carrier of Polynom-Ring R
for i being Nat holds (F.f).i = (i+1)*f.(i+1) and
A11: for f being Element of the carrier of Polynom-Ring R
for i being Nat holds (G.f).i = (i+1)*f.(i+1);
now let o be object;
assume o in the carrier of Polynom-Ring R;
then reconsider p = o as Element of the carrier of Polynom-Ring R;
now let u be object;
assume u in NAT; then
reconsider m = u as Nat;
(F.p).m = (m+1)*p.(m+1) by A10 .= (G.p).m by A11;
hence (F.p).u = (G.p).u;
end;
then F.p = G.p;
hence F.o = G.o;
end;
hence F = G;
end;
end;
registration let R;
cluster Der1(R) -> additive;
coherence
proof
now let a,b be Element of the carrier of Polynom-Ring R;
reconsider gab = (Der1(R)).a + (Der1(R)).b
as Element of the carrier of Polynom-Ring R;
reconsider a1 = a, b1 = b as sequence of the carrier of R;
reconsider ab1 = a1 + b1 as sequence of R;
reconsider ga1 = (Der1(R)).a, gb1 = (Der1(R)).b as sequence of R;
set gab1 = ga1 + gb1;
now let m be Element of NAT;
ab1 = a + b by POLYNOM3:def 10; then
((Der1(R)).(a + b)).m = (m+1)*(ab1).(m+1) by Def8
.= (m+1)*(a1.(m+1)+b1.(m+1)) by NORMSP_1:def 2
.= (m+1)*a1.(m+1)+ (m+1)*b1.(m+1) by Th1
.= ga1.m + (m+1)*b1.(m+1) by Def8
.= (ga1).m + (gb1).m by Def8
.= gab1.m by NORMSP_1:def 2;
hence ((Der1(R)).(a + b)).m = gab.m by POLYNOM3:def 10;
end;
hence (Der1(R)).(a + b) = (Der1(R)).a + (Der1(R)).b by FUNCT_2:63;
end;
hence Der1(R) is additive;
end;
end;
::::::::::::::::::::::::::::::::::::::
:: additive property for sequences
:: Map { f1, f2,...} -> {D_f1,D_f2,...}
:: (Der1(R))*p;
::::::::::::::::::::::::::::::::::::::::::
::::::::::::::::::::::::::::::::::::::::
:: Properties of Der1(R)
::::::::::::::::::::::::::::::::::::::::
reserve R for domRing;
reserve f,g for Element of the carrier of Polynom-Ring R;
theorem
for f be Element of the carrier of Polynom-Ring R, f1 be Polynomial of R
st f = f1 & f1 is constant holds (Der1(R)).f = 0_.R
proof
let f be Element of the carrier of Polynom-Ring R, f1 be Polynomial of R;
assume
A1: f = f1 & f1 is constant;
for i be Element of NAT holds ((Der1(R)).f).i = (0_.R).i
proof
let i be Element of NAT;
((Der1(R)).f).i = (i+1)*(f1.(i+1)) by A1,Def8
.= (i+1)*0.R by ALGSEQ_1:8,A1,XREAL_1:20
.= (0_.R).i by Th3;
hence thesis;
end;
hence (Der1(R)).f = 0_.R;
end;
reserve a for Element of R;
Lm3:(a|R) = <%a%>
proof
for j be Nat holds (a|R).j = <%a%>.j
proof
let j be Nat;
(a|R).j = (a * 1_.(R)).j by RING_4:16 .= <%a%>.j by POLYNOM5:29;
hence thesis;
end;
hence thesis;
end;
theorem Th27:
for i be Nat, p be Element of the carrier of Polynom-Ring R
holds ((a|R)*'p).i = a*p.i
proof
let i be Nat, p be Element of the carrier of Polynom-Ring R;
reconsider p1 = p as Polynomial of R;
per cases;
suppose
A1: i = 0; then
((a|R)*'p1).i = (<%a%>*'p1).0 by Lm3
.= (<%a,0.R%>*'p1).0 by POLYNOM5:43
.= a*p1.i by A1,UPROOTS:37;
hence thesis;
end;
suppose i <> 0; then
consider j be Nat such that
A3: i = j+ 1 by NAT_1:6;
((a|R)*'p1).i = (<%a%>*'p1).(j+1) by A3,Lm3
.= (<%a,0.R%>*'p1).(j+1) by POLYNOM5:43
.= a*p1.(j+1)+0.R*p1.j by UPROOTS:37
.= a*p1.(j+1);
hence thesis by A3;
end;
end;
theorem Th28:
for f,g being Element of the carrier of Polynom-Ring R, a be Element of R
st f = a|R holds (Der1(R)).(f*g) = (a|R)*'((Der1(R)).g)
proof
let f,g be Element of the carrier of Polynom-Ring R,
a be Element of R;
assume
A1: f = a|R;
reconsider f1 = f, g1 = g as sequence of R;
reconsider f9 = f, g9 = g as Polynomial of R;
reconsider fg0 = f * g as Element of Polynom-Ring R;
reconsider fg9 = f9 *' g9 as Element of Polynom-Ring R
by POLYNOM3:def 10;
reconsider fg1 = f1 *' g1 as sequence of R;
A2: f * g = (a|R) *' g9 by A1,POLYNOM3:def 10;
for n be Nat holds ((Der1(R)).(f*g)).n = ((a|R)*'((Der1(R)).g)).n
proof
let n be Nat;
reconsider b = g9.(n+1) as Element of R;
reconsider Dg = (Der1(R)).g as Polynomial of R;
((Der1(R)).(f*g)).n = (n+1)*((a|R)*'g9).(n+1) by A2,Def8
.= (n+1)*(a*g9.(n+1)) by Th27
.= a*((n+1)*(g9.(n+1))) by BINOM:19
.= a*((Der1(R)).g).n by Def8
.= ((a|R)*'((Der1(R)).g)).n by Th27;
hence thesis;
end;
hence thesis;
end;
theorem Th29:
for f being Element of the carrier of Polynom-Ring R, a be Element of R
st f = anpoly(a,0) holds (Der1(R)).f = 0_.R
proof
let f be Element of the carrier of Polynom-Ring R, a be Element of R;
assume
A1: f = anpoly(a,0);
for n be Element of NAT holds ((Der1(R)).f).n = (0_.R).n
proof
let n be Element of NAT;
((Der1(R)).f).n = (n+1)*(anpoly(a,0).(n+1)) by A1,Def8
.= (n+1) * 0.R by POLYDIFF:25
.= (0_.R).n by Th3;
hence thesis;
end;
hence (Der1(R)).f = 0_.R;
end;
theorem Th30:
for f being Element of the carrier of Polynom-Ring R, a be Element of R
st f = anpoly(a,1) holds (Der1(R)).f = anpoly(a,0)
proof
let f be Element of the carrier of Polynom-Ring R, a be Element of R;
reconsider f1 = f as Polynomial of R;
assume
A1: f = anpoly(a,1);
for n be Element of NAT holds ((Der1(R)).f).n = anpoly(a,0).n
proof
let n be Element of NAT;
per cases;
suppose
A2: n = 0; then
((Der1(R)).f).n = (0+1)*(f1.(0+1)) by Def8
.= 1 * a by A1,POLYDIFF:24
.= a by BINOM:13
.= anpoly(a,0).n by A2,POLYDIFF:24;
hence thesis;
end;
suppose
A3: n <> 0; then
A4: n + 1 <> 1;
((Der1(R)).f).n = (n+1)*(anpoly(a,1).(n+1)) by A1,Def8
.= (n+1) * 0.R by A4,POLYDIFF:25
.= 0.R by Th3
.= anpoly(a,0).n by A3,POLYDIFF:25;
hence thesis;
end;
end;
hence (Der1(R)).f = anpoly(a,0);
end;
theorem Th31:
for p,q be Polynomial of R st p = anpoly(1.R,1) holds
for i be Element of NAT holds (p*'q).(i+1) = q.i &(p*'q).0 = 0.R
proof
let p,q be Polynomial of R;
assume
A1: p = anpoly(1.R,1);
reconsider pq = p*'q as Polynomial of R;
A2: for i be Element of NAT holds (p*'q).(i+1) = q.i
proof
let i be Element of NAT;
consider FGi be FinSequence of the carrier of R such that
A3: len FGi = ((i+1) + 1) and
A4: (p*'q).(i+1) = Sum FGi and
A5: for k be Element of NAT st k in dom FGi holds
FGi.k = p.(k-'1)*q.((i+2) -' k) by POLYNOM3:def 9;
A6: dom FGi = Seg(i+2) by A3, FINSEQ_1:def 3;
A7: dom FGi = Seg(i+2) by A3, FINSEQ_1:def 3;
A8: 2 -' 1 = 2 -1 by XREAL_1:233;
A9: p.0 = 0.R by A1,POLYDIFF:25;
1 <= (i+1)+1 by NAT_1:11; then
A11: 1 in dom FGi by A6; then
A12: FGi/.1 = FGi.1 by PARTFUN1:def 6
.= p.(1-'1)*q.((i+2) -' 1) by A5,A11
.= 0.R * q.(i+2 -' 1) by A9,XREAL_1:232
.= 0.R;
A13: p.1 = 1.R by A1,POLYDIFF:24;
2 <= i+2 by NAT_1:11;then
2 in Seg(i+2); then
A14: 2 in dom FGi by A3, FINSEQ_1:def 3; then
A15: FGi/.2 = FGi.2 by PARTFUN1:def 6
.= p.1* q.(i+2 -' 2) by A8,A5,A14
.= q.i by A13,NAT_D:34;
A16: FGi is non empty by A3;
set FGi1 = FGi/^1;
reconsider e = 1 as Nat;
A17: (FGi|e) = <*FGi.1*> by A16,FINSEQ_5:20
.= <*FGi/.1*> by A11,PARTFUN1:def 6; then
A18: i + 2 = len( <* FGi/.1 *>^FGi1) by A3,RFINSEQ:8
.= 1 + len FGi1 by FINSEQ_5:8; then
A19: FGi1 is non empty by NAT_1:11;
A20: dom FGi1 = Seg (i+1) by A18, FINSEQ_1:def 3;
A21: 1 <= i+1 by NAT_1:11; then
A22: 1 in Seg(i+1);
A23: 1 in dom FGi1 by A20,A21;
set FGi2 = FGi1/^1;
A24: (FGi1|e) = <*FGi1.1*> by A19,FINSEQ_5:20
.= <*FGi1/.1*> by A20,A22,PARTFUN1:def 6; then
A25: i + 1 = len( <* FGi1/.1 *>^FGi2) by A18,RFINSEQ:8
.= 1 + len FGi2 by FINSEQ_5:8;
A26: FGi/.2 = FGi.2 by A14,PARTFUN1:def 6
.= (<* FGi/.1 *>^FGi1).(1+1) by A17,RFINSEQ:8
.= FGi1.1 by A23,FINSEQ_3:103
.= FGi1/.1 by A23, PARTFUN1:def 6;
A27: Sum FGi2 = 0.R
proof
for j be Element of NAT st j in dom FGi2 holds FGi2.j = 0.R
proof
let j be Element of NAT;
assume
A28: j in dom FGi2;
dom FGi2 = Seg i by A25,FINSEQ_1:def 3; then
A30: j <= i & 1 <= j by A28,FINSEQ_1:1; then
A32: j + 1 <= i + 1 by XREAL_1:6;
j+1 >= 1 by NAT_1:11; then
A33: j+1 in dom FGi1 by A20,A32;
A34: FGi.(j+2) = (<* FGi/.1 *>^FGi1).(j+1+1) by A17,RFINSEQ:8
.= FGi1.(j+1) by A33,FINSEQ_3:103
.= (<* FGi1/.1 *>^FGi2).(j+1) by A24,RFINSEQ:8
.= FGi2.j by A28,FINSEQ_3:103;
A35: j + 1 + 1 >= 1+1 by NAT_1:11,XREAL_1:6; then
A36: j+2 >= 1 by XXREAL_0:2;
j + 2 <= i + 2 by A30,XREAL_1:6; then
A38: j+2 in dom FGi by A7,A36;
j+1 >=1 +1 by A30,XREAL_1:6; then
1 <> j + 1; then
A40: p.(j+1) = 0.R by A1,POLYDIFF:25;
A41: (j+2)-'1 = (j+2) -1 by A35,XXREAL_0:2,XREAL_1:233 .= j+1;
FGi.(j+2) = p.(j+1)*q.((i+2) -' (j+2)) by A41,A5,A38
.= 0.R by A40;
hence thesis by A34;
end;
hence thesis by POLYNOM3:1;
end;
A42: Sum FGi = Sum (<* FGi/.1 *>^FGi1) by A17,RFINSEQ:8
.= FGi/.1 + Sum FGi1 by FVSUM_1:72;
Sum(FGi1) = Sum(<* FGi1/.1 *>^FGi2) by A24,RFINSEQ:8
.= FGi1/.1 + Sum FGi2 by FVSUM_1:72;
hence thesis by A4,A27,A15,A26,A12,A42;
end;
consider FG0 be FinSequence of the carrier of R such that
A44: len FG0 = 0+1 & (p*'q).0 = Sum FG0 &
for k being Element of NAT st k in dom FG0
holds FG0.k = p.(k-'1) * q.(0+1-'k) by POLYNOM3:def 9;
1 in Seg len FG0 by A44; then
1 in dom FG0 by FINSEQ_1:def 3; then
FG0.1 = p.(1-'1) * q.(0+1-'1) by A44
.= p.0 * q.(0+1-'1) by NAT_D:34
.= anpoly(1.R,1).0 * q.0 by A1,NAT_D:34
.= 0.R * q.0 by POLYDIFF:25;then
FG0 = <*0.R*> by FINSEQ_1:40,A44;
hence thesis by A2,A44,RLVECT_1:44;
end;
theorem Th32:
for f,g be Element of the carrier of Polynom-Ring R
st f = anpoly(1.R,1) holds
(Der1(R)).(f*g) = ((Der1(R)).f)*g + f*((Der1(R)).g)
proof
let f,g be Element of the carrier of Polynom-Ring R;
assume
A1: f = anpoly(1.R,1);
reconsider df1 = (Der1(R)).f, dg1 = (Der1(R)).g as Polynomial of R;
reconsider f1 = f, g1 = g as Polynomial of R;
A2: df1*'g1 = ((Der1(R)).f)*g & f1*'dg1 = f*((Der1(R)).g)
by POLYNOM3:def 10;
for i be Element of NAT holds
((Der1(R)).(f*g)).i = (df1*'g1 + f1*'dg1).i
proof
let i be Element of NAT;
f*g = f1*'g1 by POLYNOM3:def 10; then
A3: ((Der1(R)).(f*g)).i = (i+1)*(f1*'g1.(i+1)) by Def8
.= (i+1)*g1.i by A1,Th31;
A4: (df1 *' g1) = anpoly(1.R,0) *' g1 by Th30,A1
.= (1_.R) *' g1 .= g1;
A5: (df1 *' g1 + f1 *' dg1).i = g1.i + (f1 *' dg1).i by A4,NORMSP_1:def 2;
per cases;
suppose i > 0; then
reconsider j = i - 1 as Element of NAT by INT_1:3;
(f1*'dg1).(j+1) = dg1.j by Th31,A1; then
A8: (f1*'dg1).i = i*g1.i by Def8;
f*g = f1*'g1 by POLYNOM3:def 10; then
((Der1(R)).(f*g)).i = (i+1)*(f1*'g1).(i+1) by Def8
.= i*(f1*'g1).(i+1) + 1*(f1*'g1).(i+1) by BINOM:15
.= i*(f1*'g1).(i+1) + (f1*'g1).(i+1) by BINOM:13
.= i*((f1*'g1).(i+1)) + g1.i by A1,Th31
.= i*g1.i+ g1.i by A1,Th31;
hence thesis by A4,NORMSP_1:def 2,A8;
end;
suppose i <= 1; then
i <1 or i=1 by XXREAL_0:1; then
per cases by NAT_1:14;
suppose
A12: i = 1;
(f1*'dg1).(0+1) = dg1.0 by A1,Th31
.= (0+1)*g1.(0+1) by Def8.= 1* g1.1; then
(df1*'g1 + f1*'dg1).i = 1* g1.1 + 1* g1.1 by A5,A12,BINOM:13
.= ((Der1(R)).(f*g)).i by A3,A12,BINOM:15;
hence thesis;
end;
suppose
A14: i = 0; then
(df1*'g1 + f1*'dg1).i = g1.0 + 0.R by A1,A5,Th31 .= g1.0;
hence thesis by A3,A14,BINOM:13;
end;
end;
end; then
(Der1(R)).(f*g) = df1*'g1 + f1*'dg1;
hence thesis by A2,POLYNOM3:def 10;
end;
Lm4:
for p be non constant Polynomial of R holds
LM p = (p.(deg p)*anpoly(1.R,deg p -' 1))*'anpoly(1.R,1)
proof
let p be non constant Polynomial of R;
A1: p is non constant; then
A2: deg p >= 0+1 by INT_1:7;
reconsider n = deg p - 1 as Nat by A1;
len p = deg p + 1; then
p.(deg p) is non zero by ALGSEQ_1:10; then
reconsider a = p.(deg p) as non zero Element of R;
A4: anpoly(a,n) = anpoly(1.R*a,n) .= a*anpoly(1.R,n) by FIELD_1:9;
LM p = anpoly(a*1.R,n+1) by FIELD_1:11
.= (a*anpoly(1.R,n))*'anpoly(1.R,1) by A4,FIELD_1:10
.= (p.(deg p)*anpoly(1.R,deg p -' 1))*'anpoly(1.R,1) by A2,XREAL_1:233;
hence thesis;
end;
theorem
for f, g be constant Element of the carrier of Polynom-Ring R holds
(Der1(R)).(f*g) = ((Der1(R)).f)*g + f*((Der1(R)).g)
proof
let f,g be constant Element of the carrier of Polynom-Ring R;
consider a being Element of R such that
A1: f = (a|R) by RING_4:20;
consider b being Element of R such that
A2: g = b|R by RING_4:20;
A3: f = anpoly(a,0) by A1;
A4: g = anpoly(b,0) by A2;
reconsider p = f, q = g as Polynomial of R;
reconsider dp = (Der1(R)).f, dq = (Der1(R)).g as Polynomial of R;
A5: f*g = (a|R)*'(b|R) by A1,A2,POLYNOM3:def 10
.= (a * b)|R by RING_4:18;
reconsider h = f*g as Element of Polynom-Ring R;
consider c be Element of R such that
A6: h = c|R by A5;
A7: h = anpoly(c,0) by A6;
A8: dp = 0_.R by A3,Th29 .= (0.R)|R by RING_4:13;
A9: dq = 0_.R by A4,Th29 .= (0.R)|R by RING_4:13;
A10: dp*'q = (0.R*b)|R by A8,A2,RING_4:18 .= 0.R|R;
p*'dq = (a*0.R)|R by A9,A1,RING_4:18 .= 0.R|R; then
A11: dp*'q + p*'dq = 0_.R by A10,RING_4:13;
f*((Der1(R)).g) = p*'dq & ((Der1(R)).f)*g = dp*'q
by POLYNOM3:def 10; then
((Der1(R)).f)*g + f*((Der1(R)).g) = 0_.R by A11,POLYNOM3:def 10
.= (Der1(R)).(f*g) by A7,Th29;
hence thesis;
end;
theorem Th34:
for f, g be Element of the carrier of Polynom-Ring R
st f is constant holds (Der1(R)).(f*g) = ((Der1(R)).f)*g + f*((Der1(R)).g)
proof
let f,g be Element of the carrier of Polynom-Ring R;
assume f is constant; then
consider a being Element of R such that
A2: f = a|R by RING_4:20;
reconsider p = f, q = g as Polynomial of R;
reconsider dp = (Der1(R)).f, dq = (Der1(R)).g as Polynomial of R;
f = anpoly(a,0) by A2; then
A4: dp = 0_.R by Th29;
f*((Der1(R)).g) = p*'dq & ((Der1(R)).f)*g = dp*'q
by POLYNOM3:def 10; then
((Der1(R)).f)*g + f*((Der1(R)).g) = 0_.R + p*'dq by A4,POLYNOM3:def 10
.= (Der1(R)).(f*g) by A2,Th28;
hence thesis;
end;
theorem Th35:
for x,y be Element of the carrier of Polynom-Ring R st x is non constant
holds (Der1(R)).(x*y) = ((Der1(R)).x)*y + x*((Der1(R)).y)
proof
let x,y be Element of the carrier of Polynom-Ring R;
assume
A1: x is non constant;
defpred P[Nat] means
for f,g be Element of the carrier of Polynom-Ring R,
f0,g0 be Element of the carrier of Polynom-Ring R
st f0 = f & g0 = g & deg f0 -1 = $1 holds
(Der1(R)).(f0*g0) = ((Der1(R)).f0)*g0 + f0*((Der1(R)).g0);
A2: for k be Nat st for n be Nat st n < k holds P[n] holds P[k]
proof
let k be Nat;
assume
A3: for n be Nat st n < k holds P[n];
for f,g be Element of the carrier of Polynom-Ring R
st deg f -1 = k
holds (Der1(R)).(f*g) = ((Der1(R)).f)*g + f*((Der1(R)).g)
proof
let f,g be Element of the carrier of Polynom-Ring R;
assume
A4: deg f -1 = k;
reconsider f1 = f, g1 = g as Polynomial of R;
A5: f1 is non constant by A4;
A6: 1+1 <= 1+1+k by NAT_1:11;
consider u1 being Polynomial of R such that
A7: len u1 < len f1 & f1 = u1 + LM f1 &
for i be Element of NAT st i < len f1-1
holds u1.i = f1.i by A4,A6,POLYNOM4:16;
reconsider u = u1,
an = anpoly(1.R,1) as Element of Polynom-Ring R by POLYNOM3:def 10;
reconsider df1 = (Der1(R)).f, dg1 = (Der1(R)).g as Polynomial of R;
A8: LC f1 = f1.(deg f1) by A4,A6,XXREAL_0:2,XREAL_1:233;
reconsider f1 as non constant Polynomial of R by A5;
A9: LM f1 = ((LC f1)* anpoly(1.R,deg f1 -' 1))*'anpoly(1.R,1) by A8,Lm4;
A10: len f1 = deg f1 + 1;
f1.(deg f1) is non zero by A10,ALGSEQ_1:10; then
reconsider a = f1.(deg f1) as non zero Element of R;
reconsider h1 = (LC f1)*anpoly(1.R,deg f1 -' 1) as Polynomial of R;
A11: deg h1 = deg anpoly(1.R,deg f1 -' 1) by RING_5:4
.= deg f1 -' 1 by FIELD_1:4;
(Der1(R)).(f*g) = ((Der1(R)).f)*g + f*((Der1(R)).g)
proof
f1 = u1 + h1*'anpoly(1.R,1) by A7,A8,Lm4; then
A12: f*g = (u1 + h1*'anpoly(1.R,1))*'g1 by POLYNOM3:def 10
.= u1 *' g1 + (h1*'anpoly(1.R,1))*'g1 by POLYNOM3:32;
A13: deg h1 = k +1 - 1 by A4,A11,NAT_1:11,XREAL_1:233;
reconsider h = h1, ang = anpoly(1.R,1)*'g1,
an = anpoly(1.R,1), t = anpoly(1.R,1)*'g1,
LMf = LM f1 as Element of Polynom-Ring R by POLYNOM3:def 10;
reconsider t1 = anpoly(1.R,1)*'g1 as Polynomial of R;
reconsider dan1 = (Der1(R)).an, df1 = (Der1(R)).f,
dg1 = (Der1(R)).g,
du1 = (Der1(R)).u, dh1 = (Der1(R)).h as Polynomial of R;
A14: u1 *' g1 = u * g & h1*'t1 = h*t by POLYNOM3:def 10;
f*g = u1 *' g1 + h1*'(anpoly(1.R,1)*'g1) by A12,POLYNOM3:33; then
A15: f*g = u *g + h * t by A14,POLYNOM3:def 10
.= u*g + h*(an * g) by POLYNOM3:def 10;
A16: deg u1 < deg f1 by A7,XREAL_1:9;
A17: (Der1(R)).(u*g) = ((Der1(R)).u)*g + u*((Der1(R)).g)
proof
per cases;
suppose u is non constant; then
reconsider n1 = deg u1 -1 as Nat;
n1 < k by A4,A16,XREAL_1:9;
hence thesis by A3;
end;
suppose u is constant;
hence thesis by Th34;
end;
end;
A21: (Der1(R)).(h * (an*g)) =
((Der1(R)).h)*(an*g) + h*((Der1(R)).(an*g))
proof
per cases;
suppose h is non constant; then
reconsider m1 = deg h1 -1 as Nat;
m1 < k by XREAL_1:44,A13;
hence thesis by A3;
end;
suppose h is constant;
hence thesis by Th34;
end;
end;
reconsider s1 = ((Der1(R)).an)*h, t1 = an*((Der1(R)).h)
as Polynomial of R by POLYNOM3:def 10;
A25: (Der1(R)).(h * an) = ((Der1(R)).h)*an + h*((Der1(R)).an) by Th32;
A26: ((Der1(R)).h)*an = dh1*'anpoly(1.R,1) by POLYNOM3:def 10;
A27: ((Der1(R)).h)*(an * g) = (((Der1(R)).h)*an) * g by GROUP_1:def 3
.= (dh1*'anpoly(1.R,1))*'g1 by A26,POLYNOM3:def 10;
A28: (Der1(R)).(f*g)
= (((Der1(R)).u)*g + u*((Der1(R)).g)) + (Der1(R)).(h * (an * g))
by A17,A15,VECTSP_1:def 20;
u*((Der1(R)).g)= u1*'dg1 & ((Der1(R)).u)*g =du1*'g1
by POLYNOM3:def 10;
then
A30: ((Der1(R)).u)*g + u*((Der1(R)).g) =
du1 *' g1 + u1*'dg1 by POLYNOM3:def 10;
((Der1(R)).an)*g = dan1*'g1 & an*((Der1(R)).g) = anpoly(1.R,1)*'dg1
by POLYNOM3:def 10; then
((Der1(R)).an)*g + an*((Der1(R)).g)
= dan1*'g1 + anpoly(1.R,1)*'dg1 by POLYNOM3:def 10;then
A32: h*(((Der1(R)).an)*g + an*((Der1(R)).g))
= h1*'(dan1*'g1 + anpoly(1.R,1)*'dg1) by POLYNOM3:def 10;
A33: (Der1(R)).(h * (an * g)) = (((Der1(R)).h)*(an * g))
+ (h*(((Der1(R)).an)*g + an*((Der1(R)).g))) by Th32,A21
.= ((dh1*'anpoly(1.R,1))*'g1)+
(h1*'(dan1*'g1 + anpoly(1.R,1)*'dg1))
by A32,A27,POLYNOM3:def 10;
h*((Der1(R)).an) = h1*'dan1 by POLYNOM3:def 10; then
A34: ((Der1(R)).h)*an + h*((Der1(R)).an)
= dh1*'anpoly(1.R,1) + h1*'dan1 by A26,POLYNOM3:def 10;
A35: LM f1 = h*an by A9,POLYNOM3:def 10;
f1 = u + LMf by A7,POLYNOM3:def 10; then
A36: (Der1(R)).f = (Der1(R)).u + (((Der1(R)).h)*an + h*((Der1(R)).an))
by A25,A35,VECTSP_1:def 20
.= du1 + (dh1*'anpoly(1.R,1) + h1*'dan1) by A34,POLYNOM3:def 10
.= du1 + dh1*'anpoly(1.R,1) + (h1*'dan1) by POLYNOM3:26;
A37: ((Der1(R)).f)*g = df1*'g1 & f*(Der1(R)).g = f1*'dg1
by POLYNOM3:def 10;
A38: f1 = u1 + (h1*'anpoly(1.R,1)) by A7,A8,Lm4;
(Der1(R)).(f*g) = (du1 *' g1 + u1*'dg1)
+(((dh1*'anpoly(1.R,1))*'g1)+
(h1*'(dan1*'g1 + anpoly(1.R,1)*'dg1)))
by A28,A30,A33,POLYNOM3:def 10
.= du1 *' g1 + u1*'dg1 + (dh1*'anpoly(1.R,1))*'g1
+ h1*'(dan1*'g1 + anpoly(1.R,1)*'dg1) by POLYNOM3:26
.= du1 *' g1 + (dh1*'anpoly(1.R,1))*'g1 + u1*'dg1
+ (h1*'(dan1*'g1 + anpoly(1.R,1)*'dg1)) by POLYNOM3:26
.= du1 *' g1 + (dh1*'anpoly(1.R,1))*'g1 + u1*'dg1
+ (h1*'(dan1*'g1) + h1*'(anpoly(1.R,1)*'dg1)) by POLYNOM3:31
.= du1 *' g1 + (dh1*'anpoly(1.R,1))*'g1 + u1*'dg1
+ (h1*'(dan1*'g1)) + h1*'(anpoly(1.R,1)*'dg1) by POLYNOM3:26
.= du1 *' g1 + (dh1*'anpoly(1.R,1))*'g1 + u1*'dg1
+ ((h1*'dan1)*'g1) + h1*'(anpoly(1.R,1)*'dg1) by POLYNOM3:33
.= du1 *' g1 + (dh1*'anpoly(1.R,1))*'g1 + (h1*'dan1)*'g1+ u1*'dg1
+ (h1*'(anpoly(1.R,1)*'dg1)) by POLYNOM3:26
.= du1 *' g1 + (dh1*'anpoly(1.R,1))*'g1 + (h1*'dan1)*'g1+ u1*'dg1
+ (h1*'anpoly(1.R,1))*'dg1 by POLYNOM3:33
.= (du1 + dh1*'anpoly(1.R,1))*'g1 + (h1*'dan1)*'g1+ u1*'dg1
+ (h1*'anpoly(1.R,1))*'dg1 by POLYNOM3:32
.= (du1 + dh1*'anpoly(1.R,1) + (h1*'dan1))*'g1+ u1*'dg1
+ (h1*'anpoly(1.R,1))*'dg1 by POLYNOM3:32
.= (du1 + dh1*'anpoly(1.R,1) + (h1*'dan1))*'g1
+ (u1*'dg1 + (h1*'anpoly(1.R,1))*'dg1) by POLYNOM3:26
.= df1*'g1 + f1*'dg1 by A38,A36,POLYNOM3:32
.= ((Der1(R)).f)*g + f*(Der1(R)).g by A37,POLYNOM3:def 10;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
A39: for n be Nat holds P[n] from NAT_1:sch 4(A2);
ex n be Nat st deg x -1 = n by A1;
hence thesis by A39;
end;
theorem Th36:
(Der1(R)).(f*g) = ((Der1(R)).f)*g + f*((Der1(R)).g)
proof
per cases;
suppose f is non constant;
hence thesis by Th35;
end;
suppose f is constant;
hence thesis by Th34;
end;
end;
registration let R;
cluster Der1(R) -> derivation;
coherence by VECTSP_1:def 20,Th36;
end;
theorem Th37:
for x be Element of Polynom-Ring R, f be Polynomial of R
st x = f holds for n be Nat holds x|^n = f`^n
proof
let x be Element of Polynom-Ring R, f be Polynomial of R;
assume
A1: x = f;
defpred P[Nat] means x|^$1 = f`^$1;
A2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A3: P[n];
x|^(n+1) = (x|^n) * (x|^1) by BINOM:10 .= (x|^n) * x by BINOM:8
.= (f`^n) *' f by A1,A3,POLYNOM3:def 10
.= f`^(n+1) by POLYNOM5:19;
hence thesis;
end;
x|^0 = 1_(Polynom-Ring R) by BINOM:8 .= 1_.(R) by POLYNOM3:37
.= f`^0 by POLYNOM5:15; then
A4: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem
for x be Element of Polynom-Ring R
st x = anpoly(1.R,1) holds ex y be Element of Polynom-Ring R
st y = anpoly(1.R,n) & (Der1(R)).(x|^(n+1)) = (n+1)*y
proof
let x be Element of Polynom-Ring R;
assume
A1: x = anpoly(1.R,1);
reconsider x1 = anpoly(1.R,1) as Polynomial of R;
A2: <%0.R,1.R%> = (<%0.R,1.R%>)`^1 by POLYNOM5:16 .= x1 by FIELD_1:12;
reconsider D = (Der1(R)) as Derivation of Polynom-Ring R;
D.x = anpoly(1.R,0) by A1,Th30 .= 1_.R; then
(x|^n) = x1`^n & D.x = 1_.R by A1,Th37; then
A3: (x|^n)*D.x = (x1`^n)*'1_.R by POLYNOM3:def 10
.= anpoly(1.R,n) by A2,FIELD_1:12;
reconsider y = anpoly(1.R,n)
as Element of Polynom-Ring R by POLYNOM3:def 10;
D.(x|^(n+1)) = (n+1)*y by A3,Th7;
hence thesis;
end;
reserve p for Polynomial of F_Real;
definition
let p;
func poly_diff(p) -> sequence of F_Real means :Def9:
for n being Nat holds it.n = p.(n+1) * (n+1);
existence
proof
defpred P[Element of NAT,object] means $2 = p.($1+1) * ($1+1);
A1: for x being Element of NAT ex y being Element of F_Real st P[x,y];
consider f being Function of NAT,F_Real such that
A2: for x being Element of NAT holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f;
let n;
n in NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
uniqueness
proof
let f,g be sequence of F_Real such that
A3: for n being Nat holds f.n = p.(n+1) * (n+1) and
A4: for n being Nat holds g.n = p.(n+1) * (n+1);
let n be Element of NAT;
thus f.n = p.(n+1) * (n+1) by A3
.= g.n by A4;
end;
end;
theorem
for p0 be Element of Polynom-Ring F_Real, p be Polynomial of F_Real
st p0 = p holds poly_diff(p) = (Der1(F_Real)).p0
proof
let p0 be Element of Polynom-Ring F_Real, p be Polynomial of F_Real;
assume
A1: p0 = p;
for n holds (poly_diff(p)).n = ((Der1(F_Real)).p0).n
proof
let n;
(poly_diff(p)).n = p.(n+1) * (n+1) by Def9
.= (n+1)*p.(n+1) by BINOM:18
.= ((Der1(F_Real)).p0).n by A1,Def8;
hence thesis;
end;
hence thesis;
end;