set f = emb (F,I,g);
set n = card (nonConstantPolys F);
set R = Polynom-Ring ((card (nonConstantPolys F)),F);
J:
dom (canHom ((card (nonConstantPolys F)),F)) = the carrier of F
by FUNCT_2:def 1;
hereby VECTSP_1:def 19 ( emb (F,I,g) is multiplicative & emb (F,I,g) is unity-preserving )
let x,
y be
Element of
F;
((emb (F,I,g)) . x) + ((emb (F,I,g)) . y) = (emb (F,I,g)) . (x + y)A1:
(
x | (
(card (nonConstantPolys F)),
F) is
Element of
(Polynom-Ring ((card (nonConstantPolys F)),F)) &
y | (
(card (nonConstantPolys F)),
F) is
Element of
(Polynom-Ring ((card (nonConstantPolys F)),F)) )
by POLYNOM1:def 11;
reconsider xF =
x | (
(card (nonConstantPolys F)),
F),
yF =
y | (
(card (nonConstantPolys F)),
F) as
Element of
(Polynom-Ring ((card (nonConstantPolys F)),F)) by POLYNOM1:def 11;
reconsider a =
Class (
(EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),
(x | ((card (nonConstantPolys F)),F))),
b =
Class (
(EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),
(y | ((card (nonConstantPolys F)),F))) as
Element of
(KroneckerField (F,g,I)) by A1, RING_1:12;
A:
(emb (F,I,g)) . x =
(canHom I) . ((canHom ((card (nonConstantPolys F)),F)) . x)
by J, FUNCT_1:13
.=
(canHom I) . (x | ((card (nonConstantPolys F)),F))
by defcanhom
.=
Class (
(EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),
(x | ((card (nonConstantPolys F)),F)))
by A1, RING_2:def 5
;
B:
(emb (F,I,g)) . y =
(canHom I) . ((canHom ((card (nonConstantPolys F)),F)) . y)
by J, FUNCT_1:13
.=
(canHom I) . (y | ((card (nonConstantPolys F)),F))
by defcanhom
.=
Class (
(EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),
(y | ((card (nonConstantPolys F)),F)))
by A1, RING_2:def 5
;
E:
(canHom ((card (nonConstantPolys F)),F)) . (x + y) =
((canHom ((card (nonConstantPolys F)),F)) . x) + ((canHom ((card (nonConstantPolys F)),F)) . y)
by VECTSP_1:def 20
.=
xF + ((canHom ((card (nonConstantPolys F)),F)) . y)
by defcanhom
.=
xF + yF
by defcanhom
;
thus ((emb (F,I,g)) . x) + ((emb (F,I,g)) . y) =
Class (
(EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),
(xF + yF))
by A, B, RING_1:13
.=
(canHom I) . ((canHom ((card (nonConstantPolys F)),F)) . (x + y))
by E, RING_2:def 5
.=
(emb (F,I,g)) . (x + y)
by J, FUNCT_1:13
;
verum
end;
thus
emb (F,I,g) is multiplicative
; emb (F,I,g) is unity-preserving
thus
emb (F,I,g) is unity-preserving
; verum