RINGDER1: Derivation of Commutative Rings \& {L}eibnitz Formula for Power of Derivation

:: 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

:: <section0>Preliminaries</section0>

theorem Th1: :: RINGDER1:1

for L being non empty right_complementable associative Abelian add-associative right_zeroed distributive left_zeroed doubleLoopStr
for a, b being Element of L
for n being Nat holds (n * a) + (n * b) = n * (a + b)

proof end;

theorem :: RINGDER1:2

proof end;

theorem Th3: :: RINGDER1:3

for L being non empty right_complementable associative Abelian add-associative right_zeroed distributive left_zeroed doubleLoopStr
for n being Nat holds n * (0. L) = 0. L

proof end;

theorem :: RINGDER1:4

for L being non empty right_complementable associative Abelian add-associative right_zeroed distributive left_zeroed doubleLoopStr
for n being Nat holds (0. L) * n = 0. L

proof end;

definition

let R be non degenerated comRing;
let IT be Function of R,R;

attr IT is derivation means :Def1: :: RINGDER1:def 1
for x, y being Element of R holds
( IT . (x + y) = (IT . x) + (IT . y) & IT . (x * y) = (x * (IT . y)) + (y * (IT . x)) );

end;

:: deftheorem Def1 defines derivation RINGDER1:def 1 :

registration

let R be non degenerated comRing;

cluster Function-like quasi_total derivation -> additive for Element of K10(K11( the carrier of R, the carrier of R));

coherence ;

end;

registration

let R be non degenerated comRing;

cluster non empty Relation-like the carrier of R -defined the carrier of R -valued Function-like total quasi_total derivation for Element of K10(K11( the carrier of R, the carrier of R));

existence

proof end;

end;

definition

let R be non degenerated comRing;
mode Derivation of R is derivation Function of R,R;

end;

definition

let R be non degenerated comRing;

