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

for a, b being Element of L

for n being Nat holds (n * a) + (n * b) = n * (a + b)

proof end;

theorem :: RINGDER1:2

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) * b = a * (n * b)

for a, b being Element of L

for n being Nat holds (n * a) * b = a * (n * b)

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

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

for n being Nat holds (0. L) * n = 0. L

proof end;

:: deftheorem Def1 defines derivation RINGDER1:def 1 :

for R being non degenerated comRing

for IT being Function of R,R holds

( IT is derivation iff for x, y being Element of R holds

( IT . (x + y) = (IT . x) + (IT . y) & IT . (x * y) = (x * (IT . y)) + (y * (IT . x)) ) );

for R being non degenerated comRing

for IT being Function of R,R holds

( IT is derivation iff for x, y being Element of R holds

( IT . (x + y) = (IT . x) + (IT . y) & IT . (x * y) = (x * (IT . y)) + (y * (IT . x)) ) );

registration

let R be non degenerated comRing;

for b_{1} being Function of R,R st b_{1} is derivation holds

b_{1} is additive
;

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

coherence for b

b

registration

let R be non degenerated comRing;

ex b_{1} being Function of R,R st b_{1} is derivation

end;
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 ex b

proof end;

definition
end;

definition

let R be non degenerated comRing;

{ f where f is Function of R,R : f is derivation } is Subset of (Funcs (([#] R),([#] R)))

end;
func Der R -> Subset of (Funcs (([#] R),([#] R))) equals :: RINGDER1:def 2

{ f where f is Function of R,R : f is derivation } ;

coherence { f where f is Function of R,R : f is derivation } ;

{ f where f is Function of R,R : f is derivation } is Subset of (Funcs (([#] R),([#] R)))

proof end;

:: deftheorem defines Der RINGDER1:def 2 :

for R being non degenerated comRing holds Der R = { f where f is Function of R,R : f is derivation } ;

for R being non degenerated comRing holds Der R = { f where f is Function of R,R : f is derivation } ;

registration
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 )

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)

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

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;

:::::::::::::::::::::::::::::::::::::::::::::::::::::

:: 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_{1} -valued Function )

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

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)

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

::::::::::::::::::::::::::::::::::::::::

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

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

s * h is FinSequence of the carrier of R by FINSEQ_2:32;

end;
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

s * h is FinSequence of the carrier of R by FINSEQ_2:32;

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)

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'

::::::::::::::::::::::::::::::::::::::::::::::::

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

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

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

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

ex b_{1} being FinSequence of the carrier of R st

( len b_{1} = len s & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = Product (Replace (s,i,(D . (s /. i)))) ) )

for b_{1}, b_{2} being FinSequence of the carrier of R st len b_{1} = len s & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = Product (Replace (s,i,(D . (s /. i)))) ) & len b_{2} = len s & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = Product (Replace (s,i,(D . (s /. i)))) ) holds

b_{1} = b_{2}

end;
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 ( len it = len s & ( for i being Nat st i in dom it holds

it . i = Product (Replace (s,i,(D . (s /. i)))) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines DProd RINGDER1:def 3 :

for R being non degenerated comRing

for D being Derivation of R

for s, b_{4} being FinSequence of the carrier of R holds

( b_{4} = DProd (D,s) iff ( len b_{4} = len s & ( for i being Nat st i in dom b_{4} holds

b_{4} . i = Product (Replace (s,i,(D . (s /. i)))) ) ) );

for R being non degenerated comRing

for D being Derivation of R

for s, b

( b

b

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)

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)

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)

:::::::::::::::::::::::::::::::::::::::::::::::::::::::

:::::::::::::::::::::::::::::::::::::::::::::::::::::::

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

ex b_{1} being FinSequence of the carrier of R st

( len b_{1} = n + 1 & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = ((n choose (i -' 1)) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ (i -' 1)) . y) ) )

for b_{1}, b_{2} being FinSequence of the carrier of R st len b_{1} = n + 1 & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = ((n choose (i -' 1)) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ (i -' 1)) . y) ) & len b_{2} = n + 1 & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = ((n choose (i -' 1)) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ (i -' 1)) . y) ) holds

b_{1} = b_{2}

end;
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 ( 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) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines LBZ RINGDER1:def 4 :

for R being non degenerated comRing

for D being Derivation of R

for n being Nat

for x, y being Element of R

for b_{6} being FinSequence of the carrier of R holds

( b_{6} = LBZ (D,n,x,y) iff ( len b_{6} = n + 1 & ( for i being Nat st i in dom b_{6} holds

b_{6} . i = ((n choose (i -' 1)) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ (i -' 1)) . y) ) ) );

for R being non degenerated comRing

for D being Derivation of R

for n being Nat

for x, y being Element of R

for b

( b

b

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)*>

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))*>

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;

ex b_{1} being FinSequence of the carrier of R st

