let F be strict Field; for p being linear Element of the carrier of (Polynom-Ring F) holds embField (canHomP p) = F
let p be linear Element of the carrier of (Polynom-Ring F); embField (canHomP p) = F
set FP = embField (canHomP p);
set f = canHomP p;
X:
( [#] F = the carrier of F & [#] (Polynom-Ring p) = the carrier of (Polynom-Ring p) )
;
H:
the carrier of F = the carrier of (embField (canHomP p))
by polyd;
A:
( 1. (embField (canHomP p)) = 1. F & 0. (embField (canHomP p)) = 0. F )
by FIELD_2:def 7;
B: dom the addF of (embField (canHomP p)) =
[: the carrier of (embField (canHomP p)), the carrier of (embField (canHomP 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 (canHomP p)) . x = the addF of F . xlet x be
Element of
dom the
addF of
F;
the addF of (embField (canHomP 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 p) \ (rng (canHomP p))) \/ the
carrier of
F &
b in ( the carrier of (Polynom-Ring p) \ (rng (canHomP p))) \/ the
carrier of
F )
by B2, XBOOLE_0:def 3;
then reconsider a =
a,
b =
b as
Element of
carr (canHomP p) by X, FIELD_2:def 2;
thus the
addF of
(embField (canHomP p)) . x =
(addemb (canHomP p)) . (
a,
b)
by B1, B2, FIELD_2:def 7
.=
addemb (
(canHomP 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 (canHomP p)) = the addF of F
by B;
B: dom the multF of (embField (canHomP p)) =
[: the carrier of (embField (canHomP p)), the carrier of (embField (canHomP 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 (canHomP p)) . x = the multF of F . xlet x be
Element of
dom the
multF of
F;
the multF of (embField (canHomP 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 p) \ (rng (canHomP p))) \/ the
carrier of
F &
b in ( the carrier of (Polynom-Ring p) \ (rng (canHomP p))) \/ the
carrier of
F )
by B2, XBOOLE_0:def 3;
then reconsider a =
a,
b =
b as
Element of
carr (canHomP p) by X, FIELD_2:def 2;
thus the
multF of
(embField (canHomP p)) . x =
(multemb (canHomP p)) . (
a,
b)
by B1, B2, FIELD_2:def 7
.=
multemb (
(canHomP 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 (canHomP p)) = the multF of F
by B;
hence
embField (canHomP p) = F
by A, C, polyd; verum