let F be Field; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F)
for E being polynomial_disjoint Field st E = embField (emb p) holds
F is polynomial_disjoint
let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: for E being polynomial_disjoint Field st E = embField (emb p) holds
F is polynomial_disjoint
let E be polynomial_disjoint Field; :: thesis: ( E = embField (emb p) implies F is polynomial_disjoint )
assume AS1: E = embField (emb p) ; :: thesis: F is polynomial_disjoint
assume AS2: not F is polynomial_disjoint ; :: thesis: contradiction
H: F is Subfield of E by AS1, FIELD_2:17;
then reconsider K = E as FieldExtension of F by FIELD_4:7;
A: the carrier of F c= the carrier of K by H, EC_PF_1:def 1;
set o = the Element of the carrier of F /\ the carrier of (Polynom-Ring F);
([#] F) /\ ([#] (Polynom-Ring F)) <> {} by AS2, FIELD_3:def 3;
then B: ( the Element of the carrier of F /\ the carrier of (Polynom-Ring F) in the carrier of F & the Element of the carrier of F /\ the carrier of (Polynom-Ring F) in the carrier of (Polynom-Ring F) ) by XBOOLE_0:def 4;
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring K) by FIELD_4:10;
then the Element of the carrier of F /\ the carrier of (Polynom-Ring F) in ([#] K) /\ ([#] (Polynom-Ring K)) by A, B, XBOOLE_0:def 4;
hence contradiction by FIELD_3:def 3; :: thesis: verum