let F be Field; :: thesis: for p being non constant Polynomial of F
for q being non zero Polynomial of F st p *' q splits_in F holds
p splits_in F
let p be non constant Polynomial of F; :: thesis: for q being non zero Polynomial of F st p *' q splits_in F holds
p splits_in F
let q be non zero Polynomial of F; :: thesis: ( p *' q splits_in F implies p splits_in F )
assume p *' q splits_in F ; :: thesis: p splits_in F
then consider a being non zero Element of F, u being Ppoly of F such that
A: p *' q = a * u by FIELD_4:def 5;
set b = (LC p) * (a ");
B: ( LC p <> 0. F & a " <> 0. F ) by VECTSP_2:13;
C2: p is Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
not deg p <= 0 by RATFUNC1:def 2;
then C1: (len p) - 1 > 0 by HURWITZ:def 2;
then len p <> 0 ;
then len (NormPolynomial p) = len p by POLYNOM5:57;
then deg (NormPolynomial p) > 0 by C1, HURWITZ:def 2;
then ( not NormPolynomial p is constant & NormPolynomial p is monic ) by RATFUNC1:def 2;
then C: ( not ((LC p) ") * p is constant & ((LC p) ") * p is monic ) by C2, RING_4:23;
D: not (LC p) * (a ") is zero by B, VECTSP_2:def 1;
E: not (LC p) " is zero by VECTSP_2:13;
then F: ((LC p) ") * (LC p) = 1. F by VECTSP_1:def 10;
a " <> 0. F by VECTSP_2:13;
then (a ") * a = 1. F by VECTSP_1:def 10;
then u = ((a ") * a) * u
.= (a ") * (p *' q) by A, RING_4:11
.= (((LC p) ") * (LC p)) * (p *' ((a ") * q)) by F, RING_4:10
.= ((LC p) ") * ((LC p) * (p *' ((a ") * q))) by RING_4:11
.= ((LC p) ") * (p *' ((LC p) * ((a ") * q))) by RING_4:10
.= ((LC p) ") * (p *' (((LC p) * (a ")) * q)) by RING_4:11
.= (((LC p) ") * p) *' (((LC p) * (a ")) * q) by RING_4:10 ;
then ((LC p) ") * p is Ppoly of F by D, C, lemppolspl3a;
hence p splits_in F by E, lemppolspl2, lemppolspl; :: thesis: verum