set R = Polynom-Ring p;
set f = KroneckerIso p;
now for a, b being Element of (Polynom-Ring p) holds ((KroneckerIso p) . a) + ((KroneckerIso p) . b) = (KroneckerIso p) . (a + b)let a,
b be
Element of
(Polynom-Ring p);
((KroneckerIso p) . a) + ((KroneckerIso p) . b) = (KroneckerIso p) . (a + b)reconsider r =
a,
q =
b as
Element of
(Polynom-Ring F) by Lm8;
reconsider fa =
(KroneckerIso p) . a,
fb =
(KroneckerIso p) . b as
Element of
((Polynom-Ring F) / ({p} -Ideal)) by FIELD_1:def 3;
A1:
fa = Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
a)
by Def8;
A2:
fb = Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
b)
by Def8;
A3:
[a,b] in [: the carrier of (Polynom-Ring p), the carrier of (Polynom-Ring p):]
by ZFMISC_1:def 2;
A4:
a + b =
( the addF of (Polynom-Ring F) || the carrier of (Polynom-Ring p)) . (
a,
b)
by RING_4:def 8
.=
r + q
by A3, FUNCT_1:49
;
thus ((KroneckerIso p) . a) + ((KroneckerIso p) . b) =
fa + fb
by FIELD_1:def 3
.=
Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
(a + b))
by A4, A1, A2, RING_1:13
.=
(KroneckerIso p) . (a + b)
by Def8
;
verum end;
hence
KroneckerIso p is additive
; ( KroneckerIso p is multiplicative & KroneckerIso p is unity-preserving & KroneckerIso p is one-to-one & KroneckerIso p is onto )
now for a, b being Element of (Polynom-Ring p) holds ((KroneckerIso p) . a) * ((KroneckerIso p) . b) = (KroneckerIso p) . (a * b)let a,
b be
Element of
(Polynom-Ring p);
((KroneckerIso p) . a) * ((KroneckerIso p) . b) = (KroneckerIso p) . (a * b)reconsider r =
a,
q =
b as
Element of the
carrier of
(Polynom-Ring F) by Lm8;
reconsider fa =
(KroneckerIso p) . a,
fb =
(KroneckerIso p) . b as
Element of
((Polynom-Ring F) / ({p} -Ideal)) by FIELD_1:def 3;
A5:
fa = Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
a)
by Def8;
A6:
fb = Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
b)
by Def8;
A7:
[a,b] in [: the carrier of (Polynom-Ring p), the carrier of (Polynom-Ring p):]
by ZFMISC_1:def 2;
A8:
a * b =
((poly_mult_mod p) || the carrier of (Polynom-Ring p)) . (
a,
b)
by RING_4:def 8
.=
(poly_mult_mod p) . (
r,
q)
by A7, FUNCT_1:49
.=
(r *' q) mod p
by RING_4:def 7
;
reconsider c =
(r *' q) mod p as
Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
reconsider d =
(r *' q) div p as
Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
A9:
(r *' q) - ((r *' q) mod p) =
((((r *' q) div p) *' p) + ((r *' q) mod p)) - ((r *' q) mod p)
by RING_4:4
.=
((((r *' q) div p) *' p) + ((r *' q) mod p)) + (- ((r *' q) mod p))
by POLYNOM3:def 6
.=
(((r *' q) div p) *' p) + (((r *' q) mod p) + (- ((r *' q) mod p)))
by POLYNOM3:26
.=
(((r *' q) div p) *' p) + (((r *' q) mod p) - ((r *' q) mod p))
by POLYNOM3:def 6
.=
(((r *' q) div p) *' p) + (0_. F)
by POLYNOM3:29
.=
((r *' q) div p) *' p
;
r * q = r *' q
by POLYNOM3:def 10;
then A10:
(r * q) - c =
((r *' q) div p) *' p
by A9, Lm7
.=
p * d
by POLYNOM3:def 10
;
{p} -Ideal = { (p * r) where r is Element of (Polynom-Ring F) : verum }
by IDEAL_1:64;
then A11:
(r * q) - c in {p} -Ideal
by A10;
thus ((KroneckerIso p) . a) * ((KroneckerIso p) . b) =
fa * fb
by FIELD_1:def 3
.=
Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
(r * q))
by A5, A6, RING_1:14
.=
Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
(a * b))
by A11, A8, RING_1:6
.=
(KroneckerIso p) . (a * b)
by Def8
;
verum end;
hence
KroneckerIso p is multiplicative
; ( KroneckerIso p is unity-preserving & KroneckerIso p is one-to-one & KroneckerIso p is onto )
(KroneckerIso p) . (1_ (Polynom-Ring p)) =
Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(1. (Polynom-Ring p)))
by Def8
.=
Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(1_. F))
by RING_4:def 8
.=
Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(1. (Polynom-Ring F)))
by POLYNOM3:def 10
.=
1. ((Polynom-Ring F) / ({p} -Ideal))
by RING_1:def 6
.=
1_ (KroneckerField (F,p))
by FIELD_1:def 3
;
hence
KroneckerIso p is unity-preserving
; ( KroneckerIso p is one-to-one & KroneckerIso p is onto )
hence
KroneckerIso p is one-to-one
; KroneckerIso p is onto
now for x being object st x in the carrier of (KroneckerField (F,p)) holds
x in rng (KroneckerIso p)let x be
object ;
( x in the carrier of (KroneckerField (F,p)) implies x in rng (KroneckerIso p) )assume
x in the
carrier of
(KroneckerField (F,p))
;
x in rng (KroneckerIso p)then
x in the
carrier of
((Polynom-Ring F) / ({p} -Ideal))
by FIELD_1:def 3;
then consider q being
Element of the
carrier of
(Polynom-Ring F) such that A20:
x = Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
q)
by RING_1:11;
reconsider d =
q div p as
Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
p <> 0_. F
;
then consider t being
Polynomial of
F such that A21:
(
q = ((q div p) *' p) + t &
deg t < deg p )
by HURWITZ:def 5;
reconsider r =
t as
Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
q - ((q div p) *' p) =
(((q div p) *' p) + t) + (- ((q div p) *' p))
by A21, POLYNOM3:def 6
.=
t + (((q div p) *' p) + (- ((q div p) *' p)))
by POLYNOM3:26
.=
t + (((q div p) *' p) - ((q div p) *' p))
by POLYNOM3:def 6
.=
t + (0_. F)
by POLYNOM3:29
.=
t
;
then A22:
r = q mod p
by HURWITZ:def 6;
r in { q where q is Polynomial of F : deg q < deg p }
by A21;
then A23:
r in the
carrier of
(Polynom-Ring p)
by RING_4:def 8;
then A24:
r in dom (KroneckerIso p)
by FUNCT_2:def 1;
q = ((q div p) *' p) + (q mod p)
by RING_4:4;
then A25:
q - r =
(((q div p) *' p) + (q mod p)) - (q mod p)
by A22, Lm7
.=
(((q div p) *' p) + (q mod p)) + (- (q mod p))
by POLYNOM3:def 6
.=
((q div p) *' p) + ((q mod p) + (- (q mod p)))
by POLYNOM3:26
.=
((q div p) *' p) + ((q mod p) - (q mod p))
by POLYNOM3:def 6
.=
((q div p) *' p) + (0_. F)
by POLYNOM3:29
.=
p * d
by POLYNOM3:def 10
;
{p} -Ideal = { (p * r) where r is Element of (Polynom-Ring F) : verum }
by IDEAL_1:64;
then A26:
q - r in {p} -Ideal
by A25;
(KroneckerIso p) . r =
Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
r)
by A23, Def8
.=
Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
q)
by A26, RING_1:6
;
hence
x in rng (KroneckerIso p)
by A20, A24, FUNCT_1:3;
verum end;
hence
KroneckerIso p is onto
by A18, TARSKI:2; verum