let F be Field; for E being Polynom-Ring F -homomorphic FieldExtension of F
for a being Element of E holds RAdj (F,{a}) = Image (hom_Ext_eval (a,F))
let E be Polynom-Ring F -homomorphic FieldExtension of F; for a being Element of E holds RAdj (F,{a}) = Image (hom_Ext_eval (a,F))
let a be Element of E; RAdj (F,{a}) = Image (hom_Ext_eval (a,F))
A0:
F is Subring of E
by FIELD_4:def 1;
set R = Image (hom_Ext_eval (a,F));
set S = RAdj (F,{a});
set f = hom_Ext_eval (a,F);
now for o being object st o in {a} holds
o in the carrier of (Image (hom_Ext_eval (a,F)))let o be
object ;
( o in {a} implies o in the carrier of (Image (hom_Ext_eval (a,F))) )assume
o in {a}
;
o in the carrier of (Image (hom_Ext_eval (a,F)))then A1:
o = a
by TARSKI:def 1;
reconsider p =
<%(0. F),(1. F)%> as
Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
the
carrier of
(Polynom-Ring F) c= the
carrier of
(Polynom-Ring E)
by FIELD_4:10;
then reconsider q =
p as
Element of the
carrier of
(Polynom-Ring E) ;
A2:
dom (hom_Ext_eval (a,F)) = the
carrier of
(Polynom-Ring F)
by FUNCT_2:def 1;
(
0. E = 0. F &
1. E = 1. F )
by A0, C0SP1:def 3;
then A3:
q = <%(0. E),(1. E)%>
by A0, pr20;
(hom_Ext_eval (a,F)) . p =
Ext_eval (
p,
a)
by ALGNUM_1:def 11
.=
eval (
q,
a)
by FIELD_4:26
.=
(0. E) + ((1. E) * a)
by A3, POLYNOM5:44
.=
a
;
then
a in rng (hom_Ext_eval (a,F))
by A2, FUNCT_1:def 3;
hence
o in the
carrier of
(Image (hom_Ext_eval (a,F)))
by A1, RING_2:def 6;
verum end;
then A:
{a} is Subset of the carrier of (Image (hom_Ext_eval (a,F)))
by TARSKI:def 3;
F is Subring of Image (hom_Ext_eval (a,F))
by lemphi3;
then
RAdj (F,{a}) is Subring of Image (hom_Ext_eval (a,F))
by A, RAsub2;
then
the carrier of (RAdj (F,{a})) c= the carrier of (Image (hom_Ext_eval (a,F)))
by C0SP1:def 3;
then V:
the carrier of (RAdj (F,{a})) c= rng (hom_Ext_eval (a,F))
by RING_2:def 6;
rng (hom_Ext_eval (a,F)) c= the carrier of (RAdj (F,{a}))
by lemphi2;
then the carrier of (RAdj (F,{a})) =
rng (hom_Ext_eval (a,F))
by V, TARSKI:2
.=
the carrier of (Image (hom_Ext_eval (a,F)))
by RING_2:def 6
;
hence
RAdj (F,{a}) = Image (hom_Ext_eval (a,F))
by RE1; verum