let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff for E being FieldExtension of F st p splits_in E holds
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 for E being FieldExtension of F st p splits_in E holds
for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1 )

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

assume A1: for E being FieldExtension of F st p splits_in E holds
for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1 ; :: thesis: p is separable

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

let K be SplittingField of p; :: 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 A2: a is_a_root_of p,K ; :: thesis: multiplicity (p,a) = 1
p splits_in K by FIELD_8:def 1;
hence multiplicity (p,a) = 1 by A1, A2; :: thesis: verum

end;

hence p is separable ; :: thesis: verum

end;

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

assume B1: p is separable ; :: thesis: for E being FieldExtension of F st p splits_in E holds
for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1

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

let E be FieldExtension of F; :: thesis: ( p splits_in E implies for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1 )
assume B2: p splits_in E ; :: thesis: for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1
let a be Element of E; :: thesis: ( a is_a_root_of p,E implies multiplicity (p,a) = 1 )
assume B3: a is_a_root_of p,E ; :: thesis: multiplicity (p,a) = 1
set K = the SplittingField of p;
H1: Roots (E,p) = { a where a is Element of E : a is_a_root_of p,E } by FIELD_4:def 4;
reconsider E1 = E as FAdj (F,(Roots (E,p))) -extending FieldExtension of F by FIELD_4:7;
consider a1 being Element of E1 such that
H6: ( a1 = a & a1 is_a_root_of p,E1 ) by B3;
( a1 in Roots (E,p) & Roots (E,p) is Subset of (FAdj (F,(Roots (E,p)))) ) by H1, H6, FIELD_6:35;
then reconsider b = a1 as Element of (FAdj (F,(Roots (E,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 ;
H2: FAdj (F,(Roots (E,p))) is SplittingField of p by B2, FIELD_8:33;
(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 (FAdj (F,(Roots (E,p)))), the SplittingField of p such that
H3: ( f is h -extending & f is isomorphism ) by H2, 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 H4: f is F -fixing ;
f . b is_a_root_of p, the SplittingField of p

proof

reconsider K1 = the SplittingField of p as FAdj (F,(Roots (E,p))) -homomorphic Field by H3, RING_2:def 4;
reconsider f = f as Homomorphism of (FAdj (F,(Roots (E,p)))),K1 by H3;
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring (FAdj (F,(Roots (E,p))))) by FIELD_4:10;
then reconsider q = p as Element of the carrier of (Polynom-Ring (FAdj (F,(Roots (E,p))))) ;
eval (q,b) = Ext_eval (p,b) by FIELD_4:26
.= Ext_eval (p,a1) by FIELD_6:11
.= 0. E by H6, FIELD_4:def 2
.= 0. (FAdj (F,(Roots (E,p)))) by EC_PF_1:def 1 ;
then b is_a_root_of q ;
then H7: f . b 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. the SplittingField of p = Ext_eval (p,(f . b)) by H7, H8, FIELD_4:26;
hence f . b is_a_root_of p, the SplittingField of p by FIELD_4:def 2; :: thesis: verum

end;

then H5: multiplicity (p,(f . b)) = 1 by B1;
multiplicity (p,b) = multiplicity (p,(@ (b,E1))) by multi3K
.= multiplicity (p,a) by H6, FIELD_7:def 4 ;
hence multiplicity (p,a) = 1 by H4, H5, H3, multiiso; :: thesis: verum

end;

hence for E being FieldExtension of F st p splits_in E holds
for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1 ; :: thesis: verum

end;

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