let F be Field; :: thesis: for E being FieldExtension of F
for p, q being Element of the carrier of (Polynom-Ring F)
for p1, q1 being Element of the carrier of (Polynom-Ring E) st p1 = p & q1 = q holds
( q1 divides p1 iff q divides p )
let E be FieldExtension of F; :: thesis: for p, q being Element of the carrier of (Polynom-Ring F)
for p1, q1 being Element of the carrier of (Polynom-Ring E) st p1 = p & q1 = q holds
( q1 divides p1 iff q divides p )
let p, q be Element of the carrier of (Polynom-Ring F); :: thesis: for p1, q1 being Element of the carrier of (Polynom-Ring E) st p1 = p & q1 = q holds
( q1 divides p1 iff q divides p )
let p1, q1 be Element of the carrier of (Polynom-Ring E); :: thesis: ( p1 = p & q1 = q implies ( q1 divides p1 iff q divides p ) )
assume AS: ( p1 = p & q1 = q ) ; :: thesis: ( q1 divides p1 iff q divides p )

per cases ( q is zero or not q is zero ) ;

suppose q is zero ; :: thesis: ( q1 divides p1 iff q divides p )

then S1: q = 0_. F by UPROOTS:def 5;
then S2: q1 = 0_. E by AS, FIELD_4:12;

A: now :: thesis: ( q divides p implies q1 divides p1 )

assume q divides p ; :: thesis: q1 divides p1
then consider r being Polynomial of F such that
A1: (0_. F) *' r = p by S1, RING_4:1;
q1 *' p1 = p1 by S2, AS, A1, FIELD_4:12;
hence q1 divides p1 by RING_4:1; :: thesis: verum

end;

now :: thesis: ( q1 divides p1 implies q divides p )

assume q1 divides p1 ; :: thesis: q divides p
then consider r being Polynomial of E such that
A1: (0_. E) *' r = p1 by S2, RING_4:1;
q *' p = p by S1, AS, A1, FIELD_4:12;
hence q divides p by RING_4:1; :: thesis: verum

end;

hence ( q1 divides p1 iff q divides p ) by A; :: thesis: verum

end;

suppose S: not q is zero ; :: thesis: ( q1 divides p1 iff q divides p )

then q <> 0_. F ;
then q <> 0_. E by FIELD_4:12;
then S1: not q1 is zero by AS, UPROOTS:def 5;

A: now :: thesis: ( q1 divides p1 implies q divides p )

assume A1: q1 divides p1 ; :: thesis: q divides p
p gcd q = p1 gcd q1 by AS, lemgcd
.= NormPolynomial q1 by S1, A1, lemgcdn
.= NormPolynomial q by AS, FIELD_6:24 ;
hence q divides p by RING_4:25, RING_4:52; :: thesis: verum

end;

now :: thesis: ( q divides p implies q1 divides p1 )

assume A1: q divides p ; :: thesis: q1 divides p1
p1 gcd q1 = p gcd q by AS, lemgcd
.= NormPolynomial q by S, A1, lemgcdn
.= NormPolynomial q1 by AS, FIELD_6:24 ;
hence q1 divides p1 by RING_4:25, RING_4:52; :: thesis: verum

end;

hence ( q1 divides p1 iff q divides p ) by A; :: thesis: verum

end;

end;