let p be Prime; :: thesis: for n being non zero Nat
for F being p -characteristic Field
for E being SplittingField of X^ ((p |^ n),(PrimeField F)) holds E == InducedSubfield (Roots (E,(X^ ((p |^ n),(PrimeField F)))))
let n be non zero Nat; :: thesis: for F being p -characteristic Field
for E being SplittingField of X^ ((p |^ n),(PrimeField F)) holds E == InducedSubfield (Roots (E,(X^ ((p |^ n),(PrimeField F)))))
let F be p -characteristic Field; :: thesis: for E being SplittingField of X^ ((p |^ n),(PrimeField F)) holds E == InducedSubfield (Roots (E,(X^ ((p |^ n),(PrimeField F)))))
let E be SplittingField of X^ ((p |^ n),(PrimeField F)); :: thesis: E == InducedSubfield (Roots (E,(X^ ((p |^ n),(PrimeField F)))))
set K = InducedSubfield (Roots (E,(X^ ((p |^ n),(PrimeField F)))));
A: PrimeField E = PrimeField (InducedSubfield (Roots (E,(X^ ((p |^ n),(PrimeField F)))))) by RING_3:94;
PrimeField F is Subfield of E by FIELD_4:7;
then PrimeField E = PrimeField (PrimeField F) by RING_3:94
.= PrimeField F by RING_3:95 ;
then reconsider K = InducedSubfield (Roots (E,(X^ ((p |^ n),(PrimeField F))))) as FieldExtension of PrimeField F by A, FIELD_4:7;
reconsider E1 = E as K -extending FieldExtension of K by FIELD_4:7;
A: X^ ((p |^ n),(PrimeField F)) splits_in E1 by FIELD_8:def 1;
the carrier of K = Roots (E,(X^ ((p |^ n),(PrimeField F)))) by dis;
then X^ ((p |^ n),(PrimeField F)) splits_in K by A, FIELD_8:27;
hence E == InducedSubfield (Roots (E,(X^ ((p |^ n),(PrimeField F))))) by FIELD_8:def 1; :: thesis: verum