:: Derivation of Commutative Rings \& {L}eibnitz Formula for Power of :: Derivation :: by Yasushige Watase :: :: Received March 30, 2021 :: Copyright (c) 2021 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, 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; 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; 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; :: Preliminaries theorem :: RINGDER1:1 n*a + n*b = n*(a+b); theorem :: RINGDER1:2 (n*a)*b = a*(n*b); theorem :: RINGDER1:3 n*0.L = 0.L; theorem :: RINGDER1:4 0.L*n = 0.L; begin :: Definition of Derivation of Rings and Its Properties :: Definition of Derivation of Rings and Its Properties ::::::::::::::::::::::::::::::::::::: ::: 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 :: RINGDER1:def 1 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; end; registration let R; cluster derivation for Function of R,R; 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 :: RINGDER1:def 2 {f where f is Function of R,R : f is derivation }; end; registration let R; cluster Der(R) -> non empty; end; reserve D for Derivation of R; theorem :: RINGDER1:5 D.(1.R) = 0.R & D.(0.R) = 0.R; theorem :: RINGDER1:6 for n,x holds D.(n*x) = n*D.x; theorem :: RINGDER1:7 D.(x|^(m+1)) = (m+1)*((x|^m)*D.x); :::::::::::::::::::::::::::::::::::::::::::::::::::: :: 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 :: RINGDER1:8 (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; theorem :: RINGDER1:9 for n,x holds (D|^(n+1)).x = D.((D|^n).x); :::::::::::::::::::::::::::::::::::::::: ::: D.(a/b) = (b*D.a - a*F.b)/b^2 :::::::::::::::::::::::::::::::::::::::: theorem :: RINGDER1:10 for x,y,z st z*y=1.R holds y|^2*D.(x*z) = (y*D.x -x*D.y); 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; end; theorem :: RINGDER1:11 for h,s st h is additive holds h.(Sum s) = Sum(h*s); :::::::::::::::::::::::::::::::::::::::::::::::: ::: Formula ::: (f1 + f2 +...+fn)' = f1' + f2' +...+ fn' :::::::::::::::::::::::::::::::::::::::::::::::: theorem :: RINGDER1:12 for D,s holds D.(Sum s) = Sum(D*s); ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: 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 :: RINGDER1:def 3 len it = len s & for i st i in dom it holds it.i = Product (Replace(s,i,D.(s/.i))); end; theorem :: RINGDER1:13 for s holds len s = 1 implies Sum DProd(D,s)= D.(Product s); theorem :: RINGDER1:14 for t be FinSequence of the carrier of R st len t >= 1 holds Sum DProd(D,t) = D.(Product t); begin :: Proof of Leibnitz Formula for Power of Derivations ::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: 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 :: RINGDER1:def 4 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); end; theorem :: RINGDER1:15 LBZ(D,0,x,y) = <* x*y *>; theorem :: RINGDER1:16 LBZ(D,1,x,y) = <* y*D.x, x*D.y *>; 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 :: RINGDER1:def 5 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); 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 :: RINGDER1:def 6 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); 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 :: RINGDER1:def 7 len it = m & for i st i in dom it holds it.i = (m choose i)*((D|^(m +1 -'i)).x)*((D|^i).y); end; theorem :: RINGDER1:17 D.(Sum(LBZ0(D,n,x,y))) = Sum(D*(LBZ0(D,n,x,y))); theorem :: RINGDER1:18 LBZ0(D,m,x,y) = LBZ1(D,m,x,y) + LBZ2(D,m,x,y); theorem :: RINGDER1:19 Sum LBZ0(D,n,x,y) = Sum LBZ1(D,n,x,y) + Sum LBZ2(D,n,x,y); theorem :: RINGDER1:20 D*LBZ0(D,n,x,y) = Del(LBZ2(D,n+1,x,y),n+1) + Del(LBZ1(D,n+1,x,y),1); theorem :: RINGDER1:21 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)); theorem :: RINGDER1:22 LBZ(D,n+1,x,y) = <*((D|^(n+1)).x)*y *>^(LBZ0(D,n,x,y))^<* x*((D|^(n+1)).y)*> ; theorem :: RINGDER1:23 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); theorem :: RINGDER1:24 D.(Sum(LBZ(D,n+1,x,y))) = Sum(LBZ(D,n+2,x,y)); ::::::::::::::::::::::::::::::::::::::::::::::::: :: Leibniz Formula for Power of Derivation. ::::::::::::::::::::::::::::::::::::::::::::::::: theorem :: RINGDER1:25 (D|^n).(x*y) = Sum(LBZ(D,n,x,y)); begin ::Example of Derivation of Polynomial Ring over a Commutative Ring :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: :::: 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; end; definition let R be Ring; func Der1(R) -> Function of Polynom-Ring R, Polynom-Ring R means :: RINGDER1:def 8 for f being Element of the carrier of Polynom-Ring R for i being Nat holds (it.f).i = (i+1)*f.(i+1); end; registration let R; cluster Der1(R) -> additive; 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 :: RINGDER1:26 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; reserve a for Element of R; theorem :: RINGDER1:27 for i be Nat, p be Element of the carrier of Polynom-Ring R holds ((a|R)*'p).i = a*p.i; theorem :: RINGDER1:28 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); theorem :: RINGDER1:29 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; theorem :: RINGDER1:30 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); theorem :: RINGDER1:31 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; theorem :: RINGDER1:32 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); theorem :: RINGDER1:33 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); theorem :: RINGDER1:34 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); theorem :: RINGDER1:35 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); theorem :: RINGDER1:36 (Der1(R)).(f*g) = ((Der1(R)).f)*g + f*((Der1(R)).g); registration let R; cluster Der1(R) -> derivation; end; theorem :: RINGDER1:37 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; theorem :: RINGDER1:38 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; reserve p for Polynomial of F_Real; definition let p; func poly_diff(p) -> sequence of F_Real means :: RINGDER1:def 9 for n being Nat holds it.n = p.(n+1) * (n+1); end; theorem :: RINGDER1:39 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;