let F be strict Field; :: thesis: ( F is prime iff ( F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic ) )
thus ( not F is prime or F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic ) :: thesis: ( ( F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic ) implies F is prime )

proof

assume A1: F is prime ; :: thesis: ( F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic )

per cases ( Char F = 0 or Char F is prime ) by Th85;

suppose Char F = 0 ; :: thesis: ( F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic )

then F is 0 -characteristic ;
then PrimeField F, F_Rat are_isomorphic by Th100;
hence ( F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic ) by EC_PF_1:def 2, A1; :: thesis: verum

end;

suppose Char F is prime ; :: thesis: ( F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic )

then consider p being Prime such that
A2: Char F = p ;
F is p -characteristic by A2;
then A3: PrimeField F, Z/ p are_isomorphic by Th107;
PrimeField F,F are_isomorphic by EC_PF_1:def 2, A1;
hence ( F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic ) by A3, Th43; :: thesis: verum

end;

end;

end;

assume A4: ( F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic ) ; :: thesis: F is prime

per cases ( F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic ) by A4;

suppose F, F_Rat are_isomorphic ; :: thesis: F is prime

then consider f being Function of F,F_Rat such that
A5: f is RingIsomorphism ;
A6: F_Rat is F -isomorphic by A5;
then reconsider EK1 = F_Rat as F -homomorphic Field ;
reconsider f = f as Homomorphism of F,EK1 by A5;

now :: thesis: for K being Field st K is strict Subfield of F holds
K = F

let K be Field; :: thesis: ( K is strict Subfield of F implies K = F )
assume A7: K is strict Subfield of F ; :: thesis: K = F
then reconsider EK = F_Rat as K -homomorphic Field by A6, Th56;
reconsider g = f | K as Homomorphism of K,EK by A7, Th57;
A8: Image g = F_Rat by EC_PF_1:def 2;
A9: the carrier of K c= the carrier of F by A7, EC_PF_1:def 1;

now :: thesis: for x being object st x in the carrier of F holds
x in the carrier of K

let x be object ; :: thesis: ( x in the carrier of F implies x in the carrier of K )
assume x in the carrier of F ; :: thesis: x in the carrier of K
then reconsider a = x as Element of the carrier of F ;
f . a in Image g by A8;
then f . a in rng g by RING_2:def 6;
then consider y being object such that
A10: ( y in dom g & g . y = f . a ) by FUNCT_1:def 3;
reconsider y = y as Element of the carrier of K by A10;
A11: y in the carrier of F by A9;
(f | the carrier of K) . y = f . y by FUNCT_1:49;
then a = y by A10, A11, FUNCT_2:19;
hence x in the carrier of K ; :: thesis: verum

end;

then the carrier of F c= the carrier of K ;
then A12: the carrier of F = the carrier of K by A7, EC_PF_1:def 1;
( the addF of K = the addF of F || the carrier of K & the multF of K = the multF of F || the carrier of K & 1. F = 1. K & 0. F = 0. K ) by A7, EC_PF_1:def 1;
hence K = F by A7, A12; :: thesis: verum

end;

hence F is prime by EC_PF_1:def 2; :: thesis: verum

end;

suppose ex p being Prime st F, Z/ p are_isomorphic ; :: thesis: F is prime

then consider p being Prime such that
A13: F, Z/ p are_isomorphic ;
consider f being Function of F,(Z/ p) such that
A14: f is RingIsomorphism by A13;
A15: Z/ p is F -isomorphic by A14;
then reconsider EK1 = Z/ p as F -homomorphic Field ;
reconsider f = f as Homomorphism of F,EK1 by A14;

now :: thesis: for K being Field st K is strict Subfield of F holds
K = F

let K be Field; :: thesis: ( K is strict Subfield of F implies K = F )
assume A16: K is strict Subfield of F ; :: thesis: K = F
then reconsider EK = Z/ p as K -homomorphic Field by A15, Th56;
reconsider g = f | K as Homomorphism of K,EK by A16, Th57;
A17: Image g = Z/ p by EC_PF_1:def 2;
A18: the carrier of K c= the carrier of F by A16, EC_PF_1:def 1;

now :: thesis: for x being object st x in the carrier of F holds
x in the carrier of K

let x be object ; :: thesis: ( x in the carrier of F implies x in the carrier of K )
assume x in the carrier of F ; :: thesis: x in the carrier of K
then reconsider a = x as Element of the carrier of F ;
f . a in Image g by A17;
then f . a in rng g by RING_2:def 6;
then consider y being object such that
A19: ( y in dom g & g . y = f . a ) by FUNCT_1:def 3;
reconsider y = y as Element of the carrier of K by A19;
A20: y in the carrier of F by A18;
(f | the carrier of K) . y = f . y by FUNCT_1:49;
then a = y by A19, A20, FUNCT_2:19;
hence x in the carrier of K ; :: thesis: verum

end;

then the carrier of F c= the carrier of K ;
then A21: the carrier of F = the carrier of K by A16, EC_PF_1:def 1;
( the addF of K = the addF of F || the carrier of K & the multF of K = the multF of F || the carrier of K & 1. F = 1. K & 0. F = 0. K ) by A16, EC_PF_1:def 1;
hence K = F by A16, A21; :: thesis: verum

end;

hence F is prime by EC_PF_1:def 2; :: thesis: verum

end;

end;