let R be domRing; :: thesis: for p being Ppoly of R holds p is Ppoly of R, BRoots p
let p be Ppoly of R; :: thesis: p is Ppoly of R, BRoots p
defpred S1[ Nat] means for p being Ppoly of R st deg p = \$1 holds
p is Ppoly of R, BRoots p;
IA: S1
proof
now :: thesis: for p being Ppoly of R st deg p = 1 holds
p is Ppoly of R, BRoots p
let p be Ppoly of R; :: thesis: ( deg p = 1 implies p is Ppoly of R, BRoots p )
assume A0: deg p = 1 ; :: thesis: p is Ppoly of R, BRoots p
consider F being non empty FinSequence of () such that
A1: ( p = Product F & ( for i being Nat st i in dom F holds
ex a being Element of R st F . i = rpoly (1,a) ) ) by dpp1;
len F = 1 by ;
then A2: F = <*(F . 1)*> by FINSEQ_1:40;
then A3: dom F = Seg 1 by FINSEQ_1:38;
then consider a being Element of R such that
A4: F . 1 = rpoly (1,a) by ;
reconsider e = 1 as Element of dom F by ;
A5: Product F = F . e by ;
rpoly (1,a) = <%(- a),(1. R)%> by repr;
then BRoots (rpoly (1,a)) = Bag {a} by UPROOTS:54;
hence p is Ppoly of R, BRoots p by A1, A4, A5, lemacf; :: thesis: verum
end;
hence S1 ; :: thesis: verum
end;
IS: now :: thesis: for k being Nat st k >= 1 & S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( k >= 1 & S1[k] implies S1[k + 1] )
assume AS: k >= 1 ; :: thesis: ( S1[k] implies S1[k + 1] )
assume IV: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for p being Ppoly of R st deg p = k + 1 holds
p is Ppoly of R, BRoots p
let p be Ppoly of R; :: thesis: ( deg p = k + 1 implies p is Ppoly of R, BRoots p )
assume B0: deg p = k + 1 ; :: thesis: p is Ppoly of R, BRoots p
consider F being non empty FinSequence of () such that
B1: ( p = Product F & ( for i being Nat st i in dom F holds
ex a being Element of R st F . i = rpoly (1,a) ) ) by dpp1;
B1a: len F = k + 1 by ;
consider G being FinSequence, y being object such that
B2: F = G ^ <*y*> by FINSEQ_1:46;
B2a: rng G c= rng F by ;
B2b: rng F c= the carrier of () by FINSEQ_1:def 4;
then reconsider G = G as FinSequence of () by ;
B3: len F = (len G) + () by
.= (len G) + 1 by FINSEQ_1:39 ;
then reconsider G = G as non empty FinSequence of () by ;
reconsider q = Product G as Polynomial of R by POLYNOM3:def 10;
C: dom G c= dom F by ;
D: now :: thesis: for i being Nat st i in dom G holds
ex a being Element of R st G . i = rpoly (1,a)
let i be Nat; :: thesis: ( i in dom G implies ex a being Element of R st G . i = rpoly (1,a) )
assume C0: i in dom G ; :: thesis: ex a being Element of R st G . i = rpoly (1,a)
then G . i = F . i by ;
hence ex a being Element of R st G . i = rpoly (1,a) by C, C0, B1; :: thesis: verum
end;
then reconsider q = q as Ppoly of R by dpp1;
set B = BRoots q;
deg q = k by ;
then reconsider q = q as Ppoly of R, BRoots q by IV;
rng <*y*> = {y} by FINSEQ_1:39;
then G5: y in rng <*y*> by TARSKI:def 1;
rng <*y*> c= rng F by ;
then y in rng F by G5;
then reconsider y = y as Element of () by B2b;
dom <*y*> = {1} by ;
then 1 in dom <*y*> by TARSKI:def 1;
then B6: F . (k + 1) = <*y*> . 1 by
.= y by FINSEQ_1:def 8 ;
dom F = Seg (k + 1) by ;
then consider a being Element of R such that
B9: y = rpoly (1,a) by ;
reconsider r = y as Ppoly of R, Bag {a} by ;
B10: p = () * y by
.= q *' r by POLYNOM3:def 10 ;
reconsider B1 = () + () as non zero bag of the carrier of R ;
rpoly (1,a) = <%(- a),(1. R)%> by repr;
then BRoots (rpoly (1,a)) = Bag {a} by UPROOTS:54;
then BRoots p = () + () by ;
hence p is Ppoly of R, BRoots p by ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
I: for k being Nat st k >= 1 holds
S1[k] from NAT_1:sch 8(IA, IS);
reconsider n = deg p as Element of NAT by INT_1:3;
n + 1 > 0 + 1 by ;
then n >= 1 by NAT_1:13;
hence p is Ppoly of R, BRoots p by I; :: thesis: verum