let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1 ) ) )
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( p is separable iff ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1 ) ) )

A: now :: thesis: ( p is separable implies ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1 ) ) )

assume A1: p is separable ; :: thesis: ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1 ) )
set E = the SplittingField of p;
p splits_in the SplittingField of p by FIELD_8:def 1;
hence ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1 ) ) by A1; :: thesis: verum

end;

now :: thesis: ( ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1 ) ) implies p is separable )

assume ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1 ) ) ; :: thesis: p is separable
then consider E being FieldExtension of F such that
B1: ( p splits_in E & ( for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1 ) ) ;
reconsider K = FAdj (F,(Roots (E,p))) as SplittingField of p by B1, FIELD_8:33;
reconsider E = E as K -extending FieldExtension of F by FIELD_4:7;

B3: now :: thesis: for a being Element of K st a is_a_root_of p,K holds
multiplicity (p,a) = 1

let a be Element of K; :: thesis: ( a is_a_root_of p,K implies multiplicity (p,a) = 1 )
assume H0: a is_a_root_of p,K ; :: thesis: multiplicity (p,a) = 1
H1: ( Roots (E,p) = { a where a is Element of E : a is_a_root_of p,E } & Roots (K,p) = { a where a is Element of K : a is_a_root_of p,K } ) by FIELD_4:def 4;
then ( a in Roots (K,p) & Roots (K,p) c= Roots (E,p) ) by H0, FIELD_8:18;
then a in Roots (E,p) ;
then consider b being Element of E such that
B4: ( b = a & b is_a_root_of p,E ) by H1;
B5: @ (a,E) is_a_root_of p,E by B4, FIELD_7:def 4;
multiplicity (p,a) = multiplicity (p,(@ (a,E))) by multi3K;
hence multiplicity (p,a) = 1 by B1, B5; :: thesis: verum

end;

set K1 = the SplittingField of p;
id F is isomorphism ;
then reconsider F1 = F as F -isomorphic Field by RING_3:def 4;
reconsider h = id F as Isomorphism of F,F1 ;
(PolyHom h) . p = p

proof

now :: thesis: for o being object st o in NAT holds
((PolyHom h) . p) . o = p . o

let o be object ; :: thesis: ( o in NAT implies ((PolyHom h) . p) . o = p . o )
assume o in NAT ; :: thesis: ((PolyHom h) . p) . o = p . o
then reconsider m = o as Nat ;
((PolyHom h) . p) . m = h . (p . m) by FIELD_1:def 2
.= p . m ;
hence ((PolyHom h) . p) . o = p . o ; :: thesis: verum

end;

hence (PolyHom h) . p = p ; :: thesis: verum

end;

then consider f being Function of the SplittingField of p,K such that
H3: ( f is h -extending & f is isomorphism ) by FIELD_8:57;

T: now :: thesis: for a being Element of F holds f . a = a

let a be Element of F; :: thesis: f . a = a
thus f . a = h . a by H3
.= a ; :: thesis: verum

end;

then U: f is F -fixing ;

now :: thesis: for a being Element of the SplittingField of p st a is_a_root_of p, the SplittingField of p holds
multiplicity (p,a) = 1

let a be Element of the SplittingField of p; :: thesis: ( a is_a_root_of p, the SplittingField of p implies multiplicity (p,a) = 1 )
assume H0: a is_a_root_of p, the SplittingField of p ; :: thesis: multiplicity (p,a) = 1
H4: multiplicity (p,a) = multiplicity (p,(f . a)) by U, H3, multiiso;
f . a is_a_root_of p,K

proof

reconsider K2 = K as the SplittingField of p -homomorphic Field by H3, RING_2:def 4;
reconsider f = f as Homomorphism of the SplittingField of p,K2 by H3;
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring the SplittingField of p) by FIELD_4:10;
then reconsider q = p as Element of the carrier of (Polynom-Ring the SplittingField of p) ;
eval (q,a) = Ext_eval (p,a) by FIELD_4:26
.= 0. the SplittingField of p by H0, FIELD_4:def 2 ;
then a is_a_root_of q ;
then H7: f . a is_a_root_of (PolyHom f) . q by FIELD_1:33;
H8: (PolyHom f) . q = q

proof

now :: thesis: for o being object st o in NAT holds
((PolyHom f) . q) . o = q . o

let o be object ; :: thesis: ( o in NAT implies ((PolyHom f) . q) . o = q . o )
assume o in NAT ; :: thesis: ((PolyHom f) . q) . o = q . o
then reconsider m = o as Nat ;
((PolyHom f) . q) . m = f . (p . m) by FIELD_1:def 2
.= p . m by T ;
hence ((PolyHom f) . q) . o = q . o ; :: thesis: verum

end;

hence (PolyHom f) . q = q ; :: thesis: verum

end;

0. K = Ext_eval (p,(f . a)) by H7, H8, FIELD_4:26;
hence f . a is_a_root_of p,K by FIELD_4:def 2; :: thesis: verum

end;

hence multiplicity (p,a) = 1 by B3, H4; :: thesis: verum

end;

hence p is separable ; :: thesis: verum

end;

hence ( p is separable iff ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1 ) ) ) by A; :: thesis: verum