let F be strict Field; for p being linear Element of the carrier of (Polynom-Ring F) holds embField (emb p) = F
let p be linear Element of the carrier of (Polynom-Ring F); embField (emb p) = F
set FP = embField (emb p);
set f = emb p;
set K = (Polynom-Ring F) / ({p} -Ideal);
X:
( [#] ((Polynom-Ring F) / ({p} -Ideal)) = the carrier of ((Polynom-Ring F) / ({p} -Ideal)) & [#] F = the carrier of F )
;
H:
the carrier of F = the carrier of (embField (emb p))
by polyd1;
A:
( 1. (embField (emb p)) = 1. F & 0. (embField (emb p)) = 0. F )
by FIELD_2:def 7;
B: dom the addF of (embField (emb p)) =
[: the carrier of (embField (emb p)), the carrier of (embField (emb p)):]
by FUNCT_2:def 1
.=
dom the addF of F
by H, FUNCT_2:def 1
;
now for x being Element of dom the addF of F holds the addF of (embField (emb p)) . x = the addF of F . xlet x be
Element of
dom the
addF of
F;
the addF of (embField (emb p)) . x = the addF of F . xconsider o being
Element of
[: the carrier of F, the carrier of F:] such that B1:
x = o
;
consider a,
b being
object such that B2:
(
a in the
carrier of
F &
b in the
carrier of
F &
o = [a,b] )
by ZFMISC_1:def 2;
(
a in ( the carrier of ((Polynom-Ring F) / ({p} -Ideal)) \ (rng (emb p))) \/ the
carrier of
F &
b in ( the carrier of ((Polynom-Ring F) / ({p} -Ideal)) \ (rng (emb p))) \/ the
carrier of
F )
by B2, XBOOLE_0:def 3;
then reconsider a =
a,
b =
b as
Element of
carr (emb p) by X, FIELD_2:def 2;
thus the
addF of
(embField (emb p)) . x =
(addemb (emb p)) . (
a,
b)
by B1, B2, FIELD_2:def 7
.=
addemb (
(emb p),
a,
b)
by FIELD_2:def 4
.=
the
addF of
F . (
a,
b)
by B2, X, FIELD_2:def 3
.=
the
addF of
F . x
by B1, B2
;
verum end;
then C:
the addF of (embField (emb p)) = the addF of F
by B;
B: dom the multF of (embField (emb p)) =
[: the carrier of (embField (emb p)), the carrier of (embField (emb p)):]
by FUNCT_2:def 1
.=
dom the multF of F
by H, FUNCT_2:def 1
;
now for x being Element of dom the multF of F holds the multF of (embField (emb p)) . x = the multF of F . xlet x be
Element of
dom the
multF of
F;
the multF of (embField (emb p)) . x = the multF of F . xconsider o being
Element of
[: the carrier of F, the carrier of F:] such that B1:
x = o
;
consider a,
b being
object such that B2:
(
a in the
carrier of
F &
b in the
carrier of
F &
o = [a,b] )
by ZFMISC_1:def 2;
(
a in ( the carrier of ((Polynom-Ring F) / ({p} -Ideal)) \ (rng (emb p))) \/ the
carrier of
F &
b in ( the carrier of ((Polynom-Ring F) / ({p} -Ideal)) \ (rng (emb p))) \/ the
carrier of
F )
by B2, XBOOLE_0:def 3;
then reconsider a =
a,
b =
b as
Element of
carr (emb p) by X, FIELD_2:def 2;
thus the
multF of
(embField (emb p)) . x =
(multemb (emb p)) . (
a,
b)
by B1, B2, FIELD_2:def 7
.=
multemb (
(emb p),
a,
b)
by FIELD_2:def 6
.=
the
multF of
F . (
a,
b)
by B2, X, FIELD_2:def 5
.=
the
multF of
F . x
by B1, B2
;
verum end;
then
the multF of (embField (emb p)) = the multF of F
by B;
hence
embField (emb p) = F
by A, C, polyd1; verum