let L be algebraic-closed domRing; :: thesis: for p being non-zero Polynomial of L st p . ((len p) -' 1) = 1. L holds

p = poly_with_roots (BRoots p)

let p be non-zero Polynomial of L; :: thesis: ( p . ((len p) -' 1) = 1. L implies p = poly_with_roots (BRoots p) )

assume A1: p . ((len p) -' 1) = 1. L ; :: thesis: p = poly_with_roots (BRoots p)

defpred S_{1}[ Nat] means for p being non-zero Polynomial of L st len p = $1 & $1 >= 1 & p . ((len p) -' 1) = 1. L holds

p = poly_with_roots (BRoots p);

len p > 0 by Th14;

then A2: len p >= 0 + 1 by NAT_1:13;

A3: for n being Nat st n >= 1 & S_{1}[n] holds

S_{1}[n + 1]
_{1}[1]

S_{1}[n]
from NAT_1:sch 8(A15, A3);

hence p = poly_with_roots (BRoots p) by A1, A2; :: thesis: verum

p = poly_with_roots (BRoots p)

let p be non-zero Polynomial of L; :: thesis: ( p . ((len p) -' 1) = 1. L implies p = poly_with_roots (BRoots p) )

assume A1: p . ((len p) -' 1) = 1. L ; :: thesis: p = poly_with_roots (BRoots p)

defpred S

p = poly_with_roots (BRoots p);

len p > 0 by Th14;

then A2: len p >= 0 + 1 by NAT_1:13;

A3: for n being Nat st n >= 1 & S

S

proof

A15:
S
let n be Nat; :: thesis: ( n >= 1 & S_{1}[n] implies S_{1}[n + 1] )

assume that

A4: n >= 1 and

A5: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let p be non-zero Polynomial of L; :: thesis: ( len p = n + 1 & n + 1 >= 1 & p . ((len p) -' 1) = 1. L implies p = poly_with_roots (BRoots p) )

assume that

A6: len p = n + 1 and

n + 1 >= 1 and

A7: p . ((len p) -' 1) = 1. L ; :: thesis: p = poly_with_roots (BRoots p)

n + 1 > 1 by A4, NAT_1:13;

then p is with_roots by A6, POLYNOM5:def 9;

then consider x being Element of L such that

A8: x is_a_root_of p ;

set r = <%(- x),(1. L)%>;

set q = poly_quotient (p,x);

A9: p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by A8, Th47;

then reconsider q = poly_quotient (p,x) as non-zero Polynomial of L by Th31;

A10: len <%(- x),(1. L)%> = 2 by POLYNOM5:40;

then A11: <%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1) <> 0. L by Th15;

len q > 0 by Th14;

then q . ((len q) -' 1) <> 0. L by Th15;

then (<%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1)) * (q . ((len q) -' 1)) <> 0. L by A11, VECTSP_2:def 1;

then A12: len p = ((len q) + (1 + 1)) - 1 by A9, A10, POLYNOM4:10;

q . ((len q) -' 1) = 1. L by A7, A9, Th38;

then A13: q = poly_with_roots (BRoots q) by A4, A5, A6, A12;

A14: poly_with_roots (({x},1) -bag) = <%(- x),(1. L)%> by Th58;

BRoots <%(- x),(1. L)%> = ({x},1) -bag by Th51;

then BRoots p = (({x},1) -bag) + (BRoots q) by A9, Th53;

hence p = poly_with_roots (BRoots p) by A9, A13, A14, Th61; :: thesis: verum

end;assume that

A4: n >= 1 and

A5: S

let p be non-zero Polynomial of L; :: thesis: ( len p = n + 1 & n + 1 >= 1 & p . ((len p) -' 1) = 1. L implies p = poly_with_roots (BRoots p) )

assume that

A6: len p = n + 1 and

n + 1 >= 1 and

A7: p . ((len p) -' 1) = 1. L ; :: thesis: p = poly_with_roots (BRoots p)

n + 1 > 1 by A4, NAT_1:13;

then p is with_roots by A6, POLYNOM5:def 9;

then consider x being Element of L such that

A8: x is_a_root_of p ;

set r = <%(- x),(1. L)%>;

set q = poly_quotient (p,x);

A9: p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by A8, Th47;

then reconsider q = poly_quotient (p,x) as non-zero Polynomial of L by Th31;

A10: len <%(- x),(1. L)%> = 2 by POLYNOM5:40;

then A11: <%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1) <> 0. L by Th15;

len q > 0 by Th14;

then q . ((len q) -' 1) <> 0. L by Th15;

then (<%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1)) * (q . ((len q) -' 1)) <> 0. L by A11, VECTSP_2:def 1;

then A12: len p = ((len q) + (1 + 1)) - 1 by A9, A10, POLYNOM4:10;

q . ((len q) -' 1) = 1. L by A7, A9, Th38;

then A13: q = poly_with_roots (BRoots q) by A4, A5, A6, A12;

A14: poly_with_roots (({x},1) -bag) = <%(- x),(1. L)%> by Th58;

BRoots <%(- x),(1. L)%> = ({x},1) -bag by Th51;

then BRoots p = (({x},1) -bag) + (BRoots q) by A9, Th53;

hence p = poly_with_roots (BRoots p) by A9, A13, A14, Th61; :: thesis: verum

proof

for n being Nat st n >= 1 holds
let p be non-zero Polynomial of L; :: thesis: ( len p = 1 & 1 >= 1 & p . ((len p) -' 1) = 1. L implies p = poly_with_roots (BRoots p) )

assume that

A16: len p = 1 and

1 >= 1 and

A17: p . ((len p) -' 1) = 1. L ; :: thesis: p = poly_with_roots (BRoots p)

degree (BRoots p) = 0 by A16, Th54;

then A18: BRoots p = EmptyBag the carrier of L by Th9;

(len p) -' 1 = 0 by A16, XREAL_1:232;

hence p = <%(1. L)%> by A16, A17, ALGSEQ_1:def 5

.= poly_with_roots (BRoots p) by A18, Th57 ;

:: thesis: verum

end;assume that

A16: len p = 1 and

1 >= 1 and

A17: p . ((len p) -' 1) = 1. L ; :: thesis: p = poly_with_roots (BRoots p)

degree (BRoots p) = 0 by A16, Th54;

then A18: BRoots p = EmptyBag the carrier of L by Th9;

(len p) -' 1 = 0 by A16, XREAL_1:232;

hence p = <%(1. L)%> by A16, A17, ALGSEQ_1:def 5

.= poly_with_roots (BRoots p) by A18, Th57 ;

:: thesis: verum

S

hence p = poly_with_roots (BRoots p) by A1, A2; :: thesis: verum