func Der R -> Subset of (Funcs (([#] R),([#] R))) equals :: RINGDER1:def 2
{ f where f is Function of R,R : f is derivation } ;

coherence

proof end;

end;

:: deftheorem defines Der RINGDER1:def 2 :

registration

let R be non degenerated comRing;

cluster Der R -> non empty ;

correctness

proof end;

end;

theorem Th5: :: RINGDER1:5

for R being non degenerated comRing
for D being Derivation of R holds
( D . (1. R) = 0. R & D . (0. R) = 0. R )

proof end;

theorem Th6: :: RINGDER1:6

for R being non degenerated comRing
for D being Derivation of R
for n being Nat
for x being Element of R holds D . (n * x) = n * (D . x)

proof end;

theorem Th7: :: RINGDER1:7

for R being non degenerated comRing
for m being Nat
for x being Element of R
for D being Derivation of R holds D . (x |^ (m + 1)) = (m + 1) * ((x |^ m) * (D . x))

proof 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: :: RINGDER1:8

for R being non degenerated comRing
for n being Nat
for D being Derivation of R holds
( 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 b₁ -valued Function )

proof end;

theorem Th9: :: RINGDER1:9

for R being non degenerated comRing
for D being Derivation of R
for n being Nat
for x being Element of R holds (D |^ (n + 1)) . x = D . ((D |^ n) . x)

proof end;

::::::::::::::::::::::::::::::::::::::::
::: D.(a/b) = (b*D.a - a*F.b)/b^2
::::::::::::::::::::::::::::::::::::::::

theorem :: RINGDER1:10

for R being non degenerated comRing
for D being Derivation of R
for x, y, z being Element of R st z * y = 1. R holds
(y |^ 2) * (D . (x * z)) = (y * (D . x)) - (x * (D . y))

proof end;

definition

let R be non degenerated comRing;
let s be FinSequence of the carrier of R;
let h be Function of R,R;
:: original: *
redefine func h * s -> FinSequence of the carrier of R;
coherence by FINSEQ_2:32;

end;

theorem Th11: :: RINGDER1:11

for R being non degenerated comRing
for h being Function of R,R
for s being FinSequence of the carrier of R st h is additive holds
h . (Sum s) = Sum (h * s)

proof end;

::::::::::::::::::::::::::::::::::::::::::::::::
::: Formula
::: (f1 + f2 +...+fn)' = f1' + f2' +...+ fn'
::::::::::::::::::::::::::::::::::::::::::::::::

theorem :: RINGDER1:12

for R being non degenerated comRing
for D being Derivation of R
for s being FinSequence of the carrier of R 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 be non degenerated comRing;
let D be Derivation of R;
let s be FinSequence of the carrier of R;

func DProd (D,s) -> FinSequence of the carrier of R means :Def3: :: RINGDER1:def 3
( len it = len s & ( for i being Nat st i in dom it holds
it . i = Product (Replace (s,i,(D . (s /. i)))) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines DProd RINGDER1:def 3 :

theorem Th13: :: RINGDER1:13

for R being non degenerated comRing
for D being Derivation of R
for s being FinSequence of the carrier of R st len s = 1 holds
Sum (DProd (D,s)) = D . (Product s)

proof end;

theorem :: RINGDER1:14

for R being non degenerated comRing
for D being Derivation of R
for t being FinSequence of the carrier of R st len t >= 1 holds
Sum (DProd (D,t)) = D . (Product t)

proof end;

:: <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 be non degenerated comRing;
let D be Derivation of R;
let n be Nat;
let x, y be Element of R;

func LBZ (D,n,x,y) -> FinSequence of the carrier of R means :Def4: :: RINGDER1:def 4
( len it = n + 1 & ( for i being Nat st i in dom it holds
it . i = ((n choose (i -' 1)) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ (i -' 1)) . y) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines LBZ RINGDER1:def 4 :

theorem Th15: :: RINGDER1:15

for R being non degenerated comRing
for x, y being Element of R
for D being Derivation of R holds LBZ (D,0,x,y) = <*(x * y)*>

proof end;

theorem Th16: :: RINGDER1:16

for R being non degenerated comRing
for x, y being Element of R
for D being Derivation of R holds LBZ (D,1,x,y) = <*(y * (D . x)),(x * (D . y))*>

proof end;

definition

let R be non degenerated comRing;
let D be Derivation of R;
let m be Nat;
let x, y be Element of R;

func LBZ0 (D,m,x,y) -> FinSequence of the carrier of R means :Def5: :: RINGDER1:def 5
( len it = m & ( for i being Nat 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 end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines LBZ0 RINGDER1:def 5 :

definition

let R be non degenerated comRing;
let D be Derivation of R;
let m be Nat;
let x, y be Element of R;

func LBZ1 (D,m,x,y) -> FinSequence of the carrier of R means :Def6: :: RINGDER1:def 6
( len it = m & ( for i being Nat st i in dom it holds
it . i = ((m choose (i -' 1)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines LBZ1 RINGDER1:def 6 :

definition

let R be non degenerated comRing;
let D be Derivation of R;
let m be Nat;
let x, y be Element of R;

func LBZ2 (D,m,x,y) -> FinSequence of the carrier of R means :Def7: :: RINGDER1:def 7
( len it = m & ( for i being Nat st i in dom it holds
it . i = ((m choose i) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines LBZ2 RINGDER1:def 7 :

theorem :: RINGDER1:17

for R being non degenerated comRing
for n being Nat
for x, y being Element of R
for D being Derivation of R holds D . (Sum (LBZ0 (D,n,x,y))) = Sum (D * (LBZ0 (D,n,x,y))) by Th11;

theorem Th18: :: RINGDER1:18

for R being non degenerated comRing
for m being Nat
for x, y being Element of R
for D being Derivation of R holds LBZ0 (D,m,x,y) = (LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))

proof end;

theorem Th19: :: RINGDER1:19

for R being non degenerated comRing
for n being Nat
for x, y being Element of R
for D being Derivation of R holds Sum (LBZ0 (D,n,x,y)) = (Sum (LBZ1 (D,n,x,y))) + (Sum (LBZ2 (D,n,x,y)))

proof end;

theorem Th20: :: RINGDER1:20

for R being non degenerated comRing
for n being Nat
for x, y being Element of R
for D being Derivation of R holds D * (LBZ0 (D,n,x,y)) = (Del ((LBZ2 (D,(n + 1),x,y)),(n + 1))) + (Del ((LBZ1 (D,(n + 1),x,y)),1))

proof end;

Lm1: for R being non degenerated comRing
for x, y being Element of R
for D being Derivation of R
for n being Nat st 1 <= n holds
(LBZ1 (D,n,x,y)) /. 1 = ((D |^ n) . x) * (D . y)

proof end;

Lm2: for R being non degenerated comRing
for x, y being Element of R
for D being Derivation of R
for n being Nat st 1 <= n holds
(LBZ2 (D,n,x,y)) /. n = (D . x) * ((D |^ n) . y)

proof end;

theorem Th21: :: RINGDER1:21

for R being non degenerated comRing
for n being Nat
for x, y being Element of R
for D being Derivation of R holds 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 end;

theorem Th22: :: RINGDER1:22

for R being non degenerated comRing
for n being Nat
for x, y being Element of R
for D being Derivation of R holds LBZ (D,(n + 1),x,y) = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>

proof end;

theorem Th23: :: RINGDER1:23

for R being non degenerated comRing
for n being Nat
for x, y being Element of R
for D being Derivation of R holds 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 end;

theorem Th24: :: RINGDER1:24

for R being non degenerated comRing
for n being Nat
for x, y being Element of R
for D being Derivation of R holds D . (Sum (LBZ (D,(n + 1),x,y))) = Sum (LBZ (D,(n + 2),x,y))

proof end;

:::::::::::::::::::::::::::::::::::::::::::::::::
:: Leibniz Formula for Power of Derivation.
:::::::::::::::::::::::::::::::::::::::::::::::::

theorem :: RINGDER1:25

for R being non degenerated comRing
for n being Nat
for x, y being Element of R
for D being Derivation of R holds (D |^ n) . (x * y) = Sum (LBZ (D,n,x,y))

proof end;

::<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 be non degenerated comRing;
let f be Function of (Polynom-Ring R),(Polynom-Ring R);
let p be Element of the carrier of (Polynom-Ring R);
:: original: .
redefine func f . p -> Element of the carrier of (Polynom-Ring R);
coherence

proof end;

end;

definition

let R be Ring;

func Der1 R -> Function of (Polynom-Ring R),(Polynom-Ring R) means :Def8: :: 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));

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines Der1 RINGDER1:def 8 :

registration

let R be non degenerated comRing;

cluster Der1 R -> additive ;

coherence

proof end;

end;

theorem :: RINGDER1:26

for R being domRing
for f being Element of the carrier of (Polynom-Ring R)
for f1 being Polynomial of R st f = f1 & f1 is constant holds
(Der1 R) . f = 0_. R

proof end;

Lm3: for R being domRing
for a being Element of R holds a | R = <%a%>

proof end;

theorem Th27: :: RINGDER1:27

for R being domRing
for a being Element of R
for i being Nat
for p being Element of the carrier of (Polynom-Ring R) holds ((a | R) *' p) . i = a * (p . i)

proof end;

theorem Th28: :: RINGDER1:28

for R being domRing
for f, g being Element of the carrier of (Polynom-Ring R)
for a being Element of R st f = a | R holds
(Der1 R) . (f * g) = (a | R) *' ((Der1 R) . g)

proof end;

theorem Th29: :: RINGDER1:29

for R being domRing
for f being Element of the carrier of (Polynom-Ring R)
for a being Element of R st f = anpoly (a,0) holds
(Der1 R) . f = 0_. R

proof end;

theorem Th30: :: RINGDER1:30

for R being domRing
for f being Element of the carrier of (Polynom-Ring R)
for a being Element of R st f = anpoly (a,1) holds
(Der1 R) . f = anpoly (a,0)

proof end;

theorem Th31: :: RINGDER1:31

for R being domRing
for p, q being Polynomial of R st p = anpoly ((1. R),1) holds
for i being Element of NAT holds
( (p *' q) . (i + 1) = q . i & (p *' q) . 0 = 0. R )

proof end;

theorem Th32: :: RINGDER1:32

for R being domRing
for f, g being 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 end;

Lm4: for R being domRing
for p being non constant Polynomial of R holds LM p = ((p . (deg p)) * (anpoly ((1. R),((deg p) -' 1)))) *' (anpoly ((1. R),1))

proof end;

theorem :: RINGDER1:33

for R being domRing
for f, g being constant Element of the carrier of (Polynom-Ring R) holds (Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g))

proof end;

theorem Th34: :: RINGDER1:34

for R being domRing
for f, g being 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 end;

theorem Th35: :: RINGDER1:35

for R being domRing
for x, y being Element of the carrier of (Polynom-Ring R) st not x is constant holds
(Der1 R) . (x * y) = (((Der1 R) . x) * y) + (x * ((Der1 R) . y))

proof end;

theorem Th36: :: RINGDER1:36

for R being domRing
for f, g being Element of the carrier of (Polynom-Ring R) holds (Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g))

proof end;

registration

let R be domRing;

cluster Der1 R -> derivation ;

coherence by VECTSP_1:def 20, Th36;

end;

theorem Th37: :: RINGDER1:37

for R being domRing
for x being Element of (Polynom-Ring R)
for f being Polynomial of R st x = f holds
for n being Nat holds x |^ n = f `^ n

proof end;

theorem :: RINGDER1:38

for n being Nat
for R being domRing
for x being Element of (Polynom-Ring R) st x = anpoly ((1. R),1) holds
ex y being Element of (Polynom-Ring R) st
( y = anpoly ((1. R),n) & (Der1 R) . (x |^ (n + 1)) = (n + 1) * y )

proof end;

definition

let p be Polynomial of F_Real;

func poly_diff p -> sequence of F_Real means :Def9: :: RINGDER1:def 9
for n being Nat holds it . n = (p . (n + 1)) * (n + 1);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines poly_diff RINGDER1:def 9 :

theorem :: RINGDER1:39

for p0 being Element of (Polynom-Ring F_Real)
for p being Polynomial of F_Real st p0 = p holds
poly_diff p = (Der1 F_Real) . p0

proof end;