let n be Nat; for F being Field
for E being FieldExtension of F
for x being Function of n,E holds rng (hom_Ext_eval (x,F)) is Preserv of the multF of E
let F be Field; for E being FieldExtension of F
for x being Function of n,E holds rng (hom_Ext_eval (x,F)) is Preserv of the multF of E
let E be FieldExtension of F; for x being Function of n,E holds rng (hom_Ext_eval (x,F)) is Preserv of the multF of E
let x be Function of n,E; rng (hom_Ext_eval (x,F)) is Preserv of the multF of E
set f = hom_Ext_eval (x,F);
set A = the multF of E;
reconsider K = rng (hom_Ext_eval (x,F)) as Subset of E by RELAT_1:def 19;
now for x being set st x in [:K,K:] holds
the multF of E . x in rng (hom_Ext_eval (x,F))let x be
set ;
( x in [:K,K:] implies the multF of E . x in rng (hom_Ext_eval (x,F)) )assume
x in [:K,K:]
;
the multF of E . x in rng (hom_Ext_eval (x,F))then consider a,
b being
object such that A2:
a in K
and A3:
b in K
and A4:
x = [a,b]
by ZFMISC_1:def 2;
consider a1 being
Element of
E such that A5:
(
a1 = a &
a1 in rng (hom_Ext_eval (x,F)) )
by A2;
consider x1 being
object such that A6:
(
x1 in dom (hom_Ext_eval (x,F)) &
(hom_Ext_eval (x,F)) . x1 = a1 )
by A5, FUNCT_1:def 3;
reconsider x1 =
x1 as
Element of
(Polynom-Ring (n,F)) by A6;
consider a2 being
Element of
E such that A7:
(
a2 = b &
a2 in rng (hom_Ext_eval (x,F)) )
by A3;
consider x2 being
object such that A8:
(
x2 in dom (hom_Ext_eval (x,F)) &
(hom_Ext_eval (x,F)) . x2 = a2 )
by A7, FUNCT_1:def 3;
reconsider x2 =
x2 as
Element of
(Polynom-Ring (n,F)) by A8;
A9:
dom (hom_Ext_eval (x,F)) = the
carrier of
(Polynom-Ring (n,F))
by FUNCT_2:def 1;
(hom_Ext_eval (x,F)) . (x1 * x2) =
a1 * a2
by A8, A6, GROUP_6:def 6
.=
the
multF of
E . x
by A4, A5, A7
;
hence
the
multF of
E . x in rng (hom_Ext_eval (x,F))
by A9, FUNCT_1:def 3;
verum end;
hence
rng (hom_Ext_eval (x,F)) is Preserv of the multF of E
by REALSET1:def 1; verum