:: Schur's Theorem on the Stability of Networks :: by Agnieszka Rowi\'nska-Schwarzweller and Christoph Schwarzweller :: :: Received October 19, 2006 :: Copyright (c) 2006-2012 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, NUMBERS, XCMPLX_0, ALGSTR_0, VECTSP_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, ORDINAL1, NAT_1, NAT_D, XXREAL_0, FINSEQ_1, INT_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; 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, GCD_1, POLYNOM3, POLYNOM4, POLYNOM5, FUNCOP_1, CARD_1, VFUNCT_1, FUNCT_2; requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM; definitions 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 set; assume u in rng G; then consider x being set 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 A11,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) by FINSEQ_1:40 .= 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 by VECTSP_1:def 4 .= (-1_L) * (-1_L) by VECTSP_1:10 .= 0.L by A3,VECTSP_1:6; hence contradiction; end; let k be Element of NAT; A4: power(L).(-1_L,k+1) = power(L).(-1_L,k) * (-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 Element of NAT holds P[k] from NAT_1:sch 1(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 Element of NAT; assume A2: P[j]; power(L).(x,k1) * power(L).(x,j+1) = power(L).(x,k1) * (power(L).(x,j) * x) by GROUP_1:def 7 .= (power(L).(x,k1) * power(L).(x,j)) * 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) by VECTSP_1:def 4; then A3: P[0]; for k be Element of NAT holds P[k] from NAT_1:sch 1(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:2,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 Element of 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) by VECTSP_1:def 8 .= 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,VECTSP_1:def 8; 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 by VECTSP_1:def 8; then A4: P[0] by GROUP_1:def 7; for k be Element of NAT holds P[k] from NAT_1:sch 1(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 Element of NAT; assume A2: P[k]; (power(F_Complex).(z,k+1))*' = (power(F_Complex).(z,k) * z)*' by GROUP_1:def 7 .= (power(F_Complex).(z*',k)) * (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 Element of NAT holds P[k] from NAT_1:sch 1(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 Element of 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 Element of NAT holds P[k] from NAT_1:sch 1(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 Element of 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 Element of NAT holds P[k] from NAT_1:sch 1(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 Element of 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 by VECTSP_1:6; hence x * Sum(F) = Sum(x*F) by A8,RLVECT_1:43; end; then A9: P[0]; for k be Element of NAT holds P[k] from NAT_1:sch 1(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; A2: x in NAT by ORDINAL1:def 12; hence (-(-p)).x = -((-p)).x by BHSP_1:44 .= -(-(p.x)) by A2,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 Element of 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 A11,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 by FINSEQ_1:40; 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 by FUNCOP_1:7; 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 Element of NAT holds P[k] from NAT_1:sch 1(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 set; assume i9 in dom f; then reconsider i = i9 as Element of NAT; f.i = x1*(x2*p).i by POLYNOM5:def 3 .= x1*(x2*p.i) by POLYNOM5:def 3 .= (x1*x2)*p.i by GROUP_1:def 3 .= g.i by POLYNOM5:def 3; 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 set; 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 3 .= (-x)*p.i by VECTSP_1:9 .= g.i by POLYNOM5:def 3; 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 set; 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 3 .= x*(-p.i) by VECTSP_1:8 .= x*((-p).i) by BHSP_1:44 .= g.i by POLYNOM5:def 3; 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 set; assume i9 in dom f; then reconsider i = i9 as Element of NAT; f.i = (x1+x2)*p.i by POLYNOM5:def 3 .= x1*p.i+x2*p.i by VECTSP_1:def 3 .= (x1*p).i+x2*p.i by POLYNOM5:def 3 .= (x1*p).i+(x2*p).i by POLYNOM5:def 3 .= 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 set; assume i9 in dom f; then reconsider i = i9 as Element of NAT; f.i = x*(p1+p2).i by POLYNOM5:def 3 .= 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 3 .= (x*p1).i+(x*p2).i by POLYNOM5:def 3 .= 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 set; 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 3 .= rf.j by A4,A14; end; g.i = x * Sum rp by A6,POLYNOM5:def 3 .= 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; A9: k in NAT by ORDINAL1:def 12; 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 A9,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 commutative 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 commutative 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 7; 0.L = eval(p,x) by A3,POLYNOM5:def 6 .= 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 set; 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; dom(0_.(L)) = NAT by FUNCT_2:def 1; then 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); A3: dom(0_.(L)) = NAT by FUNCT_2:def 1; now let u be set; 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 A3,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 set; 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) by FUNCOP_1:13; A5: now let x9 be set; 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)) = NAT by FUNCT_2:def 1; then 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 Function of NAT,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 f = (0,k)-->(-power(L).(z,k),1_L); set a = -power(L).(z,k); 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) by FUNCOP_1:13; 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 3 .= x * 1_L by Lm10 .= p.k by A7,VECTSP_1:def 4; end; suppose k < 1; then A8: k = 0 by NAT_1:14; hence f.k = x * rpoly(1,z).0 by POLYNOM5:def 3 .= 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) by VECTSP_1:def 8 .= 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,VECTSP_1:def 8; 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 by VECTSP_1:def 8 .= 1_L * x by Lm10 .= x by VECTSP_1:def 8; 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 by VECTSP_1:def 4 .= -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 by VECTSP_1:def 8; 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 6; 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[set,set] 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 set st x in NAT ex y being set st y in the carrier of L & P[x,y] proof let u be set; assume u in NAT; then reconsider u9 = u as Element of NAT; thus ex y being set st y in the carrier of L & P[u,y] proof 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; end; consider f being Function of NAT,the carrier of L such that A4: for x being set 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 set; 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 set; 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) by VECTSP_1:def 8 .= (-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,VECTSP_1:7; 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) by VECTSP_1:def 8 .= 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 by VECTSP_1:6; 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 by VECTSP_1:6; 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 3 .= p.j * 0.L by A3,A21,A26,Lm11 .= 0.L by VECTSP_1:6; 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 3 .= p.i9 * 0.L by A29,A38,Lm11 .= 0.L by VECTSP_1:6; 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 set; 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 3 .= 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 by VECTSP_1:def 4; 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,FINSEQ_1:40; 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 6; 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 3 .= p.i * 1_L by A68,Lm10 .= p.i9 by VECTSP_1:def 4; 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 7; 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 set; 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 B1: 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; A1: len s <> 0 by B1,POLYNOM4:5; then len s + 1 > 0 + 1 by XREAL_1:6; then len s >= 1 by NAT_1:13; then A2: len s - 1 >= 1 - 1 by XREAL_1:9; s.(len(s)-1) <> 0.L by A1,Lm6; then A3: s.(len s-'1) <> 0.L by A2,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 A4: ex k being Nat st P[k]; consider k being Nat such that A5: P[k] & for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A4); consider f being Polynomial of L such that A6: f in M and A7: len f = k by A5; consider g being Polynomial of L such that A8: f = p - g *' s and 1 = 1 by A6; take g; A9: 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 A10: f = 0_.(L); reconsider s9 = deg s as Nat by B1,Lm8; A11: s9 >= 0; deg(f) = -1 by A10,Th20; hence thesis by A8,A9,A11; 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 A12: len f - 1 >= 1 - 1 by XREAL_1:9; then reconsider k9 = len f - 1 as Element of NAT by INT_1:3; A13: k = k9 + 1 by A7; dom f = NAT by FUNCT_2:def 1; then A14: 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); A15: dom(0_.(L)) = NAT by FUNCT_2:def 1; now let u be set; assume u in {degn}; then u = degn by TARSKI:def 1; hence u in NAT; end; then A16: {degn} c= NAT by TARSKI:def 3; A17: degn in {degn} by TARSKI:def 1; A18: now let x9 be set; assume x9 in NAT; then reconsider x = x9 as Element of NAT; per cases; suppose A19: x in dom({degn} --> al); then x = degn by TARSKI:def 1; then g1.x = ({degn} --> al).degn by A19,FUNCT_4:13 .= al by A17,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 by FUNCOP_1:7; hence g1.x9 in the carrier of L; end; end; dom({degn} --> al) = {degn} by FUNCOP_1:13; then dom(0_.(L))\/dom({degn}-->al) = NAT by A15,A16,XBOOLE_1:12; then dom g1 = NAT by FUNCT_4:def 1; then reconsider g1 as sequence of L by A18,FUNCT_2:3; A20: for j being Nat st j <> degn holds g1.j = 0.L proof let j be Nat; A21: 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 A21,FUNCOP_1:7; end; A22: 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 A20; end; hence thesis; end; A23: degn in {degn} by TARSKI:def 1; then degn in dom({degn} --> al) by FUNCOP_1:13; then A24: g1.degn = ({degn} --> al).degn by FUNCT_4:13 .= al by A23,FUNCOP_1:7; reconsider g1 as Polynomial of L by A22,ALGSEQ_1:def 1; set s1 = p - (g + g1) *' s; now A25: 1 <= degn + 1 by NAT_1:11; let i be Nat; A26: dom f = NAT by FUNCT_2:def 1; assume A27: i >= k9; then A28: i + 1 >= k by A13,XREAL_1:6; degn + 1 = k - deg(s) by A7; then A29: degn + 1 <= k by A2,XREAL_1:43; then A30: i + 1 - (degn + 1) is Element of NAT by A28,INT_1:5,XXREAL_0:2; A31: i in NAT by ORDINAL1:def 12; then consider sf being FinSequence of L such that A32: len sf = i+1 and A33: (g1 *' s).i = Sum sf and A34: 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; A35: dom sf = Seg(len sf) by FINSEQ_1:def 3; i + 1 >= degn + 1 by A29,A28,XXREAL_0:2; then A36: degn + 1 in dom sf by A32,A35,A25; A37: now let m be Nat; assume that A38: m in dom sf and A39: m <> degn + 1; 1 <= m by A35,A38,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 A39; hence g1.(m-'1) = 0.L by A20; end; now let i9 be Element of NAT; assume that A40: i9 in dom sf and A41: i9 <> degn + 1; sf.i9 = g1.(i9-'1) * s.(i+1-'i9) by A34,A40 .= 0.L * s.(i+1-'i9) by A37,A40,A41 .= 0.L by VECTSP_1:7; hence sf/.i9 = 0.L by A40,PARTFUN1:def 6; end; then A42: Sum sf = sf/.(degn + 1) by A36,POLYNOM2:3 .= sf.(degn+1) by A36,PARTFUN1:def 6 .= g1.(degn+1-'1) * s.(i+1-'(degn+1)) by A34,A36 .= al * s.(i+1-'(degn+1)) by A24,NAT_D:34; A43: s1 - f = (p + -(g + g1) *' s) + (-p + -(-(g *' s))) by A8,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; A44: 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 A43; then A45: s1.i = f.i + (-(g1 *' s)).i by A31,NORMSP_1:def 2 .= f.i + -(g1 *' s).i by A31,BHSP_1:44 .= f/.i + -(g1 *' s).i by A31,A26,PARTFUN1:def 6 .= f/.i + -(g1 *' s)/.i by A31,A44,PARTFUN1:def 6; A46: i in NAT by ORDINAL1:def 12; per cases by A27,XXREAL_0:1; suppose A47: i > k9; then reconsider e = i - k9 as Element of NAT by INT_1:5; i - k9 > k9 - k9 by A47,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 A48: (i - k9 - 1) + len(s) >= 0 + len(s) by XREAL_1:6; i + 1 > k9 + 1 by A47,XREAL_1:6; then i >= len f by NAT_1:13; then f.i = 0.L by ALGSEQ_1:8; then A49: f/.i = 0.L by A26,A46,PARTFUN1:def 6; i+1-'(degn+1) = i - k9 + (len(s)-1) by A30,XREAL_0:def 2; then s.(i+1-'(degn+1)) = 0.L by A48,ALGSEQ_1:8; then Sum sf = 0.L by A42,VECTSP_1:6; hence s1.i = 0.L + -(0.L) by A44,A45,A33,A46,A49,PARTFUN1:def 6 .= 0.L + 0.L by RLVECT_1:12 .= 0.L by RLVECT_1:def 4; end; suppose A50: i = k9; (i+1)-'(degn+1) = i + 1 - (degn + 1) by A30,XREAL_0:def 2 .= len s -' 1 by A2,A50,XREAL_0:def 2; then Sum sf = f.(len f-'1) * ((s.(len s-'1))" * s.(len s-'1)) by A42,GROUP_1:def 3 .= f.(len f-'1) * 1_L by A3,VECTSP_1:def 10 .= f.(len f-'1) by VECTSP_1:def 4 .= f.(len f-1) by A12,XREAL_0:def 2 .= f/.(len f-1) by A14,PARTFUN1:def 6; hence s1.i = f/.(len f-1)+-(f/.(len f-1)) by A44,A45,A33,A50, 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 A51: len(s1) < k by A13,NAT_1:13; s1 in M; hence contradiction by A5,A51; end; hence thesis by A8,A9; end; end; uniqueness proof let f1,f2 be Polynomial of L; given t1 being Polynomial of L such that A52: p = f1*'s+t1 and A53: deg t1 < deg s; given t2 being Polynomial of L such that A54: p = f2*'s+t2 and A55: deg t2 < deg s; A56: (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 A52,A54,POLYNOM3:26; then A57: 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 A58: f1 <> f2; A59: 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 A58,POLYNOM3:28; end; then reconsider d = deg(f2-f1), degs = deg(s) as Nat by B1,Lm8; deg(t1-t2) <= max(deg(t1),deg(-t2)) by Th22; then A60: deg(t1-t2) <= max(deg(t1),deg(t2)) by POLYNOM4:8; A61: deg(t1-t2) < degs proof per cases by XXREAL_0:16; suppose max(deg(t1),deg(t2))=deg(t1); hence thesis by A53,A60,XXREAL_0:2; end; suppose max(deg(t1),deg(t2))=deg(t2); hence thesis by A55,A60,XXREAL_0:2; end; end; deg(t1-t2) = d + degs by B1,A57,A56,A59,Th23; hence contradiction by A61,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 :Def7: 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 by Def7; 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,Def7; 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) by FUNCOP_1:7; 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 :Def8: 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 6; hence thesis by Def8,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 6; 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,VECTSP_1:def 4; end; hence thesis by Def8; 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 6 .= 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 by Def8; 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 by VECTSP_1:6; then A4: z is_a_root_of p by POLYNOM5:def 6; assume x * rpoly(1,z) is Hurwitz; hence Re(z) < 0 by A4,Def8; 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 6 .= 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 6; hence Re(x) < 0 by A3,Def8; end; hence z*f is Hurwitz by Def8; 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 6 .= 0.F_Complex by VECTSP_1:6; then x is_a_root_of (z*f) by POLYNOM5:def 6; hence Re(x) < 0 by A4,Def8; end; hence f is Hurwitz by Def8; 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 6; then eval(f,x) = 0.F_Complex by A2,VECTSP_1:7; hence thesis by POLYNOM5:def 6; end; suppose x is_a_root_of h; then eval(h,x) = 0.F_Complex by POLYNOM5:def 6; then eval(f,x) = 0.F_Complex by A2,VECTSP_1:6; hence thesis by POLYNOM5:def 6; 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 6 .= 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 6; hence Re(z) < 0 by A2,Def8; end; suppose eval(g,z)=0.F_Complex; then z is_a_root_of g by POLYNOM5:def 6; hence Re(z) < 0 by A3,Def8; end; end; hence f*'g is Hurwitz by Def8; 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,Def8; end; hence f is Hurwitz by Def8; 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,Def8; end; hence g is Hurwitz by Def8; 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[set,set] means ex n being Element of NAT st n = $1 & $2 = power( F_Complex).(-1_F_Complex,n) * (f.n)*'; A1: for x being set st x in NAT ex y being set st y in the carrier of F_Complex & P[x,y] proof let u be set; 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 Function of NAT,the carrier of F_Complex such that A2: for x being set 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,VECTSP_1:6; 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 set; 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 by VECTSP_1:def 8 .= 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 by VECTSP_1:6; 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; canceled; theorem Th44: 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 set; assume k9 in dom(g1*'); then reconsider k = k9 as Element of NAT; g1.k = x * f.k by POLYNOM5:def 3; 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 3; 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 Th45: 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 set; 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)*')) by VECTSP_1:8 .= -((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 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 set; 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 Th47: 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 set; 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* & xv = uv+vv* 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* and A2: xv = uv+vv*; 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* & xv = uv+vv* & 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* and A2: xv = uv+vv* 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 Th48: 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 by VECTSP_1:def 8 .= (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 by VECTSP_1:def 4 .= (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 by VECTSP_1:def 4 .= -(1_F_Complex * x) by VECTSP_1:9 .= -x by VECTSP_1:def 8; 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 by VECTSP_1:def 8; 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 by VECTSP_1:def 4 .= power(F_Complex).(-1_F_Complex,0) * (-z)*' by A9,Def9 .= 1_F_Complex * (-z)*' by GROUP_1:def 7 .= (-z)*' by VECTSP_1:def 8 .= -(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*') by RLVECT_1:def 11; end; theorem Th49: 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; now assume eval(f,x) = 0.F_Complex; then x is_a_root_of f by POLYNOM5:def 6; hence contradiction by A1,A2,Def8; end; hence thesis by COMPLEX1:47,COMPLFLD:7; end; theorem Th50: 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,Def8; A4: y = Re(y) + Im(y) * by COMPLEX1:13; A5: y - z = eval(rpoly(1,z),y) by Th29; A6: z = Re(z) + Im(z) * by COMPLEX1:13; reconsider y9 = y, z9 = z as Element of COMPLEX by COMPLFLD:def 1; A7: -y = -y9 by COMPLFLD:2; eval(rpoly(1,z)*',y) = (-y) - (z*') by Th48; then A8: eval(rpoly(1,z)*',y) = (-y9) - (z9*') by A7,COMPLFLD:3; 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, COMPLFLD:3; 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 Th44; 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,Def8; A19: y = Re(y) + Im(y) * by COMPLEX1:13; A20: y - z = eval(rpoly(1,z),y) by Th29; A21: z = Re(z) + Im(z) * by COMPLEX1:13; reconsider y9 = y, z9 = z as Element of COMPLEX by COMPLFLD:def 1; A22: -y = -y9 by COMPLFLD:2; eval(rpoly(1,z)*',y) = (-y) - (z*') by Th48; then A23: eval(rpoly(1,z)*',y) = (-y9) - (z9*') by A22,COMPLFLD:3; 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, COMPLFLD:3; 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 Th44; 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,Def8; A36: y = Re(y) + Im(y) * by COMPLEX1:13; A37: y - z = eval(rpoly(1,z),y) by Th29; A38: z = Re(z) + Im(z) * by COMPLEX1:13; reconsider y9 = y, z9 = z as Element of COMPLEX by COMPLFLD:def 1; A39: -y = -y9 by COMPLFLD:2; eval(rpoly(1,z)*',y) = (-y) - (z*') by Th48; then A40: eval(rpoly(1,z)*',y) = (-y9) - (z9*') by A39,COMPLFLD:3; 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, COMPLFLD:3; 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 Th44; 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 Element of 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 7; 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,Th47; 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,Th47; 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,Th47; 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 Element of NAT holds P[k] from NAT_1:sch 1(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 Th51: 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; A7: b19 = -(b9 * (|.a.|^2 - |.b.|^2)") by COMPLFLD:2; 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,RLVECT_1:17; 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 6 .= 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,Th49; |.eval(f,z).|=|.eval(f*',z).| by A4,A12,A18,Th50; 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,Th50; 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 by Def8; 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*')) * = (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; A29: (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 by COMPLFLD:2; A31: b19 = -b9 * (|.a.|^2 - |.b.|^2)" by COMPLFLD:2 .= (-b9) * (|.a.|^2 - |.b.|^2)"; then b1" = b19" by A5,A9,COMPLFLD:5,7; then A32: -(b1") = -(b19") by COMPLFLD:2; A33: now assume A34: b1" = 0.F_Complex; b1" * b1 = 1_F_Complex by A5,A9,A31,COMPLFLD:7,VECTSP_1:def 10; hence contradiction by A34,VECTSP_1:6; end; A35: now assume -(b1") = 0.F_Complex; then -(-b1") = 0.F_Complex by RLVECT_1:12; hence contradiction by A33,RLVECT_1:17; end; b1" = b19" by A5,A9,A31,COMPLFLD:5,7; then -(b1") = -(b19") by COMPLFLD:2; then A36: (-(b1"))" = (-(b19"))" by A35,COMPLFLD:5; (-(b1"))" = -((b1)")" by A33,Th1 .= -b1 by A5,A9,A31,COMPLFLD:7,VECTSP_1:24; then (-(b19"))" * ((a9*') * b9") = (--(b9 * (|.a.|^2 - |.b.|^2)")) * ((a9 *') * b9") by A7,A36,COMPLFLD:2 .= (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)").| by COMPLFLD:2 .= |.b * (|.a.|^2 - |.b.|^2)".| by COMPLEX1:52 .= |.b.| * |.(|.a.|^2 - |.b.|^2)".| by COMPLEX1:65; -b1 = -b19 by COMPLFLD:2; then A40: (-b19)" = (-b1)" by A10,COMPLFLD:5 .= -(b1)" by A5,A9,A31,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 by VECTSP_1:9; then -b = 0.F_Complex by A42,COMPLFLD:7; then b = - 0.F_Complex by RLVECT_1:17; 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 Th46 .= (a * f)*' + - ((b * f*')*') by Th45 .= ((a*') * (f*')) + - ((b * f*')*') by Th44 .= ((a*') * (f*')) + - ((b*') * ((f*')*')) by Th44 .= ((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; A47: -(b9*') = -(b*') by COMPLFLD:2; A48: f = (1_F_Complex) * f by POLYNOM5:27 .= ((-(b1"))" * (-(b1"))) * f by A5,A29,A9,A30,A40,COMPLFLD:7 ,VECTSP_1:def 10 .= (-(b1"))" * ((-(b1")) * f) by Th14 .= (-(b1"))" * (g*' + -((a*') * b") * (-g)) by A46,A30,A38,A47,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,A31,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 6 .= 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,Th49; |.eval(g,z).|=|.eval(g*',z).| by A51,A52,A58,Th50; 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,Th50; 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 by Def8; end; hence thesis by A11; end; end; theorem Th52: 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 6; 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,Th50; then ef1 * f - ef * (f*') is Hurwitz by A1,A4,Th51; 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 Th50; ::$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 6; 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,Th51; end; hence thesis by A1,A2,Th52; end;