let x, a be Element of F_Complex; ( x is algebraic & a <> 0. F_Complex & a in the carrier of (FQ_Ring x) implies ex b being Element of F_Complex st
( b in the carrier of (FQ_Ring x) & a * b = 1. F_Complex ) )
set COPolynomFRat = the carrier of (Polynom-Ring F_Rat);
set M = { h where h is Polynomial of F_Rat : Ext_eval (h,x) = 0. F_Complex } ;
assume that
A1:
x is algebraic
and
A2:
a <> 0. F_Complex
and
A3:
a in the carrier of (FQ_Ring x)
; ex b being Element of F_Complex st
( b in the carrier of (FQ_Ring x) & a * b = 1. F_Complex )
consider f, g being Element of (Polynom-Ring F_Rat) such that
A4:
{f} -Ideal = Ann_Poly (x,F_Rat)
and
not g in Ann_Poly (x,F_Rat)
and
A6:
a = (hom_Ext_eval (x,F_Rat)) . g
and
A7:
{f} -Ideal ,{g} -Ideal are_co-prime
by A1, A2, A3, Th84;
1. (Polynom-Ring F_Rat) in ({f} -Ideal) + ({g} -Ideal)
by A7;
then
1. (Polynom-Ring F_Rat) in { (p + q) where p, q is Element of (Polynom-Ring F_Rat) : ( p in {f} -Ideal & q in {g} -Ideal ) }
by IDEAL_1:def 19;
then consider p, q being Element of (Polynom-Ring F_Rat) such that
A10:
1. (Polynom-Ring F_Rat) = p + q
and
A11:
p in {f} -Ideal
and
A12:
q in {g} -Ideal
;
A14:
{g} -Ideal = { (g * s) where s is Element of (Polynom-Ring F_Rat) : verum }
by IDEAL_1:64;
consider s being Element of (Polynom-Ring F_Rat) such that
A15:
q = g * s
by A12, A14;
reconsider p1 = p, q1 = q, g1 = g, s1 = s as Polynomial of F_Rat by POLYNOM3:def 10;
A16:
p + q = p1 + q1
by POLYNOM3:def 10;
consider p2 being Polynomial of F_Rat such that
A17:
p2 = p
and
A18:
Ext_eval (p2,x) = 0. F_Complex
by A4, A11;
set b = Ext_eval (s1,x);
A20:
Ext_eval (s1,x) = (hom_Ext_eval (x,F_Rat)) . s1
by Def9;
A21:
dom (hom_Ext_eval (x,F_Rat)) = the carrier of (Polynom-Ring F_Rat)
by FUNCT_2:def 1;
A22:
Ext_eval (s1,x) in the carrier of (FQ_Ring x)
by A20, A21, FUNCT_1:def 3;
1. F_Complex =
Ext_eval ((1_. F_Rat),x)
by Th3, Th18
.=
Ext_eval ((p1 + q1),x)
by A10, POLYNOM3:def 10, A16
.=
(0. F_Complex) + (Ext_eval (q1,x))
by A17, A18, Th3, Th19
.=
Ext_eval ((g1 *' s1),x)
by A15, POLYNOM3:def 10
.=
(Ext_eval (g1,x)) * (Ext_eval (s1,x))
by Th3, Th24
.=
a * (Ext_eval (s1,x))
by A6, Def9
;
hence
ex b being Element of F_Complex st
( b in the carrier of (FQ_Ring x) & a * b = 1. F_Complex )
by A22; verum