let F be Field; :: thesis: for p being Polynomial of F
for a being non zero Element of F holds
( a * p splits_in F iff p splits_in F )
let p be Polynomial of F; :: thesis: for a being non zero Element of F holds
( a * p splits_in F iff p splits_in F )
let a be non zero Element of F; :: thesis: ( a * p splits_in F iff p splits_in F )
X: now :: thesis: ( p splits_in F implies a * p splits_in F )
assume p splits_in F ; :: thesis: a * p splits_in F
then consider b being non zero Element of F, q being Ppoly of F such that
A: p = b * q by FIELD_4:def 5;
a * p = (a * b) * q by A, RING_4:11;
hence a * p splits_in F by FIELD_4:def 5; :: thesis: verum
end;
now :: thesis: ( a * p splits_in F implies p splits_in F )
assume a * p splits_in F ; :: thesis: p splits_in F
then consider b being non zero Element of F, q being Ppoly of F such that
A: a * p = b * q by FIELD_4:def 5;
( a " <> 0. F & b <> 0. F ) by VECTSP_2:13;
then B: not (a ") * b is zero by VECTSP_2:def 1;
a <> 0. F ;
then (a ") * a = 1. F by VECTSP_1:def 10;
then p = ((a ") * a) * p
.= (a ") * (a * p) by RING_4:11
.= ((a ") * b) * q by A, RING_4:11 ;
hence p splits_in F by B, FIELD_4:def 5; :: thesis: verum
end;
hence ( a * p splits_in F iff p splits_in F ) by X; :: thesis: verum