( len b_{1} = m & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (((m choose (i -' 1)) + (m choose i)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) )

for b_{1}, b_{2} being FinSequence of the carrier of R st len b_{1} = m & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (((m choose (i -' 1)) + (m choose i)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) & len b_{2} = m & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = (((m choose (i -' 1)) + (m choose i)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) holds

b_{1} = b_{2}

end;
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 ( 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) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines LBZ0 RINGDER1:def 5 :

for R being non degenerated comRing

for D being Derivation of R

for m being Nat

for x, y being Element of R

for b_{6} being FinSequence of the carrier of R holds

( b_{6} = LBZ0 (D,m,x,y) iff ( len b_{6} = m & ( for i being Nat st i in dom b_{6} holds

b_{6} . i = (((m choose (i -' 1)) + (m choose i)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) ) );

for R being non degenerated comRing

for D being Derivation of R

for m being Nat

for x, y being Element of R

for b

( b

b

definition

let R be non degenerated comRing;

let D be Derivation of R;

let m be Nat;

let x, y be Element of R;

ex b_{1} being FinSequence of the carrier of R st

( len b_{1} = m & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = ((m choose (i -' 1)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) )

for b_{1}, b_{2} being FinSequence of the carrier of R st len b_{1} = m & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = ((m choose (i -' 1)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) & len b_{2} = m & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = ((m choose (i -' 1)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) holds

b_{1} = b_{2}

end;
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 ( 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) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines LBZ1 RINGDER1:def 6 :

for R being non degenerated comRing

for D being Derivation of R

for m being Nat

for x, y being Element of R

for b_{6} being FinSequence of the carrier of R holds

( b_{6} = LBZ1 (D,m,x,y) iff ( len b_{6} = m & ( for i being Nat st i in dom b_{6} holds

b_{6} . i = ((m choose (i -' 1)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) ) );

for R being non degenerated comRing

for D being Derivation of R

for m being Nat

for x, y being Element of R

for b

( b

b

definition

let R be non degenerated comRing;

let D be Derivation of R;

let m be Nat;

let x, y be Element of R;

ex b_{1} being FinSequence of the carrier of R st

( len b_{1} = m & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = ((m choose i) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) )

for b_{1}, b_{2} being FinSequence of the carrier of R st len b_{1} = m & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = ((m choose i) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) & len b_{2} = m & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = ((m choose i) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) holds

b_{1} = b_{2}

end;
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 ( 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) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def7 defines LBZ2 RINGDER1:def 7 :

for R being non degenerated comRing

for D being Derivation of R

for m being Nat

for x, y being Element of R

for b_{6} being FinSequence of the carrier of R holds

( b_{6} = LBZ2 (D,m,x,y) iff ( len b_{6} = m & ( for i being Nat st i in dom b_{6} holds

b_{6} . i = ((m choose i) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) ) );

for R being non degenerated comRing

for D being Derivation of R

for m being Nat

for x, y being Element of R

for b

( b

b

theorem :: RINGDER1:17

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

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

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

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

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))*>

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

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

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.

:::::::::::::::::::::::::::::::::::::::::::::::::

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

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

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

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

f . p is Element of the carrier of (Polynom-Ring R)

end;
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

f . p is Element of the carrier of (Polynom-Ring R)

proof end;

definition

let R be Ring;

ex b_{1} being Function of (Polynom-Ring R),(Polynom-Ring R) st

for f being Element of the carrier of (Polynom-Ring R)

for i being Nat holds (b_{1} . f) . i = (i + 1) * (f . (i + 1))

for b_{1}, b_{2} being Function of (Polynom-Ring R),(Polynom-Ring R) st ( for f being Element of the carrier of (Polynom-Ring R)

for i being Nat holds (b_{1} . f) . i = (i + 1) * (f . (i + 1)) ) & ( for f being Element of the carrier of (Polynom-Ring R)

for i being Nat holds (b_{2} . f) . i = (i + 1) * (f . (i + 1)) ) holds

b_{1} = b_{2}

end;
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 for f being Element of the carrier of (Polynom-Ring R)

for i being Nat holds (it . f) . i = (i + 1) * (f . (i + 1));

ex b

for f being Element of the carrier of (Polynom-Ring R)

for i being Nat holds (b

proof end;

uniqueness for b

for i being Nat holds (b

for i being Nat holds (b

b

proof end;

:: deftheorem Def8 defines Der1 RINGDER1:def 8 :

for R being Ring

for b_{2} being Function of (Polynom-Ring R),(Polynom-Ring R) holds

( b_{2} = Der1 R iff for f being Element of the carrier of (Polynom-Ring R)

for i being Nat holds (b_{2} . f) . i = (i + 1) * (f . (i + 1)) );

for R being Ring

for b

( b

for i being Nat holds (b

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

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)

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)

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

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)

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 )

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

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

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

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

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

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;

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

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 )

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;

ex b_{1} being sequence of F_Real st

for n being Nat holds b_{1} . n = (p . (n + 1)) * (n + 1)

for b_{1}, b_{2} being sequence of F_Real st ( for n being Nat holds b_{1} . n = (p . (n + 1)) * (n + 1) ) & ( for n being Nat holds b_{2} . n = (p . (n + 1)) * (n + 1) ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds it . n = (p . (n + 1)) * (n + 1);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def9 defines poly_diff RINGDER1:def 9 :

for p being Polynomial of F_Real

for b_{2} being sequence of F_Real holds

( b_{2} = poly_diff p iff for n being Nat holds b_{2} . n = (p . (n + 1)) * (n + 1) );

for p being Polynomial of F_Real

for b

( b

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

for p being Polynomial of F_Real st p0 = p holds

poly_diff p = (Der1 F_Real) . p0

proof end;