:: HURWITZ semantic presentation begin Lm1: for L being non empty right_complementable add-associative right_zeroed 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 non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: 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))*> ) let F be FinSequence of L; ::_thesis: 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))*> ) let G1 be FinSequence; ::_thesis: for k being Nat st G1 = F | (Seg k) & len F = k + 1 holds ( G1 is FinSequence of L & dom G1 c= dom F & len G1 = k & F = G1 ^ <*(F /. (k + 1))*> ) let k be Nat; ::_thesis: ( G1 = F | (Seg k) & len F = k + 1 implies ( G1 is FinSequence of L & dom G1 c= dom F & len G1 = k & F = G1 ^ <*(F /. (k + 1))*> ) ) assume that A1: G1 = F | (Seg k) and A2: len F = k + 1 ; ::_thesis: ( G1 is FinSequence of L & dom G1 c= dom F & len G1 = k & F = G1 ^ <*(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__::_thesis:_for_u_being_set_st_u_in_rng_G_holds_ u_in_the_carrier_of_L let u be set ; ::_thesis: ( u in rng G implies u in the carrier of L ) assume u in rng G ; ::_thesis: u in the carrier of L 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; ::_thesis: verum 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; ::_thesis: ( dom G1 c= dom F & len G1 = k & F = G1 ^ <*(F /. (k + 1))*> ) reconsider G = 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; ::_thesis: ( len G1 = k & F = G1 ^ <*(F /. (k + 1))*> ) thus len G1 = k by A1, A3, FINSEQ_1:17; ::_thesis: F = G1 ^ <*(F /. (k + 1))*> now__::_thesis:_for_j_being_Nat_st_j_in_dom_F_holds_ F_._j_=_(G_^_<*(F_/._(k_+_1))*>)_._j let j be Nat; ::_thesis: ( j in dom F implies F . b1 = (G ^ <*(F /. (k + 1))*>) . b1 ) assume A11: j in dom F ; ::_thesis: F . b1 = (G ^ <*(F /. (k + 1))*>) . b1 percases ( j in dom G or not j in dom G ) ; supposeA12: j in dom G ; ::_thesis: F . b1 = (G ^ <*(F /. (k + 1))*>) . b1 hence F . j = G . j by A1, FUNCT_1:47 .= (G ^ <*(F /. (k + 1))*>) . j by A12, FINSEQ_1:def_7 ; ::_thesis: verum end; supposeA13: not j in dom G ; ::_thesis: (G ^ <*(F /. (k + 1))*>) . b1 = F . b1 A14: dom F = Seg (len F) by FINSEQ_1:def_3; then A15: 1 <= j by A11, FINSEQ_1:1; A16: now__::_thesis:_not_j_<_k_+_1 assume j < k + 1 ; ::_thesis: contradiction then j <= k by NAT_1:13; then j in Seg k by A11, A15; hence contradiction by A1, A3, A13, FINSEQ_1:17; ::_thesis: verum 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, FINSEQ_1: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 ; ::_thesis: verum end; end; end; hence F = G1 ^ <*(F /. (k + 1))*> by A10, FINSEQ_1:13; ::_thesis: verum end; theorem Th1: :: HURWITZ:1 for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for x being Element of L st x <> 0. L holds - (x ") = (- x) " proof let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for x being Element of L st x <> 0. L holds - (x ") = (- x) " let x be Element of L; ::_thesis: ( x <> 0. L implies - (x ") = (- x) " ) assume A1: x <> 0. L ; ::_thesis: - (x ") = (- x) " A2: now__::_thesis:_not_-_x_=_0._L assume - x = 0. L ; ::_thesis: contradiction then - (- x) = 0. L by RLVECT_1:12; hence contradiction by A1, RLVECT_1:17; ::_thesis: verum 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 - (x ") = (- x) " by A2, VECTSP_1:def_10; ::_thesis: verum end; theorem Th2: :: HURWITZ:2 for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for k being Element of NAT holds (power L) . ((- (1_ L)),k) <> 0. L proof let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for k being Element of NAT holds (power L) . ((- (1_ L)),k) <> 0. L let k be Element of NAT ; ::_thesis: (power L) . ((- (1_ L)),k) <> 0. L defpred S1[ Nat] means (power L) . ((- (1_ L)),$1) <> 0. L; A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] A2: now__::_thesis:_not_-_(1__L)_=_0._L assume A3: - (1_ L) = 0. L ; ::_thesis: contradiction 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 ; ::_thesis: verum end; let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) A4: (power L) . ((- (1_ L)),(k + 1)) = ((power L) . ((- (1_ L)),k)) * (- (1_ L)) by GROUP_1:def_7; assume S1[k] ; ::_thesis: S1[k + 1] hence S1[k + 1] by A4, A2, VECTSP_1:12; ::_thesis: verum end; A5: S1[ 0 ] by GROUP_1:def_7; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A1); hence (power L) . ((- (1_ L)),k) <> 0. L ; ::_thesis: verum end; theorem Th3: :: HURWITZ:3 for L being non empty associative well-unital 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 non empty associative well-unital multLoopStr ; ::_thesis: 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)) let x be Element of L; ::_thesis: for k1, k2 being Element of NAT holds ((power L) . (x,k1)) * ((power L) . (x,k2)) = (power L) . (x,(k1 + k2)) let k1, k2 be Element of NAT ; ::_thesis: ((power L) . (x,k1)) * ((power L) . (x,k2)) = (power L) . (x,(k1 + k2)) defpred S1[ 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__::_thesis:_for_j_being_Element_of_NAT_st_S1[j]_holds_ S1[j_+_1] let j be Element of NAT ; ::_thesis: ( S1[j] implies S1[j + 1] ) assume A2: S1[j] ; ::_thesis: S1[j + 1] ((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 S1[j + 1] ; ::_thesis: verum 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: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1); then ex j being Element of NAT st ( j = k2 & ((power L) . (x,k1)) * ((power L) . (x,j)) = (power L) . (x,(k1 + j)) ) ; hence ((power L) . (x,k1)) * ((power L) . (x,k2)) = (power L) . (x,(k1 + k2)) ; ::_thesis: verum 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; ::_thesis: ( Im (- (1_ F_Complex)) = 0 & Im (0. F_Complex) = 0 ) - (1_ F_Complex) = - 1r by COMPLFLD:2, COMPLFLD:8; hence Im (- (1_ F_Complex)) = - 0 by COMPLEX1:6, COMPLEX1:17 .= 0 ; ::_thesis: Im (0. F_Complex) = 0 thus Im (0. F_Complex) = 0 by COMPLEX1:4, COMPLFLD:7; ::_thesis: verum end; theorem Th4: :: HURWITZ:4 for L being non empty right_complementable well-unital distributive add-associative right_zeroed 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 non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for k being Element of NAT holds ( (power L) . ((- (1_ L)),(2 * k)) = 1_ L & (power L) . ((- (1_ L)),((2 * k) + 1)) = - (1_ L) ) let k be Element of NAT ; ::_thesis: ( (power L) . ((- (1_ L)),(2 * k)) = 1_ L & (power L) . ((- (1_ L)),((2 * k) + 1)) = - (1_ L) ) defpred S1[ Nat] means ( (power L) . ((- (1_ L)),(2 * $1)) = 1_ L & (power L) . ((- (1_ L)),((2 * $1) + 1)) = - (1_ L) ); A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] 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 S1[k + 1] by A3; ::_thesis: verum 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: S1[ 0 ] by GROUP_1:def_7; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A1); hence ( (power L) . ((- (1_ L)),(2 * k)) = 1_ L & (power L) . ((- (1_ L)),((2 * k) + 1)) = - (1_ L) ) ; ::_thesis: verum end; theorem Th5: :: HURWITZ:5 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; ::_thesis: for k being Element of NAT holds ((power F_Complex) . (z,k)) *' = (power F_Complex) . ((z *'),k) let k be Element of NAT ; ::_thesis: ((power F_Complex) . (z,k)) *' = (power F_Complex) . ((z *'),k) defpred S1[ Nat] means ex j being Element of NAT st ( j = $1 & ((power F_Complex) . (z,j)) *' = (power F_Complex) . ((z *'),j) ); A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] ((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 S1[k + 1] ; ::_thesis: verum 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: S1[ 0 ] ; for k being Element of NAT holds S1[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 ((power F_Complex) . (z,k)) *' = (power F_Complex) . ((z *'),k) ; ::_thesis: verum end; theorem Th6: :: HURWITZ:6 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 S1[ 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; ::_thesis: ( len G = len F & ( for i being Element of NAT st i in dom G holds G /. i = (F /. i) *' ) implies Sum G = (Sum F) *' ) 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) *' ; ::_thesis: Sum G = (Sum F) *' A3: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_F,_G_being_FinSequence_of_F_Complex_st_len_F_=_len_G_&_len_F_=_k_+_1_&_(_for_i_being_Element_of_NAT_st_i_in_dom_G_holds_ G_/._i_=_(F_/._i)_*'_)_holds_ (Sum_F)_*'_=_Sum_G let F, G be FinSequence of F_Complex; ::_thesis: ( len F = len G & len F = k + 1 & ( for i being Element of NAT st i in dom G holds G /. i = (F /. i) *' ) implies (Sum F) *' = Sum G ) 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) *' ; ::_thesis: (Sum F) *' = Sum G set G1 = G | (Seg k); reconsider G1 = G | (Seg k) as FinSequence by FINSEQ_1:15; reconsider G1 = 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 = F | (Seg k) as FinSequence by FINSEQ_1:15; reconsider F1 = 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__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_G1_holds_ G1_/._i_=_(F1_/._i)_*' let i be Element of NAT ; ::_thesis: ( i in dom G1 implies G1 /. i = (F1 /. i) *' ) assume A16: i in dom G1 ; ::_thesis: G1 /. i = (F1 /. i) *' 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 ; ::_thesis: verum 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 ; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; now__::_thesis:_for_F,_G_being_FinSequence_of_F_Complex_st_len_F_=_len_G_&_len_F_=_0_&_(_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; ::_thesis: ( len F = len G & len F = 0 & ( for i being Element of NAT st i in dom G holds G /. i = (F /. i) *' ) implies Sum G = (Sum F) *' ) 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) *' ; ::_thesis: Sum G = (Sum F) *' 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; ::_thesis: verum end; then A22: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A22, A3); hence Sum G = (Sum F) *' by A1, A2; ::_thesis: verum end; theorem Th7: :: HURWITZ:7 for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for 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 non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for 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) let F1, F2 be FinSequence of L; ::_thesis: ( len F1 = len F2 & ( for i being Element of NAT st i in dom F1 holds F1 /. i = - (F2 /. i) ) implies Sum F1 = - (Sum F2) ) 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) ; ::_thesis: Sum F1 = - (Sum F2) defpred S1[ 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__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_f,_g_being_FinSequence_of_L_st_len_f_=_k_+_1_&_len_f_=_len_g_&_(_for_i_being_Element_of_NAT_st_i_in_dom_f_holds_ f_/._i_=_-_(g_/._i)_)_holds_ Sum_f_=_-_(Sum_g) let f, g be FinSequence of L; ::_thesis: ( len f = k + 1 & len f = len g & ( for i being Element of NAT st i in dom f holds f /. i = - (g /. i) ) implies Sum f = - (Sum g) ) 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) ; ::_thesis: Sum f = - (Sum g) set f1 = f | (Seg k); set g1 = g | (Seg k); reconsider f1 = f | (Seg k), g1 = g | (Seg k) as FinSequence by FINSEQ_1:15; reconsider f1 = f1, g1 = 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__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_f1_holds_ f1_/._i_=_-_(g1_/._i) A14: dom f1 c= dom f by A5, Lm1; let i be Element of NAT ; ::_thesis: ( i in dom f1 implies f1 /. i = - (g1 /. i) ) assume A15: i in dom f1 ; ::_thesis: f1 /. i = - (g1 /. i) 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 ; ::_thesis: verum 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 ; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; now__::_thesis:_for_f,_g_being_FinSequence_of_L_st_len_f_=_0_&_len_f_=_len_g_&_(_for_i_being_Element_of_NAT_st_i_in_dom_f_holds_ f_/._i_=_-_(g_/._i)_)_holds_ Sum_f_=_-_(Sum_g) let f, g be FinSequence of L; ::_thesis: ( len f = 0 & len f = len g & ( for i being Element of NAT st i in dom f holds f /. i = - (g /. i) ) implies Sum f = - (Sum g) ) 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) ; ::_thesis: Sum f = - (Sum g) 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 ; ::_thesis: verum end; then A21: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A21, A3); hence Sum F1 = - (Sum F2) by A1, A2; ::_thesis: verum end; theorem Th8: :: HURWITZ:8 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for x being Element of L for F being FinSequence of L holds x * (Sum F) = Sum (x * F) proof let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for x being Element of L for F being FinSequence of L holds x * (Sum F) = Sum (x * F) let x be Element of L; ::_thesis: for F being FinSequence of L holds x * (Sum F) = Sum (x * F) let F be FinSequence of L; ::_thesis: x * (Sum F) = Sum (x * F) defpred S1[ Nat] means for x being Element of L for F being FinSequence of L st len F = $1 holds x * (Sum F) = Sum (x * F); A1: ex n being Element of NAT st len F = n ; A2: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_x_being_Element_of_L for_F_being_FinSequence_of_L_st_len_F_=_k_+_1_holds_ x_*_(Sum_F)_=_Sum_(x_*_F) let x be Element of L; ::_thesis: for F being FinSequence of L st len F = k + 1 holds x * (Sum F) = Sum (x * F) let F be FinSequence of L; ::_thesis: ( len F = k + 1 implies x * (Sum F) = Sum (x * F) ) set G = F | (Seg k); reconsider G = F | (Seg k) as FinSequence by FINSEQ_1:15; assume A4: len F = k + 1 ; ::_thesis: x * (Sum F) = Sum (x * F) then reconsider G = 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 ; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; now__::_thesis:_for_x_being_Element_of_L for_F_being_FinSequence_of_L_st_len_F_=_0_holds_ x_*_(Sum_F)_=_Sum_(x_*_F) let x be Element of L; ::_thesis: for F being FinSequence of L st len F = 0 holds x * (Sum F) = Sum (x * F) let F be FinSequence of L; ::_thesis: ( len F = 0 implies x * (Sum F) = Sum (x * F) ) assume A7: len F = 0 ; ::_thesis: x * (Sum F) = Sum (x * F) 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; ::_thesis: verum end; then A9: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A9, A2); hence x * (Sum F) = Sum (x * F) by A1; ::_thesis: verum end; begin Lm3: for L being non empty right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of L holds - (- p) = p proof let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of L holds - (- p) = p let p be Polynomial of L; ::_thesis: - (- p) = p A1: now__::_thesis:_for_x_being_Nat_st_x_<_len_p_holds_ (-_(-_p))_._x_=_p_._x let x be Nat; ::_thesis: ( x < len p implies (- (- p)) . x = p . x ) assume x < len p ; ::_thesis: (- (- p)) . x = p . x 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 ; ::_thesis: verum end; len p = len (- p) by POLYNOM4:8 .= len (- (- p)) by POLYNOM4:8 ; hence - (- p) = p by A1, ALGSEQ_1:12; ::_thesis: verum end; theorem Th9: :: HURWITZ:9 for L being non empty right_complementable add-associative right_zeroed addLoopStr holds - (0_. L) = 0_. L proof let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: - (0_. L) = 0_. L set e = 0_. L; set f = - (0_. L); A1: for x being Nat st x < len (0_. L) holds (0_. L) . x = (- (0_. L)) . x by POLYNOM4:3; len (- (0_. L)) = len (0_. L) by POLYNOM4:8; hence - (0_. L) = 0_. L by A1, ALGSEQ_1:12; ::_thesis: verum end; Lm4: for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for p being Polynomial of L for f being Element of (Polynom-Ring L) st f = p holds - f = - p proof let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L for f being Element of (Polynom-Ring L) st f = p holds - f = - p let p be Polynomial of L; ::_thesis: for f being Element of (Polynom-Ring L) st f = p holds - f = - p let f be Element of (Polynom-Ring L); ::_thesis: ( f = p implies - f = - p ) reconsider x = - p as Element of (Polynom-Ring L) by POLYNOM3:def_10; reconsider x = x as Element of (Polynom-Ring L) ; assume f = p ; ::_thesis: - 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 - f = - p by RLVECT_1:17; ::_thesis: verum end; theorem :: HURWITZ:10 for L being non empty right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of L holds - (- p) = p by Lm3; theorem Th11: :: HURWITZ:11 for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr for p1, p2 being Polynomial of L holds - (p1 + p2) = (- p1) + (- p2) proof let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p1, p2 being Polynomial of L holds - (p1 + p2) = (- p1) + (- p2) let p1, p2 be Polynomial of L; ::_thesis: - (p1 + p2) = (- p1) + (- p2) 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 - (p1 + p2) = (- p1) + (- p2) by A3, A2, A1, POLYNOM3:def_10; ::_thesis: verum end; theorem Th12: :: HURWITZ:12 for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr for p1, p2 being Polynomial of L holds ( - (p1 *' p2) = (- p1) *' p2 & - (p1 *' p2) = p1 *' (- p2) ) proof let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p1, p2 being Polynomial of L holds ( - (p1 *' p2) = (- p1) *' p2 & - (p1 *' p2) = p1 *' (- p2) ) let p1, p2 be Polynomial of L; ::_thesis: ( - (p1 *' p2) = (- p1) *' p2 & - (p1 *' p2) = p1 *' (- p2) ) 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; ::_thesis: - (p1 *' p2) = p1 *' (- p2) - p2 = - p29 by Lm4; then p1 *' (- p2) = p19 * (- p29) by POLYNOM3:def_10; hence - (p1 *' p2) = p1 *' (- p2) by A1, VECTSP_1:8; ::_thesis: verum end; definition let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; let F be FinSequence of (Polynom-Ring L); let i be Element of NAT ; func Coeff (F,i) -> FinSequence of L means :Def1: :: HURWITZ:def 1 ( len it = len F & ( for j being Element of NAT st j in dom it holds ex p being Polynomial of L st ( p = F . j & it . j = p . i ) ) ); existence ex b1 being FinSequence of L st ( len b1 = len F & ( for j being Element of NAT st j in dom b1 holds ex p being Polynomial of L st ( p = F . j & b1 . j = p . i ) ) ) proof defpred S1[ 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) holds ex x being Element of the carrier of L st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len F) implies ex x being Element of the carrier of L st S1[k,x] ) assume A2: k in Seg (len F) ; ::_thesis: ex x being Element of the carrier of L st S1[k,x] reconsider t = F /. k as Polynomial of L by POLYNOM3:def_10; take t . i ; ::_thesis: S1[k,t . i] take t ; ::_thesis: ( t = F . k & t . i = t . i ) k in dom F by A2, FINSEQ_1:def_3; hence t = F . k by PARTFUN1:def_6; ::_thesis: t . i = t . i thus t . i = t . i ; ::_thesis: verum 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 S1[k,G . k] ) ) from FINSEQ_1:sch_5(A1); take G ; ::_thesis: ( len G = len F & ( for j being Element of NAT st j in dom G holds ex p being Polynomial of L st ( p = F . j & G . j = p . i ) ) ) thus len G = len F by A3, FINSEQ_1:def_3; ::_thesis: for j being Element of NAT st j in dom G holds ex p being Polynomial of L st ( p = F . j & G . j = p . i ) thus for j being Element of NAT st j in dom G holds ex p being Polynomial of L st ( p = F . j & G . j = p . i ) by A3; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of L st len b1 = len F & ( for j being Element of NAT st j in dom b1 holds ex p being Polynomial of L st ( p = F . j & b1 . j = p . i ) ) & len b2 = len F & ( for j being Element of NAT st j in dom b2 holds ex p being Polynomial of L st ( p = F . j & b2 . j = p . i ) ) holds b1 = b2 proof let z1, z2 be FinSequence of L; ::_thesis: ( len z1 = len F & ( for j being Element of NAT st j in dom z1 holds ex p being Polynomial of L st ( p = F . j & z1 . j = p . i ) ) & len z2 = len F & ( for j being Element of NAT st j in dom z2 holds ex p being Polynomial of L st ( p = F . j & z2 . j = p . i ) ) implies z1 = z2 ) assume that A4: len z1 = len F and A5: for j being Element of NAT st j in dom z1 holds ex p being Polynomial of L st ( p = F . j & z1 . j = p . i ) ; ::_thesis: ( not len z2 = len F or ex j being Element of NAT st ( j in dom z2 & ( for p being Polynomial of L holds ( not p = F . j or not z2 . j = p . i ) ) ) or z1 = z2 ) assume that A6: len z2 = len F and A7: for j being Element of NAT st j in dom z2 holds ex p being Polynomial of L st ( p = F . j & z2 . j = p . i ) ; ::_thesis: z1 = z2 A8: dom z1 = Seg (len F) by A4, FINSEQ_1:def_3 .= dom z2 by A6, FINSEQ_1:def_3 ; now__::_thesis:_for_k_being_Nat_st_k_in_dom_z1_holds_ z1_._k_=_z2_._k let k be Nat; ::_thesis: ( k in dom z1 implies z1 . k = z2 . k ) assume A9: k in dom z1 ; ::_thesis: z1 . k = z2 . k 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; ::_thesis: verum end; hence z1 = z2 by A8, FINSEQ_1:13; ::_thesis: verum end; end; :: deftheorem Def1 defines Coeff HURWITZ:def_1_:_ for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for F being FinSequence of (Polynom-Ring L) for i being Element of NAT for b4 being FinSequence of L holds ( b4 = Coeff (F,i) iff ( len b4 = len F & ( for j being Element of NAT st j in dom b4 holds ex p being Polynomial of L st ( p = F . j & b4 . j = p . i ) ) ) ); theorem Th13: :: HURWITZ:13 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for p being Polynomial of L for F being FinSequence of (Polynom-Ring L) st p = Sum F holds for i being Element of NAT holds p . i = Sum (Coeff (F,i)) proof let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L for F being FinSequence of (Polynom-Ring L) st p = Sum F holds for i being Element of NAT holds p . i = Sum (Coeff (F,i)) let p be Polynomial of L; ::_thesis: for F being FinSequence of (Polynom-Ring L) st p = Sum F holds for i being Element of NAT holds p . i = Sum (Coeff (F,i)) let F be FinSequence of (Polynom-Ring L); ::_thesis: ( p = Sum F implies for i being Element of NAT holds p . i = Sum (Coeff (F,i)) ) assume A1: p = Sum F ; ::_thesis: for i being Element of NAT holds p . i = Sum (Coeff (F,i)) defpred S1[ Nat] means for p being Polynomial of L for F being FinSequence of (Polynom-Ring L) st p = Sum F & len F = $1 holds for i being Element of NAT holds p . i = Sum (Coeff (F,i)); let i be Element of NAT ; ::_thesis: p . i = Sum (Coeff (F,i)) A2: ex m being Nat st len F = m ; A3: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_p_being_Polynomial_of_L for_F_being_FinSequence_of_(Polynom-Ring_L)_st_p_=_Sum_F_&_len_F_=_k_+_1_holds_ for_i_being_Element_of_NAT_holds_p_._i_=_Sum_(Coeff_(F,i)) let p be Polynomial of L; ::_thesis: for F being FinSequence of (Polynom-Ring L) st p = Sum F & len F = k + 1 holds for i being Element of NAT holds p . i = Sum (Coeff (F,i)) let F be FinSequence of (Polynom-Ring L); ::_thesis: ( p = Sum F & len F = k + 1 implies for i being Element of NAT holds p . i = Sum (Coeff (F,i)) ) assume that A5: p = Sum F and A6: len F = k + 1 ; ::_thesis: for i being Element of NAT holds p . i = Sum (Coeff (F,i)) reconsider rf = F /. (k + 1) as Polynomial of L by POLYNOM3:def_10; let i be Element of NAT ; ::_thesis: p . i = Sum (Coeff (F,i)) set G = F | (Seg k); reconsider G = F | (Seg k) as FinSequence by FINSEQ_1:15; reconsider G = 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__::_thesis:_for_j_being_Nat_st_j_in_dom_(Coeff_(F,i))_holds_ (Coeff_(F,i))_._j_=_((Coeff_(G,i))_^_<*(rf_._i)*>)_._j 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; ::_thesis: ( j in dom (Coeff (F,i)) implies (Coeff (F,i)) . b1 = ((Coeff (G,i)) ^ <*(rf . i)*>) . b1 ) assume A11: j in dom (Coeff (F,i)) ; ::_thesis: (Coeff (F,i)) . b1 = ((Coeff (G,i)) ^ <*(rf . i)*>) . b1 percases ( j in dom (Coeff (G,i)) or not j in dom (Coeff (G,i)) ) ; supposeA12: j in dom (Coeff (G,i)) ; ::_thesis: (Coeff (F,i)) . b1 = ((Coeff (G,i)) ^ <*(rf . i)*>) . b1 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; ::_thesis: verum end; supposeA15: not j in dom (Coeff (G,i)) ; ::_thesis: (Coeff (F,i)) . b1 = ((Coeff (G,i)) ^ <*(rf . i)*>) . b1 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__::_thesis:_not_j_<_k_+_1 assume j < k + 1 ; ::_thesis: contradiction then j <= k by NAT_1:13; then j in Seg k by A11, A17; hence contradiction by A8, A10, A15, FINSEQ_1:17; ::_thesis: verum 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, FINSEQ_1: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; ::_thesis: verum end; 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 ; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; now__::_thesis:_for_p_being_Polynomial_of_L for_F_being_FinSequence_of_(Polynom-Ring_L)_st_p_=_Sum_F_&_len_F_=_0_holds_ for_i_being_Element_of_NAT_holds_p_._i_=_Sum_(Coeff_(F,i)) let p be Polynomial of L; ::_thesis: for F being FinSequence of (Polynom-Ring L) st p = Sum F & len F = 0 holds for i being Element of NAT holds p . i = Sum (Coeff (F,i)) let F be FinSequence of (Polynom-Ring L); ::_thesis: ( p = Sum F & len F = 0 implies for i being Element of NAT holds p . i = Sum (Coeff (F,i)) ) assume that A24: p = Sum F and A25: len F = 0 ; ::_thesis: for i being Element of NAT holds p . i = Sum (Coeff (F,i)) let i be Element of NAT ; ::_thesis: p . i = Sum (Coeff (F,i)) 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; ::_thesis: verum end; then A27: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A27, A3); hence p . i = Sum (Coeff (F,i)) by A1, A2; ::_thesis: verum end; Lm5: for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr for p1, p2 being Polynomial of L for p29 being Element of (Polynom-Ring L) st p29 = p2 holds for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds p2 *' p1 = Sum (p29 * F) proof let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p1, p2 being Polynomial of L for p29 being Element of (Polynom-Ring L) st p29 = p2 holds for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds p2 *' p1 = Sum (p29 * F) let p1, p2 be Polynomial of L; ::_thesis: for p29 being Element of (Polynom-Ring L) st p29 = p2 holds for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds p2 *' p1 = Sum (p29 * F) let p29 be Element of (Polynom-Ring L); ::_thesis: ( p29 = p2 implies for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds p2 *' p1 = Sum (p29 * F) ) assume A1: p29 = p2 ; ::_thesis: for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds p2 *' p1 = Sum (p29 * F) reconsider p19 = p1 as Element of (Polynom-Ring L) by POLYNOM3:def_10; let F be FinSequence of (Polynom-Ring L); ::_thesis: ( p1 = Sum F implies p2 *' p1 = Sum (p29 * F) ) assume p1 = Sum F ; ::_thesis: p2 *' p1 = Sum (p29 * F) then p29 * p19 = Sum (p29 * F) by Th8; hence p2 *' p1 = Sum (p29 * F) by A1, POLYNOM3:def_10; ::_thesis: verum end; theorem Th14: :: HURWITZ:14 for L being non empty associative 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 non empty associative doubleLoopStr ; ::_thesis: for p being Polynomial of L for x1, x2 being Element of L holds x1 * (x2 * p) = (x1 * x2) * p let p be Polynomial of L; ::_thesis: for x1, x2 being Element of L holds x1 * (x2 * p) = (x1 * x2) * p let x1, x2 be Element of L; ::_thesis: x1 * (x2 * p) = (x1 * x2) * p set f = x1 * (x2 * p); set g = (x1 * x2) * p; A1: now__::_thesis:_for_i9_being_set_st_i9_in_dom_(x1_*_(x2_*_p))_holds_ (x1_*_(x2_*_p))_._i9_=_((x1_*_x2)_*_p)_._i9 let i9 be set ; ::_thesis: ( i9 in dom (x1 * (x2 * p)) implies (x1 * (x2 * p)) . i9 = ((x1 * x2) * p) . i9 ) assume i9 in dom (x1 * (x2 * p)) ; ::_thesis: (x1 * (x2 * p)) . i9 = ((x1 * x2) * p) . i9 then reconsider i = i9 as Element of NAT ; (x1 * (x2 * p)) . 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 .= ((x1 * x2) * p) . i by POLYNOM5:def_3 ; hence (x1 * (x2 * p)) . i9 = ((x1 * x2) * p) . i9 ; ::_thesis: verum end; dom (x1 * (x2 * p)) = NAT by FUNCT_2:def_1 .= dom ((x1 * x2) * p) by FUNCT_2:def_1 ; hence x1 * (x2 * p) = (x1 * x2) * p by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th15: :: HURWITZ:15 for L being non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr for p being Polynomial of L for x being Element of L holds - (x * p) = (- x) * p proof let L be non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L for x being Element of L holds - (x * p) = (- x) * p let p be Polynomial of L; ::_thesis: for x being Element of L holds - (x * p) = (- x) * p let x be Element of L; ::_thesis: - (x * p) = (- x) * p set f = - (x * p); set g = (- x) * p; A1: now__::_thesis:_for_i9_being_set_st_i9_in_dom_(-_(x_*_p))_holds_ (-_(x_*_p))_._i9_=_((-_x)_*_p)_._i9 let i9 be set ; ::_thesis: ( i9 in dom (- (x * p)) implies (- (x * p)) . i9 = ((- x) * p) . i9 ) assume i9 in dom (- (x * p)) ; ::_thesis: (- (x * p)) . i9 = ((- x) * p) . i9 then reconsider i = i9 as Element of NAT ; (- (x * p)) . i = - ((x * p) . i) by BHSP_1:44 .= - (x * (p . i)) by POLYNOM5:def_3 .= (- x) * (p . i) by VECTSP_1:9 .= ((- x) * p) . i by POLYNOM5:def_3 ; hence (- (x * p)) . i9 = ((- x) * p) . i9 ; ::_thesis: verum end; dom (- (x * p)) = NAT by FUNCT_2:def_1 .= dom ((- x) * p) by FUNCT_2:def_1 ; hence - (x * p) = (- x) * p by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th16: :: HURWITZ:16 for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr for p being Polynomial of L for x being Element of L holds - (x * p) = x * (- p) proof let L be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L for x being Element of L holds - (x * p) = x * (- p) let p be Polynomial of L; ::_thesis: for x being Element of L holds - (x * p) = x * (- p) let x be Element of L; ::_thesis: - (x * p) = x * (- p) set f = - (x * p); set g = x * (- p); A1: now__::_thesis:_for_i9_being_set_st_i9_in_dom_(-_(x_*_p))_holds_ (-_(x_*_p))_._i9_=_(x_*_(-_p))_._i9 let i9 be set ; ::_thesis: ( i9 in dom (- (x * p)) implies (- (x * p)) . i9 = (x * (- p)) . i9 ) assume i9 in dom (- (x * p)) ; ::_thesis: (- (x * p)) . i9 = (x * (- p)) . i9 then reconsider i = i9 as Element of NAT ; (- (x * p)) . 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 .= (x * (- p)) . i by POLYNOM5:def_3 ; hence (- (x * p)) . i9 = (x * (- p)) . i9 ; ::_thesis: verum end; dom (- (x * p)) = NAT by FUNCT_2:def_1 .= dom (x * (- p)) by FUNCT_2:def_1 ; hence - (x * p) = x * (- p) by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th17: :: HURWITZ:17 for L being non empty left-distributive 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 non empty left-distributive doubleLoopStr ; ::_thesis: for p being Polynomial of L for x1, x2 being Element of L holds (x1 + x2) * p = (x1 * p) + (x2 * p) let p be Polynomial of L; ::_thesis: for x1, x2 being Element of L holds (x1 + x2) * p = (x1 * p) + (x2 * p) let x1, x2 be Element of L; ::_thesis: (x1 + x2) * p = (x1 * p) + (x2 * p) set f = (x1 + x2) * p; set g = (x1 * p) + (x2 * p); A1: now__::_thesis:_for_i9_being_set_st_i9_in_dom_((x1_+_x2)_*_p)_holds_ ((x1_+_x2)_*_p)_._i9_=_((x1_*_p)_+_(x2_*_p))_._i9 let i9 be set ; ::_thesis: ( i9 in dom ((x1 + x2) * p) implies ((x1 + x2) * p) . i9 = ((x1 * p) + (x2 * p)) . i9 ) assume i9 in dom ((x1 + x2) * p) ; ::_thesis: ((x1 + x2) * p) . i9 = ((x1 * p) + (x2 * p)) . i9 then reconsider i = i9 as Element of NAT ; ((x1 + x2) * p) . 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 .= ((x1 * p) + (x2 * p)) . i by NORMSP_1:def_2 ; hence ((x1 + x2) * p) . i9 = ((x1 * p) + (x2 * p)) . i9 ; ::_thesis: verum end; dom ((x1 + x2) * p) = NAT by FUNCT_2:def_1 .= dom ((x1 * p) + (x2 * p)) by FUNCT_2:def_1 ; hence (x1 + x2) * p = (x1 * p) + (x2 * p) by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th18: :: HURWITZ:18 for L being non empty right-distributive 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 non empty right-distributive doubleLoopStr ; ::_thesis: for p1, p2 being Polynomial of L for x being Element of L holds x * (p1 + p2) = (x * p1) + (x * p2) let p1, p2 be Polynomial of L; ::_thesis: for x being Element of L holds x * (p1 + p2) = (x * p1) + (x * p2) let x be Element of L; ::_thesis: x * (p1 + p2) = (x * p1) + (x * p2) set f = x * (p1 + p2); set g = (x * p1) + (x * p2); A1: now__::_thesis:_for_i9_being_set_st_i9_in_dom_(x_*_(p1_+_p2))_holds_ (x_*_(p1_+_p2))_._i9_=_((x_*_p1)_+_(x_*_p2))_._i9 let i9 be set ; ::_thesis: ( i9 in dom (x * (p1 + p2)) implies (x * (p1 + p2)) . i9 = ((x * p1) + (x * p2)) . i9 ) assume i9 in dom (x * (p1 + p2)) ; ::_thesis: (x * (p1 + p2)) . i9 = ((x * p1) + (x * p2)) . i9 then reconsider i = i9 as Element of NAT ; (x * (p1 + p2)) . 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 .= ((x * p1) + (x * p2)) . i by NORMSP_1:def_2 ; hence (x * (p1 + p2)) . i9 = ((x * p1) + (x * p2)) . i9 ; ::_thesis: verum end; dom (x * (p1 + p2)) = NAT by FUNCT_2:def_1 .= dom ((x * p1) + (x * p2)) by FUNCT_2:def_1 ; hence x * (p1 + p2) = (x * p1) + (x * p2) by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th19: :: HURWITZ:19 for L being non empty right_complementable associative commutative distributive add-associative right_zeroed 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 non empty right_complementable associative commutative distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p1, p2 being Polynomial of L for x being Element of L holds p1 *' (x * p2) = x * (p1 *' p2) let p1, p2 be Polynomial of L; ::_thesis: for x being Element of L holds p1 *' (x * p2) = x * (p1 *' p2) let x be Element of L; ::_thesis: p1 *' (x * p2) = x * (p1 *' p2) set f = p1 *' (x * p2); set g = x * (p1 *' p2); A1: now__::_thesis:_for_i9_being_set_st_i9_in_dom_(p1_*'_(x_*_p2))_holds_ (p1_*'_(x_*_p2))_._i9_=_(x_*_(p1_*'_p2))_._i9 let i9 be set ; ::_thesis: ( i9 in dom (p1 *' (x * p2)) implies (p1 *' (x * p2)) . i9 = (x * (p1 *' p2)) . i9 ) assume i9 in dom (p1 *' (x * p2)) ; ::_thesis: (p1 *' (x * p2)) . i9 = (x * (p1 *' p2)) . i9 then reconsider i = i9 as Element of NAT ; consider rf being FinSequence of L such that A2: len rf = i + 1 and A3: (p1 *' (x * p2)) . i = Sum rf and A4: for k being 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 being 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__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_rf_holds_ (x_*_rp)_._j_=_rf_._j let j be Nat; ::_thesis: ( 1 <= j & j <= len rf implies (x * rp) . j = rf . j ) assume that A12: 1 <= j and A13: j <= len rf ; ::_thesis: (x * rp) . j = rf . j 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 ; ::_thesis: verum end; (x * (p1 *' p2)) . i = x * (Sum rp) by A6, POLYNOM5:def_3 .= Sum (x * rp) by Th8 .= (p1 *' (x * p2)) . i by A2, A3, A5, A8, A11, FINSEQ_1:6, FINSEQ_1:14 ; hence (p1 *' (x * p2)) . i9 = (x * (p1 *' p2)) . i9 ; ::_thesis: verum end; dom (p1 *' (x * p2)) = NAT by FUNCT_2:def_1 .= dom (x * (p1 *' p2)) by FUNCT_2:def_1 ; hence p1 *' (x * p2) = x * (p1 *' p2) by A1, FUNCT_1:2; ::_thesis: verum end; definition let L be non empty ZeroStr ; let p be Polynomial of L; func degree p -> Integer equals :: HURWITZ:def 2 (len p) - 1; coherence (len p) - 1 is Integer ; end; :: deftheorem defines degree HURWITZ:def_2_:_ for L being non empty ZeroStr for p being Polynomial of L holds degree p = (len p) - 1; 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 for s being AlgSequence of L st len s > 0 holds s . ((len s) - 1) <> 0. L proof let L be non empty ZeroStr ; ::_thesis: for s being AlgSequence of L st len s > 0 holds s . ((len s) - 1) <> 0. L let s be AlgSequence of L; ::_thesis: ( len s > 0 implies s . ((len s) - 1) <> 0. L ) assume len s > 0 ; ::_thesis: s . ((len s) - 1) <> 0. L 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 ; ::_thesis: contradiction now__::_thesis:_for_i_being_Nat_st_i_>=_l_holds_ s_._i_=_0._L let i be Nat; ::_thesis: ( i >= l implies s . b1 = 0. L ) assume A2: i >= l ; ::_thesis: s . b1 = 0. L percases ( i = l or i > l ) by A2, XXREAL_0:1; suppose i = l ; ::_thesis: s . b1 = 0. L hence s . i = 0. L by A1; ::_thesis: verum end; suppose i > l ; ::_thesis: s . b1 = 0. L then i >= l + 1 by NAT_1:13; hence s . i = 0. L by ALGSEQ_1:8; ::_thesis: verum end; 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; ::_thesis: verum end; theorem Th20: :: HURWITZ:20 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 ; ::_thesis: for p being Polynomial of L holds ( deg p = - 1 iff p = 0_. L ) let p be Polynomial of L; ::_thesis: ( deg p = - 1 iff p = 0_. L ) now__::_thesis:_(_p_=_0_._L_implies_deg_p_=_-_1_) assume p = 0_. L ; ::_thesis: deg p = - 1 then len p = 0 by POLYNOM4:3; hence deg p = - 1 ; ::_thesis: verum end; hence ( deg p = - 1 iff p = 0_. L ) by POLYNOM4:5; ::_thesis: verum end; Lm7: for L being non empty ZeroStr for p being Polynomial of L st deg p <> - 1 holds p . (deg p) <> 0. L proof let L be non empty ZeroStr ; ::_thesis: for p being Polynomial of L st deg p <> - 1 holds p . (deg p) <> 0. L let p be Polynomial of L; ::_thesis: ( deg p <> - 1 implies p . (deg p) <> 0. L ) assume deg p <> - 1 ; ::_thesis: p . (deg p) <> 0. L then len p <> 0 ; hence p . (deg p) <> 0. L by Lm6; ::_thesis: verum 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 ; ::_thesis: for p being Polynomial of L holds ( deg p is Element of NAT iff p <> 0_. L ) let p be Polynomial of L; ::_thesis: ( deg p is Element of NAT iff p <> 0_. L ) now__::_thesis:_(_p_<>_0_._L_implies_deg_p_is_Element_of_NAT_) assume p <> 0_. L ; ::_thesis: deg p is Element of NAT 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; ::_thesis: verum end; hence ( deg p is Element of NAT iff p <> 0_. L ) by Th20; ::_thesis: verum end; theorem :: HURWITZ:21 for L being non empty right_complementable add-associative right_zeroed 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 non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p1, p2 being Polynomial of L st deg p1 <> deg p2 holds deg (p1 + p2) = max ((deg p1),(deg p2)) let p1, p2 be Polynomial of L; ::_thesis: ( deg p1 <> deg p2 implies deg (p1 + p2) = max ((deg p1),(deg p2)) ) assume deg p1 <> deg p2 ; ::_thesis: deg (p1 + p2) = max ((deg p1),(deg p2)) then A1: deg (p1 + p2) = (max ((len p1),(len p2))) - 1 by POLYNOM4:7; percases ( max ((len p1),(len p2)) = len p1 or max ((len p1),(len p2)) = len p2 ) by XXREAL_0:16; supposeA2: max ((len p1),(len p2)) = len p1 ; ::_thesis: deg (p1 + p2) = max ((deg p1),(deg p2)) then len p2 <= len p1 by XXREAL_0:25; then deg p2 <= deg p1 by XREAL_1:9; hence deg (p1 + p2) = max ((deg p1),(deg p2)) by A1, A2, XXREAL_0:def_10; ::_thesis: verum end; supposeA3: max ((len p1),(len p2)) = len p2 ; ::_thesis: deg (p1 + p2) = max ((deg p1),(deg p2)) then len p1 <= len p2 by XXREAL_0:25; then deg p1 <= deg p2 by XREAL_1:9; hence deg (p1 + p2) = max ((deg p1),(deg p2)) by A1, A3, XXREAL_0:def_10; ::_thesis: verum end; end; end; Lm9: for L being non empty ZeroStr for p being Polynomial of L holds deg p >= - 1 proof let L be non empty ZeroStr ; ::_thesis: for p being Polynomial of L holds deg p >= - 1 let p be Polynomial of L; ::_thesis: deg p >= - 1 percases ( p = 0_. L or p <> 0_. L ) ; suppose p = 0_. L ; ::_thesis: deg p >= - 1 hence deg p >= - 1 by Th20; ::_thesis: verum end; suppose p <> 0_. L ; ::_thesis: deg p >= - 1 hence deg p >= - 1 by Lm8; ::_thesis: verum end; end; end; theorem Th22: :: HURWITZ:22 for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for p1, p2 being Polynomial of L holds deg (p1 + p2) <= max ((deg p1),(deg p2)) proof let L be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for p1, p2 being Polynomial of L holds deg (p1 + p2) <= max ((deg p1),(deg p2)) let p1, p2 be Polynomial of L; ::_thesis: deg (p1 + p2) <= max ((deg p1),(deg p2)) percases ( p1 = 0_. L or p2 = 0_. L or ( p1 <> 0_. L & p2 <> 0_. L ) ) ; supposeA1: p1 = 0_. L ; ::_thesis: deg (p1 + p2) <= max ((deg p1),(deg p2)) 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 deg (p1 + p2) <= max ((deg p1),(deg p2)) ; ::_thesis: verum end; supposeA3: p2 = 0_. L ; ::_thesis: deg (p1 + p2) <= max ((deg p1),(deg p2)) 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 deg (p1 + p2) <= max ((deg p1),(deg p2)) ; ::_thesis: verum end; supposeA5: ( p1 <> 0_. L & p2 <> 0_. L ) ; ::_thesis: deg (p1 + p2) <= max ((deg p1),(deg p2)) 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; ::_thesis: ( k >= m + 1 implies (p1 + p2) . k = 0. L ) assume A7: k >= m + 1 ; ::_thesis: (p1 + p2) . k = 0. L 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 ; ::_thesis: verum 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 deg (p1 + p2) <= max ((deg p1),(deg p2)) ; ::_thesis: verum end; end; end; theorem Th23: :: HURWITZ:23 for L being non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed domRing-like 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 non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p1, p2 being Polynomial of L st p1 <> 0_. L & p2 <> 0_. L holds deg (p1 *' p2) = (deg p1) + (deg p2) let p1, p2 be Polynomial of L; ::_thesis: ( p1 <> 0_. L & p2 <> 0_. L implies deg (p1 *' p2) = (deg p1) + (deg p2) ) assume that A1: p1 <> 0_. L and A2: p2 <> 0_. L ; ::_thesis: deg (p1 *' p2) = (deg p1) + (deg p2) 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) ; ::_thesis: verum end; theorem Th24: :: HURWITZ:24 for L being non empty right_complementable unital add-associative right_zeroed doubleLoopStr for p being Polynomial of L st deg p = 0 holds not p is with_roots proof let L be non empty right_complementable unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L st deg p = 0 holds not p is with_roots let p be Polynomial of L; ::_thesis: ( deg p = 0 implies not p is with_roots ) assume A1: deg p = 0 ; ::_thesis: not p is with_roots then A2: p = <%(p . 0)%> by ALGSEQ_1:def_5; now__::_thesis:_not_p_is_with_roots assume p is with_roots ; ::_thesis: contradiction then consider x being 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; ::_thesis: verum end; hence not p is with_roots ; ::_thesis: verum end; Lm10: for L being non empty unital doubleLoopStr for z being Element of L for k being 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 non empty unital doubleLoopStr ; ::_thesis: for z being Element of L for k being 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 ) let z be Element of L; ::_thesis: for k being 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 ) let k be Element of NAT ; ::_thesis: ( k <> 0 implies ( ((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 ) ) assume A1: k <> 0 ; ::_thesis: ( ((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 ) set t = (0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L))); set f = (0,k) --> ((- ((power L) . (z,k))),(1_ L)); set a = - ((power L) . (z,k)); A2: dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) = {0,k} by FUNCT_4:62; now__::_thesis:_for_u_being_set_st_u_in_{0,k}_holds_ u_in_NAT let u be set ; ::_thesis: ( u in {0,k} implies u in NAT ) assume u in {0,k} ; ::_thesis: u in NAT then ( u = 0 or u = k ) by TARSKI:def_2; hence u in NAT ; ::_thesis: verum 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 ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) = NAT by A2, A3, XBOOLE_1:12; 0 in dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) by A2, TARSKI:def_2; hence ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . 0 = ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) . 0 by A4, FUNCT_4:def_1 .= - ((power L) . (z,k)) by A1, FUNCT_4:63 ; ::_thesis: ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . k = 1_ L k in dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) by A2, TARSKI:def_2; hence ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . k = ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) . k by A4, FUNCT_4:def_1 .= 1_ L by FUNCT_4:63 ; ::_thesis: verum end; Lm11: for L being non empty unital doubleLoopStr for z being Element of L for k being Element of NAT for 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 non empty unital doubleLoopStr ; ::_thesis: for z being Element of L for k being Element of NAT for i being Nat st i <> 0 & i <> k holds ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . i = 0. L let z be Element of L; ::_thesis: for k being Element of NAT for i being Nat st i <> 0 & i <> k holds ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . i = 0. L let k be Element of NAT ; ::_thesis: for i being Nat st i <> 0 & i <> k holds ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . i = 0. L let i be Nat; ::_thesis: ( i <> 0 & i <> k implies ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . i = 0. L ) assume that A1: i <> 0 and A2: i <> k ; ::_thesis: ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . i = 0. L set t = (0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L))); set f = (0,k) --> ((- ((power L) . (z,k))),(1_ L)); A3: dom (0_. L) = NAT by FUNCT_2:def_1; now__::_thesis:_for_u_being_set_st_u_in_{0,k}_holds_ u_in_NAT let u be set ; ::_thesis: ( u in {0,k} implies u in NAT ) assume u in {0,k} ; ::_thesis: u in NAT then ( u = 0 or u = k ) by TARSKI:def_2; hence u in NAT ; ::_thesis: verum end; then A4: {0,k} c= NAT by TARSKI:def_3; dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) = {0,k} by FUNCT_4:62; then A5: (dom (0_. L)) \/ (dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) = NAT by A3, A4, XBOOLE_1:12; A6: i in NAT by ORDINAL1:def_12; not i in dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) by A1, A2, TARSKI:def_2; hence ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . i = (0_. L) . i by A5, A6, FUNCT_4:def_1 .= 0. L by A6, FUNCOP_1:7 ; ::_thesis: verum end; definition let L be non empty unital doubleLoopStr ; let z be Element of L; let k be Element of NAT ; func rpoly (k,z) -> Polynomial of L equals :: HURWITZ:def 3 (0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L))); coherence (0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) is Polynomial of L proof now__::_thesis:_for_u_being_set_st_u_in_{0,k}_holds_ u_in_NAT let u be set ; ::_thesis: ( u in {0,k} implies u in NAT ) assume u in {0,k} ; ::_thesis: u in NAT then ( u = 0 or u = k ) by TARSKI:def_2; hence u in NAT ; ::_thesis: verum 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 ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) = {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__::_thesis:_for_x9_being_set_st_x9_in_NAT_holds_ ((0_._L)_+*_((0,k)_-->_((-_((power_L)_._(z,k))),(1__L))))_._x9_in_the_carrier_of_L let x9 be set ; ::_thesis: ( x9 in NAT implies ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . b1 in the carrier of L ) assume x9 in NAT ; ::_thesis: ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . b1 in the carrier of L then reconsider x = x9 as Element of NAT ; percases ( ( k = 0 & x = 0 ) or ( x = 0 & k <> 0 ) or ( x = k & k <> 0 ) or ( x <> 0 & x <> k ) ) ; supposeA6: ( k = 0 & x = 0 ) ; ::_thesis: ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . b1 in the carrier of L then x in dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) by A2, TARSKI:def_2; then ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . x = ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) . x by FUNCT_4:13 .= ((0 .--> (- ((power L) . (z,k)))) +* (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 ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . x9 in the carrier of L ; ::_thesis: verum end; suppose ( x = 0 & k <> 0 ) ; ::_thesis: ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . b1 in the carrier of L then ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . x = - ((power L) . (z,k)) by Lm10; hence ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . x9 in the carrier of L ; ::_thesis: verum end; suppose ( x = k & k <> 0 ) ; ::_thesis: ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . b1 in the carrier of L then ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . x = 1_ L by Lm10; hence ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . x9 in the carrier of L ; ::_thesis: verum end; suppose ( x <> 0 & x <> k ) ; ::_thesis: ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . b1 in the carrier of L then ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . x = 0. L by Lm11; hence ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . x9 in the carrier of L ; ::_thesis: verum end; end; end; dom (0_. L) = NAT by FUNCT_2:def_1; then (dom (0_. L)) \/ (dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) = NAT by A2, A1, XBOOLE_1:12; then dom ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) = NAT by FUNCT_4:def_1; then reconsider p = (0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) as Function of NAT, the carrier of L by A5, FUNCT_2:3; reconsider p = p as sequence of L ; now__::_thesis:_for_i_being_Nat_st_i_>=_k_+_1_holds_ p_._i_=_0._L let i be Nat; ::_thesis: ( i >= k + 1 implies p . i = 0. L ) assume A7: i >= k + 1 ; ::_thesis: p . i = 0. L then i <> k by NAT_1:13; hence p . i = 0. L by A7, Lm11; ::_thesis: verum end; then reconsider p = p as AlgSequence of L by ALGSEQ_1:def_1; p is Polynomial of L ; hence (0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) is Polynomial of L ; ::_thesis: verum end; end; :: deftheorem defines rpoly HURWITZ:def_3_:_ for L being non empty unital doubleLoopStr for z being Element of L for k being Element of NAT holds rpoly (k,z) = (0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L))); theorem :: HURWITZ:25 for L being non empty unital 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 :: HURWITZ:26 for L being non empty unital 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: :: HURWITZ:27 for L being non empty non degenerated well-unital doubleLoopStr for z being Element of L for k being Element of NAT holds deg (rpoly (k,z)) = k proof let L be non empty non degenerated well-unital doubleLoopStr ; ::_thesis: for z being Element of L for k being Element of NAT holds deg (rpoly (k,z)) = k let z be Element of L; ::_thesis: for k being Element of NAT holds deg (rpoly (k,z)) = k let k be Element of NAT ; ::_thesis: deg (rpoly (k,z)) = k set t = rpoly (k,z); set f = (0,k) --> ((- ((power L) . (z,k))),(1_ L)); set a = - ((power L) . (z,k)); percases ( k = 0 or k <> 0 ) ; supposeA1: k = 0 ; ::_thesis: deg (rpoly (k,z)) = k A2: now__::_thesis:_for_m_being_Nat_st_m_is_at_least_length_of_rpoly_(k,z)_holds_ 1_<=_m let m be Nat; ::_thesis: ( m is_at_least_length_of rpoly (k,z) implies 1 <= m ) assume A3: m is_at_least_length_of rpoly (k,z) ; ::_thesis: 1 <= m now__::_thesis:_not_m_<_1 assume m < 1 ; ::_thesis: contradiction 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 ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) = {0,k} by FUNCT_4:62; then 0 in dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) by TARSKI:def_2; then (rpoly (k,z)) . 0 = ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) . 0 by FUNCT_4:13 .= ((0 .--> (- ((power L) . (z,k)))) +* (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; ::_thesis: verum end; hence 1 <= m ; ::_thesis: verum end; now__::_thesis:_for_i_being_Nat_st_i_>=_1_holds_ (rpoly_(k,z))_._i_=_0._L let i be Nat; ::_thesis: ( i >= 1 implies (rpoly (k,z)) . i = 0. L ) A7: i in NAT by ORDINAL1:def_12; assume i >= 1 ; ::_thesis: (rpoly (k,z)) . i = 0. L then not i in dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) by A1, TARSKI:def_2; hence (rpoly (k,z)) . i = (0_. L) . i by FUNCT_4:11 .= 0. L by A7, FUNCOP_1:7 ; ::_thesis: verum end; then 1 is_at_least_length_of rpoly (k,z) by ALGSEQ_1:def_2; then len (rpoly (k,z)) = 1 by A2, ALGSEQ_1:def_3; hence deg (rpoly (k,z)) = k by A1; ::_thesis: verum end; supposeA8: k <> 0 ; ::_thesis: deg (rpoly (k,z)) = k A9: now__::_thesis:_for_m_being_Nat_st_m_is_at_least_length_of_rpoly_(k,z)_holds_ k_+_1_<=_m let m be Nat; ::_thesis: ( m is_at_least_length_of rpoly (k,z) implies k + 1 <= m ) assume A10: m is_at_least_length_of rpoly (k,z) ; ::_thesis: k + 1 <= m now__::_thesis:_not_m_<_k_+_1 assume m < k + 1 ; ::_thesis: contradiction then A11: m <= k by NAT_1:13; (rpoly (k,z)) . k = 1_ L by A8, Lm10; hence contradiction by A10, A11, ALGSEQ_1:def_2; ::_thesis: verum end; hence k + 1 <= m ; ::_thesis: verum end; now__::_thesis:_for_i_being_Nat_st_i_>=_k_+_1_holds_ (rpoly_(k,z))_._i_=_0._L let i be Nat; ::_thesis: ( i >= k + 1 implies (rpoly (k,z)) . i = 0. L ) assume i >= k + 1 ; ::_thesis: (rpoly (k,z)) . i = 0. L then i > k by NAT_1:13; hence (rpoly (k,z)) . i = 0. L by Lm11; ::_thesis: verum end; then k + 1 is_at_least_length_of rpoly (k,z) by ALGSEQ_1:def_2; then len (rpoly (k,z)) = k + 1 by A9, ALGSEQ_1:def_3; hence deg (rpoly (k,z)) = k ; ::_thesis: verum end; end; end; theorem Th28: :: HURWITZ:28 for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed 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 non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: 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)) ) ) let p be Polynomial of L; ::_thesis: ( deg p = 1 iff ex x, z being Element of L st ( x <> 0. L & p = x * (rpoly (1,z)) ) ) A1: now__::_thesis:_(_deg_p_=_1_implies_ex_x,_z_being_Element_of_L_st_ (_x_<>_0._L_&_p_=_x_*_(rpoly_(1,z))_)_) set x = p . 1; set z = (- (p . 0)) * ((p . 1) "); set f = (p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) ")))); assume A2: deg p = 1 ; ::_thesis: ex x, z being Element of L st ( x <> 0. L & p = x * (rpoly (1,z)) ) then A3: len p = 1 + 1 ; then A4: p . 1 <> 0. L by ALGSEQ_1:10; A5: now__::_thesis:_for_k_being_Nat_st_k_<_len_p_holds_ ((p_._1)_*_(rpoly_(1,((-_(p_._0))_*_((p_._1)_")))))_._k_=_p_._k let k be Nat; ::_thesis: ( k < len p implies ((p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) "))))) . b1 = p . b1 ) assume k < len p ; ::_thesis: ((p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) "))))) . b1 = p . b1 then k < 1 + 1 by A2; then A6: k <= 1 by NAT_1:13; percases ( k = 1 or k < 1 ) by A6, XXREAL_0:1; supposeA7: k = 1 ; ::_thesis: ((p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) "))))) . b1 = p . b1 hence ((p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) "))))) . k = (p . 1) * ((rpoly (1,((- (p . 0)) * ((p . 1) ")))) . 1) by POLYNOM5:def_3 .= (p . 1) * (1_ L) by Lm10 .= p . k by A7, VECTSP_1:def_4 ; ::_thesis: verum end; suppose k < 1 ; ::_thesis: ((p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) "))))) . b1 = p . b1 then A8: k = 0 by NAT_1:14; hence ((p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) "))))) . k = (p . 1) * ((rpoly (1,((- (p . 0)) * ((p . 1) ")))) . 0) by POLYNOM5:def_3 .= (p . 1) * (- ((power L) . (((- (p . 0)) * ((p . 1) ")),(1 + 0)))) by Lm10 .= (p . 1) * (- (((power L) . (((- (p . 0)) * ((p . 1) ")),0)) * ((- (p . 0)) * ((p . 1) ")))) by GROUP_1:def_7 .= (p . 1) * (- ((1_ L) * ((- (p . 0)) * ((p . 1) ")))) by GROUP_1:def_7 .= (p . 1) * (- ((- (p . 0)) * ((p . 1) "))) 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 ; ::_thesis: verum end; end; end; len ((p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) "))))) = (deg (rpoly (1,((- (p . 0)) * ((p . 1) "))))) + 1 by A3, ALGSEQ_1:10, POLYNOM5:25 .= 1 + 1 by Th27 .= len p by A2 ; then p = (p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) ")))) 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; ::_thesis: verum end; now__::_thesis:_(_ex_x,_z_being_Element_of_L_st_ (_x_<>_0._L_&_p_=_x_*_(rpoly_(1,z))_)_implies_deg_p_=_1_) given x, z being Element of L such that A9: x <> 0. L and A10: p = x * (rpoly (1,z)) ; ::_thesis: deg p = 1 thus deg p = deg (rpoly (1,z)) by A9, A10, POLYNOM5:25 .= 1 by Th27 ; ::_thesis: verum end; hence ( deg p = 1 iff ex x, z being Element of L st ( x <> 0. L & p = x * (rpoly (1,z)) ) ) by A1; ::_thesis: verum end; theorem Th29: :: HURWITZ:29 for L being non empty non degenerated right_complementable well-unital Abelian add-associative right_zeroed 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 non empty non degenerated right_complementable well-unital Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for x, z being Element of L holds eval ((rpoly (1,z)),x) = x - z let x, z be Element of L; ::_thesis: eval ((rpoly (1,z)),x) = x - z set p = rpoly (1,z); consider F being FinSequence of L such that A3: eval ((rpoly (1,z)),x) = Sum F and A4: len F = len (rpoly (1,z)) and A5: for n being Element of NAT st n in dom F holds F . n = ((rpoly (1,z)) . (n -' 1)) * ((power L) . (x,(n -' 1))) by POLYNOM4:def_2; A6: deg (rpoly (1,z)) = 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 = ((rpoly (1,z)) . 1) * ((power L) . (x,(1 + 0))) by A5, A1 .= ((rpoly (1,z)) . 1) * (((power L) . (x,0)) * x) by GROUP_1:def_7 .= ((rpoly (1,z)) . 1) * ((1_ L) * x) by GROUP_1:def_7 .= ((rpoly (1,z)) . 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 = ((rpoly (1,z)) . 0) * ((power L) . (x,(1 -' 1))) by A5, A2 .= ((rpoly (1,z)) . 0) * (1_ L) by A2, GROUP_1:def_7 .= (rpoly (1,z)) . 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 ((rpoly (1,z)),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 ; ::_thesis: verum end; theorem Th30: :: HURWITZ:30 for L being non empty non degenerated right_complementable well-unital Abelian add-associative right_zeroed doubleLoopStr for z being Element of L holds z is_a_root_of rpoly (1,z) proof let L be non empty non degenerated right_complementable well-unital Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for z being Element of L holds z is_a_root_of rpoly (1,z) let z be Element of L; ::_thesis: z is_a_root_of rpoly (1,z) eval ((rpoly (1,z)),z) = z - z by Th29 .= 0. L by RLVECT_1:15 ; hence z is_a_root_of rpoly (1,z) by POLYNOM5:def_6; ::_thesis: verum end; definition let L be non empty well-unital doubleLoopStr ; let z be Element of L; let k be Nat; func qpoly (k,z) -> Polynomial of L means :Def4: :: HURWITZ:def 4 ( ( 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 ex b1 being Polynomial of L st ( ( for i being Nat st i < k holds b1 . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds b1 . i = 0. L ) ) proof defpred S1[ 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 holds ex y being set st ( y in the carrier of L & S1[x,y] ) proof let u be set ; ::_thesis: ( u in NAT implies ex y being set st ( y in the carrier of L & S1[u,y] ) ) assume u in NAT ; ::_thesis: ex y being set st ( y in the carrier of L & S1[u,y] ) then reconsider u9 = u as Element of NAT ; thus ex y being set st ( y in the carrier of L & S1[u,y] ) ::_thesis: verum proof percases ( u9 < k or u9 >= k ) ; supposeA2: u9 < k ; ::_thesis: ex y being set st ( y in the carrier of L & S1[u,y] ) 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)) ; ::_thesis: ( (power L) . (z,((k - u9) - 1)) in the carrier of L & S1[u,(power L) . (z,((k - u9) - 1))] ) (power L) . (z,m) in the carrier of L ; hence ( (power L) . (z,((k - u9) - 1)) in the carrier of L & S1[u,(power L) . (z,((k - u9) - 1))] ) by A2; ::_thesis: verum end; supposeA3: u9 >= k ; ::_thesis: ex y being set st ( y in the carrier of L & S1[u,y] ) take 0. L ; ::_thesis: ( 0. L in the carrier of L & S1[u, 0. L] ) thus ( 0. L in the carrier of L & S1[u, 0. L] ) by A3; ::_thesis: verum end; 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 S1[x,f . x] from FUNCT_2:sch_1(A1); reconsider f = f as sequence of L ; A5: for i being Nat st i >= k holds f . i = 0. L proof let i be Nat; ::_thesis: ( i >= k implies f . i = 0. L ) 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 ; ::_thesis: f . i = 0. L hence f . i = 0. L by A6; ::_thesis: verum end; then reconsider p = f as AlgSequence of L by ALGSEQ_1:def_1; take p ; ::_thesis: ( ( for i being Nat st i < k holds p . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds p . i = 0. L ) ) now__::_thesis:_for_i_being_Nat_st_i_<_k_holds_ p_._i_=_(power_L)_._(z,((k_-_i)_-_1)) let i be Nat; ::_thesis: ( i < k implies p . i = (power L) . (z,((k - i) - 1)) ) 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 ; ::_thesis: p . i = (power L) . (z,((k - i) - 1)) hence p . i = (power L) . (z,((k - i) - 1)) by A7; ::_thesis: verum end; hence ( ( for i being Nat st i < k holds p . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds p . i = 0. L ) ) by A5; ::_thesis: verum end; uniqueness for b1, b2 being Polynomial of L st ( for i being Nat st i < k holds b1 . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds b1 . i = 0. L ) & ( for i being Nat st i < k holds b2 . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds b2 . i = 0. L ) holds b1 = b2 proof let z1, z2 be AlgSequence of L; ::_thesis: ( ( for i being Nat st i < k holds z1 . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds z1 . i = 0. L ) & ( for i being Nat st i < k holds z2 . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds z2 . i = 0. L ) implies z1 = z2 ) 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 ; ::_thesis: ( ex i being Nat st ( i < k & not z2 . i = (power L) . (z,((k - i) - 1)) ) or ex i being Nat st ( i >= k & not z2 . i = 0. L ) or z1 = z2 ) 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 ; ::_thesis: z1 = z2 A12: now__::_thesis:_for_x_being_set_st_x_in_dom_z1_holds_ z1_._x_=_z2_._x let x be set ; ::_thesis: ( x in dom z1 implies z1 . b1 = z2 . b1 ) assume x in dom z1 ; ::_thesis: z1 . b1 = z2 . b1 then reconsider x9 = x as Element of NAT ; percases ( x9 < k or x9 >= k ) ; supposeA13: x9 < k ; ::_thesis: z1 . b1 = z2 . b1 hence z1 . x = (power L) . (z,((k - x9) - 1)) by A8 .= z2 . x by A10, A13 ; ::_thesis: verum end; supposeA14: x9 >= k ; ::_thesis: z1 . b1 = z2 . b1 hence z1 . x = 0. L by A9 .= z2 . x by A11, A14 ; ::_thesis: verum end; 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; ::_thesis: verum end; end; :: deftheorem Def4 defines qpoly HURWITZ:def_4_:_ for L being non empty well-unital doubleLoopStr for z being Element of L for k being Nat for b4 being Polynomial of L holds ( b4 = qpoly (k,z) iff ( ( for i being Nat st i < k holds b4 . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds b4 . i = 0. L ) ) ); theorem :: HURWITZ:31 for L being non empty non degenerated well-unital 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 non empty non degenerated well-unital doubleLoopStr ; ::_thesis: for z being Element of L for k being Element of NAT st k >= 1 holds deg (qpoly (k,z)) = k - 1 let z be Element of L; ::_thesis: for k being Element of NAT st k >= 1 holds deg (qpoly (k,z)) = k - 1 let k be Element of NAT ; ::_thesis: ( k >= 1 implies deg (qpoly (k,z)) = k - 1 ) set p = qpoly (k,z); A1: k - 1 < k - 0 by XREAL_1:10; assume k >= 1 ; ::_thesis: deg (qpoly (k,z)) = 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 (qpoly (k,z)) . (k - 1) = (power L) . (z,0) by A1, Def4 .= 1_ L by GROUP_1:def_7 ; then A2: (qpoly (k,z)) . (k - 1) <> 0. L ; A3: now__::_thesis:_for_m_being_Nat_st_m_is_at_least_length_of_qpoly_(k,z)_holds_ k_<=_m let m be Nat; ::_thesis: ( m is_at_least_length_of qpoly (k,z) implies k <= m ) assume A4: m is_at_least_length_of qpoly (k,z) ; ::_thesis: k <= m now__::_thesis:_not_k_>_m assume k > m ; ::_thesis: contradiction then k9 + 1 > m ; then k9 >= m by NAT_1:13; hence contradiction by A2, A4, ALGSEQ_1:def_2; ::_thesis: verum end; hence k <= m ; ::_thesis: verum end; for i being Nat st i >= k holds (qpoly (k,z)) . i = 0. L by Def4; then k is_at_least_length_of qpoly (k,z) by ALGSEQ_1:def_2; hence deg (qpoly (k,z)) = k - 1 by A3, ALGSEQ_1:def_3; ::_thesis: verum end; theorem Th32: :: HURWITZ:32 for L being non empty right_complementable commutative left-distributive well-unital add-associative right_zeroed 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 non empty right_complementable commutative left-distributive well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: 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) let z be Element of L; ::_thesis: for k being Element of NAT st k > 1 holds (rpoly (1,z)) *' (qpoly (k,z)) = rpoly (k,z) let k be Element of NAT ; ::_thesis: ( k > 1 implies (rpoly (1,z)) *' (qpoly (k,z)) = rpoly (k,z) ) set p = (rpoly (1,z)) *' (qpoly (k,z)); set u = rpoly (k,z); assume A1: k > 1 ; ::_thesis: (rpoly (1,z)) *' (qpoly (k,z)) = rpoly (k,z) 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__::_thesis:_for_i9_being_set_st_i9_in_dom_((rpoly_(1,z))_*'_(qpoly_(k,z)))_holds_ ((rpoly_(1,z))_*'_(qpoly_(k,z)))_._i9_=_(rpoly_(k,z))_._i9 A5: 1 - 1 >= 0 ; let i9 be set ; ::_thesis: ( i9 in dom ((rpoly (1,z)) *' (qpoly (k,z))) implies ((rpoly (1,z)) *' (qpoly (k,z))) . b1 = (rpoly (k,z)) . b1 ) A6: 0 + 1 = 1 ; assume i9 in dom ((rpoly (1,z)) *' (qpoly (k,z))) ; ::_thesis: ((rpoly (1,z)) *' (qpoly (k,z))) . b1 = (rpoly (k,z)) . b1 then reconsider i = i9 as Element of NAT ; consider fp being FinSequence of L such that A7: len fp = i + 1 and A8: ((rpoly (1,z)) *' (qpoly (k,z))) . i = Sum fp and A9: for j being 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__::_thesis:_for_j_being_Element_of_NAT_st_j_in_dom_fp_&_j_<>_1_&_j_<>_2_holds_ fp_._j_=_0._L let j be Element of NAT ; ::_thesis: ( j in dom fp & j <> 1 & j <> 2 implies fp . j = 0. L ) assume that A14: j in dom fp and A15: j <> 1 and A16: j <> 2 ; ::_thesis: fp . j = 0. L A17: j in Seg (len fp) by A14, FINSEQ_1:def_3; now__::_thesis:_(_not_j_-'_1_=_0_&_not_j_-'_1_=_1_) assume A18: ( j -' 1 = 0 or j -' 1 = 1 ) ; ::_thesis: contradiction percases ( j - 1 >= 0 or j - 1 < 0 ) ; suppose j - 1 >= 0 ; ::_thesis: contradiction then j -' 1 = j - 1 by XREAL_0:def_2; hence contradiction by A15, A16, A18; ::_thesis: verum end; suppose j - 1 < 0 ; ::_thesis: contradiction then (j - 1) + 1 < 0 + 1 by XREAL_1:8; hence contradiction by A17, FINSEQ_1:1; ::_thesis: verum end; 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; ::_thesis: verum end; A20: now__::_thesis:_(_i_<>_0_implies_((rpoly_(1,z))_*'_(qpoly_(k,z)))_._i_=_(fp_/._1)_+_(fp_/._2)_) 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 ; ::_thesis: ((rpoly (1,z)) *' (qpoly (k,z))) . i = (fp /. 1) + (fp /. 2) 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__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_g2_&_i_<>_1_holds_ g2_/._i_=_0._L let i be Element of NAT ; ::_thesis: ( i in dom g2 & i <> 1 implies g2 /. i = 0. L ) assume that A30: i in dom g2 and A31: i <> 1 ; ::_thesis: g2 /. i = 0. L 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; ::_thesis: verum 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 ((rpoly (1,z)) *' (qpoly (k,z))) . i = (Sum g1) + (fp /. 2) by A8, A24, RLVECT_1:41 .= (fp /. 1) + (fp /. 2) by A25, RLVECT_1:44 ; ::_thesis: verum end; A38: 2 - 1 >= 0 ; A39: now__::_thesis:_(_i_<>_0_implies_fp_/._2_=_(qpoly_(k,z))_._(i_-'_1)_) assume i <> 0 ; ::_thesis: fp /. 2 = (qpoly (k,z)) . (i -' 1) 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 ; ::_thesis: verum end; percases ( i < k or i = k or i > k ) by XXREAL_0:1; supposeA43: i < k ; ::_thesis: ((rpoly (1,z)) *' (qpoly (k,z))) . b1 = (rpoly (k,z)) . b1 percases ( i = 0 or i > 0 ) ; supposeA44: i = 0 ; ::_thesis: ((rpoly (1,z)) *' (qpoly (k,z))) . b1 = (rpoly (k,z)) . b1 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 ((rpoly (1,z)) *' (qpoly (k,z))) . 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 .= (rpoly (k,z)) . i9 by A1, A44, Lm10 ; ::_thesis: verum end; supposeA47: i > 0 ; ::_thesis: ((rpoly (1,z)) *' (qpoly (k,z))) . b1 = (rpoly (k,z)) . b1 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 ((rpoly (1,z)) *' (qpoly (k,z))) . 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 .= (rpoly (k,z)) . i9 by A43, A47, Lm11 ; ::_thesis: verum end; end; end; supposeA52: i = k ; ::_thesis: ((rpoly (1,z)) *' (qpoly (k,z))) . b1 = (rpoly (k,z)) . b1 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 ((rpoly (1,z)) *' (qpoly (k,z))) . 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 .= (rpoly (k,z)) . i9 by A1, A52, Lm10 ; ::_thesis: verum end; supposeA55: i > k ; ::_thesis: ((rpoly (1,z)) *' (qpoly (k,z))) . b1 = (rpoly (k,z)) . b1 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 ((rpoly (1,z)) *' (qpoly (k,z))) . i9 = (qpoly (k,z)) . (i -' 1) by A39, A20, A55, ALGSTR_1:def_2 .= 0. L by A56, A57, Def4 .= (rpoly (k,z)) . i9 by A55, Lm11 ; ::_thesis: verum end; end; end; dom ((rpoly (1,z)) *' (qpoly (k,z))) = NAT by FUNCT_2:def_1 .= dom (rpoly (k,z)) by FUNCT_2:def_1 ; hence (rpoly (1,z)) *' (qpoly (k,z)) = rpoly (k,z) by A4, FUNCT_1:2; ::_thesis: verum end; theorem Th33: :: HURWITZ:33 for L being non empty right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for p being Polynomial of L for z being Element of L st z is_a_root_of p holds ex s being Polynomial of L st p = (rpoly (1,z)) *' s proof let L be non empty right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L for z being Element of L st z is_a_root_of p holds ex s being Polynomial of L st p = (rpoly (1,z)) *' s let p be Polynomial of L; ::_thesis: for z being Element of L st z is_a_root_of p holds ex s being Polynomial of L st p = (rpoly (1,z)) *' s let z be Element of L; ::_thesis: ( z is_a_root_of p implies ex s being Polynomial of L st p = (rpoly (1,z)) *' s ) assume A1: z is_a_root_of p ; ::_thesis: ex s being Polynomial of L st p = (rpoly (1,z)) *' s set m = len p; percases ( len p = 0 or len p > 0 ) ; supposeA2: len p = 0 ; ::_thesis: ex s being Polynomial of L st p = (rpoly (1,z)) *' s take 0_. L ; ::_thesis: p = (rpoly (1,z)) *' (0_. L) p = 0_. L by A2, POLYNOM4:5; hence p = (rpoly (1,z)) *' (0_. L) by POLYNOM3:34; ::_thesis: verum end; supposeA3: len p > 0 ; ::_thesis: ex s being Polynomial of L st p = (rpoly (1,z)) *' s then len p >= 0 + 1 by NAT_1:13; then reconsider m1 = (len p) - 1 as Element of NAT by INT_1:5; defpred S1[ set , set ] means ex u being Element of L ex b being Element of NAT st ( u = p . $1 & b = $1 & $2 = u * (rpoly (b,z)) ); defpred S2[ set , set ] means ( ( $1 = 1 & $2 = (p . 1) * (1_. L) ) or ( $1 <> 1 & ex u being Element of L 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 holds ex x being Element of the carrier of (Polynom-Ring L) st S2[k,x] proof let k be Nat; ::_thesis: ( k in Seg m1 implies ex x being Element of the carrier of (Polynom-Ring L) st S2[k,x] ) A5: dom p = NAT by FUNCT_2:def_1; assume k in Seg m1 ; ::_thesis: ex x being Element of the carrier of (Polynom-Ring L) st S2[k,x] then A6: 1 <= k by FINSEQ_1:1; percases ( k = 1 or k > 1 ) by A6, XXREAL_0:1; supposeA7: k = 1 ; ::_thesis: ex x being Element of the carrier of (Polynom-Ring L) st S2[k,x] reconsider t = (p . 1) * (1_. L) as Element of the carrier of (Polynom-Ring L) by POLYNOM3:def_10; take t ; ::_thesis: S2[k,t] thus S2[k,t] by A7; ::_thesis: verum end; supposeA8: k > 1 ; ::_thesis: ex x being Element of the carrier of (Polynom-Ring L) st S2[k,x] reconsider t = (p /. k) * (qpoly (k,z)) as Element of the carrier of (Polynom-Ring L) by POLYNOM3:def_10; take t ; ::_thesis: S2[k,t] ex u being Element of L ex b being Element of NAT st ( u = p . k & b = k & t = u * (qpoly (b,z)) ) proof take p /. k ; ::_thesis: ex b being Element of NAT st ( p /. k = p . k & b = k & t = (p /. k) * (qpoly (b,z)) ) reconsider b = k as Element of NAT by ORDINAL1:def_12; take b ; ::_thesis: ( p /. k = p . k & b = k & t = (p /. k) * (qpoly (b,z)) ) b in NAT ; hence ( p /. k = p . k & b = k & t = (p /. k) * (qpoly (b,z)) ) by A5, PARTFUN1:def_6; ::_thesis: verum end; hence S2[k,t] by A8; ::_thesis: verum end; 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 S2[k,hs . k] ) ) from FINSEQ_1:sch_5(A4); A10: now__::_thesis:_for_i_being_Element_of_NAT_st_1_<_i_&_i_<=_(len_p)_-_1_holds_ hs_._i_=_(p_._i)_*_(qpoly_(i,z)) let i be Element of NAT ; ::_thesis: ( 1 < i & i <= (len p) - 1 implies hs . i = (p . i) * (qpoly (i,z)) ) assume that A11: 1 < i and A12: i <= (len p) - 1 ; ::_thesis: hs . i = (p . i) * (qpoly (i,z)) i in Seg m1 by A11, A12; then ex u being Element of L 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)) ; ::_thesis: verum end; A13: for k being Nat st k in Seg m1 holds ex x being Element of the carrier of (Polynom-Ring L) st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg m1 implies ex x being Element of the carrier of (Polynom-Ring L) st S1[k,x] ) assume k in Seg m1 ; ::_thesis: ex x being Element of the carrier of (Polynom-Ring L) st S1[k,x] 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 ; ::_thesis: S1[k,t] take p /. k ; ::_thesis: ex b being Element of NAT st ( p /. k = p . k & b = k & t = (p /. k) * (rpoly (b,z)) ) take k1 ; ::_thesis: ( p /. k = p . k & k1 = k & t = (p /. k) * (rpoly (k1,z)) ) A14: k1 in NAT ; dom p = NAT by FUNCT_2:def_1; hence ( p /. k = p . k & k1 = k & t = (p /. k) * (rpoly (k1,z)) ) by A14, PARTFUN1:def_6; ::_thesis: verum 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 S1[k,h . k] ) ) from FINSEQ_1:sch_5(A13); set s = Sum hs; set rs = Sum h; reconsider s = Sum hs, rs = Sum h as Polynomial of L by POLYNOM3:def_10; A16: now__::_thesis:_for_k_being_Element_of_NAT_st_1_<=_k_&_k_<=_m1_holds_ h_._k_=_(p_._k)_*_(rpoly_(k,z)) let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= m1 implies h . k = (p . k) * (rpoly (k,z)) ) assume that A17: 1 <= k and A18: k <= m1 ; ::_thesis: h . k = (p . k) * (rpoly (k,z)) k in Seg m1 by A17, A18; then ex u being Element of L 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)) ; ::_thesis: verum end; A19: m1 + 1 = len p ; A20: now__::_thesis:_for_i_being_Element_of_NAT_st_i_>=_len_p_holds_ rs_._i_=_0._L let i be Element of NAT ; ::_thesis: ( i >= len p implies rs . i = 0. L ) assume A21: i >= len p ; ::_thesis: rs . i = 0. L set co = Coeff (h,i); A22: dom h = Seg (len h) by FINSEQ_1:def_3 .= Seg (len (Coeff (h,i))) by Def1 .= dom (Coeff (h,i)) by FINSEQ_1:def_3 ; now__::_thesis:_for_j_being_Element_of_NAT_st_j_in_dom_(Coeff_(h,i))_holds_ (Coeff_(h,i))_._j_=_0._L let j be Element of NAT ; ::_thesis: ( j in dom (Coeff (h,i)) implies (Coeff (h,i)) . j = 0. L ) assume A23: j in dom (Coeff (h,i)) ; ::_thesis: (Coeff (h,i)) . j = 0. L then A24: ex ci being Polynomial of L st ( ci = h . j & (Coeff (h,i)) . 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 (Coeff (h,i)) . 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 ; ::_thesis: verum end; then Sum (Coeff (h,i)) = 0. L by POLYNOM3:1; hence rs . i = 0. L by Th13; ::_thesis: verum end; A27: len h = m1 by A15, FINSEQ_1:def_3; A28: now__::_thesis:_for_i_being_Element_of_NAT_st_i_>_0_&_i_<_len_p_holds_ rs_._i_=_((p_._i)_*_(rpoly_(i,z)))_._i let i be Element of NAT ; ::_thesis: ( i > 0 & i < len p implies rs . i = ((p . i) * (rpoly (i,z))) . i ) assume that A29: i > 0 and A30: i < len p ; ::_thesis: rs . i = ((p . i) * (rpoly (i,z))) . i 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 (Coeff (h,i))) by Def1 .= dom (Coeff (h,i)) by FINSEQ_1:def_3 ; i in Seg (len h) by A27, A32, A31; then A35: i in dom (Coeff (h,i)) by A34, FINSEQ_1:def_3; then A36: ex cc being Polynomial of L st ( cc = h . i & (Coeff (h,i)) . i = cc . i ) by Def1; now__::_thesis:_for_i9_being_Element_of_NAT_st_i9_in_dom_(Coeff_(h,i))_&_i9_<>_i_holds_ (Coeff_(h,i))_/._i9_=_0._L let i9 be Element of NAT ; ::_thesis: ( i9 in dom (Coeff (h,i)) & i9 <> i implies (Coeff (h,i)) /. i9 = 0. L ) assume that A37: i9 in dom (Coeff (h,i)) and A38: i9 <> i ; ::_thesis: (Coeff (h,i)) /. i9 = 0. L A39: ex ci being Polynomial of L st ( ci = h . i9 & (Coeff (h,i)) . i9 = ci . i ) by A37, Def1; A40: i9 <= (len p) - 1 by A15, A34, A37, FINSEQ_1:1; 1 <= i9 by A15, A34, A37, FINSEQ_1:1; then (Coeff (h,i)) . 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 (Coeff (h,i)) /. i9 = 0. L by A37, PARTFUN1:def_6; ::_thesis: verum end; then Sum (Coeff (h,i)) = (Coeff (h,i)) /. i by A35, POLYNOM2:3 .= (Coeff (h,i)) . i by A35, PARTFUN1:def_6 ; hence rs . i = ((p . i) * (rpoly (i,z))) . i by A36, A33, Th13; ::_thesis: verum end; A41: now__::_thesis:_for_i9_being_set_st_i9_in_dom_p_holds_ p_._i9_=_rs_._i9 let i9 be set ; ::_thesis: ( i9 in dom p implies p . b1 = rs . b1 ) assume i9 in dom p ; ::_thesis: p . b1 = rs . b1 then reconsider i = i9 as Element of NAT ; percases ( i = 0 or i > 0 ) ; supposeA42: i = 0 ; ::_thesis: p . b1 = rs . b1 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))*> ^ (Coeff (h,0)); A46: len (<*(- (p . 0))*> ^ (Coeff (h,0))) = (len <*(- (p . 0))*>) + (len (Coeff (h,0))) by FINSEQ_1:22 .= 1 + (len (Coeff (h,0))) by FINSEQ_1:39 ; then A47: len (<*(- (p . 0))*> ^ (Coeff (h,0))) = 1 + (len h) by Def1 .= len evp by A27, A44 ; then A48: dom (<*(- (p . 0))*> ^ (Coeff (h,0))) = 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 (Coeff (h,0))) by Def1 .= dom (Coeff (h,0)) by FINSEQ_1:def_3 ; A50: now__::_thesis:_for_j_being_Element_of_NAT_st_j_in_dom_(Coeff_(h,0))_holds_ (Coeff_(h,0))_._j_=_-_((p_._j)_*_((power_L)_._(z,j))) let j be Element of NAT ; ::_thesis: ( j in dom (Coeff (h,0)) implies (Coeff (h,0)) . j = - ((p . j) * ((power L) . (z,j))) ) reconsider aj = - ((power L) . (z,j)) as Element of L ; assume A51: j in dom (Coeff (h,0)) ; ::_thesis: (Coeff (h,0)) . j = - ((p . j) * ((power L) . (z,j))) 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 & (Coeff (h,0)) . j = ci . i ) by A42, A51, Def1; hence (Coeff (h,0)) . 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 ; ::_thesis: verum end; now__::_thesis:_for_j_being_Element_of_NAT_st_j_in_dom_(<*(-_(p_._0))*>_^_(Coeff_(h,0)))_holds_ (<*(-_(p_._0))*>_^_(Coeff_(h,0)))_/._j_=_-_(evp_/._j) let j be Element of NAT ; ::_thesis: ( j in dom (<*(- (p . 0))*> ^ (Coeff (h,0))) implies (<*(- (p . 0))*> ^ (Coeff (h,0))) /. b1 = - (evp /. b1) ) A54: dom <*(- (p . 0))*> = {1} by FINSEQ_1:2, FINSEQ_1:38; assume A55: j in dom (<*(- (p . 0))*> ^ (Coeff (h,0))) ; ::_thesis: (<*(- (p . 0))*> ^ (Coeff (h,0))) /. b1 = - (evp /. b1) 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 (<*(- (p . 0))*> ^ (Coeff (h,0)))) by A55, FINSEQ_1:def_3; then A58: 1 <= j by FINSEQ_1:1; A59: j <= len (<*(- (p . 0))*> ^ (Coeff (h,0))) by A57, FINSEQ_1:1; percases ( j = 1 or j > 1 ) by A58, XXREAL_0:1; supposeA60: j = 1 ; ::_thesis: (<*(- (p . 0))*> ^ (Coeff (h,0))) /. b1 = - (evp /. b1) 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 (<*(- (p . 0))*> ^ (Coeff (h,0))) . j = <*(- (p . 0))*> . j by FINSEQ_1:def_7 .= - (p . 0) by A60, FINSEQ_1:40 ; hence (<*(- (p . 0))*> ^ (Coeff (h,0))) /. j = - (evp /. j) by A55, A61, PARTFUN1:def_6; ::_thesis: verum end; supposeA62: j > 1 ; ::_thesis: (<*(- (p . 0))*> ^ (Coeff (h,0))) /. b1 = - (evp /. b1) 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 (<*(- (p . 0))*> ^ (Coeff (h,0)))) - 1 by A59, XREAL_1:9; then j1 in Seg (len (Coeff (h,0))) by A46, A63; then A64: j1 in dom (Coeff (h,0)) by FINSEQ_1:def_3; A65: j <= len (<*(- (p . 0))*> ^ (Coeff (h,0))) 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 (<*(- (p . 0))*> ^ (Coeff (h,0))) . j = (Coeff (h,0)) . (j - (len <*(- (p . 0))*>)) by A65, FINSEQ_1:24 .= (Coeff (h,0)) . (j - 1) by FINSEQ_1:40 .= - ((p . j1) * ((power L) . (z,j1))) by A50, A64 ; hence (<*(- (p . 0))*> ^ (Coeff (h,0))) /. j = - (evp /. j) by A55, A56, A66, PARTFUN1:def_6; ::_thesis: verum end; end; end; then A67: - (Sum evp) = Sum (<*(- (p . 0))*> ^ (Coeff (h,0))) by A47, Th7 .= (Sum <*(- (p . 0))*>) + (Sum (Coeff (h,0))) by RLVECT_1:41 .= (- (p . 0)) + (Sum (Coeff (h,0))) by RLVECT_1:44 ; Sum evp = 0. L by A1, A43, POLYNOM5:def_6; then 0. L = (- (p . 0)) + (Sum (Coeff (h,0))) by A67, RLVECT_1:12; then p . 0 = (p . 0) + ((- (p . 0)) + (Sum (Coeff (h,0)))) by ALGSTR_1:def_2 .= ((p . 0) + (- (p . 0))) + (Sum (Coeff (h,0))) by RLVECT_1:def_3 .= (0. L) + (Sum (Coeff (h,0))) by RLVECT_1:5 .= Sum (Coeff (h,0)) by ALGSTR_1:def_2 ; hence p . i9 = rs . i9 by A42, Th13; ::_thesis: verum end; supposeA68: i > 0 ; ::_thesis: rs . b1 = p . b1 percases ( i >= len p or i < len p ) ; supposeA69: i >= len p ; ::_thesis: rs . b1 = p . b1 hence rs . i9 = 0. L by A20 .= p . i9 by A69, ALGSEQ_1:8 ; ::_thesis: verum end; suppose i < len p ; ::_thesis: rs . b1 = p . b1 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 ; ::_thesis: verum end; end; end; end; end; now__::_thesis:_not_m1_<_1 assume m1 < 1 ; ::_thesis: contradiction then deg p = 0 by NAT_1:14; then not p is with_roots by Th24; hence contradiction by A1, POLYNOM5:def_7; ::_thesis: verum end; then 1 in Seg m1 ; then A70: hs . 1 = (p . 1) * (1_. L) by A9; A71: now__::_thesis:_for_i9_being_set_st_i9_in_dom_rs_holds_ rs_._i9_=_((rpoly_(1,z))_*'_s)_._i9 reconsider r1z = rpoly (1,z) as Element of (Polynom-Ring L) by POLYNOM3:def_10; let i9 be set ; ::_thesis: ( i9 in dom rs implies rs . i9 = ((rpoly (1,z)) *' s) . i9 ) assume i9 in dom rs ; ::_thesis: rs . i9 = ((rpoly (1,z)) *' s) . i9 A72: dom (r1z * hs) = dom h by A9, A15, POLYNOM1:def_1; now__::_thesis:_for_k_being_Nat_st_k_in_dom_h_holds_ (r1z_*_hs)_._k_=_h_._k let k be Nat; ::_thesis: ( k in dom h implies (r1z * hs) . b1 = h . b1 ) assume A73: k in dom h ; ::_thesis: (r1z * hs) . b1 = h . b1 then A74: 1 <= k by A15, FINSEQ_1:1; A75: k <= m1 by A15, A73, FINSEQ_1:1; percases ( k = 1 or k > 1 ) by A74, XXREAL_0:1; supposeA76: k = 1 ; ::_thesis: (r1z * hs) . b1 = h . b1 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 ; ::_thesis: verum end; supposeA78: k > 1 ; ::_thesis: (r1z * hs) . b1 = h . b1 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 ; ::_thesis: verum end; end; end; then r1z * hs = h by A72, FINSEQ_1:13; hence rs . i9 = ((rpoly (1,z)) *' s) . i9 by Lm5; ::_thesis: verum end; take s ; ::_thesis: p = (rpoly (1,z)) *' 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 p = (rpoly (1,z)) *' s by A80, A41, FUNCT_1:2; ::_thesis: verum end; end; end; begin definition let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; let p, s be Polynomial of L; assume B1: s <> 0_. L ; funcp div s -> Polynomial of L means :Def5: :: HURWITZ:def 5 ex t being Polynomial of L st ( p = (it *' s) + t & deg t < deg s ); existence ex b1, t being Polynomial of L st ( p = (b1 *' s) + t & deg t < deg s ) proof set M = { (p - (u *' s)) where u is Polynomial of L : 1 = 1 } ; defpred S1[ Nat] means ex t being Polynomial of L st ( t in { (p - (u *' s)) where u is Polynomial of L : 1 = 1 } & 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 { (p - (u *' s)) where u is Polynomial of L : 1 = 1 } ; then ex t being Polynomial of L st ( t in { (p - (u *' s)) where u is Polynomial of L : 1 = 1 } & len t = len p ) ; then A4: ex k being Nat st S1[k] ; consider k being Nat such that A5: ( S1[k] & ( for n being Nat st S1[n] holds k <= n ) ) from NAT_1:sch_5(A4); consider f being Polynomial of L such that A6: f in { (p - (u *' s)) where u is Polynomial of L : 1 = 1 } 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 ; ::_thesis: ex t being Polynomial of L st ( p = (g *' s) + t & deg t < deg s ) 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 ; percases ( f = 0_. L or f <> 0_. L ) ; supposeA10: f = 0_. L ; ::_thesis: ex t being Polynomial of L st ( p = (g *' s) + t & deg t < deg s ) reconsider s9 = deg s as Nat by B1, Lm8; A11: s9 >= 0 ; deg f = - 1 by A10, Th20; hence ex t being Polynomial of L st ( p = (g *' s) + t & deg t < deg s ) by A8, A9, A11; ::_thesis: verum end; suppose f <> 0_. L ; ::_thesis: ex t being Polynomial of L st ( p = (g *' s) + t & deg t < deg s ) 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__::_thesis:_not_deg_f_>=_deg_s assume deg f >= deg s ; ::_thesis: contradiction 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} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))); A15: dom (0_. L) = NAT by FUNCT_2:def_1; now__::_thesis:_for_u_being_set_st_u_in_{degn}_holds_ u_in_NAT let u be set ; ::_thesis: ( u in {degn} implies u in NAT ) assume u in {degn} ; ::_thesis: u in NAT then u = degn by TARSKI:def_1; hence u in NAT ; ::_thesis: verum end; then A16: {degn} c= NAT by TARSKI:def_3; A17: degn in {degn} by TARSKI:def_1; A18: now__::_thesis:_for_x9_being_set_st_x9_in_NAT_holds_ ((0_._L)_+*_({degn}_-->_((f_._((len_f)_-'_1))_*_((s_._((len_s)_-'_1))_"))))_._x9_in_the_carrier_of_L let x9 be set ; ::_thesis: ( x9 in NAT implies ((0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")))) . b1 in the carrier of L ) assume x9 in NAT ; ::_thesis: ((0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")))) . b1 in the carrier of L then reconsider x = x9 as Element of NAT ; percases ( x in dom ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))) or not x in dom ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))) ) ; supposeA19: x in dom ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))) ; ::_thesis: ((0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")))) . b1 in the carrier of L then x = degn by TARSKI:def_1; then ((0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")))) . x = ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))) . degn by A19, FUNCT_4:13 .= (f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ") by A17, FUNCOP_1:7 ; hence ((0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")))) . x9 in the carrier of L ; ::_thesis: verum end; suppose not x in dom ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))) ; ::_thesis: ((0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")))) . b1 in the carrier of L then ((0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")))) . x = (0_. L) . x by FUNCT_4:11 .= 0. L by FUNCOP_1:7 ; hence ((0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")))) . x9 in the carrier of L ; ::_thesis: verum end; end; end; dom ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))) = {degn} by FUNCOP_1:13; then (dom (0_. L)) \/ (dom ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")))) = NAT by A15, A16, XBOOLE_1:12; then dom ((0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")))) = NAT by FUNCT_4:def_1; then reconsider g1 = (0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))) 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; ::_thesis: ( j <> degn implies g1 . j = 0. L ) A21: j in NAT by ORDINAL1:def_12; assume j <> degn ; ::_thesis: g1 . j = 0. L then not j in dom ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))) by TARSKI:def_1; hence g1 . j = (0_. L) . j by FUNCT_4:11 .= 0. L by A21, FUNCOP_1:7 ; ::_thesis: verum end; A22: ex l being Nat st for i being Nat st i >= l holds g1 . i = 0. L proof take l = degn + 1; ::_thesis: for i being Nat st i >= l holds g1 . i = 0. L now__::_thesis:_for_i_being_Nat_st_i_>=_l_holds_ g1_._i_=_0._L let i be Nat; ::_thesis: ( i >= l implies g1 . i = 0. L ) assume i >= l ; ::_thesis: g1 . i = 0. L then i <> degn by NAT_1:13; hence g1 . i = 0. L by A20; ::_thesis: verum end; hence for i being Nat st i >= l holds g1 . i = 0. L ; ::_thesis: verum end; A23: degn in {degn} by TARSKI:def_1; then degn in dom ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))) by FUNCOP_1:13; then A24: g1 . degn = ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))) . degn by FUNCT_4:13 .= (f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ") by A23, FUNCOP_1:7 ; reconsider g1 = g1 as Polynomial of L by A22, ALGSEQ_1:def_1; set s1 = p - ((g + g1) *' s); now__::_thesis:_for_i_being_Nat_st_i_>=_k9_holds_ (p_-_((g_+_g1)_*'_s))_._i_=_0._L A25: 1 <= degn + 1 by NAT_1:11; let i be Nat; ::_thesis: ( i >= k9 implies (p - ((g + g1) *' s)) . b1 = 0. L ) A26: dom f = NAT by FUNCT_2:def_1; assume A27: i >= k9 ; ::_thesis: (p - ((g + g1) *' s)) . b1 = 0. L 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__::_thesis:_for_m_being_Nat_st_m_in_dom_sf_&_m_<>_degn_+_1_holds_ g1_._(m_-'_1)_=_0._L let m be Nat; ::_thesis: ( m in dom sf & m <> degn + 1 implies g1 . (m -' 1) = 0. L ) assume that A38: m in dom sf and A39: m <> degn + 1 ; ::_thesis: g1 . (m -' 1) = 0. L 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; ::_thesis: verum end; now__::_thesis:_for_i9_being_Element_of_NAT_st_i9_in_dom_sf_&_i9_<>_degn_+_1_holds_ sf_/._i9_=_0._L let i9 be Element of NAT ; ::_thesis: ( i9 in dom sf & i9 <> degn + 1 implies sf /. i9 = 0. L ) assume that A40: i9 in dom sf and A41: i9 <> degn + 1 ; ::_thesis: sf /. i9 = 0. L 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; ::_thesis: verum 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 .= ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")) * (s . ((i + 1) -' (degn + 1))) by A24, NAT_D:34 ; A43: (p - ((g + g1) *' s)) - 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; p - ((g + g1) *' s) = (p - ((g + g1) *' s)) + (0_. L) by POLYNOM3:28 .= (p - ((g + g1) *' s)) + (f - f) by POLYNOM3:29 .= ((p - ((g + g1) *' s)) + (- f)) + f by POLYNOM3:26 .= f - (g1 *' s) by A43 ; then A45: (p - ((g + g1) *' s)) . 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; percases ( i > k9 or i = k9 ) by A27, XXREAL_0:1; supposeA47: i > k9 ; ::_thesis: (p - ((g + g1) *' s)) . b1 = 0. L 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 (p - ((g + g1) *' s)) . 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 ; ::_thesis: verum end; supposeA50: i = k9 ; ::_thesis: (p - ((g + g1) *' s)) . b1 = 0. L (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 (p - ((g + g1) *' s)) . i = (f /. ((len f) - 1)) + (- (f /. ((len f) - 1))) by A44, A45, A33, A50, PARTFUN1:def_6 .= 0. L by RLVECT_1:5 ; ::_thesis: verum end; end; end; then k9 is_at_least_length_of p - ((g + g1) *' s) by ALGSEQ_1:def_2; then len (p - ((g + g1) *' s)) <= k9 by ALGSEQ_1:def_3; then A51: len (p - ((g + g1) *' s)) < k by A13, NAT_1:13; p - ((g + g1) *' s) in { (p - (u *' s)) where u is Polynomial of L : 1 = 1 } ; hence contradiction by A5, A51; ::_thesis: verum end; hence ex t being Polynomial of L st ( p = (g *' s) + t & deg t < deg s ) by A8, A9; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Polynomial of L st ex t being Polynomial of L st ( p = (b1 *' s) + t & deg t < deg s ) & ex t being Polynomial of L st ( p = (b2 *' s) + t & deg t < deg s ) holds b1 = b2 proof let f1, f2 be Polynomial of L; ::_thesis: ( ex t being Polynomial of L st ( p = (f1 *' s) + t & deg t < deg s ) & ex t being Polynomial of L st ( p = (f2 *' s) + t & deg t < deg s ) implies f1 = f2 ) given t1 being Polynomial of L such that A52: p = (f1 *' s) + t1 and A53: deg t1 < deg s ; ::_thesis: ( for t being Polynomial of L holds ( not p = (f2 *' s) + t or not deg t < deg s ) or f1 = f2 ) given t2 being Polynomial of L such that A54: p = (f2 *' s) + t2 and A55: deg t2 < deg s ; ::_thesis: f1 = f2 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__::_thesis:_not_f1_<>_f2 assume A58: f1 <> f2 ; ::_thesis: contradiction A59: now__::_thesis:_not_f2_-_f1_=_0_._L assume f2 - f1 = 0_. L ; ::_thesis: contradiction 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; ::_thesis: verum 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 percases ( max ((deg t1),(deg t2)) = deg t1 or max ((deg t1),(deg t2)) = deg t2 ) by XXREAL_0:16; suppose max ((deg t1),(deg t2)) = deg t1 ; ::_thesis: deg (t1 - t2) < degs hence deg (t1 - t2) < degs by A53, A60, XXREAL_0:2; ::_thesis: verum end; suppose max ((deg t1),(deg t2)) = deg t2 ; ::_thesis: deg (t1 - t2) < degs hence deg (t1 - t2) < degs by A55, A60, XXREAL_0:2; ::_thesis: verum end; end; end; deg (t1 - t2) = d + degs by B1, A57, A56, A59, Th23; hence contradiction by A61, NAT_1:11; ::_thesis: verum end; hence f1 = f2 ; ::_thesis: verum end; end; :: deftheorem Def5 defines div HURWITZ:def_5_:_ for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for p, s being Polynomial of L st s <> 0_. L holds for b4 being Polynomial of L holds ( b4 = p div s iff ex t being Polynomial of L st ( p = (b4 *' s) + t & deg t < deg s ) ); definition let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; let p, s be Polynomial of L; funcp mod s -> Polynomial of L equals :: HURWITZ:def 6 p - ((p div s) *' s); coherence p - ((p div s) *' s) is Polynomial of L ; end; :: deftheorem defines mod HURWITZ:def_6_:_ for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for p, s being Polynomial of L holds p mod s = p - ((p div s) *' s); definition let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; let p, s be Polynomial of L; preds divides p means :Def7: :: HURWITZ:def 7 p mod s = 0_. L; end; :: deftheorem Def7 defines divides HURWITZ:def_7_:_ for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for p, s being Polynomial of L holds ( s divides p iff p mod s = 0_. L ); theorem Th34: :: HURWITZ:34 for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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 non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 ) let p, s be Polynomial of L; ::_thesis: ( s <> 0_. L implies ( s divides p iff ex t being Polynomial of L st t *' s = p ) ) assume A1: s <> 0_. L ; ::_thesis: ( s divides p iff ex t being Polynomial of L st t *' s = p ) A2: now__::_thesis:_(_ex_t_being_Polynomial_of_L_st_t_*'_s_=_p_implies_s_divides_p_) (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 ; ::_thesis: s divides 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; ::_thesis: verum end; now__::_thesis:_(_s_divides_p_implies_ex_t_being_Polynomial_of_L_st_t_*'_s_=_p_) assume A5: s divides p ; ::_thesis: ex t being Polynomial of L st t *' s = 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 ; ::_thesis: verum end; hence ( s divides p iff ex t being Polynomial of L st t *' s = p ) by A2; ::_thesis: verum end; theorem :: HURWITZ:35 for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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 non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let p be Polynomial of L; ::_thesis: for z being Element of L st z is_a_root_of p holds rpoly (1,z) divides p let z be Element of L; ::_thesis: ( z is_a_root_of p implies rpoly (1,z) divides p ) (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 ; ::_thesis: rpoly (1,z) divides p then ex s being Polynomial of L st p = (rpoly (1,z)) *' s by Th33; hence rpoly (1,z) divides p by A1, Th34; ::_thesis: verum end; theorem :: HURWITZ:36 for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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 non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let p be Polynomial of L; ::_thesis: 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 let z be Element of L; ::_thesis: ( p <> 0_. L & z is_a_root_of p implies deg (p div (rpoly (1,z))) = (deg p) - 1 ) assume that A1: p <> 0_. L and A2: z is_a_root_of p ; ::_thesis: deg (p div (rpoly (1,z))) = (deg p) - 1 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; ::_thesis: ( p = (s *' (rpoly (1,z))) + t & deg t < deg (rpoly (1,z)) ) thus (s *' (rpoly (1,z))) + t = p by A3, POLYNOM3:28; ::_thesis: deg t < deg (rpoly (1,z)) deg t = - 1 by Th20; hence deg t < deg (rpoly (1,z)) by Th27; ::_thesis: verum 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 deg (p div (rpoly (1,z))) = (deg p) - 1 by A4, A5, Def5; ::_thesis: verum end; begin definition let f be Polynomial of F_Complex; attrf is Hurwitz means :Def8: :: HURWITZ:def 8 for z being Element of F_Complex st z is_a_root_of f holds Re z < 0 ; end; :: deftheorem Def8 defines Hurwitz HURWITZ:def_8_:_ for f being Polynomial of F_Complex holds ( f is Hurwitz iff for z being Element of F_Complex st z is_a_root_of f holds Re z < 0 ); theorem :: HURWITZ:37 not 0_. F_Complex is 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 not 0_. F_Complex is Hurwitz by Def8, COMPLEX1:6, COMPLFLD:8; ::_thesis: verum end; theorem :: HURWITZ:38 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; ::_thesis: ( x <> 0. F_Complex implies x * (1_. F_Complex) is Hurwitz ) set p = x * (1_. F_Complex); assume A1: x <> 0. F_Complex ; ::_thesis: x * (1_. F_Complex) is Hurwitz now__::_thesis:_for_z_being_Element_of_F_Complex_st_z_is_a_root_of_x_*_(1_._F_Complex)_holds_ Re_z_<_0 let z be Element of F_Complex; ::_thesis: ( z is_a_root_of x * (1_. F_Complex) implies Re z < 0 ) assume z is_a_root_of x * (1_. F_Complex) ; ::_thesis: Re z < 0 then A2: eval ((x * (1_. F_Complex)),z) = 0. F_Complex by POLYNOM5:def_6; eval ((x * (1_. F_Complex)),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; ::_thesis: verum end; hence x * (1_. F_Complex) is Hurwitz by Def8; ::_thesis: verum end; theorem Th39: :: HURWITZ:39 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; ::_thesis: ( x <> 0. F_Complex implies ( x * (rpoly (1,z)) is Hurwitz iff Re z < 0 ) ) set p = x * (rpoly (1,z)); assume A1: x <> 0. F_Complex ; ::_thesis: ( x * (rpoly (1,z)) is Hurwitz iff Re z < 0 ) A2: now__::_thesis:_(_Re_z_<_0_implies_x_*_(rpoly_(1,z))_is_Hurwitz_) assume A3: Re z < 0 ; ::_thesis: x * (rpoly (1,z)) is Hurwitz now__::_thesis:_for_y_being_Element_of_F_Complex_st_y_is_a_root_of_x_*_(rpoly_(1,z))_holds_ Re_y_<_0 let y be Element of F_Complex; ::_thesis: ( y is_a_root_of x * (rpoly (1,z)) implies Re y < 0 ) assume y is_a_root_of x * (rpoly (1,z)) ; ::_thesis: Re y < 0 then 0. F_Complex = eval ((x * (rpoly (1,z))),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; ::_thesis: verum end; hence x * (rpoly (1,z)) is Hurwitz by Def8; ::_thesis: verum end; now__::_thesis:_(_x_*_(rpoly_(1,z))_is_Hurwitz_implies_Re_z_<_0_) eval ((x * (rpoly (1,z))),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 x * (rpoly (1,z)) by POLYNOM5:def_6; assume x * (rpoly (1,z)) is Hurwitz ; ::_thesis: Re z < 0 hence Re z < 0 by A4, Def8; ::_thesis: verum end; hence ( x * (rpoly (1,z)) is Hurwitz iff Re z < 0 ) by A2; ::_thesis: verum end; theorem Th40: :: HURWITZ:40 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; ::_thesis: for z being Element of F_Complex st z <> 0. F_Complex holds ( f is Hurwitz iff z * f is Hurwitz ) let z be Element of F_Complex; ::_thesis: ( z <> 0. F_Complex implies ( f is Hurwitz iff z * f is Hurwitz ) ) assume A1: z <> 0. F_Complex ; ::_thesis: ( f is Hurwitz iff z * f is Hurwitz ) A2: now__::_thesis:_(_f_is_Hurwitz_implies_z_*_f_is_Hurwitz_) assume A3: f is Hurwitz ; ::_thesis: z * f is Hurwitz now__::_thesis:_for_x_being_Element_of_F_Complex_st_x_is_a_root_of_z_*_f_holds_ Re_x_<_0 let x be Element of F_Complex; ::_thesis: ( x is_a_root_of z * f implies Re x < 0 ) assume x is_a_root_of z * f ; ::_thesis: Re x < 0 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; ::_thesis: verum end; hence z * f is Hurwitz by Def8; ::_thesis: verum end; now__::_thesis:_(_z_*_f_is_Hurwitz_implies_f_is_Hurwitz_) assume A4: z * f is Hurwitz ; ::_thesis: f is Hurwitz now__::_thesis:_for_x_being_Element_of_F_Complex_st_x_is_a_root_of_f_holds_ Re_x_<_0 let x be Element of F_Complex; ::_thesis: ( x is_a_root_of f implies Re x < 0 ) assume A5: x is_a_root_of f ; ::_thesis: Re x < 0 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; ::_thesis: verum end; hence f is Hurwitz by Def8; ::_thesis: verum end; hence ( f is Hurwitz iff z * f is Hurwitz ) by A2; ::_thesis: verum end; Lm12: for f, g, h being Polynomial of F_Complex st f = g *' h holds for x being Element of F_Complex st ( x is_a_root_of g or x is_a_root_of h ) holds x is_a_root_of f proof let f, g, h be Polynomial of F_Complex; ::_thesis: ( f = g *' h implies for x being Element of F_Complex st ( x is_a_root_of g or x is_a_root_of h ) holds x is_a_root_of f ) assume A1: f = g *' h ; ::_thesis: for x being Element of F_Complex st ( x is_a_root_of g or x is_a_root_of h ) holds x is_a_root_of f let x be Element of F_Complex; ::_thesis: ( ( x is_a_root_of g or x is_a_root_of h ) implies x is_a_root_of f ) 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 ) ; ::_thesis: x is_a_root_of f percases ( x is_a_root_of g or x is_a_root_of h ) by A3; suppose x is_a_root_of g ; ::_thesis: x is_a_root_of f then eval (g,x) = 0. F_Complex by POLYNOM5:def_6; then eval (f,x) = 0. F_Complex by A2, VECTSP_1:7; hence x is_a_root_of f by POLYNOM5:def_6; ::_thesis: verum end; suppose x is_a_root_of h ; ::_thesis: x is_a_root_of f then eval (h,x) = 0. F_Complex by POLYNOM5:def_6; then eval (f,x) = 0. F_Complex by A2, VECTSP_1:6; hence x is_a_root_of f by POLYNOM5:def_6; ::_thesis: verum end; end; end; theorem Th41: :: HURWITZ:41 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; ::_thesis: ( f *' g is Hurwitz iff ( f is Hurwitz & g is Hurwitz ) ) A1: now__::_thesis:_(_f_is_Hurwitz_&_g_is_Hurwitz_implies_f_*'_g_is_Hurwitz_) assume that A2: f is Hurwitz and A3: g is Hurwitz ; ::_thesis: f *' g is Hurwitz now__::_thesis:_for_z_being_Element_of_F_Complex_st_z_is_a_root_of_f_*'_g_holds_ Re_z_<_0 let z be Element of F_Complex; ::_thesis: ( z is_a_root_of f *' g implies Re b1 < 0 ) assume z is_a_root_of f *' g ; ::_thesis: Re b1 < 0 then A4: 0. F_Complex = eval ((f *' g),z) by POLYNOM5:def_6 .= (eval (f,z)) * (eval (g,z)) by POLYNOM4:24 ; percases ( eval (f,z) = 0. F_Complex or eval (g,z) = 0. F_Complex ) by A4, VECTSP_1:12; suppose eval (f,z) = 0. F_Complex ; ::_thesis: Re b1 < 0 then z is_a_root_of f by POLYNOM5:def_6; hence Re z < 0 by A2, Def8; ::_thesis: verum end; suppose eval (g,z) = 0. F_Complex ; ::_thesis: Re b1 < 0 then z is_a_root_of g by POLYNOM5:def_6; hence Re z < 0 by A3, Def8; ::_thesis: verum end; end; end; hence f *' g is Hurwitz by Def8; ::_thesis: verum end; now__::_thesis:_(_f_*'_g_is_Hurwitz_implies_(_f_is_Hurwitz_&_g_is_Hurwitz_)_) assume A5: f *' g is Hurwitz ; ::_thesis: ( f is Hurwitz & g is Hurwitz ) now__::_thesis:_for_z_being_Element_of_F_Complex_st_z_is_a_root_of_f_holds_ Re_z_<_0 let z be Element of F_Complex; ::_thesis: ( z is_a_root_of f implies Re z < 0 ) assume z is_a_root_of f ; ::_thesis: Re z < 0 then z is_a_root_of f *' g by Lm12; hence Re z < 0 by A5, Def8; ::_thesis: verum end; hence f is Hurwitz by Def8; ::_thesis: g is Hurwitz now__::_thesis:_for_z_being_Element_of_F_Complex_st_z_is_a_root_of_g_holds_ Re_z_<_0 let z be Element of F_Complex; ::_thesis: ( z is_a_root_of g implies Re z < 0 ) assume z is_a_root_of g ; ::_thesis: Re z < 0 then z is_a_root_of f *' g by Lm12; hence Re z < 0 by A5, Def8; ::_thesis: verum end; hence g is Hurwitz by Def8; ::_thesis: verum end; hence ( f *' g is Hurwitz iff ( f is Hurwitz & g is Hurwitz ) ) by A1; ::_thesis: verum end; definition let f be Polynomial of F_Complex; funcf *' -> Polynomial of F_Complex means :Def9: :: HURWITZ:def 9 for i being Element of NAT holds it . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *'); existence ex b1 being Polynomial of F_Complex st for i being Element of NAT holds b1 . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') proof defpred S1[ 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 holds ex y being set st ( y in the carrier of F_Complex & S1[x,y] ) proof let u be set ; ::_thesis: ( u in NAT implies ex y being set st ( y in the carrier of F_Complex & S1[u,y] ) ) assume u in NAT ; ::_thesis: ex y being set st ( y in the carrier of F_Complex & S1[u,y] ) then reconsider u9 = u as Element of NAT ; take ((power F_Complex) . ((- (1_ F_Complex)),u9)) * ((f . u9) *') ; ::_thesis: ( ((power F_Complex) . ((- (1_ F_Complex)),u9)) * ((f . u9) *') in the carrier of F_Complex & S1[u,((power F_Complex) . ((- (1_ F_Complex)),u9)) * ((f . u9) *')] ) thus ( ((power F_Complex) . ((- (1_ F_Complex)),u9)) * ((f . u9) *') in the carrier of F_Complex & S1[u,((power F_Complex) . ((- (1_ F_Complex)),u9)) * ((f . u9) *')] ) ; ::_thesis: verum end; consider g being Function of NAT, the carrier of F_Complex such that A2: for x being set st x in NAT holds S1[x,g . x] from FUNCT_2:sch_1(A1); reconsider g = 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; ::_thesis: for i being Nat st i >= n holds g . i = 0. F_Complex now__::_thesis:_for_i_being_Nat_st_i_>=_n_holds_ g_._i_=_0._F_Complex let i be Nat; ::_thesis: ( i >= n implies g . i = 0. F_Complex ) reconsider i1 = i as Element of NAT by ORDINAL1:def_12; assume A3: i >= n ; ::_thesis: g . i = 0. F_Complex 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 ; ::_thesis: verum end; hence for i being Nat st i >= n holds g . i = 0. F_Complex ; ::_thesis: verum end; then reconsider p = g as AlgSequence of F_Complex by ALGSEQ_1:def_1; take p ; ::_thesis: for i being Element of NAT holds p . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') now__::_thesis:_for_i_being_Element_of_NAT_holds_p_._i_=_((power_F_Complex)_._((-_(1__F_Complex)),i))_*_((f_._i)_*') let i be Element of NAT ; ::_thesis: p . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') 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) *') ; ::_thesis: verum end; hence for i being Element of NAT holds p . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ; ::_thesis: verum end; uniqueness for b1, b2 being Polynomial of F_Complex st ( for i being Element of NAT holds b1 . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ) & ( for i being Element of NAT holds b2 . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ) holds b1 = b2 proof let z1, z2 be AlgSequence of F_Complex; ::_thesis: ( ( for i being Element of NAT holds z1 . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ) & ( for i being Element of NAT holds z2 . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ) implies z1 = z2 ) assume A4: for i being Element of NAT holds z1 . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ; ::_thesis: ( ex i being Element of NAT st not z2 . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') or z1 = z2 ) assume A5: for i being Element of NAT holds z2 . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ; ::_thesis: z1 = z2 A6: now__::_thesis:_for_x_being_set_st_x_in_dom_z1_holds_ z1_._x_=_z2_._x let x be set ; ::_thesis: ( x in dom z1 implies z1 . x = z2 . x ) assume x in dom z1 ; ::_thesis: z1 . x = z2 . x 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 ; ::_thesis: verum end; dom z1 = NAT by FUNCT_2:def_1 .= dom z2 by FUNCT_2:def_1 ; hence z1 = z2 by A6, FUNCT_1:2; ::_thesis: verum end; involutiveness for b1, b2 being Polynomial of F_Complex st ( for i being Element of NAT holds b1 . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((b2 . i) *') ) holds for i being Element of NAT holds b2 . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((b1 . i) *') proof let g, f be Polynomial of F_Complex; ::_thesis: ( ( for i being Element of NAT holds g . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ) implies for i being Element of NAT holds f . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((g . i) *') ) assume A7: for i being Element of NAT holds g . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ; ::_thesis: for i being Element of NAT holds f . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((g . i) *') let i be Element of NAT ; ::_thesis: f . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((g . i) *') 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 ; ::_thesis: verum end; end; :: deftheorem Def9 defines *' HURWITZ:def_9_:_ for f, b2 being Polynomial of F_Complex holds ( b2 = f *' iff for i being Element of NAT holds b2 . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ); theorem Th42: :: HURWITZ:42 for f being Polynomial of F_Complex holds deg (f *') = deg f proof let f be Polynomial of F_Complex; ::_thesis: deg (f *') = deg f A1: for k being Nat holds ( f . k = 0. F_Complex iff (f *') . k = 0. F_Complex ) proof let k be Nat; ::_thesis: ( f . k = 0. F_Complex iff (f *') . k = 0. F_Complex ) reconsider k1 = k as Element of NAT by ORDINAL1:def_12; hereby ::_thesis: ( (f *') . k = 0. F_Complex implies f . k = 0. F_Complex ) assume f . k = 0. F_Complex ; ::_thesis: (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 ; ::_thesis: verum end; assume (f *') . k = 0. F_Complex ; ::_thesis: 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 f . k = 0. F_Complex by COMPLEX1:28, COMPLFLD:7; ::_thesis: verum end; A3: now__::_thesis:_not_len_f_>_len_(f_*') assume A4: len f > len (f *') ; ::_thesis: contradiction 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; ::_thesis: verum end; now__::_thesis:_for_i_being_Nat_st_i_>=_len_f_holds_ (f_*')_._i_=_0._F_Complex let i be Nat; ::_thesis: ( i >= len f implies (f *') . i = 0. F_Complex ) assume i >= len f ; ::_thesis: (f *') . i = 0. F_Complex then f . i = 0. F_Complex by ALGSEQ_1:8; hence (f *') . i = 0. F_Complex by A1; ::_thesis: verum 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 deg (f *') = deg f by A3, XXREAL_0:1; ::_thesis: verum end; theorem :: HURWITZ:43 canceled; theorem Th44: :: HURWITZ:44 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; ::_thesis: for z being Element of F_Complex holds (z * f) *' = (z *') * (f *') let x be Element of F_Complex; ::_thesis: (x * f) *' = (x *') * (f *') set g1 = x * f; set g2 = (x *') * (f *'); A1: now__::_thesis:_for_k9_being_set_st_k9_in_dom_((x_*_f)_*')_holds_ ((x_*_f)_*')_._k9_=_((x_*')_*_(f_*'))_._k9 let k9 be set ; ::_thesis: ( k9 in dom ((x * f) *') implies ((x * f) *') . k9 = ((x *') * (f *')) . k9 ) assume k9 in dom ((x * f) *') ; ::_thesis: ((x * f) *') . k9 = ((x *') * (f *')) . k9 then reconsider k = k9 as Element of NAT ; (x * f) . k = x * (f . k) by POLYNOM5:def_3; then ((x * f) *') . 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 ((x * f) *') . k9 = ((x *') * (f *')) . k9 by POLYNOM5:def_3; ::_thesis: verum end; dom ((x * f) *') = NAT by FUNCT_2:def_1 .= dom ((x *') * (f *')) by FUNCT_2:def_1 ; hence (x * f) *' = (x *') * (f *') by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th45: :: HURWITZ:45 for f being Polynomial of F_Complex holds (- f) *' = - (f *') proof let f be Polynomial of F_Complex; ::_thesis: (- f) *' = - (f *') set h1 = - f; A1: now__::_thesis:_for_k9_being_set_st_k9_in_dom_((-_f)_*')_holds_ ((-_f)_*')_._k9_=_(-_(f_*'))_._k9 let k9 be set ; ::_thesis: ( k9 in dom ((- f) *') implies ((- f) *') . k9 = (- (f *')) . k9 ) assume k9 in dom ((- f) *') ; ::_thesis: ((- f) *') . k9 = (- (f *')) . k9 then reconsider k = k9 as Element of NAT ; (- f) . k = - (f . k) by BHSP_1:44; then ((- f) *') . 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 ((- f) *') . k9 = (- (f *')) . k9 by BHSP_1:44; ::_thesis: verum end; dom ((- f) *') = NAT by FUNCT_2:def_1 .= dom (- (f *')) by FUNCT_2:def_1 ; hence (- f) *' = - (f *') by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th46: :: HURWITZ:46 for f, g being Polynomial of F_Complex holds (f + g) *' = (f *') + (g *') proof let f, g be Polynomial of F_Complex; ::_thesis: (f + g) *' = (f *') + (g *') set h1 = f + g; A1: now__::_thesis:_for_k9_being_set_st_k9_in_dom_((f_+_g)_*')_holds_ ((f_+_g)_*')_._k9_=_((f_*')_+_(g_*'))_._k9 let k9 be set ; ::_thesis: ( k9 in dom ((f + g) *') implies ((f + g) *') . k9 = ((f *') + (g *')) . k9 ) assume k9 in dom ((f + g) *') ; ::_thesis: ((f + g) *') . k9 = ((f *') + (g *')) . k9 then reconsider k = k9 as Element of NAT ; (f + g) . k = (f . k) + (g . k) by NORMSP_1:def_2; then ((f + g) *') . 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 ((f + g) *') . k9 = ((f *') + (g *')) . k9 by NORMSP_1:def_2; ::_thesis: verum end; dom ((f + g) *') = NAT by FUNCT_2:def_1 .= dom ((f *') + (g *')) by FUNCT_2:def_1 ; hence (f + g) *' = (f *') + (g *') by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th47: :: HURWITZ:47 for f, g being Polynomial of F_Complex holds (f *' g) *' = (f *') *' (g *') proof let f, g be Polynomial of F_Complex; ::_thesis: (f *' g) *' = (f *') *' (g *') set h1 = f *' g; A1: now__::_thesis:_for_k9_being_set_st_k9_in_dom_((f_*'_g)_*')_holds_ ((f_*'_g)_*')_._k9_=_((f_*')_*'_(g_*'))_._k9 let k9 be set ; ::_thesis: ( k9 in dom ((f *' g) *') implies ((f *' g) *') . k9 = ((f *') *' (g *')) . k9 ) assume k9 in dom ((f *' g) *') ; ::_thesis: ((f *' g) *') . k9 = ((f *') *' (g *')) . k9 then reconsider k = k9 as Element of NAT ; consider s being FinSequence of F_Complex such that A2: len s = k + 1 and A3: (f *' g) . k = Sum s and A4: for j being Element of NAT st j in dom s holds s . j = (f . (j -' 1)) * (g . ((k + 1) -' j)) by POLYNOM3:def_9; defpred S1[ 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 being 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) holds ex x being Element of F_Complex st S1[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 S1[j,u . j] ) ) from FINSEQ_1:sch_5(A8); A10: now__::_thesis:_for_j_being_Element_of_NAT_st_j_in_dom_u_holds_ u_/._j_=_(s_/._j)_*' let j be Element of NAT ; ::_thesis: ( j in dom u implies u /. j = (s /. j) *' ) assume A11: j in dom u ; ::_thesis: u /. j = (s /. j) *' hence u /. j = u . j by PARTFUN1:def_6 .= (s /. j) *' by A9, A11 ; ::_thesis: verum 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__::_thesis:_for_j_being_Element_of_NAT_st_j_in_dom_t_holds_ t_._j_=_((power_F_Complex)_._((-_(1__F_Complex)),k))_*_((s_/._j)_*') let j be Element of NAT ; ::_thesis: ( j in dom t implies t . j = ((power F_Complex) . ((- (1_ F_Complex)),k)) * ((s /. j) *') ) assume A15: j in dom t ; ::_thesis: t . j = ((power F_Complex) . ((- (1_ F_Complex)),k)) * ((s /. j) *') 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 ; ::_thesis: verum end; A20: ((power F_Complex) . ((- (1_ F_Complex)),k)) * u = t proof set b = (power F_Complex) . ((- (1_ F_Complex)),k); set a = ((power F_Complex) . ((- (1_ F_Complex)),k)) * u; A21: dom (((power F_Complex) . ((- (1_ F_Complex)),k)) * u) = dom u by POLYNOM1:def_1; now__::_thesis:_for_j_being_Nat_st_j_in_dom_t_holds_ (((power_F_Complex)_._((-_(1__F_Complex)),k))_*_u)_._j_=_t_._j let j be Nat; ::_thesis: ( j in dom t implies (((power F_Complex) . ((- (1_ F_Complex)),k)) * u) . j = t . j ) assume A22: j in dom t ; ::_thesis: (((power F_Complex) . ((- (1_ F_Complex)),k)) * u) . j = t . j hence (((power F_Complex) . ((- (1_ F_Complex)),k)) * u) . j = (((power F_Complex) . ((- (1_ F_Complex)),k)) * u) /. j by A12, A21, PARTFUN1:def_6 .= ((power F_Complex) . ((- (1_ F_Complex)),k)) * (u /. j) by A12, A22, POLYNOM1:def_1 .= ((power F_Complex) . ((- (1_ F_Complex)),k)) * ((s /. j) *') by A10, A12, A22 .= t . j by A14, A22 ; ::_thesis: verum end; hence ((power F_Complex) . ((- (1_ F_Complex)),k)) * u = t by A12, A21, FINSEQ_1:13; ::_thesis: verum end; len u = len s by A9, FINSEQ_1:def_3; then Sum u = (Sum s) *' by A10, Th6; then ((f *' g) *') . k = ((power F_Complex) . ((- (1_ F_Complex)),k)) * (Sum u) by A3, Def9 .= ((f *') *' (g *')) . k by A6, A20, Th8 ; hence ((f *' g) *') . k9 = ((f *') *' (g *')) . k9 ; ::_thesis: verum end; dom ((f *' g) *') = NAT by FUNCT_2:def_1 .= dom ((f *') *' (g *')) by FUNCT_2:def_1 ; hence (f *' g) *' = (f *') *' (g *') by A1, FUNCT_1:2; ::_thesis: verum 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 ; ::_thesis: 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 let u, v, uv, vv be Element of REAL ; ::_thesis: ( x = u + (v * ) & xv = uv + (vv * ) implies (|.(x + (xv *')).| ^2) - (|.(x - xv).| ^2) = (4 * u) * uv ) assume that A1: x = u + (v * ) and A2: xv = uv + (vv * ) ; ::_thesis: (|.(x + (xv *')).| ^2) - (|.(x - xv).| ^2) = (4 * u) * uv 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 (|.(x + (xv *')).| ^2) - (|.(x - xv).| ^2) = (4 * u) * uv by A5, A6, A8, A7, SQUARE_1:def_2; ::_thesis: verum 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 ; ::_thesis: 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 *')).| ) ) let u, v, uv, vv be Element of REAL ; ::_thesis: ( x = u + (v * ) & xv = uv + (vv * ) & uv < 0 implies ( ( u < 0 implies |.(x - xv).| < |.(x + (xv *')).| ) & ( u > 0 implies |.(x - xv).| > |.(x + (xv *')).| ) & ( u = 0 implies |.(x - xv).| = |.(x + (xv *')).| ) ) ) assume that A1: x = u + (v * ) and A2: xv = uv + (vv * ) and A3: uv < 0 ; ::_thesis: ( ( u < 0 implies |.(x - xv).| < |.(x + (xv *')).| ) & ( u > 0 implies |.(x - xv).| > |.(x + (xv *')).| ) & ( u = 0 implies |.(x - xv).| = |.(x + (xv *')).| ) ) now__::_thesis:_(_u_<_0_implies_|.(x_+_(xv_*')).|_>_|.(x_-_xv).|_) assume u < 0 ; ::_thesis: |.(x + (xv *')).| > |.(x - xv).| 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; ::_thesis: verum end; hence ( u < 0 implies |.(x - xv).| < |.(x + (xv *')).| ) ; ::_thesis: ( ( u > 0 implies |.(x - xv).| > |.(x + (xv *')).| ) & ( u = 0 implies |.(x - xv).| = |.(x + (xv *')).| ) ) now__::_thesis:_(_u_>_0_implies_|.(x_+_(xv_*')).|_<_|.(x_-_xv).|_) assume u > 0 ; ::_thesis: |.(x + (xv *')).| < |.(x - xv).| 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; ::_thesis: verum end; hence ( u > 0 implies |.(x - xv).| > |.(x + (xv *')).| ) ; ::_thesis: ( u = 0 implies |.(x - xv).| = |.(x + (xv *')).| ) now__::_thesis:_(_u_=_0_implies_|.(x_-_xv).|_=_|.(x_+_(xv_*')).|_) assume u = 0 ; ::_thesis: |.(x - xv).| = |.(x + (xv *')).| then (4 * u) * uv = 0 ; then A6: (|.(x + (xv *')).| ^2) - (|.(x - xv).| ^2) = 0 by A1, A2, Lm13; now__::_thesis:_not_|.(x_-_xv).|_<>_|.(x_+_(xv_*')).| assume A7: |.(x - xv).| <> |.(x + (xv *')).| ; ::_thesis: contradiction percases ( |.(x - xv).| > |.(x + (xv *')).| or |.(x - xv).| < |.(x + (xv *')).| ) by A7, XXREAL_0:1; suppose |.(x - xv).| > |.(x + (xv *')).| ; ::_thesis: contradiction hence contradiction by A6, COMPLEX1:46, SQUARE_1:16; ::_thesis: verum end; suppose |.(x - xv).| < |.(x + (xv *')).| ; ::_thesis: contradiction hence contradiction by A6, COMPLEX1:46, SQUARE_1:16; ::_thesis: verum end; end; end; hence |.(x - xv).| = |.(x + (xv *')).| ; ::_thesis: verum end; hence ( u = 0 implies |.(x - xv).| = |.(x + (xv *')).| ) ; ::_thesis: verum end; theorem Th48: :: HURWITZ:48 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; ::_thesis: eval (((rpoly (1,z)) *'),x) = (- x) - (z *') set p = (rpoly (1,z)) *' ; consider F being FinSequence of F_Complex such that A1: eval (((rpoly (1,z)) *'),x) = Sum F and A2: len F = len ((rpoly (1,z)) *') and A3: for n being Element of NAT st n in dom F holds F . n = (((rpoly (1,z)) *') . (n -' 1)) * ((power F_Complex) . (x,(n -' 1))) by POLYNOM4:def_2; A4: deg ((rpoly (1,z)) *') = 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 ((rpoly (1,z)) *') = 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 = (((rpoly (1,z)) *') . 1) * ((power F_Complex) . (x,(1 + 0))) by A3, A7 .= (((rpoly (1,z)) *') . 1) * (((power F_Complex) . (x,0)) * x) by GROUP_1:def_7 .= (((rpoly (1,z)) *') . 1) * ((1_ F_Complex) * x) by GROUP_1:def_7 .= (((rpoly (1,z)) *') . 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 = (((rpoly (1,z)) *') . 0) * ((power F_Complex) . (x,0)) by A3, A6 .= (((rpoly (1,z)) *') . 0) * (1_ F_Complex) by GROUP_1:def_7 .= ((rpoly (1,z)) *') . 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 (((rpoly (1,z)) *'),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 ; ::_thesis: verum end; theorem Th49: :: HURWITZ:49 for f being Polynomial of F_Complex st f is Hurwitz holds for x being Element of F_Complex st Re x >= 0 holds 0 < |.(eval (f,x)).| proof let f be Polynomial of F_Complex; ::_thesis: ( f is Hurwitz implies for x being Element of F_Complex st Re x >= 0 holds 0 < |.(eval (f,x)).| ) assume A1: f is Hurwitz ; ::_thesis: for x being Element of F_Complex st Re x >= 0 holds 0 < |.(eval (f,x)).| let x be Element of F_Complex; ::_thesis: ( Re x >= 0 implies 0 < |.(eval (f,x)).| ) assume A2: Re x >= 0 ; ::_thesis: 0 < |.(eval (f,x)).| now__::_thesis:_not_eval_(f,x)_=_0._F_Complex assume eval (f,x) = 0. F_Complex ; ::_thesis: contradiction then x is_a_root_of f by POLYNOM5:def_6; hence contradiction by A1, A2, Def8; ::_thesis: verum end; hence 0 < |.(eval (f,x)).| by COMPLEX1:47, COMPLFLD:7; ::_thesis: verum end; theorem Th50: :: HURWITZ:50 for f being Polynomial of F_Complex st deg f >= 1 & f is Hurwitz holds 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__::_thesis:_for_y,_z_being_Element_of_F_Complex_st_rpoly_(1,z)_is_Hurwitz_&_Re_y_>_0_holds_ |.(eval_((rpoly_(1,z)),y)).|_>_|.(eval_(((rpoly_(1,z))_*'),y)).| let y, z be Element of F_Complex; ::_thesis: ( rpoly (1,z) is Hurwitz & Re y > 0 implies |.(eval ((rpoly (1,z)),y)).| > |.(eval (((rpoly (1,z)) *'),y)).| ) assume A2: rpoly (1,z) is Hurwitz ; ::_thesis: ( Re y > 0 implies |.(eval ((rpoly (1,z)),y)).| > |.(eval (((rpoly (1,z)) *'),y)).| ) 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 ; ::_thesis: |.(eval ((rpoly (1,z)),y)).| > |.(eval (((rpoly (1,z)) *'),y)).| 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; ::_thesis: verum end; A10: now__::_thesis:_for_a,_y,_z_being_Element_of_F_Complex_st_rpoly_(1,z)_is_Hurwitz_&_a_<>_0._F_Complex_&_Re_y_>_0_holds_ |.(eval_((a_*_(rpoly_(1,z))),y)).|_>_|.(eval_(((a_*_(rpoly_(1,z)))_*'),y)).| let a, y, z be Element of F_Complex; ::_thesis: ( rpoly (1,z) is Hurwitz & a <> 0. F_Complex & Re y > 0 implies |.(eval ((a * (rpoly (1,z))),y)).| > |.(eval (((a * (rpoly (1,z))) *'),y)).| ) assume that A11: rpoly (1,z) is Hurwitz and A12: a <> 0. F_Complex ; ::_thesis: ( Re y > 0 implies |.(eval ((a * (rpoly (1,z))),y)).| > |.(eval (((a * (rpoly (1,z))) *'),y)).| ) assume A13: Re y > 0 ; ::_thesis: |.(eval ((a * (rpoly (1,z))),y)).| > |.(eval (((a * (rpoly (1,z))) *'),y)).| 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; ::_thesis: verum end; A16: now__::_thesis:_for_y,_z_being_Element_of_F_Complex_st_rpoly_(1,z)_is_Hurwitz_&_Re_y_<_0_holds_ |.(eval_((rpoly_(1,z)),y)).|_<_|.(eval_(((rpoly_(1,z))_*'),y)).| let y, z be Element of F_Complex; ::_thesis: ( rpoly (1,z) is Hurwitz & Re y < 0 implies |.(eval ((rpoly (1,z)),y)).| < |.(eval (((rpoly (1,z)) *'),y)).| ) assume A17: rpoly (1,z) is Hurwitz ; ::_thesis: ( Re y < 0 implies |.(eval ((rpoly (1,z)),y)).| < |.(eval (((rpoly (1,z)) *'),y)).| ) 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 ; ::_thesis: |.(eval ((rpoly (1,z)),y)).| < |.(eval (((rpoly (1,z)) *'),y)).| 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; ::_thesis: verum end; A25: now__::_thesis:_for_a,_y,_z_being_Element_of_F_Complex_st_rpoly_(1,z)_is_Hurwitz_&_a_<>_0._F_Complex_&_Re_y_<_0_holds_ |.(eval_((a_*_(rpoly_(1,z))),y)).|_<_|.(eval_(((a_*_(rpoly_(1,z)))_*'),y)).| let a, y, z be Element of F_Complex; ::_thesis: ( rpoly (1,z) is Hurwitz & a <> 0. F_Complex & Re y < 0 implies |.(eval ((a * (rpoly (1,z))),y)).| < |.(eval (((a * (rpoly (1,z))) *'),y)).| ) assume that A26: rpoly (1,z) is Hurwitz and A27: a <> 0. F_Complex ; ::_thesis: ( Re y < 0 implies |.(eval ((a * (rpoly (1,z))),y)).| < |.(eval (((a * (rpoly (1,z))) *'),y)).| ) assume A28: Re y < 0 ; ::_thesis: |.(eval ((a * (rpoly (1,z))),y)).| < |.(eval (((a * (rpoly (1,z))) *'),y)).| 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; ::_thesis: verum end; defpred S1[ Nat] means for f being Polynomial of F_Complex st deg f >= 1 & f is Hurwitz & deg f = $1 holds 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; ::_thesis: ( deg f >= 1 & f is Hurwitz implies 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)).| ) ) ) assume that A31: deg f >= 1 and A32: f is Hurwitz ; ::_thesis: 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)).| ) ) A33: now__::_thesis:_for_y,_z_being_Element_of_F_Complex_st_rpoly_(1,z)_is_Hurwitz_&_Re_y_=_0_holds_ |.(eval_((rpoly_(1,z)),y)).|_=_|.(eval_(((rpoly_(1,z))_*'),y)).| let y, z be Element of F_Complex; ::_thesis: ( rpoly (1,z) is Hurwitz & Re y = 0 implies |.(eval ((rpoly (1,z)),y)).| = |.(eval (((rpoly (1,z)) *'),y)).| ) assume A34: rpoly (1,z) is Hurwitz ; ::_thesis: ( Re y = 0 implies |.(eval ((rpoly (1,z)),y)).| = |.(eval (((rpoly (1,z)) *'),y)).| ) 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 ; ::_thesis: |.(eval ((rpoly (1,z)),y)).| = |.(eval (((rpoly (1,z)) *'),y)).| 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; ::_thesis: verum end; A42: now__::_thesis:_for_a,_y,_z_being_Element_of_F_Complex_st_rpoly_(1,z)_is_Hurwitz_&_a_<>_0._F_Complex_&_Re_y_=_0_holds_ |.(eval_((a_*_(rpoly_(1,z))),y)).|_=_|.(eval_(((a_*_(rpoly_(1,z)))_*'),y)).| let a, y, z be Element of F_Complex; ::_thesis: ( rpoly (1,z) is Hurwitz & a <> 0. F_Complex & Re y = 0 implies |.(eval ((a * (rpoly (1,z))),y)).| = |.(eval (((a * (rpoly (1,z))) *'),y)).| ) assume that A43: rpoly (1,z) is Hurwitz and a <> 0. F_Complex ; ::_thesis: ( Re y = 0 implies |.(eval ((a * (rpoly (1,z))),y)).| = |.(eval (((a * (rpoly (1,z))) *'),y)).| ) 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 ; ::_thesis: |.(eval ((a * (rpoly (1,z))),y)).| = |.(eval (((a * (rpoly (1,z))) *'),y)).| hence |.(eval ((a * (rpoly (1,z))),y)).| = |.(eval (((a * (rpoly (1,z))) *'),y)).| by A33, A43, A44, A45; ::_thesis: verum end; A46: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A47: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_f_being_Polynomial_of_F_Complex_st_deg_f_>=_1_&_f_is_Hurwitz_&_deg_f_=_k_+_1_holds_ 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; ::_thesis: ( deg f >= 1 & f is Hurwitz & deg f = k + 1 implies for x being Element of F_Complex holds ( ( Re b3 < 0 implies |.(eval (b2,b3)).| < |.(eval ((b2 *'),b3)).| ) & ( Re b3 > 0 implies |.(eval (b2,b3)).| > |.(eval ((b2 *'),b3)).| ) & ( Re b3 = 0 implies |.(eval (b2,b3)).| = |.(eval ((b2 *'),b3)).| ) ) ) assume that A48: deg f >= 1 and A49: f is Hurwitz and A50: deg f = k + 1 ; ::_thesis: for x being Element of F_Complex holds ( ( Re b3 < 0 implies |.(eval (b2,b3)).| < |.(eval ((b2 *'),b3)).| ) & ( Re b3 > 0 implies |.(eval (b2,b3)).| > |.(eval ((b2 *'),b3)).| ) & ( Re b3 = 0 implies |.(eval (b2,b3)).| = |.(eval ((b2 *'),b3)).| ) ) let x be Element of F_Complex; ::_thesis: ( ( Re b2 < 0 implies |.(eval (b1,b2)).| < |.(eval ((b1 *'),b2)).| ) & ( Re b2 > 0 implies |.(eval (b1,b2)).| > |.(eval ((b1 *'),b2)).| ) & ( Re b2 = 0 implies |.(eval (b1,b2)).| = |.(eval ((b1 *'),b2)).| ) ) percases ( k + 1 = 1 or k + 1 > 1 ) by A48, A50, XXREAL_0:1; suppose k + 1 = 1 ; ::_thesis: ( ( Re b2 < 0 implies |.(eval (b1,b2)).| < |.(eval ((b1 *'),b2)).| ) & ( Re b2 > 0 implies |.(eval (b1,b2)).| > |.(eval ((b1 *'),b2)).| ) & ( Re b2 = 0 implies |.(eval (b1,b2)).| = |.(eval ((b1 *'),b2)).| ) ) 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; ::_thesis: verum end; supposeA53: k + 1 > 1 ; ::_thesis: ( ( Re b2 < 0 implies |.(eval (b1,b2)).| < |.(eval ((b1 *'),b2)).| ) & ( Re b2 > 0 implies |.(eval (b1,b2)).| > |.(eval ((b1 *'),b2)).| ) & ( Re b2 = 0 implies |.(eval (b1,b2)).| = |.(eval ((b1 *'),b2)).| ) ) 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__::_thesis:_(_Re_x_>_0_implies_|.(eval_(f,x)).|_>_|.(eval_((f_*'),x)).|_) 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 ; ::_thesis: |.(eval (f,x)).| > |.(eval ((f *'),x)).| 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; ::_thesis: verum end; A69: now__::_thesis:_(_Re_x_<_0_implies_|.(eval_(f,x)).|_<_|.(eval_((f_*'),x)).|_) 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 ; ::_thesis: |.(eval (f,x)).| < |.(eval ((f *'),x)).| 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; ::_thesis: verum end; now__::_thesis:_(_Re_x_=_0_implies_|.(eval_(f,x)).|_=_|.(eval_((f_*'),x)).|_) 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 ; ::_thesis: |.(eval (f,x)).| = |.(eval ((f *'),x)).| 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; ::_thesis: verum 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; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; let x be Element of F_Complex; ::_thesis: ( ( 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)).| ) ) A79: S1[ 0 ] ; A80: for k being Element of NAT holds S1[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 ( ( 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 A31, A32, A80; ::_thesis: verum 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 :: HURWITZ:def 10 ((eval ((f *'),z)) * f) - ((eval (f,z)) * (f *')); coherence ((eval ((f *'),z)) * f) - ((eval (f,z)) * (f *')) is Polynomial of F_Complex ; end; :: deftheorem defines F* HURWITZ:def_10_:_ for f being Polynomial of F_Complex for z being Element of F_Complex holds F* (f,z) = ((eval ((f *'),z)) * f) - ((eval (f,z)) * (f *')); theorem Th51: :: HURWITZ:51 for a, b being Element of F_Complex st |.a.| > |.b.| holds 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; ::_thesis: ( |.a.| > |.b.| implies for f being Polynomial of F_Complex st deg f >= 1 holds ( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz ) ) assume A1: |.a.| > |.b.| ; ::_thesis: for f being Polynomial of F_Complex st deg f >= 1 holds ( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz ) 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; ::_thesis: ( deg f >= 1 implies ( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz ) ) assume A4: deg f >= 1 ; ::_thesis: ( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz ) set g = (a * f) - (b * (f *')); percases ( b = 0. F_Complex or b <> 0. F_Complex ) ; suppose b = 0. F_Complex ; ::_thesis: ( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz ) then (a * f) - (b * (f *')) = (a * f) - (0_. F_Complex) by POLYNOM5:26 .= (a * f) + (0_. F_Complex) by Th9 .= a * f by POLYNOM3:28 ; hence ( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz ) by A3, Th40; ::_thesis: verum end; supposeA5: b <> 0. F_Complex ; ::_thesis: ( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz ) 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; set b1 = - (b * zz); reconsider a19 = (a *') * zz, b19 = - (b * zz) 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: - (- (b * zz)) <> 0. F_Complex by A5, COMPLFLD:7, RLVECT_1:17; A11: now__::_thesis:_(_f_is_Hurwitz_implies_(a_*_f)_-_(b_*_(f_*'))_is_Hurwitz_) assume A12: f is Hurwitz ; ::_thesis: (a * f) - (b * (f *')) is Hurwitz now__::_thesis:_for_z_being_Element_of_F_Complex_st_z_is_a_root_of_(a_*_f)_-_(b_*_(f_*'))_holds_ Re_z_<_0 let z be Element of F_Complex; ::_thesis: ( z is_a_root_of (a * f) - (b * (f *')) implies Re z < 0 ) assume z is_a_root_of (a * f) - (b * (f *')) ; ::_thesis: Re z < 0 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__::_thesis:_not_Re_z_>=_0 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 ; ::_thesis: contradiction percases ( Re z = 0 or Re z > 0 ) by A17; supposeA18: Re z = 0 ; ::_thesis: contradiction 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; ::_thesis: verum end; suppose Re z > 0 ; ::_thesis: contradiction 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; ::_thesis: verum end; end; end; hence Re z < 0 ; ::_thesis: verum end; hence (a * f) - (b * (f *')) is Hurwitz by Def8; ::_thesis: verum end; A22: |.((a *') * zz).| = |.(a *').| * |.(((|.a.| ^2) - (|.b.| ^2)) ").| by COMPLEX1:65 .= |.a.| * |.(((|.a.| ^2) - (|.b.| ^2)) ").| by COMPLEX1:53 ; A23: now__::_thesis:_for_z_being_Element_of_COMPLEX_holds_(z_*')_*_z_=_|.z.|_^2 let z be Element of COMPLEX ; ::_thesis: (z *') * z = |.z.| ^2 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; ::_thesis: verum 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 (- (b * zz)) " = b19 " by A5, A9, COMPLFLD:5, COMPLFLD:7; then A32: - ((- (b * zz)) ") = - (b19 ") by COMPLFLD:2; A33: now__::_thesis:_not_(-_(b_*_zz))_"_=_0._F_Complex assume A34: (- (b * zz)) " = 0. F_Complex ; ::_thesis: contradiction ((- (b * zz)) ") * (- (b * zz)) = 1_ F_Complex by A5, A9, A31, COMPLFLD:7, VECTSP_1:def_10; hence contradiction by A34, VECTSP_1:6; ::_thesis: verum end; A35: now__::_thesis:_not_-_((-_(b_*_zz))_")_=_0._F_Complex assume - ((- (b * zz)) ") = 0. F_Complex ; ::_thesis: contradiction then - (- ((- (b * zz)) ")) = 0. F_Complex by RLVECT_1:12; hence contradiction by A33, RLVECT_1:17; ::_thesis: verum end; (- (b * zz)) " = b19 " by A5, A9, A31, COMPLFLD:5, COMPLFLD:7; then - ((- (b * zz)) ") = - (b19 ") by COMPLFLD:2; then A36: (- ((- (b * zz)) ")) " = (- (b19 ")) " by A35, COMPLFLD:5; (- ((- (b * zz)) ")) " = - (((- (b * zz)) ") ") by A33, Th1 .= - (- (b * zz)) 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: ((- ((- (b * zz)) ")) ") * ((a *') * (b ")) = (a *') * zz by A35, A6, A32, COMPLFLD:5; A38: (a9 *') * ((b9 ") * a9) = (a *') * ((b ") * a) by A5, COMPLFLD:5; A39: |.(- (b * zz)).| = |.(- (b * (((|.a.| ^2) - (|.b.| ^2)) "))).| by COMPLFLD:2 .= |.(b * (((|.a.| ^2) - (|.b.| ^2)) ")).| by COMPLEX1:52 .= |.b.| * |.(((|.a.| ^2) - (|.b.| ^2)) ").| by COMPLEX1:65 ; - (- (b * zz)) = - b19 by COMPLFLD:2; then A40: (- b19) " = (- (- (b * zz))) " by A10, COMPLFLD:5 .= - ((- (b * zz)) ") 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__::_thesis:_not_b19_=_0._F_Complex assume b19 = 0. F_Complex ; ::_thesis: contradiction 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; ::_thesis: verum end; (b * (f *')) + ((a * f) - (b * (f *'))) = (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) - ((a * f) - (b * (f *'))) = ((b * (f *')) + ((a * f) - (b * (f *')))) - ((a * f) - (b * (f *'))) by POLYNOM3:28 .= (b * (f *')) + (((a * f) - (b * (f *'))) - ((a * f) - (b * (f *')))) 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) - ((a * f) - (b * (f *')))) by A44, POLYNOM3:28 ; ((a * f) - (b * (f *'))) *' = ((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 ((a * f) - (b * (f *'))) *' = ((a *') * (((b ") * (a * f)) + ((b ") * (- ((a * f) - (b * (f *'))))))) + (- ((b *') * f)) by A45, Th18 .= (((a *') * ((b ") * (a * f))) + ((a *') * ((b ") * (- ((a * f) - (b * (f *'))))))) + (- ((b *') * f)) by Th18 .= ((a *') * ((b ") * (- ((a * f) - (b * (f *')))))) + (((a *') * ((b ") * (a * f))) + (- ((b *') * f))) by POLYNOM3:26 .= ((a *') * ((b ") * (- ((a * f) - (b * (f *')))))) + (((a *') * (((b ") * a) * f)) + (- ((b *') * f))) by Th14 .= ((a *') * ((b ") * (- ((a * f) - (b * (f *')))))) + ((((a *') * ((b ") * a)) * f) + (- ((b *') * f))) by Th14 .= ((a *') * ((b ") * (- ((a * f) - (b * (f *')))))) + ((((a *') * ((b ") * a)) * f) + ((- (b *')) * f)) by Th15 .= ((a *') * ((b ") * (- ((a * f) - (b * (f *')))))) + ((((a *') * ((b ") * a)) + (- (b *'))) * f) by Th17 .= (((a *') * (b ")) * (- ((a * f) - (b * (f *'))))) + ((((a *') * ((b ") * a)) + (- (b *'))) * f) by Th14 ; then A46: (((a * f) - (b * (f *'))) *') + (- (((a *') * (b ")) * (- ((a * f) - (b * (f *')))))) = ((((a *') * ((b ") * a)) + (- (b *'))) * f) + ((((a *') * (b ")) * (- ((a * f) - (b * (f *'))))) - (((a *') * (b ")) * (- ((a * f) - (b * (f *')))))) 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 .= (((- ((- (b * zz)) ")) ") * (- ((- (b * zz)) "))) * f by A5, A29, A9, A30, A40, COMPLFLD:7, VECTSP_1:def_10 .= ((- ((- (b * zz)) ")) ") * ((- ((- (b * zz)) ")) * f) by Th14 .= ((- ((- (b * zz)) ")) ") * ((((a * f) - (b * (f *'))) *') + (- (((a *') * (b ")) * (- ((a * f) - (b * (f *'))))))) by A46, A30, A38, A47, A40, POLYNOM3:28 .= (((- ((- (b * zz)) ")) ") * (((a * f) - (b * (f *'))) *')) + (((- ((- (b * zz)) ")) ") * (- (((a *') * (b ")) * (- ((a * f) - (b * (f *'))))))) by Th18 .= (((- ((- (b * zz)) ")) ") * (((a * f) - (b * (f *'))) *')) + (((- ((- (b * zz)) ")) ") * (((a *') * (b ")) * (- (- ((a * f) - (b * (f *'))))))) by Th16 .= (((- ((- (b * zz)) ")) ") * (((a * f) - (b * (f *'))) *')) + (((- ((- (b * zz)) ")) ") * (((a *') * (b ")) * ((a * f) - (b * (f *'))))) by Lm3 .= (((- ((- (b * zz)) ")) ") * (((a * f) - (b * (f *'))) *')) + (((a *') * zz) * ((a * f) - (b * (f *')))) by A37, Th14 .= ((((- (- (b * zz))) ") ") * (((a * f) - (b * (f *'))) *')) + (((a *') * zz) * ((a * f) - (b * (f *')))) by A5, A9, A31, Th1, COMPLFLD:7 .= ((- (- (b * zz))) * (((a * f) - (b * (f *'))) *')) + (((a *') * zz) * ((a * f) - (b * (f *')))) by A10, VECTSP_1:24 .= (- ((- (b * zz)) * (((a * f) - (b * (f *'))) *'))) + (((a *') * zz) * ((a * f) - (b * (f *')))) by Th15 ; then deg f <= max ((deg (((a *') * zz) * ((a * f) - (b * (f *'))))),(deg (- ((- (b * zz)) * (((a * f) - (b * (f *'))) *'))))) by Th22; then A49: deg f <= max ((deg (((a *') * zz) * ((a * f) - (b * (f *'))))),(deg ((- (b * zz)) * (((a * f) - (b * (f *'))) *')))) by POLYNOM4:8; |.(((|.a.| ^2) - (|.b.| ^2)) ").| > 0 by A42, COMPLEX1:47; then A50: |.((a *') * zz).| > |.(- (b * zz)).| by A1, A22, A39, XREAL_1:68; then |.((a *') * zz).| > 0 by COMPLEX1:46; then (a *') * zz <> 0. F_Complex by COMPLEX1:47, COMPLFLD:7; then deg f <= max ((deg ((a * f) - (b * (f *')))),(deg ((- (b * zz)) * (((a * f) - (b * (f *'))) *')))) by A49, POLYNOM5:25; then deg f <= max ((deg ((a * f) - (b * (f *')))),(deg (((a * f) - (b * (f *'))) *'))) by A43, POLYNOM5:25; then deg f <= max ((deg ((a * f) - (b * (f *')))),(deg ((a * f) - (b * (f *'))))) by Th42; then A51: deg ((a * f) - (b * (f *'))) >= 1 by A4, XXREAL_0:2; now__::_thesis:_(_(a_*_f)_-_(b_*_(f_*'))_is_Hurwitz_implies_f_is_Hurwitz_) assume A52: (a * f) - (b * (f *')) is Hurwitz ; ::_thesis: f is Hurwitz now__::_thesis:_for_z_being_Element_of_F_Complex_st_z_is_a_root_of_f_holds_ Re_z_<_0 let z be Element of F_Complex; ::_thesis: ( z is_a_root_of f implies Re z < 0 ) assume z is_a_root_of f ; ::_thesis: Re z < 0 then A53: 0. F_Complex = eval (((((a *') * zz) * ((a * f) - (b * (f *')))) - ((- (b * zz)) * (((a * f) - (b * (f *'))) *'))),z) by A48, POLYNOM5:def_6 .= (eval ((((a *') * zz) * ((a * f) - (b * (f *')))),z)) - (eval (((- (b * zz)) * (((a * f) - (b * (f *'))) *')),z)) by POLYNOM4:21 .= (((a *') * zz) * (eval (((a * f) - (b * (f *'))),z))) - (eval (((- (b * zz)) * (((a * f) - (b * (f *'))) *')),z)) by POLYNOM5:30 .= (((a *') * zz) * (eval (((a * f) - (b * (f *'))),z))) - ((- (b * zz)) * (eval ((((a * f) - (b * (f *'))) *'),z))) by POLYNOM5:30 ; now__::_thesis:_not_Re_z_>=_0 A54: 0 <= |.(- (b * zz)).| by COMPLEX1:46; A55: |.((a *') * zz).| * |.(eval (((a * f) - (b * (f *'))),z)).| = |.(((a *') * zz) * (eval (((a * f) - (b * (f *'))),z))).| by COMPLEX1:65; A56: |.(- (b * zz)).| * |.(eval ((((a * f) - (b * (f *'))) *'),z)).| = |.((- (b * zz)) * (eval ((((a * f) - (b * (f *'))) *'),z))).| by COMPLEX1:65; assume A57: Re z >= 0 ; ::_thesis: contradiction percases ( Re z = 0 or Re z > 0 ) by A57; supposeA58: Re z = 0 ; ::_thesis: contradiction then A59: |.(eval (((a * f) - (b * (f *'))),z)).| > 0 by A52, Th49; |.(eval (((a * f) - (b * (f *'))),z)).| = |.(eval ((((a * f) - (b * (f *'))) *'),z)).| by A51, A52, A58, Th50; then |.((a *') * zz).| * |.(eval (((a * f) - (b * (f *'))),z)).| > |.(- (b * zz)).| * |.(eval ((((a * f) - (b * (f *'))) *'),z)).| by A50, A59, XREAL_1:68; hence contradiction by A53, A55, A56, VECTSP_1:19; ::_thesis: verum end; suppose Re z > 0 ; ::_thesis: contradiction then A60: |.(eval (((a * f) - (b * (f *'))),z)).| > |.(eval ((((a * f) - (b * (f *'))) *'),z)).| by A51, A52, Th50; then |.(eval (((a * f) - (b * (f *'))),z)).| > 0 by COMPLEX1:46; then A61: |.((a *') * zz).| * |.(eval (((a * f) - (b * (f *'))),z)).| > |.(- (b * zz)).| * |.(eval (((a * f) - (b * (f *'))),z)).| by A50, XREAL_1:68; |.(- (b * zz)).| * |.(eval (((a * f) - (b * (f *'))),z)).| >= |.(- (b * zz)).| * |.(eval ((((a * f) - (b * (f *'))) *'),z)).| by A54, A60, XREAL_1:64; hence contradiction by A53, A55, A56, A61, VECTSP_1:19; ::_thesis: verum end; end; end; hence Re z < 0 ; ::_thesis: verum end; hence f is Hurwitz by Def8; ::_thesis: verum end; hence ( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz ) by A11; ::_thesis: verum end; end; end; theorem Th52: :: HURWITZ:52 for f being Polynomial of F_Complex st deg f >= 1 holds for rho being Element of F_Complex st Re rho < 0 & f is Hurwitz holds (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz proof let f be Polynomial of F_Complex; ::_thesis: ( deg f >= 1 implies for rho being Element of F_Complex st Re rho < 0 & f is Hurwitz holds (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz ) assume A1: deg f >= 1 ; ::_thesis: for rho being Element of F_Complex st Re rho < 0 & f is Hurwitz holds (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz let rho be Element of F_Complex; ::_thesis: ( Re rho < 0 & f is Hurwitz implies (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz ) assume A2: Re rho < 0 ; ::_thesis: ( not f is Hurwitz or (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz ) 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 ; ::_thesis: (F* (f,rho)) div (rpoly (1,rho)) 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 (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz by A5, A6, Def5; ::_thesis: verum end; theorem :: HURWITZ:53 for f being Polynomial of F_Complex st deg f >= 1 & ex rho being Element of F_Complex st ( Re rho < 0 & |.(eval (f,rho)).| >= |.(eval ((f *'),rho)).| ) holds not f is Hurwitz by Th50; theorem :: HURWITZ:54 for f being Polynomial of F_Complex st deg f >= 1 holds 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; ::_thesis: ( deg f >= 1 implies 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 ) ) assume A1: deg f >= 1 ; ::_thesis: 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 ) let rho be Element of F_Complex; ::_thesis: ( Re rho < 0 & |.(eval (f,rho)).| < |.(eval ((f *'),rho)).| implies ( f is Hurwitz iff (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz ) ) assume that A2: Re rho < 0 and A3: |.(eval (f,rho)).| < |.(eval ((f *'),rho)).| ; ::_thesis: ( f is Hurwitz iff (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz ) reconsider ef = eval (f,rho), ef1 = eval ((f *'),rho) as Element of F_Complex ; now__::_thesis:_(_(F*_(f,rho))_div_(rpoly_(1,rho))_is_Hurwitz_implies_f_is_Hurwitz_) - 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 ; ::_thesis: f is Hurwitz then F* (f,rho) is Hurwitz by A6, A7, Th41; hence f is Hurwitz by A1, A3, Th51; ::_thesis: verum end; hence ( f is Hurwitz iff (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz ) by A1, A2, Th52; ::_thesis: verum end;