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