:: Schur's Theorem on the Stability of Networks
:: by Agnieszka Rowi\'nska-Schwarzweller and Christoph Schwarzweller
::
:: Received October 19, 2006
:: Copyright (c) 2006-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 NUMBERS, RLVECT_1, ALGSTR_0, XBOOLE_0, FINSEQ_1, NAT_1, RELAT_1,
ARYTM_3, TARSKI, ORDINAL4, PARTFUN1, XXREAL_0, FUNCT_1, SUBSET_1,
STRUCT_0, BINOP_1, VECTSP_1, LATTICES, SUPINF_2, ARYTM_1, GROUP_1,
CARD_1, MESFUNC1, COMPLFLD, COMPLEX1, CARD_3, POLYNOM1, POLYNOM3,
SGRAPH1, INT_1, ALGSEQ_1, VECTSP_2, POLYNOM5, AFINSQ_1, POLYNOM2,
FUNCT_4, FUNCOP_1, XCMPLX_0, SQUARE_1, HURWITZ;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XCMPLX_0,
ALGSTR_0, VECTSP_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NAT_D,
XXREAL_0, FINSEQ_1, INT_1, NAT_1, FUNCOP_1, STRUCT_0, RLVECT_1, VFUNCT_1,
GROUP_1, POLYNOM1, COMPLEX1, COMPLFLD, BINOP_1, NORMSP_1, ALGSEQ_1,
FUNCT_4, POLYNOM3, POLYNOM4, POLYNOM5, VECTSP_1, SQUARE_1;
constructors BINOP_1, REAL_1, SQUARE_1, FINSOP_1, BINARITH, VECTSP_2,
ALGSTR_1, POLYNOM4, POLYNOM5, NAT_D, RELSET_1, FVSUM_1, VFUNCT_1,
ALGSEQ_1, BINOP_2, COMPLFLD;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XCMPLX_0, XXREAL_0, XREAL_0,
SQUARE_1, NAT_1, INT_1, FINSEQ_1, STRUCT_0, VECTSP_1, COMPLFLD, ALGSTR_1,
POLYNOM3, POLYNOM4, POLYNOM5, FUNCOP_1, CARD_1, VFUNCT_1, FUNCT_2,
MEMBERED;
requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
equalities FINSEQ_1, POLYNOM3, COMPLEX1, SQUARE_1, FUNCOP_1;
theorems GROUP_1, VECTSP_1, ALGSEQ_1, NAT_1, FUNCT_1, FUNCT_2, XREAL_1,
SQUARE_1, VECTSP_2, INT_1, FINSEQ_1, RLVECT_1, POLYNOM4, TARSKI, FUNCT_4,
POLYNOM3, XBOOLE_1, POLYNOM2, FUNCOP_1, XCMPLX_1, XCMPLX_0, COMPLFLD,
POLYNOM5, XXREAL_0, ALGSTR_1, COMPLEX1, FINSEQ_2, POLYNOM1, FINSEQ_3,
BHSP_1, NORMSP_1, ORDINAL1, PARTFUN1, XREAL_0, NAT_D;
schemes NAT_1, FUNCT_2, FINSEQ_1;
begin :: Preliminaries
Lm1: for L being add-associative right_zeroed right_complementable non empty
addLoopStr for F being FinSequence of L for G being FinSequence for k being
Nat st G = F|(Seg k) & len F = k + 1 holds G is FinSequence of L & dom G c= dom
F & len G = k & F = G ^ <*F/.(k+1)*>
proof
let L be add-associative right_zeroed right_complementable non empty
addLoopStr;
let F be FinSequence of L;
let G1 be FinSequence;
let k be Nat;
assume that
A1: G1 = F|(Seg k) and
A2: len F = k + 1;
reconsider G = G1 as FinSequence;
A3: k <= len F by A2,NAT_1:13;
then
A4: len G = k by A1,FINSEQ_1:17;
now
let u be object;
assume u in rng G;
then consider x being object such that
A5: x in dom G and
A6: G.x = u by FUNCT_1:def 3;
reconsider x9 = x as Element of NAT by A5;
x9 <= len G by A5,FINSEQ_3:25;
then
A7: x9 <= len F by A2,A4,NAT_1:12;
1 <= x9 by A5,FINSEQ_3:25;
then
A8: x in dom F by A7,FINSEQ_3:25;
G.x = F.x by A1,A5,FUNCT_1:47
.= F/.x by A8,PARTFUN1:def 6;
hence u in the carrier of L by A6;
end;
then
A9: rng G c= the carrier of L by TARSKI:def 3;
hence G1 is FinSequence of L by FINSEQ_1:def 4;
reconsider G as FinSequence of L by A9,FINSEQ_1:def 4;
A10: dom(G^<*F/.(k+1)*>) = Seg(len G + len <*F/.(k+1)*>) by FINSEQ_1:def 7
.= Seg(k+1) by A4,FINSEQ_1:40
.= dom F by A2,FINSEQ_1:def 3;
hence dom G1 c= dom F by FINSEQ_1:26;
thus len G1 = k by A1,A3,FINSEQ_1:17;
now
let j be Nat;
assume
A11: j in dom F;
per cases;
suppose
A12: j in dom G;
hence F.j = G.j by A1,FUNCT_1:47
.= (G^<*F/.(k+1)*>).j by A12,FINSEQ_1:def 7;
end;
suppose
A13: not j in dom G;
A14: dom F = Seg len F by FINSEQ_1:def 3;
then
A15: 1 <= j by A11,FINSEQ_1:1;
A16: now
assume j < k + 1;
then j <= k by NAT_1:13;
then j in Seg k by A15;
hence contradiction by A1,A3,A13,FINSEQ_1:17;
end;
j <= k + 1 by A2,A11,A14,FINSEQ_1:1;
then
A17: j = k + 1 by A16,XXREAL_0:1;
dom <*F/.(k+1)*> = {1} by FINSEQ_1:2,38;
then 1 in dom <*F/.(k+1)*> by TARSKI:def 1;
hence (G^<*F/.(k+1)*>).j = <*F/.(k+1)*>.1 by A4,A17,FINSEQ_1:def 7
.= F/.(k+1)
.= F.j by A11,A17,PARTFUN1:def 6;
end;
end;
hence thesis by A10,FINSEQ_1:13;
end;
theorem Th1:
for L being add-associative right_zeroed right_complementable
associative commutative well-unital distributive almost_left_invertible non
empty doubleLoopStr for x being Element of L st x <> 0.L holds -(x") = (-x)"
proof
let L be add-associative right_zeroed right_complementable associative
commutative well-unital distributive almost_left_invertible non empty
doubleLoopStr;
let x be Element of L;
assume
A1: x <> 0.L;
A2: now
assume -x = 0.L;
then --x = 0.L by RLVECT_1:12;
hence contradiction by A1,RLVECT_1:17;
end;
(-x) * (-(x")) = -((-x) * x") by VECTSP_1:8
.= -(-(x * x")) by VECTSP_1:8
.= -(- 1_L) by A1,VECTSP_1:def 10
.= 1_L by RLVECT_1:17;
hence thesis by A2,VECTSP_1:def 10;
end;
theorem Th2:
for L being add-associative right_zeroed right_complementable
associative commutative well-unital almost_left_invertible distributive non
degenerated non empty doubleLoopStr for k being Element of NAT holds power(L)
.(-1_L,k) <> 0.L
proof
let L be add-associative right_zeroed right_complementable associative
commutative well-unital almost_left_invertible distributive non degenerated
non empty doubleLoopStr, k be Element of NAT;
defpred P[Nat] means power(L).(-1_L,$1) <> 0.L;
A1: now
A2: now
assume
A3: -1_L = 0.L;
1_L = 1_L * 1_L
.= (-1_L) * (-1_L) by VECTSP_1:10
.= 0.L by A3;
hence contradiction;
end;
let k be Nat;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
A4: power(L).(-1_L,kk+1) = power(L).(-1_L,kk) * (-1_L) by GROUP_1:def 7;
assume P[k];
hence P[k+1] by A4,A2,VECTSP_1:12;
end;
A5: P[0] by GROUP_1:def 7;
for k be Nat holds P[k] from NAT_1:sch 2(A5,A1);
hence thesis;
end;
theorem Th3:
for L being associative well-unital non empty multLoopStr for x
being Element of L for k1,k2 being Element of NAT holds power(L).(x,k1) * power
(L).(x,k2) = power(L).(x,k1+k2)
proof
let L be associative well-unital non empty multLoopStr, x be Element of L,
k1,k2 be Element of NAT;
defpred P[Nat] means ex j being Element of NAT st j = $1 & power(L).(x,k1) *
power(L).(x,j) = power(L).(x,k1+j);
A1: now
let j be Nat;
reconsider jj=j as Element of NAT by ORDINAL1:def 12;
assume
A2: P[j];
power(L).(x,k1) * power(L).(x,j+1) = power(L).(x,k1) * (power(L).(x,jj)
* x) by GROUP_1:def 7
.= (power(L).(x,k1) * power(L).(x,jj)) * x by GROUP_1:def 3
.= power(L).(x,(k1+j)+1) by A2,GROUP_1:def 7
.= power(L).(x,k1+(j+1));
hence P[j+1];
end;
1_L = 1.L;
then power(L).(x,k1) * power(L).(x,0) = power(L).(x,k1) * 1.L by
GROUP_1:def 7
.= power(L).(x,k1+0);
then
A3: P[0];
for k be Nat holds P[k] from NAT_1:sch 2(A3,A1);
then
ex j be Element of NAT st j = k2 & power(L).(x,k1) * power(L).(x,j) =
power(L).(x,k1+j);
hence thesis;
end;
Lm2: Im(1_F_Complex) = 0 & Im(-1_F_Complex) = 0 & Im(0.F_Complex) = 0
proof
thus Im(1_F_Complex) = 0 by COMPLEX1:6,COMPLFLD:8;
-1_F_Complex = -1r by COMPLFLD:8;
hence Im(-1_F_Complex) = -0 by COMPLEX1:6,17
.= 0;
thus thesis by COMPLEX1:4,COMPLFLD:7;
end;
theorem Th4:
for L being add-associative right_zeroed right_complementable
well-unital distributive non empty doubleLoopStr for k being Element of NAT
holds power(L).(-1_L,2*k) = 1_L & power(L).(-1_L,2*k+1) = -1_L
proof
let L be add-associative right_zeroed right_complementable well-unital
distributive non empty doubleLoopStr, k be Element of NAT;
defpred P[Nat] means power(L).(-1_L,2*$1) = 1_L & power(L).(-1_L,2*$1+1) = -
1_L;
A1: now
let k be Nat;
assume
A2: P[k];
A3: power(L).(-1_L,2*(k+1)) = power(L).(-1_L,(2*k+1)+1)
.= power(L).(-1_L,2*k+1) * (-1_L) by GROUP_1:def 7
.= - (1_L * (-1_L)) by A2,VECTSP_1:9
.= - (- 1_L)
.= 1_L by RLVECT_1:17;
power(L).(-1_L,2*(k+1)+1) = power(L).(-1_L,2*(k+1)) * (-1_L) by
GROUP_1:def 7
.= - (1_L) by A3;
hence P[k+1] by A3;
end;
power(L).(-1_L,2*0+1) = power(L).(-1_L,0) * (-1_L) by GROUP_1:def 7
.= 1_L * (-1_L) by GROUP_1:def 7
.= -1_L;
then
A4: P[0] by GROUP_1:def 7;
for k be Nat holds P[k] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
theorem Th5:
for z being Element of F_Complex for k being Element of NAT holds
(power(F_Complex).(z,k))*' = power(F_Complex).(z*',k)
proof
let z be Element of F_Complex, k be Element of NAT;
defpred P[Nat] means ex j be Element of NAT st j = $1 & (power(F_Complex).(z
,j))*' = power(F_Complex).(z*',j);
A1: now
let k be Nat;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
assume
A2: P[k];
(power(F_Complex).(z,k+1))*' = (power(F_Complex).(z,kk) * z)*' by
GROUP_1:def 7
.= (power(F_Complex).(z*',kk)) * (z*') by A2,COMPLFLD:54
.= power(F_Complex).(z*',k+1) by GROUP_1:def 7;
hence P[k+1];
end;
(power(F_Complex).(z,0))*' = (1_F_Complex)*' by GROUP_1:def 7
.= 1_F_Complex by Lm2,COMPLEX1:38
.= power(F_Complex).(z*',0) by GROUP_1:def 7;
then
A3: P[0];
for k be Nat holds P[k] from NAT_1:sch 2(A3,A1);
then ex j being Element of NAT st j = k & (power(F_Complex).(z,j))*' =
power(F_Complex).(z*',j);
hence thesis;
end;
theorem Th6:
for F,G being FinSequence of F_Complex st len G = len F & for i
being Element of NAT st i in dom G holds G/.i = (F/.i)*' holds Sum G = (Sum F)
*'
proof
defpred P[Nat] means for F,G being FinSequence of F_Complex st len G = len F
& len F = $1 & for i being Element of NAT st i in dom G holds G/.i = (F/.i)*'
holds Sum G = (Sum F)*';
let F,G be FinSequence of F_Complex;
assume that
A1: len G = len F and
A2: for i being Element of NAT st i in dom G holds G/.i = (F/.i)*';
A3: now
let k be Nat;
assume
A4: P[k];
now
let F,G be FinSequence of F_Complex;
assume that
A5: len F = len G and
A6: len F = k+1 and
A7: for i being Element of NAT st i in dom G holds G/.i=(F/.i)*';
set G1 = G|(Seg k);
reconsider G1 as FinSequence by FINSEQ_1:15;
reconsider G1 as FinSequence of F_Complex by A5,A6,Lm1;
A8: G = G1^<*G/.(k+1)*> by A5,A6,Lm1;
set F1 = F|(Seg k);
reconsider F1 as FinSequence by FINSEQ_1:15;
reconsider F1 as FinSequence of F_Complex by A6,Lm1;
A9: len F1 = k by A6,Lm1;
A10: len G1 = k by A5,A6,Lm1;
then
A11: dom G1 = Seg len F1 by A9,FINSEQ_1:def 3
.= dom F1 by FINSEQ_1:def 3;
1 <= k + 1 by NAT_1:11;
then
A12: k + 1 in dom G by A5,A6,FINSEQ_3:25;
A13: F = F1^<*F/.(k+1)*> by A6,Lm1;
A14: dom G = Seg len F by A5,FINSEQ_1:def 3
.= dom F by FINSEQ_1:def 3;
A15: now
let i be Element of NAT;
assume
A16: i in dom G1;
A17: dom G1 c= dom G by A5,A6,Lm1;
then
A18: F/.i = F.i by A14,A16,PARTFUN1:def 6
.= F1.i by A13,A11,A16,FINSEQ_1:def 7
.= F1/.i by A11,A16,PARTFUN1:def 6;
thus G1/.i = G1.i by A16,PARTFUN1:def 6
.= G.i by A8,A16,FINSEQ_1:def 7
.= G/.i by A16,A17,PARTFUN1:def 6
.= (F1/.i)*' by A7,A16,A17,A18;
end;
thus (Sum F)*' = (Sum F1 + Sum<*F/.(k+1)*>)*' by A13,RLVECT_1:41
.= (Sum F1)*' + (Sum<*F/.(k+1)*>)*' by COMPLFLD:51
.= Sum G1 + (Sum<*F/.(k+1)*>)*' by A4,A10,A9,A15
.= Sum G1 + (F/.(k+1))*' by RLVECT_1:44
.= Sum G1 + G/.(k+1) by A7,A12
.= Sum G1 + Sum<*G/.(k+1)*> by RLVECT_1:44
.= Sum G by A8,RLVECT_1:41;
end;
hence P[k+1];
end;
now
let F,G be FinSequence of F_Complex;
assume that
A19: len F = len G and
A20: len F = 0 and
for i being Element of NAT st i in dom G holds G/.i=(F/.i)*';
F = <*>(the carrier of F_Complex) by A20;
then Sum(F) = 0.F_Complex by RLVECT_1:43;
then
A21: Sum(F) = (0.F_Complex)*' by Lm2,COMPLEX1:38;
G = <*>(the carrier of F_Complex) by A19,A20;
hence Sum G = Sum(F)*' by A21,RLVECT_1:43;
end;
then
A22: P[0];
for k be Nat holds P[k] from NAT_1:sch 2(A22,A3);
hence thesis by A1,A2;
end;
theorem Th7:
for L being add-associative right_zeroed right_complementable
Abelian non empty addLoopStr, F1,F2 being FinSequence of L st len F1 = len F2
& for i being Element of NAT st i in dom F1 holds F1/.i = -(F2/.i) holds Sum F1
= - Sum F2
proof
let L be add-associative right_zeroed right_complementable Abelian non
empty addLoopStr, F1,F2 being FinSequence of L;
assume that
A1: len F1 = len F2 and
A2: for i being Element of NAT st i in dom F1 holds F1/.i = -(F2/.i);
defpred P[Nat] means for F1,F2 being FinSequence of L st len F1 = $1 & len
F1 = len F2 & for i being Element of NAT st i in dom F1 holds F1/.i = -(F2/.i)
holds Sum F1 = - Sum F2;
A3: now
let k be Nat;
assume
A4: P[k];
now
let f,g be FinSequence of L;
assume that
A5: len f = k+1 and
A6: len f = len g and
A7: for i being Element of NAT st i in dom f holds f/.i = -(g/.i);
set f1 = f|(Seg k), g1 = g|(Seg k);
reconsider f1, g1 as FinSequence by FINSEQ_1:15;
reconsider f1,g1 as FinSequence of L by A5,A6,Lm1;
A8: len f1 = k by A5,Lm1;
A9: len g1 = k by A5,A6,Lm1;
then
A10: dom f1 = Seg len g1 by A8,FINSEQ_1:def 3
.= dom g1 by FINSEQ_1:def 3;
A11: f = f1^<*f/.(k+1)*> by A5,Lm1;
A12: g = g1^<*g/.(k+1)*> by A5,A6,Lm1;
A13: now
A14: dom f1 c= dom f by A5,Lm1;
let i be Element of NAT;
assume
A15: i in dom f1;
dom g1 c= dom g by A5,A6,Lm1;
then
A16: g/.i = g.i by A10,A15,PARTFUN1:def 6
.= g1.i by A12,A10,A15,FINSEQ_1:def 7
.= g1/.i by A10,A15,PARTFUN1:def 6;
thus f1/.i = f1.i by A15,PARTFUN1:def 6
.= f.i by A11,A15,FINSEQ_1:def 7
.= f/.i by A15,A14,PARTFUN1:def 6
.= -(g1/.i) by A7,A15,A14,A16;
end;
1 <= k + 1 by NAT_1:11;
then
A17: k+1 in dom f by A5,FINSEQ_3:25;
thus Sum f = Sum f1 + Sum <*f/.(k+1)*> by A11,RLVECT_1:41
.= -(Sum g1) + Sum <*f/.(k+1)*> by A4,A8,A9,A13
.= -(Sum g1) + f/.(k+1) by RLVECT_1:44
.= -(Sum g1) + -(g/.(k+1)) by A7,A17
.= -(Sum g1 + g/.(k+1)) by RLVECT_1:31
.= -(Sum g1 + Sum<*g/.(k+1)*>) by RLVECT_1:44
.= -Sum g by A12,RLVECT_1:41;
end;
hence P[k+1];
end;
now
let f,g be FinSequence of L;
assume that
A18: len f = 0 and
A19: len f = len g and
for i being Element of NAT st i in dom f holds f/.i = -(g/.i);
A20: g = <*>(the carrier of L) by A18,A19;
f = <*>(the carrier of L) by A18;
hence Sum f = 0.L by RLVECT_1:43
.= - 0.L by RLVECT_1:12
.= -(Sum g) by A20,RLVECT_1:43;
end;
then
A21: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A21,A3);
hence thesis by A1,A2;
end;
theorem Th8:
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr for x being Element of L for F being
FinSequence of L holds x * Sum(F) = Sum(x*F)
proof
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr;
let x be Element of L;
let F be FinSequence of L;
defpred P[Nat] means for x being Element of L, F being FinSequence of L st
len F = $1 holds x * Sum(F) = Sum(x*F);
A1: ex n be Element of NAT st len F = n;
A2: now
let k be Nat;
assume
A3: P[k];
now
let x be Element of L;
let F be FinSequence of L;
set G = F|(Seg k);
reconsider G as FinSequence by FINSEQ_1:15;
assume
A4: len F = k+1;
then reconsider G as FinSequence of L by Lm1;
A5: len G = k by A4,Lm1;
A6: F = G^<*F/.(k+1)*> by A4,Lm1;
thus x * Sum(F) = x * Sum(G^<*F/.(k+1)*>) by A4,Lm1
.= x * (Sum G + Sum<*F/.(k+1)*>) by RLVECT_1:41
.= x * Sum G + x * Sum<*F/.(k+1)*> by VECTSP_1:def 2
.= Sum(x * G) + x * Sum<*F/.(k+1)*> by A3,A5
.= Sum(x * G) + x * F/.(k+1) by RLVECT_1:44
.= Sum(x * G) + Sum(<*x*F/.(k+1)*>) by RLVECT_1:44
.= Sum(x * G) + Sum(x*<*F/.(k+1)*>) by POLYNOM1:8
.= Sum((x * G)^(x*<*F/.(k+1)*>)) by RLVECT_1:41
.= Sum(x*F) by A6,POLYNOM1:10;
end;
hence P[k+1];
end;
now
let x be Element of L, F be FinSequence of L;
assume
A7: len F = 0;
Seg(len(x*F)) = dom(x*F) by FINSEQ_1:def 3
.= dom F by POLYNOM1:def 1
.= Seg len F by FINSEQ_1:def 3;
then len(x*F) = 0 by A7;
then
A8: (x*F) = <*>the carrier of L;
F = <*>the carrier of L by A7;
then Sum(F) = 0.L by RLVECT_1:43;
then x * Sum(F) = 0.L;
hence x * Sum(F) = Sum(x*F) by A8,RLVECT_1:43;
end;
then
A9: P[0];
for k be Nat holds P[k] from NAT_1:sch 2(A9,A2);
hence thesis by A1;
end;
begin :: More about Polynomials
Lm3: for L being add-associative right_zeroed right_complementable non empty
addLoopStr for p being Polynomial of L holds -(-p) = p
proof
let L be add-associative right_zeroed right_complementable non empty
addLoopStr;
let p be Polynomial of L;
A1: now
let x be Nat;
assume x < len p;
thus (-(-p)).x = -((-p)).x by BHSP_1:44
.= -(-(p.x)) by BHSP_1:44
.= p.x by RLVECT_1:17;
end;
len p = len(-p) by POLYNOM4:8
.= len(-(-p)) by POLYNOM4:8;
hence thesis by A1,ALGSEQ_1:12;
end;
theorem Th9:
for L being add-associative right_zeroed right_complementable
non empty addLoopStr holds -0_.(L) = 0_.(L)
proof
let L be add-associative right_zeroed right_complementable non empty
addLoopStr;
set e = 0_.(L), f = - 0_.(L);
A1: for x being Nat st x < len e holds e.x = f.x by POLYNOM4:3;
len f = len e by POLYNOM4:8;
hence thesis by A1,ALGSEQ_1:12;
end;
Lm4: for L being add-associative right_complementable right_zeroed
distributive non empty doubleLoopStr, p being Polynomial of L for f being
Element of Polynom-Ring(L) holds f = p implies -f = -p
proof
let L be add-associative right_complementable right_zeroed distributive non
empty doubleLoopStr, p be Polynomial of L;
let f be Element of Polynom-Ring(L);
reconsider x = -p as Element of Polynom-Ring(L) by POLYNOM3:def 10;
reconsider x as Element of Polynom-Ring(L);
assume f = p;
then f + x = p - p by POLYNOM3:def 10
.= 0_.(L) by POLYNOM3:29
.= 0.(Polynom-Ring(L)) by POLYNOM3:def 10;
then f = - x by RLVECT_1:6;
hence thesis by RLVECT_1:17;
end;
theorem
for L being add-associative right_zeroed right_complementable non
empty addLoopStr for p being Polynomial of L holds -(-p) = p by Lm3;
theorem Th11:
for L being add-associative right_zeroed right_complementable
Abelian distributive non empty doubleLoopStr for p1,p2 being Polynomial of L
holds -(p1 + p2) = (-p1) + (-p2)
proof
let L be add-associative right_zeroed right_complementable distributive
Abelian non empty doubleLoopStr;
let p1,p2 be Polynomial of L;
reconsider p19=p1,p29=p2 as Element of Polynom-Ring(L) by POLYNOM3:def 10;
A1: -(p19+p29) = -p19+-p29 by RLVECT_1:31;
A2: -p2=-p29 by Lm4;
p1 + p2 = p19 + p29 by POLYNOM3:def 10;
then
A3: -(p1+p2)=-(p19+p29) by Lm4;
-p1=-p19 by Lm4;
hence thesis by A3,A2,A1,POLYNOM3:def 10;
end;
theorem Th12:
for L being add-associative right_zeroed right_complementable
distributive Abelian non empty doubleLoopStr for p1,p2 being Polynomial of L
holds -(p1 *' p2) = (-p1) *' p2 & -(p1 *' p2) = p1 *' (-p2)
proof
let L be add-associative right_zeroed right_complementable distributive
Abelian non empty doubleLoopStr;
let p1,p2 be Polynomial of L;
reconsider p19=p1,p29=p2 as Element of Polynom-Ring(L) by POLYNOM3:def 10;
p1*'p2= p19*p29 by POLYNOM3:def 10;
then
A1: -(p1*'p2)=-(p19*p29) by Lm4;
-p1 = -p19 by Lm4;
then (-p1) *' p2 = (-p19) * p29 by POLYNOM3:def 10;
hence -(p1 *' p2) = (-p1) *' p2 by A1,VECTSP_1:9;
-p2 = -p29 by Lm4;
then p1 *' (-p2) = p19 * (-p29) by POLYNOM3:def 10;
hence thesis by A1,VECTSP_1:8;
end;
definition
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr;
let F be FinSequence of Polynom-Ring(L);
let i be Element of NAT;
func Coeff(F,i) -> FinSequence of L means
:Def1:
len it = len F & for j
being Element of NAT st j in dom it ex p being Polynomial of L st p = F.j & it.
j = p.i;
existence
proof
defpred P[set,set] means ex p being Polynomial of L st p = F.$1 & $2 = p.i;
A1: for k being Nat st k in Seg(len F) ex x being Element of the carrier
of L st P[k,x]
proof
let k be Nat;
assume
A2: k in Seg len F;
reconsider t = F/.k as Polynomial of L by POLYNOM3:def 10;
take t.i;
take t;
k in dom F by A2,FINSEQ_1:def 3;
hence t = F.k by PARTFUN1:def 6;
thus thesis;
end;
consider G being FinSequence of L such that
A3: dom G = Seg len F & for k being Nat st k in Seg len F holds P[k,G.
k] from FINSEQ_1:sch 5(A1);
take G;
thus len G = len F by A3,FINSEQ_1:def 3;
thus thesis by A3;
end;
uniqueness
proof
let z1,z2 be FinSequence of L;
assume that
A4: len z1 = len F and
A5: for j being Element of NAT st j in dom z1 ex p being Polynomial of
L st p = F.j & z1.j = p.i;
assume that
A6: len z2 = len F and
A7: for j being Element of NAT st j in dom z2 ex p being Polynomial of
L st p = F.j & z2.j = p.i;
A8: dom z1 = Seg len F by A4,FINSEQ_1:def 3
.= dom z2 by A6,FINSEQ_1:def 3;
now
let k be Nat;
assume
A9: k in dom z1;
then
A10: ex p1 being Polynomial of L st p1 = F.k & z1.k = p1.i by A5;
ex p2 being Polynomial of L st p2 = F.k & z2.k = p2.i by A7,A8,A9;
hence z1.k = z2.k by A10;
end;
hence thesis by A8,FINSEQ_1:13;
end;
end;
theorem Th13:
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr for p being Polynomial of L for F being
FinSequence of Polynom-Ring(L) st p = Sum F for i being Element of NAT holds p.
i = Sum Coeff(F,i)
proof
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr, p be Polynomial of L;
let F be FinSequence of Polynom-Ring(L);
assume
A1: p = Sum F;
defpred P[Nat] means for p being Polynomial of L for F being FinSequence of
Polynom-Ring(L) st p = Sum F & len F = $1 for i being Element of NAT holds p.i
= Sum Coeff(F,i);
let i be Element of NAT;
A2: ex m being Nat st len F = m;
A3: now
let k be Nat;
assume
A4: P[k];
now
let p be Polynomial of L;
let F be FinSequence of Polynom-Ring(L);
assume that
A5: p = Sum F and
A6: len F = k+1;
reconsider rf = F/.(k+1) as Polynomial of L by POLYNOM3:def 10;
let i be Element of NAT;
set G = F|(Seg k);
reconsider G as FinSequence by FINSEQ_1:15;
reconsider G as FinSequence of Polynom-Ring(L) by A6,Lm1;
A7: len G = k by A6,Lm1;
A8: k <= len F by A6,NAT_1:13;
A9: now
A10: dom Coeff(G,i) = Seg(len(Coeff(G,i))) by FINSEQ_1:def 3
.= Seg len G by Def1
.= dom G by FINSEQ_1:def 3;
let j be Nat;
assume
A11: j in dom Coeff(F,i);
per cases;
suppose
A12: j in dom Coeff(G,i);
then
A13: (Coeff(G,i)^<*rf.i*>).j = Coeff(G,i).j by FINSEQ_1:def 7;
A14: ex p being Polynomial of L st p = F.j & Coeff(F,i).j = p. i
by A11,Def1;
ex p1 being Polynomial of L st p1 = G.j & Coeff(G,i).j = p1.i
by A12,Def1;
hence Coeff(F,i).j = (Coeff(G,i)^<*rf.i*>).j by A10,A12,A13,A14,
FUNCT_1:47;
end;
suppose
A15: not j in dom Coeff(G,i);
A16: dom Coeff(F,i) = Seg(len Coeff(F,i)) by FINSEQ_1:def 3
.= Seg len F by Def1;
then
A17: 1 <= j by A11,FINSEQ_1:1;
A18: now
assume j < k + 1;
then j <= k by NAT_1:13;
then j in Seg k by A17;
hence contradiction by A8,A10,A15,FINSEQ_1:17;
end;
j <= k + 1 by A6,A11,A16,FINSEQ_1:1;
then
A19: j = k + 1 by A18,XXREAL_0:1;
dom <*rf.i*> = {1} by FINSEQ_1:2,38;
then
A20: 1 in dom <*rf.i*> by TARSKI:def 1;
1 <= k + 1 by NAT_1:11;
then
A21: k + 1 in dom F by A6,FINSEQ_3:25;
A22: ex p being Polynomial of L st p = F.j & Coeff(F,i).j = p. i
by A11,Def1;
len Coeff(G,i) = k by A7,Def1;
then (Coeff(G,i)^<*rf.i*>).j = <*rf.i*>.1 by A19,A20,FINSEQ_1:def 7
.= rf.i;
hence Coeff(F,i).j = (Coeff(G,i)^<*rf.i*>).j by A19,A22,A21,
PARTFUN1:def 6;
end;
end;
len(Coeff(G,i)^<*rf.i*>) = len Coeff(G,i) + len <*rf.i*> by FINSEQ_1:22
.= len Coeff(G,i) + 1 by FINSEQ_1:39
.= k + 1 by A7,Def1
.= len Coeff(F,i) by A6,Def1;
then dom Coeff(F,i) = Seg(len(Coeff(G,i)^<*rf.i*>)) by FINSEQ_1:def 3
.= dom(Coeff(G,i)^<*rf.i*>) by FINSEQ_1:def 3;
then
A23: Coeff(F,i) = Coeff(G,i)^<*rf.i*> by A9,FINSEQ_1:13;
reconsider pg = Sum G as Polynomial of L by POLYNOM3:def 10;
F = G^<*F/.(k+1)*> by A6,Lm1;
then Sum F = Sum G + Sum <*F/.(k+1)*> by RLVECT_1:41
.= Sum G + F/.(k+1) by RLVECT_1:44
.= pg + rf by POLYNOM3:def 10;
hence p.i = pg.i + rf.i by A5,NORMSP_1:def 2
.= Sum Coeff(G,i) + rf.i by A4,A7
.= Sum Coeff(G,i) + Sum <*rf.i*> by RLVECT_1:44
.= Sum Coeff(F,i) by A23,RLVECT_1:41;
end;
hence P[k+1];
end;
now
let p be Polynomial of L;
let F be FinSequence of Polynom-Ring(L);
assume that
A24: p = Sum F and
A25: len F = 0;
let i be Element of NAT;
F = <*>(the carrier of Polynom-Ring(L)) by A25;
then Sum F = 0.(Polynom-Ring(L)) by RLVECT_1:43;
then p = 0_.(L) by A24,POLYNOM3:def 10;
then
A26: p.i = 0.L;
len Coeff(F,i) = 0 by A25,Def1;
then Coeff(F,i) = <*>(the carrier of L);
hence p.i = Sum Coeff(F,i) by A26,RLVECT_1:43;
end;
then
A27: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A27,A3);
hence thesis by A1,A2;
end;
Lm5: for L being add-associative right_zeroed right_complementable
distributive Abelian non empty doubleLoopStr for p1,p2 being Polynomial of L
for p29 being Element of Polynom-Ring(L) st p29 = p2 for F being FinSequence of
Polynom-Ring(L) st p1 = Sum F holds p2 *' p1 = Sum(p29*F)
proof
let L be add-associative right_zeroed right_complementable distributive
Abelian non empty doubleLoopStr, p1,p2 be Polynomial of L;
let p29 be Element of Polynom-Ring(L);
assume
A1: p29 = p2;
reconsider p19 = p1 as Element of Polynom-Ring(L) by POLYNOM3:def 10;
let F be FinSequence of Polynom-Ring(L);
assume p1 = Sum F;
then p29 * p19 = Sum(p29*F) by Th8;
hence thesis by A1,POLYNOM3:def 10;
end;
theorem Th14:
for L being associative non empty doubleLoopStr for p being
Polynomial of L for x1, x2 being Element of L holds x1 * (x2 * p) = (x1 * x2) *
p
proof
let L be associative non empty doubleLoopStr, p being Polynomial of L;
let x1, x2 be Element of L;
set f = x1 * (x2 * p), g = (x1 * x2) * p;
A1: now
let i9 be object;
assume i9 in dom f;
then reconsider i = i9 as Element of NAT;
f.i = x1*(x2*p).i by POLYNOM5:def 4
.= x1*(x2*p.i) by POLYNOM5:def 4
.= (x1*x2)*p.i by GROUP_1:def 3
.= g.i by POLYNOM5:def 4;
hence f.i9 = g.i9;
end;
dom f = NAT by FUNCT_2:def 1
.= dom g by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th15:
for L being add-associative right_zeroed right_complementable
left-distributive non empty doubleLoopStr for p being Polynomial of L for x
being Element of L holds - (x * p) = (-x) * p
proof
let L be add-associative right_zeroed right_complementable left-distributive
non empty doubleLoopStr, p be Polynomial of L;
let x be Element of L;
set f = - (x * p), g = (-x) * p;
A1: now
let i9 be object;
assume i9 in dom f;
then reconsider i = i9 as Element of NAT;
f.i = -((x*p).i) by BHSP_1:44
.= -(x*p.i) by POLYNOM5:def 4
.= (-x)*p.i by VECTSP_1:9
.= g.i by POLYNOM5:def 4;
hence f.i9 = g.i9;
end;
dom f = NAT by FUNCT_2:def 1
.= dom g by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th16:
for L being add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr for p being Polynomial of L for x
being Element of L holds - (x * p) = x * (-p)
proof
let L be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr, p be Polynomial of L;
let x be Element of L;
set f = - (x * p), g = x * (-p);
A1: now
let i9 be object;
assume i9 in dom f;
then reconsider i = i9 as Element of NAT;
f.i = -((x*p).i) by BHSP_1:44
.= -(x*p.i) by POLYNOM5:def 4
.= x*(-p.i) by VECTSP_1:8
.= x*((-p).i) by BHSP_1:44
.= g.i by POLYNOM5:def 4;
hence f.i9 = g.i9;
end;
dom f = NAT by FUNCT_2:def 1
.= dom g by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th17:
for L being left-distributive non empty doubleLoopStr for p
being Polynomial of L for x1, x2 being Element of L holds (x1 + x2) * p = x1 *
p + x2 * p
proof
let L be left-distributive non empty doubleLoopStr, p be Polynomial of L;
let x1,x2 be Element of L;
set f = (x1 + x2) * p, g = x1 * p + x2 * p;
A1: now
let i9 be object;
assume i9 in dom f;
then reconsider i = i9 as Element of NAT;
f.i = (x1+x2)*p.i by POLYNOM5:def 4
.= x1*p.i+x2*p.i by VECTSP_1:def 3
.= (x1*p).i+x2*p.i by POLYNOM5:def 4
.= (x1*p).i+(x2*p).i by POLYNOM5:def 4
.= g.i by NORMSP_1:def 2;
hence f.i9 = g.i9;
end;
dom f = NAT by FUNCT_2:def 1
.= dom g by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th18:
for L being right-distributive non empty doubleLoopStr for p1,
p2 being Polynomial of L for x being Element of L holds x * (p1 + p2) = (x * p1
) + (x * p2)
proof
let L be right-distributive non empty doubleLoopStr, p1,p2 be Polynomial
of L;
let x be Element of L;
set f = x * (p1 + p2), g = (x * p1) + (x * p2);
A1: now
let i9 be object;
assume i9 in dom f;
then reconsider i = i9 as Element of NAT;
f.i = x*(p1+p2).i by POLYNOM5:def 4
.= x*(p1.i+p2.i) by NORMSP_1:def 2
.= x*p1.i+x*p2.i by VECTSP_1:def 2
.= (x*p1).i+x*p2.i by POLYNOM5:def 4
.= (x*p1).i+(x*p2).i by POLYNOM5:def 4
.= g.i by NORMSP_1:def 2;
hence f.i9 = g.i9;
end;
dom f = NAT by FUNCT_2:def 1
.= dom g by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th19:
for L being add-associative right_zeroed right_complementable
distributive commutative associative non empty doubleLoopStr for p1,p2 being
Polynomial of L for x being Element of L holds p1 *' (x * p2) = x * (p1 *' p2)
proof
let L be add-associative right_zeroed right_complementable distributive
commutative associative non empty doubleLoopStr, p1,p2 be Polynomial of L;
let x be Element of L;
set f = p1 *' (x * p2), g = x * (p1 *' p2);
A1: now
let i9 be object;
assume i9 in dom f;
then reconsider i = i9 as Element of NAT;
consider rf being FinSequence of L such that
A2: len rf = i+1 and
A3: f.i = Sum rf and
A4: for k be Element of NAT st k in dom rf holds rf.k = p1.(k-'1) * (x
* p2).(i+1-'k) by POLYNOM3:def 9;
consider rp being FinSequence of L such that
A5: len rp = i+1 and
A6: (p1*'p2).i = Sum rp and
A7: for k be Element of NAT st k in dom rp holds rp.k = p1.(k-'1) * p2
.( i+1-'k) by POLYNOM3:def 9;
A8: Seg(len(x*rp)) = dom(x*rp) by FINSEQ_1:def 3
.= dom rp by POLYNOM1:def 1
.= Seg len rp by FINSEQ_1:def 3;
then
A9: dom(x*rp) = Seg len rf by A2,A5,FINSEQ_1:def 3
.= dom rf by FINSEQ_1:def 3;
A10: dom(x*rp) = dom rp by POLYNOM1:def 1;
A11: now
let j be Nat;
assume that
A12: 1 <= j and
A13: j <= len rf;
A14: j in dom rf by A12,A13,FINSEQ_3:25;
then
A15: rp/.j = rp.j by A9,A10,PARTFUN1:def 6;
thus (x*rp).j = (x*rp)/.j by A9,A14,PARTFUN1:def 6
.= x * (rp/.j) by A9,A10,A14,POLYNOM1:def 1
.= x * (p1.(j-'1) * p2.(i+1-'j)) by A7,A9,A10,A14,A15
.= p1.(j-'1) * (x * p2.(i+1-'j)) by GROUP_1:def 3
.= p1.(j-'1) * (x*p2).(i+1-'j) by POLYNOM5:def 4
.= rf.j by A4,A14;
end;
g.i = x * Sum rp by A6,POLYNOM5:def 4
.= Sum(x * rp) by Th8
.= f.i by A2,A3,A5,A8,A11,FINSEQ_1:6,14;
hence f.i9 = g.i9;
end;
dom f = NAT by FUNCT_2:def 1
.= dom g by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
definition
let L be non empty ZeroStr;
let p be Polynomial of L;
func degree p -> Integer equals
len p - 1;
coherence;
end;
notation
let L be non empty ZeroStr;
let p be Polynomial of L;
synonym deg p for degree p;
end;
Lm6: for L being non empty ZeroStr, s being AlgSequence of L holds len(s) > 0
implies s.(len(s)-1) <> 0.L
proof
let L be non empty ZeroStr, s be AlgSequence of L;
assume len(s) > 0;
then len(s) >= 0 + 1 by NAT_1:13;
then len(s) - 1 >= 1 - 1 by XREAL_1:9;
then reconsider l = len(s) - 1 as Element of NAT by INT_1:3;
assume
A1: s.(len(s)-1) = 0.L;
now
let i be Nat;
assume
A2: i >= l;
per cases by A2,XXREAL_0:1;
suppose
i = l;
hence s.i = 0.L by A1;
end;
suppose
i > l;
then i >= l + 1 by NAT_1:13;
hence s.i = 0.L by ALGSEQ_1:8;
end;
end;
then
A3: l is_at_least_length_of s by ALGSEQ_1:def 2;
len(s) < len(s) + 1 by NAT_1:13;
then len(s) - 1 < len(s) + 1 - 1 by XREAL_1:9;
hence contradiction by A3,ALGSEQ_1:def 3;
end;
theorem Th20:
for L being non empty ZeroStr for p being Polynomial of L holds
deg p = -1 iff p = 0_.(L)
proof
let L be non empty ZeroStr;
let p be Polynomial of L;
now
assume p = 0_.(L);
then len p = 0 by POLYNOM4:3;
hence deg p = -1;
end;
hence thesis by POLYNOM4:5;
end;
Lm7: for L being non empty ZeroStr, p being Polynomial of L holds deg p <> - 1
implies p.deg(p) <> 0.L
proof
let L be non empty ZeroStr, p be Polynomial of L;
assume deg p <> -1;
then len p <> 0;
hence thesis by Lm6;
end;
Lm8: for L being non empty ZeroStr for p being Polynomial of L holds deg p is
Element of NAT iff p <> 0_.(L)
proof
let L be non empty ZeroStr;
let p be Polynomial of L;
now
assume p <> 0_.(L);
then len p <> 0 by POLYNOM4:5;
then len p + 1 > 0 + 1 by XREAL_1:6;
then len p >= 1 by NAT_1:13;
then len p - 1 >= 1 - 1 by XREAL_1:9;
hence deg(p) is Element of NAT by INT_1:3;
end;
hence thesis by Th20;
end;
theorem
for L being add-associative right_zeroed right_complementable non
empty addLoopStr for p1,p2 being Polynomial of L st deg p1 <> deg p2 holds deg
(p1 + p2) = max(deg(p1),deg(p2))
proof
let L be add-associative right_zeroed right_complementable non empty
addLoopStr;
let p1,p2 be Polynomial of L;
assume deg p1 <> deg p2;
then
A1: deg(p1+p2) = max(len(p1),len(p2)) - 1 by POLYNOM4:7;
per cases by XXREAL_0:16;
suppose
A2: max(len(p1),len(p2)) = len(p1);
then len p2 <= len p1 by XXREAL_0:25;
then deg p2 <= deg p1 by XREAL_1:9;
hence thesis by A1,A2,XXREAL_0:def 10;
end;
suppose
A3: max(len(p1),len(p2)) = len(p2);
then len p1 <= len p2 by XXREAL_0:25;
then deg p1 <= deg p2 by XREAL_1:9;
hence thesis by A1,A3,XXREAL_0:def 10;
end;
end;
Lm9: for L being non empty ZeroStr, p being Polynomial of L holds deg p >= -1
proof
let L be non empty ZeroStr, p be Polynomial of L;
per cases;
suppose
p = 0_.(L);
hence thesis by Th20;
end;
suppose
p <> 0_.(L);
hence thesis by Lm8;
end;
end;
theorem Th22:
for L being add-associative right_zeroed right_complementable
Abelian non empty addLoopStr for p1,p2 being Polynomial of L holds deg(p1 +
p2) <= max(deg(p1),deg(p2))
proof
let L be add-associative right_zeroed right_complementable Abelian non
empty addLoopStr;
let p1,p2 be Polynomial of L;
per cases;
suppose
A1: p1 = 0_.(L);
then deg(p1) = -1 by Th20;
then
A2: deg(p2) >= deg(p1) by Lm9;
deg(p1 + p2) = deg(p2) by A1,POLYNOM3:28
.= max(deg(p1),deg(p2)) by A2,XXREAL_0:def 10;
hence thesis;
end;
suppose
A3: p2 = 0_.(L);
then deg(p2) = -1 by Th20;
then
A4: deg(p1) >= deg(p2) by Lm9;
deg(p1 + p2) = deg(p1) by A3,POLYNOM3:28
.= max(deg(p1),deg(p2)) by A4,XXREAL_0:def 10;
hence thesis;
end;
suppose
A5: p1 <> 0_.(L) & p2 <> 0_.(L);
then
A6: deg(p2) is Element of NAT by Lm8;
deg(p1) is Element of NAT by A5,Lm8;
then reconsider m = max(deg(p1),deg(p2)) as Element of NAT by A6,
XXREAL_0:16;
for k being Nat st k >= m+1 holds (p1+p2).k = 0.L
proof
let k be Nat;
assume
A7: k >= m + 1;
deg(p2) <= m by XXREAL_0:25;
then deg(p2) + 1 <= m + 1 by XREAL_1:6;
then
A8: p2.k = 0.L by A7,ALGSEQ_1:8,XXREAL_0:2;
deg(p1) <= m by XXREAL_0:25;
then deg(p1) + 1 <= m + 1 by XREAL_1:6;
then p1.k = 0.L by A7,ALGSEQ_1:8,XXREAL_0:2;
hence (p1+p2).k = 0.L + 0.L by A8,NORMSP_1:def 2
.= 0.L by RLVECT_1:def 4;
end;
then m+1 is_at_least_length_of (p1+p2) by ALGSEQ_1:def 2;
then len(p1+p2)<=m+1 by ALGSEQ_1:def 3;
then len(p1+p2)-1<=m+1-1 by XREAL_1:9;
hence thesis;
end;
end;
theorem Th23:
for L being add-associative right_zeroed right_complementable
distributive associative well-unital domRing-like non empty
doubleLoopStr for p1,p2 being Polynomial of L st p1 <> 0_.(L) & p2 <> 0_.(L)
holds deg(p1 *' p2) = deg(p1) + deg(p2)
proof
let L be add-associative right_zeroed right_complementable distributive
associative well-unital domRing-like non empty doubleLoopStr;
let p1,p2 be Polynomial of L;
assume that
A1: p1 <> 0_.(L) and
A2: p2 <> 0_.(L);
A3: dom p2 = NAT by FUNCT_2:def 1;
deg p2 is Element of NAT by A2,Lm8;
then
A4: p2/.(deg(p2)) = p2.(deg(p2)) by A3,PARTFUN1:def 6;
deg p2 <> -1 by A2,Th20;
then
A5: p2/.(deg(p2)) <> 0.L by A4,Lm7;
A6: dom p1 = NAT by FUNCT_2:def 1;
deg p1 is Element of NAT by A1,Lm8;
then
A7: p1/.(deg(p1)) = p1.(deg(p1)) by A6,PARTFUN1:def 6;
len p2 <> 0 by A2,POLYNOM4:5;
then len p2 + 1 > 0 + 1 by XREAL_1:6;
then len p2 >= 1 by NAT_1:13;
then len p2 - 1 >= 1 - 1 by XREAL_1:9;
then
A8: p2/.(deg(p2)) = p2.(len p2-'1) by A4,XREAL_0:def 2;
deg p1 <> -1 by A1,Th20;
then
A9: p1/.(deg(p1)) <> 0.L by A7,Lm7;
len p1 <> 0 by A1,POLYNOM4:5;
then len p1 + 1 > 0 + 1 by XREAL_1:6;
then len p1 >= 1 by NAT_1:13;
then len p1 - 1 >= 1 - 1 by XREAL_1:9;
then p1/.(deg(p1)) = p1.(len p1-'1) by A7,XREAL_0:def 2;
then p1.(len p1 -'1) * p2.(len p2 -'1) <> 0.L by A8,A9,A5,VECTSP_2:def 1;
hence deg(p1*'p2) = (len p1 + len p2 - 1)-1 by POLYNOM4:10
.= deg p1 + deg p2;
end;
theorem Th24:
for L being add-associative right_zeroed right_complementable
unital non empty doubleLoopStr for p being Polynomial of L st deg p = 0 holds
not(p is with_roots)
proof
let L be add-associative right_zeroed right_complementable unital non empty
doubleLoopStr, p be Polynomial of L;
assume
A1: deg p = 0;
then
A2: p = <%p.0%> by ALGSEQ_1:def 5;
now
assume p is with_roots;
then consider x be Element of L such that
A3: x is_a_root_of p by POLYNOM5:def 8;
0.L = eval(p,x) by A3,POLYNOM5:def 7
.= p.0 by A2,POLYNOM5:37;
hence contradiction by A1,A2,ALGSEQ_1:14;
end;
hence thesis;
end;
Lm10: for L being unital non empty doubleLoopStr for z be Element of L, k be
Element of NAT st k <> 0 holds (0_.(L) +* (0,k)-->(-power(L).(z,k),1_L)).0 = -
power(L).(z,k) & (0_.(L) +* (0,k)-->(-power(L).(z,k),1_L)).k = 1_L
proof
let L be unital non empty doubleLoopStr;
let z be Element of L;
let k be Element of NAT;
assume
A1: k <> 0;
set t = 0_.(L) +* (0,k)-->(-power(L).(z,k),1_L), f = (0,k)-->(-power(L).(z,k
),1_L), a = -power(L).(z,k);
A2: dom f = {0,k} by FUNCT_4:62;
now
let u be object;
assume u in {0,k};
then u = 0 or u = k by TARSKI:def 2;
hence u in NAT;
end;
then
A3: {0,k} c= NAT by TARSKI:def 3;
A4: dom(0_.(L)) \/ dom(f) = NAT by A2,A3,XBOOLE_1:12;
0 in dom f by A2,TARSKI:def 2;
hence t.0 = f.0 by A4,FUNCT_4:def 1
.= a by A1,FUNCT_4:63;
k in dom f by A2,TARSKI:def 2;
hence t.k = f.k by A4,FUNCT_4:def 1
.= 1_L by FUNCT_4:63;
end;
Lm11: for L being unital non empty doubleLoopStr for z being Element of L, k
be Element of NAT,i being Nat st i <> 0 & i <> k holds (0_.(L) +* (0,k)-->(-
power(L).(z,k),1_L)).i = 0.L
proof
let L be unital non empty doubleLoopStr;
let z be Element of L, k be Element of NAT,i be Nat;
assume that
A1: i <> 0 and
A2: i <> k;
set t = 0_.(L) +* (0,k)-->(-power(L).(z,k),1_L), f = (0,k)-->(-power(L).(z,k
),1_L);
now
let u be object;
assume u in {0,k};
then u = 0 or u = k by TARSKI:def 2;
hence u in NAT;
end;
then
A4: {0,k} c= NAT by TARSKI:def 3;
dom f = {0,k} by FUNCT_4:62;
then
A5: dom(0_.(L)) \/ dom(f) = NAT by A4,XBOOLE_1:12;
A6: i in NAT by ORDINAL1:def 12;
not i in dom f by A1,A2,TARSKI:def 2;
hence t.i = (0_.(L)).i by A5,A6,FUNCT_4:def 1
.= 0.L by A6,FUNCOP_1:7;
end;
:: the polynomials x^k - z^k
definition
let L be unital non empty doubleLoopStr;
let z be Element of L;
let k be Element of NAT;
func rpoly(k,z) -> Polynomial of L equals
0_.(L) +* (0,k)-->(-power(L).(z,k),1_L);
coherence
proof
now
let u be object;
assume u in {0,k};
then u = 0 or u = k by TARSKI:def 2;
hence u in NAT;
end;
then
A1: {0,k} c= NAT by TARSKI:def 3;
set a = -power(L).(z,k);
set p = 0_.(L) +* (0,k)-->(-power(L).(z,k),1_L);
set f = (0,k)-->(-power(L).(z,k),1_L);
A2: dom f = {0,k} by FUNCT_4:62;
A3: k in {k} by TARSKI:def 1;
then
A4: k in dom({k} --> 1_L);
A5: now
let x9 be object;
assume x9 in NAT;
then reconsider x = x9 as Element of NAT;
per cases;
suppose
A6: k = 0 & x = 0;
then x in dom f by A2,TARSKI:def 2;
then p.x = f.x by FUNCT_4:13
.= ((0 .--> a) +* (k .--> 1_L)).x by FUNCT_4:def 4
.= (k .--> 1_L).x by A4,A6,FUNCT_4:13
.= 1_L by A3,A6,FUNCOP_1:7;
hence p.x9 in the carrier of L;
end;
suppose
x = 0 & k <> 0;
then p.x = -power(L).(z,k) by Lm10;
hence p.x9 in the carrier of L;
end;
suppose
x = k & k <> 0;
then p.x = 1_L by Lm10;
hence p.x9 in the carrier of L;
end;
suppose
x <> 0 & x <> k;
then p.x = 0.L by Lm11;
hence p.x9 in the carrier of L;
end;
end;
dom(0_.(L)) \/ dom(f) = NAT by A2,A1,XBOOLE_1:12;
then dom p = NAT by FUNCT_4:def 1;
then reconsider p as sequence of the carrier of L by A5,FUNCT_2:3;
reconsider p as sequence of L;
now
let i be Nat;
assume
A7: i >= k + 1;
then i <> k by NAT_1:13;
hence p.i = 0.L by A7,Lm11;
end;
then reconsider p as AlgSequence of L by ALGSEQ_1:def 1;
p is Polynomial of L;
hence thesis;
end;
end;
theorem
for L being unital non empty doubleLoopStr for z being Element of L
for k being Element of NAT st k <> 0 holds rpoly(k,z).0 = -power(L).(z,k) &
rpoly(k,z).k = 1_L by Lm10;
theorem
for L being unital non empty doubleLoopStr for z being Element of L
for i,k being Element of NAT st i <> 0 & i <> k holds rpoly(k,z).i = 0.L by
Lm11;
theorem Th27:
for L being well-unital non degenerated non empty doubleLoopStr
for z being Element of L for k being Element of NAT holds deg rpoly(k,z) = k
proof
let L be well-unital non degenerated non empty doubleLoopStr;
let z be Element of L;
let k be Element of NAT;
set t = rpoly(k,z);
set a = -power(L).(z,k);
set f = (0,k)-->(a,1_L);
per cases;
suppose
A1: k = 0;
A2: now
let m be Nat;
assume
A3: m is_at_least_length_of t;
now
assume m < 1;
then
A4: m = 0 by NAT_1:14;
A5: k in {k} by TARSKI:def 1;
then
A6: k in dom({k}-->1_L);
dom f = {0,k} by FUNCT_4:62;
then 0 in dom f by TARSKI:def 2;
then t.0 = f.0 by FUNCT_4:13
.= ((0 .-->a)+*(k.-->1_L)).0 by FUNCT_4:def 4
.= (0 .--> 1_L).0 by A1,A6,FUNCT_4:13
.= 1_L by A1,A5,FUNCOP_1:7;
hence contradiction by A3,A4,ALGSEQ_1:def 2;
end;
hence 1 <= m;
end;
now
let i be Nat;
A7: i in NAT by ORDINAL1:def 12;
assume i >= 1;
then not i in dom f by A1,TARSKI:def 2;
hence t.i = (0_.(L)).i by FUNCT_4:11
.= 0.L by A7,FUNCOP_1:7;
end;
then 1 is_at_least_length_of t by ALGSEQ_1:def 2;
then len rpoly(k,z) = 1 by A2,ALGSEQ_1:def 3;
hence thesis by A1;
end;
suppose
A8: k <> 0;
A9: now
let m be Nat;
assume
A10: m is_at_least_length_of t;
now
assume m < k + 1;
then
A11: m <= k by NAT_1:13;
t.k = 1_L by A8,Lm10;
hence contradiction by A10,A11,ALGSEQ_1:def 2;
end;
hence k+1 <= m;
end;
now
let i be Nat;
assume i >= k+1;
then i > k by NAT_1:13;
hence t.i = 0.L by Lm11;
end;
then (k+1) is_at_least_length_of t by ALGSEQ_1:def 2;
then len rpoly(k,z) = k + 1 by A9,ALGSEQ_1:def 3;
hence thesis;
end;
end;
theorem Th28:
for L being add-associative right_zeroed right_complementable
well-unital commutative associative distributive almost_left_invertible non
degenerated non empty doubleLoopStr for p being Polynomial of L holds deg(p)
= 1 iff ex x,z being Element of L st x <> 0.L & p = x * rpoly(1,z)
proof
let L be add-associative right_zeroed right_complementable well-unital
commutative associative distributive almost_left_invertible non degenerated
non empty doubleLoopStr, p be Polynomial of L;
A1: now
set x = p.1, z = (-p.0)*(p.1)";
set f = x * rpoly(1,z);
assume
A2: deg(p) = 1;
then
A3: len p = 1 + 1;
then
A4: x <> 0.L by ALGSEQ_1:10;
A5: now
let k be Nat;
assume k < len p;
then k < 1+1 by A2;
then
A6: k <= 1 by NAT_1:13;
per cases by A6,XXREAL_0:1;
suppose
A7: k = 1;
hence f.k = x * rpoly(1,z).1 by POLYNOM5:def 4
.= x * 1_L by Lm10
.= p.k by A7;
end;
suppose
k < 1;
then
A8: k = 0 by NAT_1:14;
hence f.k = x * rpoly(1,z).0 by POLYNOM5:def 4
.= x * (-(power(L).(z,1+0))) by Lm10
.= x * (-(power(L).(z,0) * z)) by GROUP_1:def 7
.= x * (-(1_L * z)) by GROUP_1:def 7
.= x * (- z)
.= p.1 * (-(-(p.0*(p.1)"))) by VECTSP_1:9
.= p.1 * (p.0*(p.1)") by RLVECT_1:17
.= (p.1 * (p.1)") * p.0 by GROUP_1:def 3
.= 1_L * p.0 by A4,VECTSP_1:def 10
.= p.k by A8;
end;
end;
len f = deg(rpoly(1,z)) + 1 by A3,ALGSEQ_1:10,POLYNOM5:25
.= 1+1 by Th27
.= len p by A2;
then p = f by A5,ALGSEQ_1:12;
hence ex x,z being Element of L st x <> 0.L & p = x * rpoly(1,z) by A3,
ALGSEQ_1:10;
end;
now
given x,z being Element of L such that
A9: x <> 0.L and
A10: p = x * rpoly(1,z);
thus deg p = deg rpoly(1,z) by A9,A10,POLYNOM5:25
.= 1 by Th27;
end;
hence thesis by A1;
end;
theorem Th29:
for L being add-associative right_zeroed right_complementable
Abelian well-unital non degenerated non empty doubleLoopStr for x,z being
Element of L holds eval(rpoly(1,z),x) = x - z
proof
A1: 2-'1 = 2-1 by XREAL_0:def 2;
A2: 1-'1 = 1-1 by XREAL_0:def 2;
let L be add-associative right_zeroed right_complementable Abelian
well-unital non degenerated non empty doubleLoopStr, x,z be Element of L;
set p = rpoly(1,z);
consider F be FinSequence of L such that
A3: eval(p,x) = Sum F and
A4: len F = len p and
A5: for n be Element of NAT st n in dom F holds F.n = p.(n-'1) * (power
L).(x,n-'1) by POLYNOM4:def 2;
A6: deg p = 1 by Th27;
then
A7: F = <*F.1,F.2*> by A4,FINSEQ_1:44
.= <*F.1*>^<*F.2*>;
2 in Seg(len F) by A4,A6;
then 2 in dom F by FINSEQ_1:def 3;
then
A8: F.2 = p.1* (power L).(x,1+0) by A5,A1
.= p.1* ((power L).(x,0) * x) by GROUP_1:def 7
.= p.1* (1_L * x) by GROUP_1:def 7
.= p.1* x
.= 1_L * x by Lm10
.= x;
1 in Seg len F by A4,A6,FINSEQ_1:2;
then 1 in dom F by FINSEQ_1:def 3;
then F.1 = p.0* (power L).(x,1-'1) by A5,A2
.= p.0 * 1_L by A2,GROUP_1:def 7
.= p.0
.= -power(L).(z,1+0) by Lm10
.= -(power(L).(z,0) * z) by GROUP_1:def 7
.= -(1_L * z) by GROUP_1:def 7
.= -z;
hence eval(p,x) = Sum(<*-z*>) + Sum(<*x*>) by A3,A7,A8,RLVECT_1:41
.= Sum(<*-z*>) + x by RLVECT_1:44
.= -z + x by RLVECT_1:44
.= x - z by RLVECT_1:def 11;
end;
theorem Th30:
for L being add-associative right_zeroed right_complementable
well-unital Abelian non degenerated non empty doubleLoopStr for z being
Element of L holds z is_a_root_of rpoly(1,z)
proof
let L be Abelian well-unital add-associative right_zeroed non degenerated
right_complementable non empty doubleLoopStr, z be Element of L;
eval(rpoly(1,z),z) = z - z by Th29
.= 0.L by RLVECT_1:15;
hence thesis by POLYNOM5:def 7;
end;
:: the polynomials x^(k-1) + x^(k-2)*z + x^(k-3)*z^2 + ... + x*z^(k-2) + z^(k-1)
definition
let L be well-unital non empty doubleLoopStr;
let z be Element of L;
let k be Nat;
func qpoly(k,z) -> Polynomial of L means
:Def4:
(for i being Nat st i < k
holds it.i = power(L).(z,k-i-1)) & for i being Nat st i >= k holds it.i = 0.L;
existence
proof
defpred P[object,object] means
ex n being Element of NAT st n = $1 & (n < k
implies $2 = power(L).(z,k-n-1)) & (n >= k implies $2 = 0.L);
A1: for x being object st x in NAT
ex y being object st y in the carrier of L & P[x,y]
proof
let u be object;
assume u in NAT;
then reconsider u9 = u as Element of NAT;
per cases;
suppose
A2: u9 < k;
then reconsider ku = k - u9 as Element of NAT by INT_1:5;
k - k < ku by A2,XREAL_1:10;
then 0 + 1 < ku + 1 by XREAL_1:6;
then 1 <= k-u9 by NAT_1:13;
then reconsider m = k-u9-1 as Element of NAT by INT_1:5;
take power(L).(z,k-u9-1);
power(L).(z,m) in the carrier of L;
hence thesis by A2;
end;
suppose
A3: u9 >= k;
take 0.L;
thus thesis by A3;
end;
end;
consider f being sequence of the carrier of L such that
A4: for x being object st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A1);
reconsider f as sequence of L;
A5: for i being Nat st i >= k holds f.i = 0.L
proof
let i be Nat;
i in NAT by ORDINAL1:def 12;
then
A6: ex n being Element of NAT st n = i &( n < k implies f.i = power(L)
.(z,k-n-1))&( n >= k implies f.i = 0.L) by A4;
assume i >= k;
hence thesis by A6;
end;
then reconsider p = f as AlgSequence of L by ALGSEQ_1:def 1;
take p;
now
let i be Nat;
i in NAT by ORDINAL1:def 12;
then
A7: ex n being Element of NAT st n = i &( n < k implies f.i = power(L)
.(z,k-n-1))&( n >= k implies f.i = 0.L) by A4;
assume i < k;
hence p.i = power(L).(z,k-i-1) by A7;
end;
hence thesis by A5;
end;
uniqueness
proof
let z1,z2 be AlgSequence of L;
assume that
A8: for i being Nat st i < k holds z1.i = power(L).(z,k-i-1) and
A9: for i being Nat st i >= k holds z1.i = 0.L;
assume that
A10: for i being Nat st i < k holds z2.i = power(L).(z,k-i-1) and
A11: for i being Nat st i >= k holds z2.i = 0.L;
A12: now
let x be object;
assume x in dom z1;
then reconsider x9 = x as Element of NAT;
per cases;
suppose
A13: x9 < k;
hence z1.x = power(L).(z,k-x9-1) by A8
.= z2.x by A10,A13;
end;
suppose
A14: x9 >= k;
hence z1.x = 0.L by A9
.= z2.x by A11,A14;
end;
end;
dom z1 = NAT by FUNCT_2:def 1
.= dom z2 by FUNCT_2:def 1;
hence z1 = z2 by A12,FUNCT_1:2;
end;
end;
theorem
for L being well-unital non degenerated non empty doubleLoopStr for
z being Element of L for k being Element of NAT st k >= 1 holds deg qpoly(k,z)
= k - 1
proof
let L be well-unital non degenerated non empty doubleLoopStr;
let z be Element of L;
let k be Element of NAT;
set p = qpoly(k,z);
A1: k - 1 < k - 0 by XREAL_1:10;
assume k >= 1;
then k - 1 >= 1 - 1 by XREAL_1:9;
then reconsider k9 = k - 1 as Element of NAT by INT_1:3;
k - k9 - 1 = 0;
then p.(k-1) = power(L).(z,0) by A1,Def4
.= 1_L by GROUP_1:def 7;
then
A2: p.(k-1) <> 0.L;
A3: now
let m be Nat;
assume
A4: m is_at_least_length_of p;
now
assume k > m;
then k9 + 1 > m;
then k9 >= m by NAT_1:13;
hence contradiction by A2,A4,ALGSEQ_1:def 2;
end;
hence k <= m;
end;
for i being Nat st i >= k holds p.i = 0.L by Def4;
then k is_at_least_length_of p by ALGSEQ_1:def 2;
hence thesis by A3,ALGSEQ_1:def 3;
end;
theorem Th32:
for L being add-associative right_zeroed right_complementable
left-distributive well-unital commutative non empty doubleLoopStr for z being
Element of L for k being Element of NAT st k > 1 holds rpoly(1,z) *' qpoly(k,z)
= rpoly(k,z)
proof
let L be add-associative right_zeroed right_complementable left-distributive
well-unital commutative non empty doubleLoopStr;
let z be Element of L, k be Element of NAT;
set p = rpoly(1,z) *' qpoly(k,z), u = rpoly(k,z);
assume
A1: k > 1;
then reconsider k1 = k - 1 as Element of NAT by INT_1:5;
k1 + 1 = k;
then
A2: k1 <= k by INT_1:6;
k1 <> k;
then
A3: k1 < k by A2,XXREAL_0:1;
A4: now
A5: 1 - 1 >= 0;
let i9 be object;
A6: 0 + 1 = 1;
assume i9 in dom p;
then reconsider i = i9 as Element of NAT;
consider fp being FinSequence of L such that
A7: len fp = i+1 and
A8: p.i = Sum fp and
A9: for j be Element of NAT st j in dom fp holds fp.j = rpoly(1,z).(j
-'1 ) * qpoly(k,z).(i+1-'j) by POLYNOM3:def 9;
A10: i + 1 - 2 = i - 1;
len fp >= 1 by A7,NAT_1:11;
then 1 in Seg(len fp);
then
A11: 1 in dom fp by FINSEQ_1:def 3;
then
A12: fp/.1 = fp.1 by PARTFUN1:def 6
.= rpoly(1,z).(1-'1) * qpoly(k,z).(i+1-'1) by A9,A11
.= rpoly(1,z).0 * qpoly(k,z).(i+1-'1) by A5,XREAL_0:def 2
.= (-power(L).(z,1)) * qpoly(k,z).(i+1-'1) by Lm10
.= (-power(L).(z,0)*z) * qpoly(k,z).(i+1-'1) by A6,GROUP_1:def 7
.= (-(1_L*z)) * qpoly(k,z).(i+1-'1) by GROUP_1:def 7
.= (-z) * qpoly(k,z).(i+1-'1)
.= (-z) * qpoly(k,z).i by NAT_D:34;
A13: now
let j be Element of NAT;
assume that
A14: j in dom fp and
A15: j <> 1 and
A16: j <> 2;
A17: j in Seg(len fp) by A14,FINSEQ_1:def 3;
now
assume
A18: j-'1 = 0 or j-'1 = 1;
per cases;
suppose
j-1 >= 0;
then j-'1 = j - 1 by XREAL_0:def 2;
hence contradiction by A15,A16,A18;
end;
suppose
j-1 < 0;
then j-1+1 < 0 + 1 by XREAL_1:8;
hence contradiction by A17,FINSEQ_1:1;
end;
end;
then
A19: rpoly(1,z).(j-'1) = 0.L by Lm11;
fp.j = rpoly(1,z).(j-'1) * qpoly(k,z).(i+1-'j) by A9,A14;
hence fp.j = 0.L by A19;
end;
A20: now
A21: 1 + 1 = 2;
consider g1,g2 being FinSequence of L such that
A22: len g1 = 1 and
A23: len g2 = i and
A24: fp = g1 ^ g2 by A7,FINSEQ_2:23;
A25: g1 = <*g1.1*> by A22,FINSEQ_1:40
.= <*fp.1*> by A22,A24,FINSEQ_1:64
.= <*fp/.1*> by A11,PARTFUN1:def 6;
assume i <> 0;
then
A26: i+1 > 0+1 by XREAL_1:8;
then
A27: i >= 1 by NAT_1:13;
then 1 in Seg len g2 by A23;
then
A28: 1 in dom g2 by FINSEQ_1:def 3;
1+1 <= len fp by A7,A26,NAT_1:13;
then 2 in Seg(len fp);
then
A29: 2 in dom fp by FINSEQ_1:def 3;
now
let i be Element of NAT;
assume that
A30: i in dom g2 and
A31: i <> 1;
A32: i+1<>2 by A31;
A33: 1 <= i + 1 by NAT_1:11;
A34: i in Seg(len g2) by A30,FINSEQ_1:def 3;
then
A35: i <= len g2 by FINSEQ_1:1;
len fp = 1 + len g2 by A22,A24,FINSEQ_1:22;
then i + 1 <= len fp by A35,XREAL_1:6;
then i + 1 in Seg(len fp) by A33;
then
A36: i+1 in dom fp by FINSEQ_1:def 3;
i+1<>0+1 by A34,FINSEQ_1:1;
then
A37: fp.(i+1)=0.L by A13,A36,A32;
1 <= i by A34,FINSEQ_1:1;
then g2.i = fp.(i+1) by A22,A24,A35,FINSEQ_1:65;
hence g2/.i = 0.L by A30,A37,PARTFUN1:def 6;
end;
then Sum g2 = g2/.1 by A28,POLYNOM2:3
.= g2.1 by A28,PARTFUN1:def 6
.= fp.2 by A27,A22,A23,A24,A21,FINSEQ_1:65
.= fp/.2 by A29,PARTFUN1:def 6;
hence p.i = Sum(g1) + fp/.2 by A8,A24,RLVECT_1:41
.= fp/.1 + fp/.2 by A25,RLVECT_1:44;
end;
A38: 2 - 1 >= 0;
A39: now
assume i <> 0;
then
A40: i + 1 > 0 + 1 by XREAL_1:8;
then i >= 1 by NAT_1:13;
then reconsider i1 = i-1 as Element of NAT by INT_1:5;
len fp >= 1+1 by A7,A40,NAT_1:13;
then 2 in Seg(len fp);
then
A41: 2 in dom fp by FINSEQ_1:def 3;
then
A42: fp.2 = rpoly(1,z).(2-'1) * qpoly(k,z).(i+1-'2) by A9
.= rpoly(1,z).1 * qpoly(k,z).(i+1-'2) by A38,XREAL_0:def 2
.= 1_L * qpoly(k,z).(i+1-'2) by Lm10
.= qpoly(k,z).(i+1-'2)
.= qpoly(k,z).i1 by A10,XREAL_0:def 2;
thus fp/.2 = fp.2 by A41,PARTFUN1:def 6
.= qpoly(k,z).(i-'1) by A42,XREAL_0:def 2;
end;
per cases by XXREAL_0:1;
suppose
A43: i < k;
per cases;
suppose
A44: i = 0;
A45: k-0-1 = k1;
A46: k1 + 1 = k;
fp = <*fp.1*> by A7,A44,FINSEQ_1:40
.= <*fp/.1*> by A11,PARTFUN1:def 6;
hence p.i9 = (-z) * qpoly(k,z).0 by A8,A12,A44,RLVECT_1:44
.= (-z) * power(L).(z,k1) by A45,A46,Def4
.= -(z* power(L).(z,k1)) by VECTSP_1:9
.= - power(L).(z,k) by A46,GROUP_1:def 7
.= u.i9 by A1,A44,Lm10;
end;
suppose
A47: i > 0;
then i + 1 > 0 + 1 by XREAL_1:6;
then i >= 1 by NAT_1:13;
then i - 1 >= 1 - 1 by XREAL_1:9;
then i -' 1 = i - 1 by XREAL_0:def 2;
then
A48: k- (i-'1) - 1 = k - i;
k - i > i - i by A43,XREAL_1:9;
then reconsider ki = k - i as Element of NAT by INT_1:3;
ki > i - i by A43,XREAL_1:9;
then ki + 1 > 0 + 1 by XREAL_1:6;
then ki >= 1 by NAT_1:13;
then reconsider ki1 = k-i-1 as Element of NAT by INT_1:5;
A49: k-1 < k-0 by XREAL_1:10;
i-1 < k-1 by A43,XREAL_1:9;
then
A50: i - 1 < k by A49,XXREAL_0:2;
A51: ki1 + 1 = ki;
thus p.i9 = ((-z)*power(L).(z,ki1))+qpoly(k,z).(i-'1) by A12,A39,A20
,A43,A47,Def4
.= ((-z) * power(L).(z,ki1)) + power(L).(z,ki) by A48,A50,Def4
.= (-(z * power(L).(z,ki1))) + power(L).(z,ki) by VECTSP_1:9
.= - power(L).(z,ki) + power(L).(z,ki) by A51,GROUP_1:def 7
.= 0.L by RLVECT_1:5
.= u.i9 by A43,A47,Lm11;
end;
end;
suppose
A52: i = k;
then i - 1 >= 1 - 1 by A1,XREAL_1:9;
then
A53: i -' 1 = i - 1 by XREAL_0:def 2;
A54: k - k1 - 1 = 0;
fp/.1 = (-z) * 0.L by A12,A52,Def4
.= 0.L;
hence p.i9 = qpoly(k,z).(k1) by A39,A20,A52,A53,ALGSTR_1:def 2
.= power(L).(z,0) by A3,A54,Def4
.= 1_L by GROUP_1:def 7
.= u.i9 by A1,A52,Lm10;
end;
suppose
A55: i > k;
then i + 1 > 0 + 1 by XREAL_1:6;
then i >= 1 by NAT_1:13;
then i - 1 >= 1 - 1 by XREAL_1:9;
then
A56: i -' 1 = i - 1 by XREAL_0:def 2;
i >= k+1 by A55,NAT_1:13;
then
A57: i - 1 >= k + 1 - 1 by XREAL_1:9;
fp/.1 = (-z) * 0.L by A12,A55,Def4
.= 0.L;
hence p.i9 = qpoly(k,z).(i-'1) by A39,A20,A55,ALGSTR_1:def 2
.= 0.L by A56,A57,Def4
.= u.i9 by A55,Lm11;
end;
end;
dom p = NAT by FUNCT_2:def 1
.= dom u by FUNCT_2:def 1;
hence thesis by A4,FUNCT_1:2;
end;
theorem Th33:
for L being Abelian add-associative right_zeroed
right_complementable well-unital associative distributive commutative non
empty doubleLoopStr for p being Polynomial of L for z being Element of L st z
is_a_root_of p ex s being Polynomial of L st p = rpoly(1,z) *' s
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital distributive associative commutative non empty doubleLoopStr;
let p be Polynomial of L;
let z be Element of L;
assume
A1: z is_a_root_of p;
set m = len p;
per cases;
suppose
A2: m = 0;
take 0_.(L);
p = 0_.(L) by A2,POLYNOM4:5;
hence thesis by POLYNOM3:34;
end;
suppose
A3: m > 0;
then m >= 0+1 by NAT_1:13;
then reconsider m1 = m - 1 as Element of NAT by INT_1:5;
defpred Pr[set,set] means ex u being Element of L st ex b being Element of
NAT st u = p.$1 & b = $1 & $2 = u * rpoly(b,z);
defpred Pq[set,set] means ($1 = 1 & $2 = p.1 * 1_.(L)) or ($1 <> 1 & ex u
being Element of L st ex b being Element of NAT st u = p.$1 & b = $1 & $2 = u*
qpoly(b,z));
A4: for k being Nat st k in Seg(m1) ex x being Element of the carrier of
Polynom-Ring(L) st Pq[k,x]
proof
let k be Nat;
A5: dom p = NAT by FUNCT_2:def 1;
assume k in Seg(m1);
then
A6: 1 <= k by FINSEQ_1:1;
per cases by A6,XXREAL_0:1;
suppose
A7: k = 1;
reconsider t = p.1 * 1_.(L) as Element of the carrier of Polynom-Ring(
L) by POLYNOM3:def 10;
take t;
thus thesis by A7;
end;
suppose
A8: k > 1;
reconsider t = p/.k * qpoly(k,z) as Element of the carrier of
Polynom-Ring(L) by POLYNOM3:def 10;
take t;
ex u being Element of L st ex b being Element of NAT st u = p.k &
b = k & t = u*qpoly(b,z)
proof
take p/.k;
reconsider b = k as Element of NAT by ORDINAL1:def 12;
take b;
b in NAT;
hence thesis by A5,PARTFUN1:def 6;
end;
hence thesis by A8;
end;
end;
consider hs being FinSequence of Polynom-Ring(L) such that
A9: dom hs = Seg m1 & for k being Nat st k in Seg(m1) holds Pq[k,hs.k
] from FINSEQ_1:sch 5(A4);
A10: now
let i be Element of NAT;
assume that
A11: 1 < i and
A12: i <= m-1;
i in Seg m1 by A11,A12;
then ex u being Element of L st ex b being Element of NAT st u = p.i &
b = i & hs.i = u*qpoly(b,z) by A9,A11;
hence hs.i = p.i * qpoly(i,z);
end;
A13: for k being Nat st k in Seg(m1) ex x being Element of the carrier of
Polynom-Ring(L) st Pr[k,x]
proof
let k be Nat;
assume k in Seg(m1);
then reconsider k1=k as Element of NAT;
reconsider t = p/.k * rpoly(k1,z) as Element of the carrier of
Polynom-Ring(L) by POLYNOM3:def 10;
take t;
take p/.k;
take k1;
A14: k1 in NAT;
dom p = NAT by FUNCT_2:def 1;
hence thesis by A14,PARTFUN1:def 6;
end;
consider h being FinSequence of Polynom-Ring(L) such that
A15: dom h = Seg m1 & for k being Nat st k in Seg(m1) holds Pr[k,h.k]
from FINSEQ_1:sch 5(A13);
set s = Sum hs, rs = Sum h;
reconsider s, rs as Polynomial of L by POLYNOM3:def 10;
A16: now
let k be Element of NAT;
assume that
A17: 1 <= k and
A18: k <= m1;
k in Seg(m1) by A17,A18;
then ex u being Element of L st ex b being Element of NAT st u = p.k &
b = k & h.k = u*rpoly(b,z) by A15;
hence h.k = p.k * rpoly(k,z);
end;
A19: m1 + 1 = m;
A20: now
let i be Element of NAT;
assume
A21: i >= len p;
set co = Coeff(h,i);
A22: dom h = Seg(len h) by FINSEQ_1:def 3
.= Seg(len co) by Def1
.= dom co by FINSEQ_1:def 3;
now
let j be Element of NAT;
assume
A23: j in dom co;
then
A24: ex ci being Polynomial of L st ci = h.j & co.j = ci.i by Def1;
A25: j <= m1 by A15,A22,A23,FINSEQ_1:1;
then
A26: j <> i by A19,A21,NAT_1:16,XXREAL_0:2;
1 <= j by A15,A22,A23,FINSEQ_1:1;
hence co.j = (p.j * rpoly(j,z)).i by A16,A24,A25
.= p.j * rpoly(j,z).i by POLYNOM5:def 4
.= p.j * 0.L by A3,A21,A26,Lm11
.= 0.L;
end;
then Sum co = 0.L by POLYNOM3:1;
hence rs.i = 0.L by Th13;
end;
A27: len h = m1 by A15,FINSEQ_1:def 3;
A28: now
let i be Element of NAT;
assume that
A29: i > 0 and
A30: i < len p;
i < m1 + 1 by A30;
then
A31: i <= m1 by NAT_1:13;
i + 1 > 0 + 1 by A29,XREAL_1:8;
then
A32: i >= 1 by NAT_1:13;
then
A33: h.i = p.i * rpoly(i,z) by A16,A31;
set co = Coeff(h,i);
A34: dom h = Seg len h by FINSEQ_1:def 3
.= Seg len co by Def1
.= dom co by FINSEQ_1:def 3;
i in Seg len h by A27,A32,A31;
then
A35: i in dom co by A34,FINSEQ_1:def 3;
then
A36: ex cc being Polynomial of L st cc = h.i & co.i = cc.i by Def1;
now
let i9 be Element of NAT;
assume that
A37: i9 in dom co and
A38: i9 <> i;
A39: ex ci being Polynomial of L st ci = h.i9 & co.i9 = ci.i by A37,Def1;
A40: i9 <= m-1 by A15,A34,A37,FINSEQ_1:1;
1 <= i9 by A15,A34,A37,FINSEQ_1:1;
then co.i9 = (p.i9 * rpoly(i9,z)).i by A16,A39,A40
.= p.i9 * rpoly(i9,z).i by POLYNOM5:def 4
.= p.i9 * 0.L by A29,A38,Lm11
.= 0.L;
hence co/.i9 = 0.L by A37,PARTFUN1:def 6;
end;
then Sum co = co/.i by A35,POLYNOM2:3
.= co.i by A35,PARTFUN1:def 6;
hence rs.i = (p.i * rpoly(i,z)).i by A36,A33,Th13;
end;
A41: now
let i9 be object;
assume i9 in dom p;
then reconsider i = i9 as Element of NAT;
per cases;
suppose
A42: i = 0;
set co = Coeff(h,0);
consider evp being FinSequence of L such that
A43: eval(p,z) = Sum evp and
A44: len evp = len p and
A45: for n being Element of NAT st n in dom evp holds evp.n = p.(n
-'1) * (power L).(z,n-'1) by POLYNOM4:def 2;
set cop = <*-(p.0)*> ^ co;
A46: len cop = len <*-(p.0)*> + len co by FINSEQ_1:22
.= 1 + len co by FINSEQ_1:39;
then
A47: len cop = 1 + len h by Def1
.= len evp by A27,A44;
then
A48: dom cop = Seg(len evp) by FINSEQ_1:def 3
.= dom evp by FINSEQ_1:def 3;
A49: dom h = Seg len h by FINSEQ_1:def 3
.= Seg len co by Def1
.= dom co by FINSEQ_1:def 3;
A50: now
let j be Element of NAT;
reconsider aj = -power(L).(z,j) as Element of L;
assume
A51: j in dom co;
then
A52: 1 <= j by A15,A49,FINSEQ_1:1;
A53: j <= m1 by A15,A49,A51,FINSEQ_1:1;
ex ci being Polynomial of L st ci = h.j & co.j = ci.i by A42,A51,Def1
;
hence co.j = (p.j * rpoly(j,z)).i by A16,A52,A53
.= p.j * rpoly(j,z).i by POLYNOM5:def 4
.= p.j * aj by A42,A52,Lm10
.= -(p.j * power(L).(z,j)) by VECTSP_1:8;
end;
now
let j be Element of NAT;
A54: dom <*-(p.0)*> = {1} by FINSEQ_1:2,38;
assume
A55: j in dom cop;
then
A56: evp/.j = evp.j by A48,PARTFUN1:def 6
.= p.(j-'1) * (power L).(z,j-'1) by A45,A48,A55;
A57: j in Seg len cop by A55,FINSEQ_1:def 3;
then
A58: 1 <= j by FINSEQ_1:1;
A59: j <= len cop by A57,FINSEQ_1:1;
per cases by A58,XXREAL_0:1;
suppose
A60: j = 1;
then j -' 1 = 1 - 1 by XREAL_0:def 2;
then
A61: evp/.j = p.0 * 1_L by A56,GROUP_1:def 7
.= p.0;
j in dom <*-(p.0)*> by A54,A60,TARSKI:def 1;
then cop.j = <*-(p.0)*>.j by FINSEQ_1:def 7
.= -(p.0) by A60;
hence cop/.j = - evp/.j by A55,A61,PARTFUN1:def 6;
end;
suppose
A62: j > 1;
then reconsider j1 = j - 1 as Element of NAT by INT_1:5;
1 < j1 + 1 by A62;
then
A63: 1 <= j1 by NAT_1:13;
j1 <= len cop - 1 by A59,XREAL_1:9;
then j1 in Seg(len co) by A46,A63;
then
A64: j1 in dom co by FINSEQ_1:def 3;
A65: j <= len cop by A57,FINSEQ_1:1;
j-1 >= 1-1 by A62,XREAL_1:9;
then
A66: j-'1 = j-1 by XREAL_0:def 2;
len<*-(p.0)*> < j by A62,FINSEQ_1:40;
then cop.j = co.(j - len <*-(p.0)*>) by A65,FINSEQ_1:24
.= co.(j - 1) by FINSEQ_1:40
.= -(p.j1 * power(L).(z,j1)) by A50,A64;
hence cop/.j = - evp/.j by A55,A56,A66,PARTFUN1:def 6;
end;
end;
then
A67: - Sum evp = Sum cop by A47,Th7
.= Sum <*-(p.0)*> + Sum co by RLVECT_1:41
.= -(p.0) + Sum co by RLVECT_1:44;
Sum evp = 0.L by A1,A43,POLYNOM5:def 7;
then 0.L = -(p.0) + Sum co by A67,RLVECT_1:12;
then p.0 = p.0 + (-(p.0) + Sum co) by ALGSTR_1:def 2
.= (p.0 + -(p.0)) + Sum co by RLVECT_1:def 3
.= 0.L + Sum co by RLVECT_1:5
.= Sum co by ALGSTR_1:def 2;
hence p.i9 = rs.i9 by A42,Th13;
end;
suppose
A68: i > 0;
per cases;
suppose
A69: i >= len p;
hence rs.i9 = 0.L by A20
.= p.i9 by A69,ALGSEQ_1:8;
end;
suppose
i < len p;
hence rs.i9 = (p.i * rpoly(i,z)).i by A28,A68
.= p.i * rpoly(i,z).i by POLYNOM5:def 4
.= p.i * 1_L by A68,Lm10
.= p.i9;
end;
end;
end;
now
assume m1 < 1;
then deg p = 0 by NAT_1:14;
then not p is with_roots by Th24;
hence contradiction by A1,POLYNOM5:def 8;
end;
then 1 in Seg m1;
then
A70: hs.1 = p.1*1_.(L) by A9;
A71: now
reconsider r1z = rpoly(1,z) as Element of Polynom-Ring(L) by
POLYNOM3:def 10;
let i9 be object;
assume i9 in dom rs;
A72: dom(r1z * hs) = dom h by A9,A15,POLYNOM1:def 1;
now
let k be Nat;
assume
A73: k in dom h;
then
A74: 1 <= k by A15,FINSEQ_1:1;
A75: k <= m1 by A15,A73,FINSEQ_1:1;
per cases by A74,XXREAL_0:1;
suppose
A76: k = 1;
then
A77: hs/.k = p.1*1_.(L) by A9,A70,A15,A73,PARTFUN1:def 6;
thus (r1z*hs).k = (r1z*hs)/.k by A72,A73,PARTFUN1:def 6
.= r1z * hs/.k by A9,A15,A73,POLYNOM1:def 1
.= rpoly(1,z) *' (p.1 * 1_.(L)) by A77,POLYNOM3:def 10
.= p.1 * (rpoly(1,z) *' 1_.(L)) by Th19
.= p.1 * rpoly(1,z) by POLYNOM3:35
.= h.k by A16,A75,A76;
end;
suppose
A78: k > 1;
reconsider k1 = k as Element of NAT by A73;
A79: hs/.k = hs.k by A9,A15,A73,PARTFUN1:def 6
.= p.k1 * qpoly(k1,z) by A10,A75,A78;
thus (r1z*hs).k = (r1z*hs)/.k by A72,A73,PARTFUN1:def 6
.= r1z * hs/.k by A9,A15,A73,POLYNOM1:def 1
.= rpoly(1,z) *' (p.k1*qpoly(k1,z)) by A79,POLYNOM3:def 10
.= p.k1 * (rpoly(1,z) *' qpoly(k1,z)) by Th19
.= p.k1 * rpoly(k1,z) by A78,Th32
.= h.k by A16,A74,A75;
end;
end;
then r1z * hs = h by A72,FINSEQ_1:13;
hence rs.i9 = (rpoly(1,z) *' s).i9 by Lm5;
end;
take s;
dom(rpoly(1,z) *' s) = NAT by FUNCT_2:def 1
.= dom rs by FUNCT_2:def 1;
then
A80: rpoly(1,z) *' s = rs by A71,FUNCT_1:2;
dom p = NAT by FUNCT_2:def 1
.= dom rs by FUNCT_2:def 1;
hence thesis by A80,A41,FUNCT_1:2;
end;
end;
begin :: Division of Polynomials
definition
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive almost_left_invertible non
empty doubleLoopStr;
let p,s be Polynomial of L such that
A1: s <> 0_.(L);
func p div s -> Polynomial of L means
:Def5:
ex t being Polynomial of L st p = it *' s + t & deg t < deg s;
existence
proof
set M = { p - u *' s where u is Polynomial of L : 1 = 1 };
defpred P[Nat] means ex t being Polynomial of L st t in M & len t = $1;
A2: len s <> 0 by A1,POLYNOM4:5;
then len s + 1 > 0 + 1 by XREAL_1:6;
then len s >= 1 by NAT_1:13;
then
A3: len s - 1 >= 1 - 1 by XREAL_1:9;
s.(len(s)-1) <> 0.L by A2,Lm6;
then
A4: s.(len s-'1) <> 0.L by A3,XREAL_0:def 2;
p = p + 0_.(L) by POLYNOM3:28
.= p + -0_.(L) by Th9
.= p - ((0_.(L)) *' s) by POLYNOM4:2;
then p in M;
then ex t being Polynomial of L st t in M & len t = len p;
then
A5: ex k being Nat st P[k];
consider k being Nat such that
A6: P[k] & for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A5);
consider f being Polynomial of L such that
A7: f in M and
A8: len f = k by A6;
consider g being Polynomial of L such that
A9: f = p - g *' s and
1 = 1 by A7;
take g;
A10: g *' s + (p - g *' s) = (g *' s + -(g *' s)) + p by POLYNOM3:26
.= (g *' s - g *' s ) + p
.= 0_.(L) + p by POLYNOM3:29
.= p by POLYNOM3:28;
per cases;
suppose
A11: f = 0_.(L);
reconsider s9 = deg s as Nat by A1,Lm8;
A12: s9 >= 0;
deg(f) = -1 by A11,Th20;
hence thesis by A9,A10,A12;
end;
suppose
f <> 0_.(L);
then len f <> 0 by POLYNOM4:5;
then len f + 1 > 0 + 1 by XREAL_1:6;
then len f >= 1 by NAT_1:13;
then
A13: len f - 1 >= 1 - 1 by XREAL_1:9;
then reconsider k9 = len f - 1 as Element of NAT by INT_1:3;
A14: k = k9 + 1 by A8;
dom f = NAT by FUNCT_2:def 1;
then
A15: k9 in dom f;
now
assume deg f >= deg s;
then reconsider degn = deg(f) - deg(s) as Element of NAT by INT_1:5;
set al = f.(len f -' 1) * (s.(len s -' 1))";
set g1 = 0_.(L)+*({degn} --> al);
now
let u be object;
assume u in {degn};
then u = degn by TARSKI:def 1;
hence u in NAT;
end;
then
A17: {degn} c= NAT by TARSKI:def 3;
A18: degn in {degn} by TARSKI:def 1;
A19: now
let x9 be object;
assume x9 in NAT;
then reconsider x = x9 as Element of NAT;
per cases;
suppose
A20: x in dom({degn} --> al);
then x = degn by TARSKI:def 1;
then g1.x = ({degn} --> al).degn by A20,FUNCT_4:13
.= al by A18,FUNCOP_1:7;
hence g1.x9 in the carrier of L;
end;
suppose
not x in dom({degn} --> al);
then g1.x = (0_.(L)).x by FUNCT_4:11
.= 0.L;
hence g1.x9 in the carrier of L;
end;
end;
dom(0_.(L))\/dom({degn}-->al) = NAT by A17,XBOOLE_1:12;
then dom g1 = NAT by FUNCT_4:def 1;
then reconsider g1 as sequence of L by A19,FUNCT_2:3;
A21: for j being Nat st j <> degn holds g1.j = 0.L
proof
let j be Nat;
A22: j in NAT by ORDINAL1:def 12;
assume j <> degn;
then not j in dom({degn} --> al) by TARSKI:def 1;
hence g1.j = (0_.(L)).j by FUNCT_4:11
.= 0.L by A22,FUNCOP_1:7;
end;
A23: ex l being Nat st for i being Nat st i>=l holds g1.i = 0.L
proof
take l = degn + 1;
now
let i be Nat;
assume i >= l;
then i <> degn by NAT_1:13;
hence g1.i = 0.L by A21;
end;
hence thesis;
end;
A24: degn in {degn} by TARSKI:def 1;
then degn in dom({degn} --> al);
then
A25: g1.degn = ({degn} --> al).degn by FUNCT_4:13
.= al by A24,FUNCOP_1:7;
reconsider g1 as Polynomial of L by A23,ALGSEQ_1:def 1;
set s1 = p - (g + g1) *' s;
now
A26: 1 <= degn + 1 by NAT_1:11;
let i be Nat;
A27: dom f = NAT by FUNCT_2:def 1;
assume
A28: i >= k9;
then
A29: i + 1 >= k by A14,XREAL_1:6;
degn + 1 = k - deg(s) by A8;
then
A30: degn + 1 <= k by A3,XREAL_1:43;
then
A31: i + 1 - (degn + 1) is Element of NAT by A29,INT_1:5,XXREAL_0:2;
A32: i in NAT by ORDINAL1:def 12;
then consider sf being FinSequence of L such that
A33: len sf = i+1 and
A34: (g1 *' s).i = Sum sf and
A35: for m being Element of NAT st m in dom sf holds sf.m = g1.(
m-'1) * s.(i+1-'m) by POLYNOM3:def 9;
A36: dom sf = Seg(len sf) by FINSEQ_1:def 3;
i + 1 >= degn + 1 by A30,A29,XXREAL_0:2;
then
A37: degn + 1 in dom sf by A33,A36,A26;
A38: now
let m be Nat;
assume that
A39: m in dom sf and
A40: m <> degn + 1;
1 <= m by A36,A39,FINSEQ_1:1;
then m - 1 >= 1 - 1 by XREAL_1:9;
then m-'1 = m-1 by XREAL_0:def 2;
then (m-'1) <> degn by A40;
hence g1.(m-'1) = 0.L by A21;
end;
now
let i9 be Element of NAT;
assume that
A41: i9 in dom sf and
A42: i9 <> degn + 1;
sf.i9 = g1.(i9-'1) * s.(i+1-'i9) by A35,A41
.= 0.L * s.(i+1-'i9) by A38,A41,A42
.= 0.L;
hence sf/.i9 = 0.L by A41,PARTFUN1:def 6;
end;
then
A43: Sum sf = sf/.(degn + 1) by A37,POLYNOM2:3
.= sf.(degn+1) by A37,PARTFUN1:def 6
.= g1.(degn+1-'1) * s.(i+1-'(degn+1)) by A35,A37
.= al * s.(i+1-'(degn+1)) by A25,NAT_D:34;
A44: s1 - f = (p + -(g + g1) *' s) + (-p + -(-(g *' s))) by A9,Th11
.= ((p + -(g + g1) *' s) + -p) + -(-(g *' s)) by POLYNOM3:26
.= ((p - p) + -(g + g1) *' s) + -(-(g *' s)) by POLYNOM3:26
.= (0_.(L) + -(g+g1) *' s) + -(-(g*'s)) by POLYNOM3:29
.= (-(g + g1) *' s) + -(-(g *' s)) by POLYNOM3:28
.= ((-(g + g1)) *' s) + -(-(g *' s)) by Th12
.= ((-g + -g1) *' s) + -(-(g *' s)) by Th11
.= (((-g) + (-g1)) *' s) + g *' s by Lm3
.= ((-g) *' s + (-g1) *' s) + g *' s by POLYNOM3:32
.= (-g1) *' s + ((-g) *' s + g *' s) by POLYNOM3:26
.= (-g1) *' s + (g *' s - g *' s) by Th12
.= (-g1) *' s + 0_.(L) by POLYNOM3:29
.= (-g1) *' s by POLYNOM3:28
.= -(g1 *' s) by Th12;
A45: dom(g1 *' s) = NAT by FUNCT_2:def 1;
s1 = s1 + 0_.(L) by POLYNOM3:28
.= s1 + (f - f) by POLYNOM3:29
.= (s1 + -f) + f by POLYNOM3:26
.= f - g1 *' s by A44;
then
A46: s1.i = f.i + (-(g1 *' s)).i by NORMSP_1:def 2
.= f.i + -(g1 *' s).i by BHSP_1:44
.= f/.i + -(g1 *' s).i by A32,A27,PARTFUN1:def 6
.= f/.i + -(g1 *' s)/.i by A32,A45,PARTFUN1:def 6;
A47: i in NAT by ORDINAL1:def 12;
per cases by A28,XXREAL_0:1;
suppose
A48: i > k9;
then reconsider e = i - k9 as Element of NAT by INT_1:5;
i - k9 > k9 - k9 by A48,XREAL_1:9;
then e + 1 > 0 + 1 by XREAL_1:6;
then e >= 1 by NAT_1:13;
then i - k9 - 1 >= 1 - 1 by XREAL_1:9;
then
A49: (i - k9 - 1) + len(s) >= 0 + len(s) by XREAL_1:6;
i + 1 > k9 + 1 by A48,XREAL_1:6;
then i >= len f by NAT_1:13;
then f.i = 0.L by ALGSEQ_1:8;
then
A50: f/.i = 0.L by A27,A47,PARTFUN1:def 6;
i+1-'(degn+1) = i - k9 + (len(s)-1) by A31,XREAL_0:def 2;
then s.(i+1-'(degn+1)) = 0.L by A49,ALGSEQ_1:8;
then Sum sf = 0.L by A43;
hence s1.i = 0.L + -(0.L) by A45,A46,A34,A47,A50,PARTFUN1:def 6
.= 0.L + 0.L by RLVECT_1:12
.= 0.L by RLVECT_1:def 4;
end;
suppose
A51: i = k9;
(i+1)-'(degn+1) = i + 1 - (degn + 1) by A31,XREAL_0:def 2
.= len s -' 1 by A3,A51,XREAL_0:def 2;
then Sum sf = f.(len f-'1) * ((s.(len s-'1))" * s.(len s-'1)) by
A43,GROUP_1:def 3
.= f.(len f-'1) * 1_L by A4,VECTSP_1:def 10
.= f.(len f-'1)
.= f.(len f-1) by A13,XREAL_0:def 2
.= f/.(len f-1) by A15,PARTFUN1:def 6;
hence s1.i = f/.(len f-1)+-(f/.(len f-1)) by A45,A46,A34,A51,
PARTFUN1:def 6
.= 0.L by RLVECT_1:5;
end;
end;
then k9 is_at_least_length_of s1 by ALGSEQ_1:def 2;
then len(s1) <= k9 by ALGSEQ_1:def 3;
then
A52: len(s1) < k by A14,NAT_1:13;
s1 in M;
hence contradiction by A6,A52;
end;
hence thesis by A9,A10;
end;
end;
uniqueness
proof
let f1,f2 be Polynomial of L;
given t1 being Polynomial of L such that
A53: p = f1*'s+t1 and
A54: deg t1 < deg s;
given t2 being Polynomial of L such that
A55: p = f2*'s+t2 and
A56: deg t2 < deg s;
A57: (f2 - f1) *' s = f2 *' s + (-f1) *' s by POLYNOM3:32
.= f2 *' s - f1*' s by Th12;
f2 *' s = f2 *' s + 0_.(L) by POLYNOM3:28
.= f2 *' s + (t2 - t2) by POLYNOM3:29
.= (f1 *' s + t1) + -t2 by A53,A55,POLYNOM3:26;
then
A58: f2 *' s - f1 *' s = (f1 *' s + (t1 + -t2)) + -(f1 *' s) by POLYNOM3:26
.= (t1 + -t2) + (f1 *' s -(f1 *' s)) by POLYNOM3:26
.= (t1 + -t2) + 0_.(L) by POLYNOM3:29
.= t1 - t2 by POLYNOM3:28;
now
assume
A59: f1 <> f2;
A60: now
assume f2 - f1 = 0_.(L);
then f1 = (f2 + -f1) + f1 by POLYNOM3:28
.= f2 + (f1 - f1) by POLYNOM3:26
.= f2 + 0_.(L) by POLYNOM3:29;
hence contradiction by A59,POLYNOM3:28;
end;
then reconsider d = deg(f2-f1), degs = deg(s) as Nat by A1,Lm8;
deg(t1-t2) <= max(deg(t1),deg(-t2)) by Th22;
then
A61: deg(t1-t2) <= max(deg(t1),deg(t2)) by POLYNOM4:8;
A62: deg(t1-t2) < degs
proof
per cases by XXREAL_0:16;
suppose
max(deg(t1),deg(t2))=deg(t1);
hence thesis by A54,A61,XXREAL_0:2;
end;
suppose
max(deg(t1),deg(t2))=deg(t2);
hence thesis by A56,A61,XXREAL_0:2;
end;
end;
deg(t1-t2) = d + degs by A1,A58,A57,A60,Th23;
hence contradiction by A62,NAT_1:11;
end;
hence thesis;
end;
end;
definition
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive almost_left_invertible non
empty doubleLoopStr;
let p,s be Polynomial of L;
func p mod s -> Polynomial of L equals
p - (p div s) *' s;
coherence;
end;
definition
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive almost_left_invertible non
empty doubleLoopStr;
let p,s be Polynomial of L;
pred s divides p means
p mod s = 0_.(L);
end;
theorem Th34:
for L being Abelian add-associative right_zeroed
right_complementable well-unital associative commutative distributive
almost_left_invertible non empty doubleLoopStr for p,s being Polynomial of L
st s <> 0_.(L) holds s divides p iff ex t being Polynomial of L st t *' s = p
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive almost_left_invertible non
empty doubleLoopStr;
let p,s be Polynomial of L;
assume
A1: s <> 0_.(L);
A2: now
deg(s) - 0 > 0 - 1 by A1,Lm8;
then
A3: deg 0_.(L) < deg s by Th20;
given t being Polynomial of L such that
A4: t *' s = p;
p = t *' s + 0_.(L) by A4,POLYNOM3:28;
then p div s = t by A3,Def5;
then p mod s = 0_.(L) by A4,POLYNOM3:29;
hence s divides p;
end;
now
assume
A5: s divides p;
consider t being Polynomial of L such that
A6: p = (p div s) *' s + t and
deg t < deg s by A1,Def5;
p mod s = t + ((p div s) *' s - ((p div s) *' s)) by A6,POLYNOM3:26
.= t + 0_.(L) by POLYNOM3:29
.= t by POLYNOM3:28;
then t = 0_.(L) by A5;
then p = (p div s) *' s by A6,POLYNOM3:28;
hence ex t being Polynomial of L st t *' s = p;
end;
hence thesis by A2;
end;
theorem
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive almost_left_invertible non
degenerated non empty doubleLoopStr for p being Polynomial of L for z being
Element of L st z is_a_root_of p holds rpoly(1,z) divides p
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive almost_left_invertible non
degenerated non empty doubleLoopStr, p be Polynomial of L;
let z be Element of L;
rpoly(1,z).1 = 1_L by Lm10;
then
A1: rpoly(1,z) <> 0_.(L);
assume z is_a_root_of p;
then ex s being Polynomial of L st p = rpoly(1,z) *' s by Th33;
hence thesis by A1,Th34;
end;
theorem
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive almost_left_invertible non
degenerated non empty doubleLoopStr for p being Polynomial of L for z being
Element of L st p <> 0_.(L) & z is_a_root_of p holds deg(p div rpoly(1,z)) =
deg(p) - 1
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive almost_left_invertible non
degenerated non empty doubleLoopStr, p be Polynomial of L;
let z be Element of L;
assume that
A1: p <> 0_.(L) and
A2: z is_a_root_of p;
consider s being Polynomial of L such that
A3: p = rpoly(1,z) *' s by A2,Th33;
A4: rpoly(1,z) <> 0_.(L) by A1,A3,POLYNOM4:2;
A5: ex t being Polynomial of L st p = s *' rpoly(1,z) + t & deg t < deg
rpoly(1,z)
proof
take t = 0_.(L);
thus s *' rpoly(1,z) + t = p by A3,POLYNOM3:28;
deg t = -1 by Th20;
hence thesis by Th27;
end;
s <> 0_.(L) by A1,A3,POLYNOM3:34;
then deg p = deg(rpoly(1,z)) + deg(s) by A3,A4,Th23
.= 1 + deg(s) by Th27;
hence thesis by A4,A5,Def5;
end;
begin :: Schur's Theorem
definition
let f be Polynomial of F_Complex;
attr f is Hurwitz means
for z being Element of F_Complex st z is_a_root_of f holds Re(z) < 0;
end;
theorem
0_.(F_Complex) is non Hurwitz
proof
eval(0_.(F_Complex),1_F_Complex) = 0.F_Complex by POLYNOM4:17;
then 1_F_Complex is_a_root_of 0_.(F_Complex) by POLYNOM5:def 7;
hence thesis by COMPLEX1:6,COMPLFLD:8;
end;
theorem
for x being Element of F_Complex st x <> 0.F_Complex holds x * 1_.(
F_Complex) is Hurwitz
proof
let x be Element of F_Complex;
set p = x * 1_.(F_Complex);
assume
A1: x <> 0.F_Complex;
now
let z be Element of F_Complex;
assume z is_a_root_of p;
then
A2: eval(p,z) = 0.F_Complex by POLYNOM5:def 7;
eval(p,z) = x * eval(1_.(F_Complex),z) by POLYNOM5:30
.= x * 1_F_Complex by POLYNOM4:18;
hence Re(z) < 0 by A1,A2;
end;
hence thesis;
end;
theorem Th39:
for x,z being Element of F_Complex st x <> 0.F_Complex holds x *
rpoly(1,z) is Hurwitz iff Re(z) < 0
proof
let x,z be Element of F_Complex;
set p = x * rpoly(1,z);
assume
A1: x <> 0.F_Complex;
A2: now
assume
A3: Re(z) < 0;
now
let y be Element of F_Complex;
assume y is_a_root_of p;
then 0.F_Complex = eval(p,y) by POLYNOM5:def 7
.= x * eval(rpoly(1,z),y) by POLYNOM5:30
.= x * (y - z) by Th29;
then y - z = 0.F_Complex by A1,VECTSP_1:12;
hence Re(y) < 0 by A3,RLVECT_1:21;
end;
hence p is Hurwitz;
end;
now
eval(p,z) = x * eval(rpoly(1,z),z) by POLYNOM5:30
.= x * (z - z) by Th29
.= x * 0.F_Complex by RLVECT_1:15
.= 0.F_Complex;
then
A4: z is_a_root_of p by POLYNOM5:def 7;
assume x * rpoly(1,z) is Hurwitz;
hence Re(z) < 0 by A4;
end;
hence thesis by A2;
end;
theorem Th40:
for f being Polynomial of F_Complex for z being Element of
F_Complex st z <> 0.F_Complex holds f is Hurwitz iff z * f is Hurwitz
proof
let f be Polynomial of F_Complex;
let z be Element of F_Complex;
assume
A1: z <> 0.F_Complex;
A2: now
assume
A3: f is Hurwitz;
now
let x be Element of F_Complex;
assume x is_a_root_of (z*f);
then 0.F_Complex = eval(z*f,x) by POLYNOM5:def 7
.= z * eval(f,x) by POLYNOM5:30;
then eval(f,x) = 0.F_Complex by A1,VECTSP_1:12;
then x is_a_root_of f by POLYNOM5:def 7;
hence Re(x) < 0 by A3;
end;
hence z*f is Hurwitz;
end;
now
assume
A4: z*f is Hurwitz;
now
let x be Element of F_Complex;
assume
A5: x is_a_root_of f;
eval(z*f,x) = z * eval(f,x) by POLYNOM5:30
.= z * 0.F_Complex by A5,POLYNOM5:def 7
.= 0.F_Complex;
then x is_a_root_of (z*f) by POLYNOM5:def 7;
hence Re(x) < 0 by A4;
end;
hence f is Hurwitz;
end;
hence thesis by A2;
end;
Lm12: for f,g,h being Polynomial of F_Complex st f = g *' h for x being
Element of F_Complex holds (x is_a_root_of g or x is_a_root_of h) implies x
is_a_root_of f
proof
let f,g,h be Polynomial of F_Complex;
assume
A1: f = g *' h;
let x be Element of F_Complex;
A2: eval(f,x) = eval(g,x) * eval(h,x) by A1,POLYNOM4:24;
assume
A3: x is_a_root_of g or x is_a_root_of h;
per cases by A3;
suppose
x is_a_root_of g;
then eval(g,x) = 0.F_Complex by POLYNOM5:def 7;
then eval(f,x) = 0.F_Complex by A2;
hence thesis by POLYNOM5:def 7;
end;
suppose
x is_a_root_of h;
then eval(h,x) = 0.F_Complex by POLYNOM5:def 7;
then eval(f,x) = 0.F_Complex by A2;
hence thesis by POLYNOM5:def 7;
end;
end;
theorem Th41:
for f,g being Polynomial of F_Complex holds f *' g is Hurwitz
iff f is Hurwitz & g is Hurwitz
proof
let f,g be Polynomial of F_Complex;
A1: now
assume that
A2: f is Hurwitz and
A3: g is Hurwitz;
now
let z be Element of F_Complex;
assume z is_a_root_of f*'g;
then
A4: 0.F_Complex = eval(f*'g,z) by POLYNOM5:def 7
.= eval(f,z) * eval(g,z) by POLYNOM4:24;
per cases by A4,VECTSP_1:12;
suppose
eval(f,z)=0.F_Complex;
then z is_a_root_of f by POLYNOM5:def 7;
hence Re(z) < 0 by A2;
end;
suppose
eval(g,z)=0.F_Complex;
then z is_a_root_of g by POLYNOM5:def 7;
hence Re(z) < 0 by A3;
end;
end;
hence f*'g is Hurwitz;
end;
now
assume
A5: f*'g is Hurwitz;
now
let z be Element of F_Complex;
assume z is_a_root_of f;
then z is_a_root_of (f*'g) by Lm12;
hence Re(z) < 0 by A5;
end;
hence f is Hurwitz;
now
let z be Element of F_Complex;
assume z is_a_root_of g;
then z is_a_root_of (f*'g) by Lm12;
hence Re(z) < 0 by A5;
end;
hence g is Hurwitz;
end;
hence thesis by A1;
end;
definition
let f be Polynomial of F_Complex;
func f*' -> Polynomial of F_Complex means
:Def9:
for i being Element of NAT
holds it.i = power(F_Complex).(-1_F_Complex,i) * (f.i)*';
existence
proof
defpred P[object,object] means
ex n being Element of NAT st n = $1 & $2 = power(
F_Complex).(-1_F_Complex,n) * (f.n)*';
A1: for x being object st x in NAT
ex y being object st y in the carrier of F_Complex & P[x,y]
proof
let u be object;
assume u in NAT;
then reconsider u9 = u as Element of NAT;
take power(F_Complex).(-1_F_Complex,u9) * (f.u9)*';
thus thesis;
end;
consider g being sequence of the carrier of F_Complex such that
A2: for x being object st x in NAT holds P[x,g.x] from FUNCT_2:sch 1(A1);
reconsider g as sequence of F_Complex;
ex n being Nat st for i being Nat st i >= n holds g.i = 0.F_Complex
proof
take n = len f;
now
let i be Nat;
reconsider i1=i as Element of NAT by ORDINAL1:def 12;
assume
A3: i >= n;
ex m being Element of NAT st m = i1 & g.i1 = power( F_Complex).(
-1_F_Complex,m) * (f.m)*' by A2;
hence
g.i = power(F_Complex).(-1_F_Complex,i1) * (0.F_Complex)*' by A3,
ALGSEQ_1:8
.= 0.F_Complex by COMPLFLD:47;
end;
hence thesis;
end;
then reconsider p = g as AlgSequence of F_Complex by ALGSEQ_1:def 1;
take p;
now
let i be Element of NAT;
ex n being Element of NAT st n = i & p.i = power( F_Complex).(-
1_F_Complex,n) * (f.n)*' by A2;
hence p.i = power(F_Complex).(-1_F_Complex,i) * (f.i)*';
end;
hence thesis;
end;
uniqueness
proof
let z1,z2 be AlgSequence of F_Complex;
assume
A4: for i being Element of NAT holds z1.i = power(F_Complex).(-
1_F_Complex,i) * (f.i)*';
assume
A5: for i being Element of NAT holds z2.i = power(F_Complex).(-
1_F_Complex,i) * (f.i)*';
A6: now
let x be object;
assume x in dom z1;
then reconsider x9 = x as Element of NAT;
thus z1.x = power(F_Complex).(-1_F_Complex,x9) * (f.x9)*' by A4
.= z2.x by A5;
end;
dom z1 = NAT by FUNCT_2:def 1
.= dom z2 by FUNCT_2:def 1;
hence z1 = z2 by A6,FUNCT_1:2;
end;
involutiveness
proof let g,f be Polynomial of F_Complex such that
A7: for i being Element of NAT
holds g.i = power(F_Complex).(-1_F_Complex,i) * (f.i)*';
let i be Element of NAT;
thus f.i = 1_F_Complex * f.i
.= power(F_Complex).(-1_F_Complex,2*i) * f.i by Th4
.= power(F_Complex).(-1_F_Complex,i+i) * f.i
.= (power(F_Complex).(-1_F_Complex,i) *
power(F_Complex).(-1_F_Complex,i)) * f.i by Th3
.= (power(F_Complex).(-1_F_Complex,i) *
power(F_Complex).((-1_F_Complex)*',i)) * f.i by Lm2,COMPLEX1:38
.= (power(F_Complex).(-1_F_Complex,i) *
(power(F_Complex).(-1_F_Complex,i))*') * f.i by Th5
.= power(F_Complex).(-1_F_Complex,i) *
(((power(F_Complex).(-1_F_Complex,i))*') * (f.i)*'*')
.= power(F_Complex).(-1_F_Complex,i) *
(power(F_Complex).(-1_F_Complex,i) * (f.i)*')*' by COMPLFLD:54
.= power(F_Complex).(-1_F_Complex,i) * (g.i)*' by A7;
end;
end;
theorem Th42:
for f being Polynomial of F_Complex holds deg(f*') = deg(f)
proof
let f be Polynomial of F_Complex;
A1: for k being Nat holds f.k = 0.F_Complex iff (f*').k = 0.F_Complex
proof
let k be Nat;
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
hereby
assume f.k = 0.F_Complex;
hence (f*').k = power(F_Complex).(-1_F_Complex,k1) * 0.F_Complex by Def9,
COMPLFLD:47
.= 0.F_Complex;
end;
assume (f*').k = 0.F_Complex;
then
A2: 0.F_Complex = power(F_Complex).(-1_F_Complex,k1) * ((f.k)*') by Def9;
power(F_Complex).(-1_F_Complex,k1) <> 0.F_Complex by Th2;
then (f.k)*' = 0.F_Complex by A2,VECTSP_1:12;
hence thesis by COMPLEX1:28,COMPLFLD:7;
end;
A3: now
assume
A4: len f > len(f*');
then len f + 1 > 0 + 1 by XREAL_1:6;
then len f >= 1 by NAT_1:13;
then reconsider l = len(f)-1 as Element of NAT by INT_1:5;
l + 1 > len(f*') by A4;
then l >= len(f*') by NAT_1:13;
then
A5: (f*').l = 0.F_Complex by ALGSEQ_1:8;
len f = l + 1;
then f.l <> 0.F_Complex by ALGSEQ_1:10;
hence contradiction by A1,A5;
end;
now
let i be Nat;
assume i >= len f;
then f.i = 0.F_Complex by ALGSEQ_1:8;
hence (f*').i = 0.F_Complex by A1;
end;
then len f is_at_least_length_of (f*') by ALGSEQ_1:def 2;
then len f >= len (f*') by ALGSEQ_1:def 3;
hence thesis by A3,XXREAL_0:1;
end;
::$CT
theorem Th43:
for f being Polynomial of F_Complex for z being Element of
F_Complex holds (z * f)*' = (z*') * (f*')
proof
let f be Polynomial of F_Complex;
let x be Element of F_Complex;
set g1 = x * f, g2 = (x*') * (f*');
A1: now
let k9 be object;
assume k9 in dom(g1*');
then reconsider k = k9 as Element of NAT;
g1.k = x * f.k by POLYNOM5:def 4;
then (g1*').k = power(F_Complex).(-1_F_Complex,k) * (x * f.k)*' by Def9
.= power(F_Complex).(-1_F_Complex,k) * ((x*') * ((f.k)*')) by COMPLFLD:54
.= (x*') * (power(F_Complex).(-1_F_Complex,k) * ((f.k)*'))
.= (x*') * (f*').k by Def9;
hence (g1*').k9 = g2.k9 by POLYNOM5:def 4;
end;
dom(g1*') = NAT by FUNCT_2:def 1
.= dom g2 by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th44:
for f being Polynomial of F_Complex holds (-f)*' = -(f*')
proof
let f be Polynomial of F_Complex;
set h1 = -f;
A1: now
let k9 be object;
assume k9 in dom(h1*');
then reconsider k = k9 as Element of NAT;
h1.k = -f.k by BHSP_1:44;
then (h1*').k = power(F_Complex).(-1_F_Complex,k) * (-f.k)*' by Def9
.= power(F_Complex).(-1_F_Complex,k) * (-((f.k)*')) by COMPLFLD:52
.= -(power(F_Complex).(-1_F_Complex,k) * ((f.k)*'))
.= -((f*').k) by Def9;
hence (h1*').k9 = (-(f*')).k9 by BHSP_1:44;
end;
dom(h1*') = NAT by FUNCT_2:def 1
.= dom(-(f*')) by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th45:
for f,g being Polynomial of F_Complex holds (f + g)*' = (f*') + (g*')
proof
let f,g be Polynomial of F_Complex;
set h1 = f+g;
A1: now
let k9 be object;
assume k9 in dom(h1*');
then reconsider k = k9 as Element of NAT;
h1.k = f.k + g.k by NORMSP_1:def 2;
then (h1*').k = power(F_Complex).(-1_F_Complex,k) * (f.k + g.k)*' by Def9
.= power(F_Complex).(-1_F_Complex,k) * ((f.k)*' + (g.k)*') by COMPLFLD:51
.= (power(F_Complex).(-1_F_Complex,k) * (f.k)*') + (power(F_Complex).(
-1_F_Complex,k) * (g.k)*')
.= (f*').k + (power(F_Complex).(-1_F_Complex,k) * (g.k)*') by Def9
.= (f*').k + (g*').k by Def9;
hence (h1*').k9 = ((f*') + (g*')).k9 by NORMSP_1:def 2;
end;
dom(h1*') = NAT by FUNCT_2:def 1
.= dom((f*') + (g*')) by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th46:
for f,g being Polynomial of F_Complex holds (f *' g)*' = (f*') *' (g*')
proof
let f,g be Polynomial of F_Complex;
set h1 = f*'g;
A1: now
let k9 be object;
assume k9 in dom(h1*');
then reconsider k = k9 as Element of NAT;
consider s being FinSequence of F_Complex such that
A2: len s = k+1 and
A3: h1.k = Sum s and
A4: for j be Element of NAT st j in dom s holds s.j = f.(j-'1) * g.(k+
1 -'j) by POLYNOM3:def 9;
defpred P[set,set] means $2 = (s/.$1)*';
consider t being FinSequence of F_Complex such that
A5: len t = k+1 and
A6: ((f*') *' (g*')).k = Sum t and
A7: for j be Element of NAT st j in dom t holds t.j = (f*').(j-'1) * (
g *').(k+1-'j) by POLYNOM3:def 9;
A8: for j being Nat st j in Seg(len s) ex x being Element of F_Complex st
P[j,x];
consider u being FinSequence of F_Complex such that
A9: dom u = Seg(len s) & for j being Nat st j in Seg(len s) holds P[j
,u.j] from FINSEQ_1:sch 5(A8);
A10: now
let j be Element of NAT;
assume
A11: j in dom u;
hence u/.j = u.j by PARTFUN1:def 6
.= (s/.j)*' by A9,A11;
end;
A12: dom u = Seg(len t) by A2,A5,A9
.= dom t by FINSEQ_1:def 3;
A13: dom s = Seg(len t) by A2,A5,FINSEQ_1:def 3
.= dom t by FINSEQ_1:def 3;
A14: now
let j be Element of NAT;
assume
A15: j in dom t;
then s.j = s/.j by A13,PARTFUN1:def 6;
then
A16: (s/.j)*' = (f.(j-'1) * g.(k+1-'j))*' by A4,A13,A15;
A17: j in Seg(len t) by A15,FINSEQ_1:def 3;
then j <= k+1 by A5,FINSEQ_1:1;
then
A18: k + 1 - j >= j - j by XREAL_1:9;
1 <= j by A17,FINSEQ_1:1;
then j - 1 >= 1 - 1 by XREAL_1:9;
then
A19: (j-'1) + (k+1-'j) = j-1 + (k+1-'j) by XREAL_0:def 2
.= j - 1 + (k + 1 - j) by A18,XREAL_0:def 2
.= k;
thus t.j = (f*').(j-'1) * (g*').(k+1-'j) by A7,A15
.= (power(F_Complex).(-1_F_Complex,j-'1) * (f.(j-'1))*') * (g*').(k+
1-'j) by Def9
.= (power(F_Complex).(-1_F_Complex,j-'1) * (f.(j-'1))*') * (power(
F_Complex).(-1_F_Complex,k+1-'j) * (g.(k+1-'j))*') by Def9
.= (power(F_Complex).(-1_F_Complex,j-'1) * power(F_Complex).(-
1_F_Complex,k+1-'j)) * (((f.(j-'1))*') * (g.(k+1-'j))*')
.= power(F_Complex).(-1_F_Complex,k) * (((f.(j-'1))*') * (g.(k+1-'j)
)*') by A19,Th3
.= power(F_Complex).(-1_F_Complex,k) * (s/.j)*' by A16,COMPLFLD:54;
end;
A20: power(F_Complex).(-1_F_Complex,k) * u = t
proof
set b = power(F_Complex).(-1_F_Complex,k);
set a = b * u;
A21: dom a = dom u by POLYNOM1:def 1;
now
let j be Nat;
assume
A22: j in dom t;
hence a.j = a/.j by A12,A21,PARTFUN1:def 6
.= b * u/.j by A12,A22,POLYNOM1:def 1
.= b * (s/.j)*' by A10,A12,A22
.= t.j by A14,A22;
end;
hence thesis by A12,A21,FINSEQ_1:13;
end;
len u = len s by A9,FINSEQ_1:def 3;
then Sum u = (Sum s)*' by A10,Th6;
then (h1*').k = power(F_Complex).(-1_F_Complex,k) * (Sum u) by A3,Def9
.= ((f*') *' (g*')).k by A6,A20,Th8;
hence (h1*').k9 = ((f*') *' (g*')).k9;
end;
dom(h1*') = NAT by FUNCT_2:def 1
.= dom((f*') *' (g*')) by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
end;
Lm13: for x,xv being Element of COMPLEX for u,v,uv,vv being Element of REAL st
x = u+v*<i> & xv = uv+vv*<i> holds |.x + (xv*').|^2 - |.x - xv.|^2 = 4 * u * uv
proof
let x,xv be Element of COMPLEX, u,v,uv,vv be Element of REAL;
assume that
A1: x = u+v*<i> and
A2: xv = uv+vv*<i>;
A3: (u + uv)^2 >= 0 by XREAL_1:63;
A4: (v + -vv)^2 >= 0 by XREAL_1:63;
|.(x + xv*').| = sqrt((Re(x) + Re(xv*'))^2 + (Im (x + xv*'))^2) by COMPLEX1:8
.= sqrt((u + Re(xv*'))^2 + (Im (x + xv*'))^2) by A1,COMPLEX1:12
.= sqrt((u + Re(xv))^2 + (Im (x + xv*'))^2) by COMPLEX1:27
.= sqrt((u + uv)^2 + (Im (x + xv*'))^2) by A2,COMPLEX1:12
.= sqrt((u + uv)^2 + (Im(x) + Im(xv*'))^2) by COMPLEX1:8
.= sqrt((u + uv)^2 + (v + Im(xv*'))^2) by A1,COMPLEX1:12
.= sqrt((u + uv)^2 + (v + -Im(xv))^2) by COMPLEX1:27
.= sqrt((u + uv)^2 + (v + -vv)^2) by A2,COMPLEX1:12;
then
A5: |.(x + xv*').|^2 = (u + uv)^2 + (v + -vv)^2 by A3,A4,SQUARE_1:def 2;
A6: (u - uv)^2 >= 0 by XREAL_1:63;
A7: ((u + uv)^2 + (v + -vv)^2) - ((u - uv)^2 + (v-vv)^2) = 4 * u * uv;
A8: (v -vv)^2 >= 0 by XREAL_1:63;
|.(x - xv).| = sqrt(((Re x)-(Re xv))^2 + (Im (x - xv))^2) by COMPLEX1:19
.= sqrt((u-(Re xv))^2 + (Im (x - xv))^2) by A1,COMPLEX1:12
.= sqrt((u-uv)^2 + (Im (x - xv))^2) by A2,COMPLEX1:12
.= sqrt((u-uv)^2 + (Im(x) - Im(xv))^2) by COMPLEX1:19
.= sqrt((u-uv)^2 + (v - Im(xv))^2) by A1,COMPLEX1:12
.= sqrt((u-uv)^2 + (v-vv)^2) by A2,COMPLEX1:12;
hence thesis by A5,A6,A8,A7,SQUARE_1:def 2;
end;
Lm14: for x,xv being Element of COMPLEX for u,v,uv,vv being Element of REAL st
x = u+v*<i> & xv = uv+vv*<i> & uv < 0 holds (u < 0 implies |.(x - xv).| < |.(x
+ xv*').|) & (u > 0 implies |.(x - xv).| > |.(x + xv*').|) & (u = 0 implies |.(
x - xv).| = |.(x + xv*').|)
proof
let x,xv be Element of COMPLEX, u,v,uv,vv be Element of REAL;
assume that
A1: x = u+v*<i> and
A2: xv = uv+vv*<i> and
A3: uv < 0;
now
assume u < 0;
then 4 * u * uv > 0 by A3;
then |.x + (xv*').|^2 - |.x - xv.|^2 > 0 by A1,A2,Lm13;
then
A4: (|.x + (xv*').|^2 - |.x - xv.|^2) + |.x - xv.|^2 > 0 + |.x - xv.|^2 by
XREAL_1:6;
0 <= |.x + (xv*').| by COMPLEX1:46;
hence |.(x + xv*').| > |.(x - xv).| by A4,XREAL_1:66;
end;
hence u < 0 implies |.(x - xv).| < |.(x + xv*').|;
now
assume u > 0;
then 4 * u * uv < 0 by A3;
then |.x + (xv*').|^2 - |.x - xv.|^2 < 0 by A1,A2,Lm13;
then
A5: (|.x + (xv*').|^2 - |.x - xv.|^2) + |.x - xv.|^2 < 0 + |.x - xv.|^2
by XREAL_1:6;
0 <= |.x - xv.| by COMPLEX1:46;
hence |.(x + xv*').| < |.(x - xv).| by A5,XREAL_1:66;
end;
hence u > 0 implies |.(x - xv).| > |.(x + xv*').|;
now
assume u = 0;
then 4 * u * uv = 0;
then
A6: |.x + (xv*').|^2 - |.x - xv.|^2 = 0 by A1,A2,Lm13;
now
assume
A7: |.(x - xv).| <> |.(x + xv*').|;
per cases by A7,XXREAL_0:1;
suppose
|.(x - xv).| > |.(x + xv*').|;
hence contradiction by A6,COMPLEX1:46,SQUARE_1:16;
end;
suppose
|.(x - xv).| < |.(x + xv*').|;
hence contradiction by A6,COMPLEX1:46,SQUARE_1:16;
end;
end;
hence |.(x - xv).| = |.(x + xv*').|;
end;
hence thesis;
end;
theorem Th47:
for x,z being Element of F_Complex holds eval(rpoly(1,z)*',x) = -x - (z*')
proof
let x,z be Element of F_Complex;
set p = rpoly(1,z)*';
consider F be FinSequence of F_Complex such that
A1: eval(p,x) = Sum F and
A2: len F = len p and
A3: for n be Element of NAT st n in dom F holds F.n = p.(n-'1) * (power
F_Complex).(x,n-'1) by POLYNOM4:def 2;
A4: deg p = deg rpoly(1,z) by Th42
.= 1 by Th27;
then
A5: F = <*F.1,F.2*> by A2,FINSEQ_1:44
.= <*F.1*>^<*F.2*>;
len p = 1 + 1 by A4;
then 1 in Seg(len F) by A2;
then
A6: 1 in dom F by FINSEQ_1:def 3;
A7: 2-'1 = 2-1 by XREAL_0:def 2;
2 in Seg(len F) by A2,A4;
then 2 in dom F by FINSEQ_1:def 3;
then
A8: F.2 = p.1 * (power F_Complex).(x,1+0) by A3,A7
.= p.1 * ((power F_Complex).(x,0) * x) by GROUP_1:def 7
.= p.1 * (1_F_Complex * x) by GROUP_1:def 7
.= p.1 * x
.= (power(F_Complex).(-1_F_Complex,1) * (rpoly(1,z).1)*') * x by Def9
.= (power(F_Complex).(-1_F_Complex,1) * (1_F_Complex)) * x by Lm10,
COMPLFLD:49
.= power(F_Complex).(-1_F_Complex,1+0) * x
.= (power(F_Complex).(-1_F_Complex,0) * (-1_F_Complex)) * x by
GROUP_1:def 7
.= (1_F_Complex * (-1_F_Complex)) * x by GROUP_1:def 7
.= (-(1_F_Complex)) * x
.= -(1_F_Complex * x)
.= -x;
A9: rpoly(1,z).0 = -power(F_Complex).(z,1+0) by Lm10
.= -(power(F_Complex).(z,0) * z) by GROUP_1:def 7
.= -(1_F_Complex * z) by GROUP_1:def 7
.= -z;
1-'1 = 1-1 by XREAL_0:def 2;
then F.1 = p.0 * (power F_Complex).(x,0) by A3,A6
.= p.0 * 1_F_Complex by GROUP_1:def 7
.= p.0
.= power(F_Complex).(-1_F_Complex,0) * (-z)*' by A9,Def9
.= 1_F_Complex * (-z)*' by GROUP_1:def 7
.= (-z)*'
.= -(z*') by COMPLFLD:52;
hence eval(p,x) = Sum(<*-(z*')*>) + Sum(<*-x*>) by A1,A5,A8,RLVECT_1:41
.= Sum(<*-(z*')*>) + -x by RLVECT_1:44
.= -(z*') + -x by RLVECT_1:44
.= -x - (z*');
end;
theorem Th48:
for f being Polynomial of F_Complex st f is Hurwitz for x being
Element of F_Complex st Re(x) >= 0 holds 0 < |.eval(f,x).|
proof
let f be Polynomial of F_Complex;
assume
A1: f is Hurwitz;
let x be Element of F_Complex;
assume
A2: Re(x) >= 0;
eval(f,x) <> 0.F_Complex by A1,A2,POLYNOM5:def 7;
hence thesis by COMPLEX1:47,COMPLFLD:7;
end;
theorem Th49:
for f being Polynomial of F_Complex st deg(f) >= 1 & f is
Hurwitz for x being Element of F_Complex holds (Re(x) < 0 implies |.eval(f,x).|
< |.eval(f*',x).|) & (Re(x) > 0 implies |.eval(f,x).| > |.eval(f*',x).|) & (Re(
x) = 0 implies |.eval(f,x).| = |.eval(f*',x).|)
proof
A1: now
let y,z be Element of F_Complex;
assume
A2: rpoly(1,z) is Hurwitz;
z is_a_root_of rpoly(1,z) by Th30;
then
A3: Re(z) < 0 by A2;
A4: y = Re(y) + Im(y) * <i> by COMPLEX1:13;
A5: y - z = eval(rpoly(1,z),y) by Th29;
A6: z = Re(z) + Im(z) * <i> by COMPLEX1:13;
reconsider y9 = y, z9 = z as Element of COMPLEX by COMPLFLD:def 1;
eval(rpoly(1,z)*',y) = (-y) - (z*') by Th47;
then
A8: eval(rpoly(1,z)*',y) = (-y9) - (z9*');
A9: |.(y9 + (z9*')).| = |.-(y9 + (z9*')).| by COMPLEX1:52;
assume Re(y) > 0;
then |.y9 - z9.| > |.y9 + (z9*').| by A3,A4,A6,Lm14;
hence |.eval(rpoly(1,z),y).| > |.eval((rpoly(1,z))*',y).| by A5,A8,A9;
end;
A10: now
let a,y,z be Element of F_Complex;
assume that
A11: rpoly(1,z) is Hurwitz and
A12: a <> 0.F_Complex;
assume
A13: Re(y) > 0;
A14: |.a.| * |.eval((rpoly(1,z))*',y).| = |.a*'.| * |.eval((rpoly(1,z))*',
y).| by COMPLEX1:53
.= |.a*' * eval((rpoly(1,z))*',y).| by COMPLEX1:65
.= |.eval((a*')*(rpoly(1,z))*',y).| by POLYNOM5:30
.= |.eval((a*rpoly(1,z))*',y).| by Th43;
A15: |.eval(a*rpoly(1,z),y).| = |.a * eval(rpoly(1,z),y).| by POLYNOM5:30
.= |.a.| * |.eval(rpoly(1,z),y).| by COMPLEX1:65;
|.a.| > 0 by A12,COMPLEX1:47,COMPLFLD:7;
hence
|.eval(a*rpoly(1,z),y).|>|.eval((a*rpoly(1,z))*',y).| by A1,A11,A13,A15,A14
,XREAL_1:68;
end;
A16: now
let y,z be Element of F_Complex;
assume
A17: rpoly(1,z) is Hurwitz;
z is_a_root_of rpoly(1,z) by Th30;
then
A18: Re(z) < 0 by A17;
A19: y = Re(y) + Im(y) * <i> by COMPLEX1:13;
A20: y - z = eval(rpoly(1,z),y) by Th29;
A21: z = Re(z) + Im(z) * <i> by COMPLEX1:13;
reconsider y9 = y, z9 = z as Element of COMPLEX by COMPLFLD:def 1;
eval(rpoly(1,z)*',y) = (-y) - (z*') by Th47;
then
A23: eval(rpoly(1,z)*',y) = (-y9) - (z9*');
A24: |.(y9 + (z9*')).| = |.-(y9 + (z9*')).| by COMPLEX1:52;
assume Re(y) < 0;
then |.y9 - z9.| < |.y9 + (z9*').| by A18,A19,A21,Lm14;
hence |.eval(rpoly(1,z),y).| < |.eval((rpoly(1,z))*',y).| by A20,A23,A24;
end;
A25: now
let a,y,z be Element of F_Complex;
assume that
A26: rpoly(1,z) is Hurwitz and
A27: a <> 0.F_Complex;
assume
A28: Re(y) < 0;
A29: |.a.| * |.eval((rpoly(1,z))*',y).| = |.a*'.| * |.eval((rpoly(1,z))*',
y).| by COMPLEX1:53
.= |.a*' * eval((rpoly(1,z))*',y).| by COMPLEX1:65
.= |.eval((a*')*(rpoly(1,z))*',y).| by POLYNOM5:30
.= |.eval((a*rpoly(1,z))*',y).| by Th43;
A30: |.eval(a*rpoly(1,z),y).| = |.a * eval(rpoly(1,z),y).| by POLYNOM5:30
.= |.a.| * |.eval(rpoly(1,z),y).| by COMPLEX1:65;
|.a.| > 0 by A27,COMPLEX1:47,COMPLFLD:7;
hence |.eval(a*rpoly(1,z),y).|<|.eval((a*rpoly(1,z))*',y).| by A16,A26,A28
,A30,A29,XREAL_1:68;
end;
defpred P[Nat] means for f being Polynomial of F_Complex st deg(f) >= 1 & f
is Hurwitz & deg(f) = $1 for x being Element of F_Complex holds (Re(x) < 0
implies |.eval(f,x).| < |.eval(f*',x).|) & (Re(x) > 0 implies |.eval(f,x).| >
|.eval(f*',x).|) & (Re(x) = 0 implies |.eval(f,x).| = |.eval(f*',x).|);
let f be Polynomial of F_Complex;
assume that
A31: deg(f) >= 1 and
A32: f is Hurwitz;
A33: now
let y,z be Element of F_Complex;
assume
A34: rpoly(1,z) is Hurwitz;
z is_a_root_of rpoly(1,z) by Th30;
then
A35: Re(z) < 0 by A34;
A36: y = Re(y) + Im(y) * <i> by COMPLEX1:13;
A37: y - z = eval(rpoly(1,z),y) by Th29;
A38: z = Re(z) + Im(z) * <i> by COMPLEX1:13;
reconsider y9 = y, z9 = z as Element of COMPLEX by COMPLFLD:def 1;
eval(rpoly(1,z)*',y) = (-y) - (z*') by Th47;
then
A40: eval(rpoly(1,z)*',y) = (-y9) - (z9*');
A41: |.(y9 + (z9*')).| = |.-(y9 + (z9*')).| by COMPLEX1:52;
assume Re(y) = 0;
then |.y9 - z9.| = |.y9 + (z9*').| by A35,A36,A38,Lm14;
hence |.eval(rpoly(1,z),y).| = |.eval((rpoly(1,z))*',y).| by A37,A40,A41;
end;
A42: now
let a,y,z be Element of F_Complex;
assume that
A43: rpoly(1,z) is Hurwitz and
a <> 0.F_Complex;
A44: |.eval(a*rpoly(1,z),y).| = |.a * eval(rpoly(1,z),y).| by POLYNOM5:30
.= |.a.| * |.eval(rpoly(1,z),y).| by COMPLEX1:65;
A45: |.a.| * |.eval((rpoly(1,z))*',y).| = |.a*'.| * |.eval((rpoly(1,z))*',
y).| by COMPLEX1:53
.= |.a*' * eval((rpoly(1,z))*',y).| by COMPLEX1:65
.= |.eval((a*')*(rpoly(1,z))*',y).| by POLYNOM5:30
.= |.eval((a*rpoly(1,z))*',y).| by Th43;
assume Re(y) = 0;
hence |.eval(a*rpoly(1,z),y).| = |.eval((a*rpoly(1,z))*',y).| by A33,A43
,A44,A45;
end;
A46: now
let k be Nat;
assume
A47: P[k];
now
let f be Polynomial of F_Complex;
assume that
A48: deg(f) >= 1 and
A49: f is Hurwitz and
A50: deg(f) = k+1;
let x be Element of F_Complex;
per cases by A48,A50,XXREAL_0:1;
suppose
k+1 = 1;
then consider z1,z2 being Element of F_Complex such that
A51: z1 <> 0.F_Complex and
A52: f = z1 * rpoly(1,z2) by A50,Th28;
rpoly(1,z2) is Hurwitz by A49,A51,A52,Th40;
hence (Re(x) < 0 implies |.eval(f,x).| < |.eval(f*',x).|) & (Re(x) > 0
implies |.eval(f,x).| > |.eval(f*',x).|) & (Re(x) = 0 implies |.eval(f,x).| =
|.eval(f*',x).|) by A25,A10,A42,A51,A52;
end;
suppose
A53: k+1 > 1;
A54: k + 1 + 1 > k + 1 + 0 by XREAL_1:6;
then
A55: f <> 0_.(F_Complex) by A50,POLYNOM4:3;
len f > 1 by A48,A50,A54,XXREAL_0:2;
then f is with_roots by POLYNOM5:74;
then consider z being Element of F_Complex such that
A56: z is_a_root_of f by POLYNOM5:def 8;
consider f1 being Polynomial of F_Complex such that
A57: f = rpoly(1,z) *' f1 by A56,Th33;
A58: f1 <> 0_.(F_Complex) by A57,A55,POLYNOM3:34;
rpoly(1,z) <> 0_.(F_Complex) by A57,A55,POLYNOM3:34;
then
A59: deg f = deg(rpoly(1,z)) + deg(f1) by A57,A58,Th23
.= 1 + deg(f1) by Th27;
A60: rpoly(1,z) is Hurwitz by A49,A57,Th41;
A61: f1 is Hurwitz by A49,A57,Th41;
A62: k >= 1 by A53,NAT_1:13;
A63: now
reconsider r19 = eval(rpoly(1,z)*',x), e19 = eval(f1*',x) as Element
of COMPLEX by COMPLFLD:def 1;
reconsider r9 = eval(rpoly(1,z),x), e9 = eval(f1,x) as Element of
COMPLEX by COMPLFLD:def 1;
A64: eval(rpoly(1,z)*',x) * eval(f1*',x) = eval((rpoly(1,z)*')*'((
f1)*'),x) by POLYNOM4:24;
assume
A65: Re(x) > 0;
then
A66: |.e9.| > |.e19.| by A47,A50,A59,A61,A62;
0 <= |.r19.| by COMPLEX1:46;
then
A67: |.r19.| * |.e9.| >= |.r19.| * |.e19.| by A66,XREAL_1:64;
0 <= |.e19.| by COMPLEX1:46;
then |.r9.| * |.e9.| > |.r19.| * |.e9.| by A1,A60,A65,A66,XREAL_1:68;
then |.r9.| * |.e9.| > |.r19.| * |.e19.| by A67,XXREAL_0:2;
then |.r9 * e9.| > |.r19.| * |.e19.| by COMPLEX1:65;
then
A68: |.eval(rpoly(1,z),x) * eval(f1,x).| > |.eval((rpoly(1,z))*',x)
* eval(f1*',x).| by COMPLEX1:65;
eval(rpoly(1,z),x) * eval(f1,x) = eval(rpoly(1,z)*'f1,x) by
POLYNOM4:24;
hence |.eval(f,x).| > |.eval(f*',x).| by A57,A68,A64,Th46;
end;
A69: now
reconsider r19 = eval(rpoly(1,z)*',x), e19 = eval(f1*',x) as Element
of COMPLEX by COMPLFLD:def 1;
reconsider r9 = eval(rpoly(1,z),x), e9 = eval(f1,x) as Element of
COMPLEX by COMPLFLD:def 1;
A70: 0 <= |.r9.| by COMPLEX1:46;
assume
A71: Re(x) < 0;
then
A72: |.r9.| < |.r19.| by A16,A60;
0 <= |.e9.| by COMPLEX1:46;
then
A73: |.r9.| * |.e9.| <= |.r19.| * |.e9.| by A72,XREAL_1:64;
|.e9.| < |.e19.| by A47,A50,A59,A61,A62,A71;
then |.r19.| * |.e9.| < |.r19.| * |.e19.| by A72,A70,XREAL_1:68;
then |.r9.| * |.e9.| < |.r19.| * |.e19.| by A73,XXREAL_0:2;
then |.r9 * e9.| < |.r19.| * |.e19.| by COMPLEX1:65;
then
A74: |.eval(rpoly(1,z),x) * eval(f1,x).| < |.eval((rpoly(1,z))*',x)
* eval(f1*',x).| by COMPLEX1:65;
A75: eval(rpoly(1,z)*',x) * eval(f1*',x) = eval((rpoly(1,z)*')*'((f1
)*'),x) by POLYNOM4:24;
eval(rpoly(1,z),x) * eval(f1,x) = eval(rpoly(1,z)*'f1,x) by
POLYNOM4:24;
hence |.eval(f,x).| < |.eval(f*',x).| by A57,A74,A75,Th46;
end;
now
reconsider r19 = eval(rpoly(1,z)*',x), e19 = eval(f1*',x) as Element
of COMPLEX by COMPLFLD:def 1;
reconsider r9 = eval(rpoly(1,z),x), e9 = eval(f1,x) as Element of
COMPLEX by COMPLFLD:def 1;
A76: eval(rpoly(1,z)*',x) * eval(f1*',x) = eval((rpoly(1,z)*')*'((
f1)*'),x) by POLYNOM4:24;
assume
A77: Re(x) = 0;
then |.eval(f1,x).| = |.eval(f1*',x).| by A47,A50,A59,A61,A62;
then |.r9.| * |.e9.| = |.r19.| * |.e19.| by A33,A60,A77;
then |.r9 * e9.| = |.r19.| * |.e19.| by COMPLEX1:65;
then
A78: |.eval(rpoly(1,z),x) * eval(f1,x).| = |.eval((rpoly(1,z))*',x)
* eval(f1*',x).| by COMPLEX1:65;
eval(rpoly(1,z),x) * eval(f1,x) = eval(rpoly(1,z)*'f1,x) by
POLYNOM4:24;
hence |.eval(f,x).| = |.eval(f*',x).| by A57,A78,A76,Th46;
end;
hence (Re(x) < 0 implies |.eval(f,x).| < |.eval(f*',x).|) & (Re(x) > 0
implies |.eval(f,x).| > |.eval(f*',x).|) & (Re(x) = 0 implies |.eval(f,x).| =
|.eval(f*',x).|) by A69,A63;
end;
end;
hence P[k+1];
end;
let x be Element of F_Complex;
A79: P[0];
A80: for k be Nat holds P[k] from NAT_1:sch 2(A79,A46);
f <> 0_.(F_Complex) by A31,Th20;
then deg f is Element of NAT by Lm8;
hence thesis by A31,A32,A80;
end;
definition
let f be Polynomial of F_Complex;
let z be Element of F_Complex;
func F*(f,z) -> Polynomial of F_Complex equals
eval(f*',z) * f - eval(f,z) *
f*';
coherence;
end;
theorem Th50:
for a,b being Element of F_Complex st |.a.| > |.b.| for f being
Polynomial of F_Complex st deg(f) >= 1 holds f is Hurwitz iff a * f - b * (f*')
is Hurwitz
proof
let a,b be Element of F_Complex;
assume
A1: |.a.| > |.b.|;
then
A2: 0 < |.a.| by COMPLEX1:46;
then
A3: a <> 0.F_Complex by COMPLEX1:47,COMPLFLD:7;
let f be Polynomial of F_Complex;
assume
A4: deg(f) >= 1;
set g = a * f - b * f*';
per cases;
suppose
b = 0.F_Complex;
then g = a * f - 0_.(F_Complex) by POLYNOM5:26
.= a * f + 0_.(F_Complex) by Th9
.= a * f by POLYNOM3:28;
hence thesis by A3,Th40;
end;
suppose
A5: b <> 0.F_Complex;
reconsider a9=a, b9=b as Element of COMPLEX by COMPLFLD:def 1;
(|.a.|^2 - |.b.|^2)" in COMPLEX by XCMPLX_0:def 2;
then reconsider zz = (|.a.|^2 - |.b.|^2)" as Element of F_Complex by
COMPLFLD:def 1;
set a1 = (a*') * zz, b1 = - b * zz;
reconsider a19 = a1, b19 = b1 as Element of COMPLEX by COMPLFLD:def 1;
A6: ((a*') * b") = ((a9*') * b9") by A5,COMPLFLD:5;
A8: 0 < |.b.| by A5,COMPLEX1:47,COMPLFLD:7;
then |.a9.|*|.b9.| > |.b9.|*|.b9.| by A1,XREAL_1:68;
then
A9: |.a9.|^2 - |.b9.|^2 <> 0 by A1,A2,XREAL_1:68;
then A10: -b1 <> 0.F_Complex by A5,COMPLFLD:7;
A11: now
assume
A12: f is Hurwitz;
now
let z be Element of F_Complex;
assume z is_a_root_of g;
then
A13: 0.F_Complex = eval(a * f - b * f*',z) by POLYNOM5:def 7
.= eval(a * f,z) - eval(b * f*',z) by POLYNOM4:21
.= a * eval(f,z) - eval(b * f*',z) by POLYNOM5:30
.= a * eval(f,z) - b * eval(f*',z) by POLYNOM5:30;
now
A14: 0 <= |.b.| by COMPLEX1:46;
A15: |.a.| * |.eval(f,z).| = |.a * eval(f,z).| by COMPLEX1:65;
A16: |.b.| * |.eval(f*',z).| = |.b * eval(f*',z).| by COMPLEX1:65;
assume
A17: Re(z) >= 0;
per cases by A17;
suppose
A18: Re(z) = 0;
then
A19: |.eval(f,z).|>0 by A12,Th48;
|.eval(f,z).|=|.eval(f*',z).| by A4,A12,A18,Th49;
then |.a.|*|.eval(f,z).| > |.b.|*|.eval(f*',z).| by A1,A19,
XREAL_1:68;
hence contradiction by A13,A15,A16,VECTSP_1:19;
end;
suppose
Re(z) > 0;
then
A20: |.eval(f,z).| > |.eval(f*',z).| by A4,A12,Th49;
then |.eval(f,z).| > 0 by COMPLEX1:46;
then
A21: |.a.| * |.eval(f,z).| > |.b.| * |.eval(f,z).| by A1,XREAL_1:68;
|.b.|*|.eval(f,z).| >= |.b.|*|.eval(f*',z).| by A14,A20,XREAL_1:64;
hence contradiction by A13,A15,A16,A21,VECTSP_1:19;
end;
end;
hence Re(z) < 0;
end;
hence g is Hurwitz;
end;
A22: |.a1.| = |.a*'.| * |.(|.a.|^2 - |.b.|^2)".| by COMPLEX1:65
.= |.a.| * |.(|.a.|^2 - |.b.|^2)".| by COMPLEX1:53;
A23: now
let z be Element of COMPLEX;
A24: Im(z*z*') = 0 by COMPLEX1:40;
A25: Re(z*z*') +(Im(z*z*')) * <i> = (z*z*') by COMPLEX1:13;
A26: (Im z)^2 >= 0 by XREAL_1:63;
A27: (Re z)^2 >= 0 by XREAL_1:63;
Re(z*z*') = (Re z)^2 + (Im z)^2 by COMPLEX1:40;
hence z*' * z = |.z.|^2 by A24,A25,A27,A26,SQUARE_1:def 2;
end;
then
A28: b9*' * b9 = |.b9.|^2;
(a9*' * a9) * (b9") - (b9*') = (|.a9.|^2 * (b9") - (b9*')) * 1 by A23
.= (|.a9.|^2 * (b9")-(b9*')) * (b9*b9") by A5,COMPLFLD:7,XCMPLX_0:def 7
.= ((|.a9.|^2 * ((b9") * b9)) - |.b9.|^2) * b9" by A28
.= (|.a9.|^2 * 1 - |.b9.|^2) * b9" by A5,COMPLFLD:7,XCMPLX_0:def 7;
then
A30: -((a9*' * a9) * (b9") - (b9*'))" = -((|.a9.|^2 - |.b9.|^2)" * (b9")")
by XCMPLX_1:204
.= b19;
b1" = b19" by A5,A9,COMPLFLD:5,7;
then
A32: -(b1") = -(b19");
A33: now
assume
A34: b1" = 0.F_Complex;
b1" * b1 = 1_F_Complex by A5,A9,COMPLFLD:7,VECTSP_1:def 10;
hence contradiction by A34;
end;
A35: now
assume -(b1") = 0.F_Complex;
then -(-b1") = 0.F_Complex by RLVECT_1:12;
hence contradiction by A33;
end;
b1" = b19" by A5,A9,COMPLFLD:5,7;
then -(b1") = -(b19");
then
A36: (-(b1"))" = (-(b19"))" by A35,COMPLFLD:5;
(-(b1"))" = -((b1)")" by A33,Th1
.= -b1 by A5,A9,COMPLFLD:7,VECTSP_1:24;
then (-(b19"))" * ((a9*') * b9") = (--(b9 * (|.a.|^2 - |.b.|^2)")) * ((a9
*') * b9") by A36
.= (b9 * (b9")) * ((|.a.|^2 - |.b.|^2)") * (a9*')
.= 1 * ((|.a.|^2 - |.b.|^2)") * (a9*') by A5,COMPLFLD:7,XCMPLX_0:def 7
.= a19;
then
A37: ((-(b1"))") * ((a*') * b") = a1 by A35,A6,A32,COMPLFLD:5;
A38: (a9*') * (b9" * a9) = (a*') * (b" * a) by A5,COMPLFLD:5;
A39: |.b1.| = |.-(b * (|.a.|^2 - |.b.|^2)").|
.= |.b * (|.a.|^2 - |.b.|^2)".| by COMPLEX1:52
.= |.b.| * |.(|.a.|^2 - |.b.|^2)".| by COMPLEX1:65;
A40: (-b19)" = (-b1)" by A10,COMPLFLD:5
.= -(b1)" by A5,A9,Th1,COMPLFLD:7;
A41: |.b.| * |.a.| > |.b.| * |.b.| by A1,A8,XREAL_1:68;
|.a.| * |.a.| > |.b.| * |.a.| by A1,A2,XREAL_1:68;
then |.a.|^2 > |.b.| * |.b.| by A41,XXREAL_0:2;
then
A42: |.a.|^2 - |.b.|^2 > |.b.|^2 - |.b.|^2 by XREAL_1:9;
A43: now
assume b19 = 0.F_Complex;
then (- b) * zz = 0.F_Complex;
then -b = 0.F_Complex by A42,COMPLFLD:7;
then b = - 0.F_Complex;
hence contradiction by A5,RLVECT_1:12;
end;
b * f*' + g = a * f + (-(b * f*') + b * f*') by POLYNOM3:26
.= a * f + (b * f*' - b * f*')
.= a * f + 0_.(F_Complex) by POLYNOM3:29;
then
A44: a * f - g = (b * f*' + g) - g by POLYNOM3:28
.= b * f*' + (g - g) by POLYNOM3:26
.= b * f*' + 0_.(F_Complex) by POLYNOM3:29;
A45: f*' = (1_F_Complex) * (f*') by POLYNOM5:27
.= (b" * b) * (f*') by A5,VECTSP_1:def 10
.= b" * (b * (f*')) by Th14
.= b" * (a * f - g) by A44,POLYNOM3:28;
g*' = (a * f)*' + (-(b * f*'))*' by Th45
.= (a * f)*' + - ((b * f*')*') by Th44
.= ((a*') * (f*')) + - ((b * f*')*') by Th43
.= ((a*') * (f*')) + - ((b*') * ((f*')*')) by Th43
.= ((a*') * (f*')) + - ((b*') * f);
then g*' = ((a*')*((b" * (a * f))+(b" * (-g)))) + (-((b*') * f)) by A45
,Th18
.= ((a*') * (b" * (a * f)) + ((a*') * (b" * (-g)))) + (-((b*') * f))
by Th18
.= (a*') * (b" * (-g)) + ((a*') * (b" * (a * f)) + (-((b*') * f))) by
POLYNOM3:26
.= (a*') * (b" * (-g)) + ((a*') * ((b" * a) * f) + (-((b*') * f))) by
Th14
.= (a*') * (b" * (-g)) + (((a*') * (b" * a)) * f + (-((b*') * f))) by
Th14
.= (a*') * (b" * (-g)) + (((a*') * (b" * a)) * f + ((-b*') * f)) by Th15
.= (a*') * (b" * (-g)) + (((a*') * (b" * a)) + -(b*')) * f by Th17
.= ((a*') * b") * (-g) + (((a*') * (b" * a)) + -(b*')) * f by Th14;
then
A46: g*' + -((a*') * b") * (-g) = (((a*') * (b" * a)) + -(b*')) * f + (((a
*') * b") * (-g) - ((a*') * b") * (-g)) by POLYNOM3:26
.= (((a*') * (b" * a)) + -(b*')) * f + 0_.(F_Complex) by POLYNOM3:29;
A48: f = (1_F_Complex) * f by POLYNOM5:27
.= ((-(b1"))" * (-(b1"))) * f by A5,A9,A40,COMPLFLD:7
,VECTSP_1:def 10
.= (-(b1"))" * ((-(b1")) * f) by Th14
.= (-(b1"))" * (g*' + -((a*') * b") * (-g)) by A46,A30,A38,A40,
POLYNOM3:28
.= (-(b1"))" * g*' + (-(b1"))" * (-((a*') * b") * (-g)) by Th18
.= (-(b1"))" * g*' + (-(b1"))" * (((a*') * b") * (--g)) by Th16
.= (-(b1"))" * g*' + (-(b1"))" * (((a*') * b") * g) by Lm3
.= (-(b1"))" * g*' + a1 * g by A37,Th14
.= ((-b1)")" * g*' + a1 * g by A5,A9,Th1,COMPLFLD:7
.= (-b1) * g*' + a1 * g by A10,VECTSP_1:24
.= -(b1 * g*') + a1 * g by Th15;
then deg f <= max(deg(a1 * g),deg(-(b1 * g*'))) by Th22;
then
A49: deg f <= max(deg(a1 * g),deg(b1 * g*')) by POLYNOM4:8;
|. (|.a.|^2 - |.b.|^2)" .| > 0 by A42,COMPLEX1:47;
then
A50: |.a1.| > |.b1.| by A1,A22,A39,XREAL_1:68;
then |.a1.| > 0 by COMPLEX1:46;
then a1 <> 0.F_Complex by COMPLEX1:47,COMPLFLD:7;
then deg f <= max(deg(g),deg(b1 * g*')) by A49,POLYNOM5:25;
then deg f <= max(deg(g),deg(g*')) by A43,POLYNOM5:25;
then deg f <= max(deg(g),deg(g)) by Th42;
then
A51: deg(g) >= 1 by A4,XXREAL_0:2;
now
assume
A52: g is Hurwitz;
now
let z be Element of F_Complex;
assume z is_a_root_of f;
then
A53: 0.F_Complex = eval(a1 * g - b1 * g*',z) by A48,POLYNOM5:def 7
.= eval(a1 * g,z) - eval(b1 * g*',z) by POLYNOM4:21
.= a1 * eval(g,z) - eval(b1 * g*',z) by POLYNOM5:30
.= a1 * eval(g,z) - b1 * eval(g*',z) by POLYNOM5:30;
now
A54: 0 <= |.b1.| by COMPLEX1:46;
A55: |.a1.| * |.eval(g,z).| = |.a1 * eval(g,z).| by COMPLEX1:65;
A56: |.b1.| * |.eval(g*',z).| = |.b1 * eval(g*',z).| by COMPLEX1:65;
assume
A57: Re(z) >= 0;
per cases by A57;
suppose
A58: Re(z) = 0;
then
A59: |.eval(g,z).|>0 by A52,Th48;
|.eval(g,z).|=|.eval(g*',z).| by A51,A52,A58,Th49;
then |.a1.|*|.eval(g,z).| > |.b1.|*|.eval(g*',z).| by A50,A59,
XREAL_1:68;
hence contradiction by A53,A55,A56,VECTSP_1:19;
end;
suppose
Re(z) > 0;
then
A60: |.eval(g,z).| > |.eval(g*',z).| by A51,A52,Th49;
then |.eval(g,z).| > 0 by COMPLEX1:46;
then
A61: |.a1.| * |.eval(g,z).| > |.b1.| * |.eval(g,z).| by A50,XREAL_1:68;
|.b1.|*|.eval(g,z).| >= |.b1.|*|.eval(g*',z).| by A54,A60,
XREAL_1:64;
hence contradiction by A53,A55,A56,A61,VECTSP_1:19;
end;
end;
hence Re(z) < 0;
end;
hence f is Hurwitz;
end;
hence thesis by A11;
end;
end;
theorem Th51:
for f being Polynomial of F_Complex st deg(f) >= 1 for rho being
Element of F_Complex st Re(rho) < 0 holds f is Hurwitz implies F*(f,rho) div
rpoly(1,rho) is Hurwitz
proof
let f be Polynomial of F_Complex;
assume
A1: deg(f) >= 1;
let rho be Element of F_Complex;
assume
A2: Re(rho) < 0;
reconsider ef = eval(f,rho), ef1 = eval(f*',rho) as Element of F_Complex;
eval(ef1 * f - ef * (f*'),rho) = eval(ef1*f,rho) - eval(ef*(f*'),rho) by
POLYNOM4:21
.= ef1 * eval(f,rho) - eval(ef*(f*'),rho) by POLYNOM5:30
.= ef1 * eval(f,rho) - ef * eval((f*'),rho) by POLYNOM5:30
.= 0.F_Complex by RLVECT_1:15;
then rho is_a_root_of (ef1 * f - ef * (f*')) by POLYNOM5:def 7;
then consider s being Polynomial of F_Complex such that
A3: ef1 * f - ef * (f*') = rpoly(1,rho) *' s by Th33;
assume
A4: f is Hurwitz;
then |.eval(f,rho).| < |.eval(f*',rho).| by A1,A2,Th49;
then ef1 * f - ef * (f*') is Hurwitz by A1,A4,Th50;
then
A5: s is Hurwitz by A3,Th41;
-1 < deg rpoly(1,rho) by Th27;
then
A6: deg 0_.(F_Complex) < deg rpoly(1,rho) by Th20;
ef1 * f - ef * (f*') = s *' rpoly(1,rho) + 0_.(F_Complex) by A3,POLYNOM3:28;
hence thesis by A5,A6,Def5;
end;
theorem
for f being Polynomial of F_Complex st deg(f) >= 1 holds (ex rho being
Element of F_Complex st Re(rho) < 0 & |.eval(f,rho).| >= |.eval(f*',rho).|)
implies f is non Hurwitz by Th49;
::$N Schur's criterion
theorem
for f being Polynomial of F_Complex st deg(f) >= 1 for rho being
Element of F_Complex st Re(rho) < 0 & |.eval(f,rho).| < |.eval(f*',rho).| holds
f is Hurwitz iff F*(f,rho) div rpoly(1,rho) is Hurwitz
proof
let f be Polynomial of F_Complex;
assume
A1: deg(f) >= 1;
let rho be Element of F_Complex;
assume that
A2: Re(rho) < 0 and
A3: |.eval(f,rho).| < |.eval(f*',rho).|;
reconsider ef = eval(f,rho), ef1 = eval(f*',rho) as Element of F_Complex;
now
-1 < deg rpoly(1,rho) by Th27;
then
A4: deg 0_.(F_Complex) < deg rpoly(1,rho) by Th20;
eval(ef1 * f - ef * (f*'),rho) = eval(ef1*f,rho) - eval(ef*(f*'),rho)
by POLYNOM4:21
.= ef1 * eval(f,rho) - eval(ef*(f*'),rho) by POLYNOM5:30
.= ef1 * eval(f,rho) - ef * eval((f*'),rho) by POLYNOM5:30
.= 0.F_Complex by RLVECT_1:15;
then rho is_a_root_of (ef1 * f - ef * (f*')) by POLYNOM5:def 7;
then consider t being Polynomial of F_Complex such that
A5: F*(f,rho) = rpoly(1,rho) *' t by Th33;
F*(f,rho) = rpoly(1,rho) *' t + 0_.(F_Complex) by A5,POLYNOM3:28;
then
A6: F*(f,rho) = (F*(f,rho) div rpoly(1,rho)) *' rpoly(1,rho) by A5,A4,Def5;
(1_F_Complex) * rpoly(1,rho) is Hurwitz by A2,Th39;
then
A7: rpoly(1,rho) is Hurwitz by POLYNOM5:27;
assume F*(f,rho) div rpoly(1,rho) is Hurwitz;
then F*(f,rho) is Hurwitz by A6,A7,Th41;
hence f is Hurwitz by A1,A3,Th50;
end;
hence thesis by A1,A2,Th51;
end;