let F be Field; for p being linear Element of the carrier of (Polynom-Ring F) holds
( (Polynom-Ring F) / ({p} -Ideal),F are_isomorphic & the carrier of (embField (emb p)) = the carrier of F )
let p be linear Element of the carrier of (Polynom-Ring F); ( (Polynom-Ring F) / ({p} -Ideal),F are_isomorphic & the carrier of (embField (emb p)) = the carrier of F )
set FP = (Polynom-Ring F) / ({p} -Ideal);
set I = {p} -Ideal ;
set f = emb p;
set FX = Polynom-Ring F;
A:
(Polynom-Ring F) / ({p} -Ideal), Polynom-Ring p are_isomorphic
by RING_4:48;
Polynom-Ring p,F are_isomorphic
by polyd;
hence
(Polynom-Ring F) / ({p} -Ideal),F are_isomorphic
by A, RING_3:44; the carrier of (embField (emb p)) = the carrier of F
B:
now for q being Element of the carrier of (Polynom-Ring F) ex r being constant Element of the carrier of (Polynom-Ring F) st Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),r)let q be
Element of the
carrier of
(Polynom-Ring F);
ex r being constant Element of the carrier of (Polynom-Ring F) st Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),r)B1:
q = ((q div p) *' p) + (q mod p)
by RING_4:4;
reconsider r =
q mod p,
d =
q div p as
Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
deg r < deg p
by divmod;
then
deg r < 1
by defl;
then
(deg r) + 1
<= 1
by INT_1:7;
then
((deg r) + 1) - 1
<= 1
- 1
by XREAL_1:9;
then reconsider r =
r as
constant Element of the
carrier of
(Polynom-Ring F) by RING_4:def 4;
(q div p) *' p = d * p
by POLYNOM3:def 10;
then
q = (d * p) + r
by B1, POLYNOM3:def 10;
then B2:
q - r =
(d * p) + (r - r)
by RLVECT_1:28
.=
(d * p) + (0. (Polynom-Ring F))
by RLVECT_1:15
;
{p} -Ideal = { (p * c) where c is Element of (Polynom-Ring F) : verum }
by IDEAL_1:64;
then
p * d in {p} -Ideal
;
then
d * p in {p} -Ideal
by GROUP_1:def 12;
then
Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
q)
= Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
r)
by B2, RING_1:6;
hence
ex
r being
constant Element of the
carrier of
(Polynom-Ring F) st
Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
q)
= Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
r)
;
verum end;
E:
now for o being object st o in the carrier of ((Polynom-Ring F) / ({p} -Ideal)) holds
o in rng (emb p)let o be
object ;
( o in the carrier of ((Polynom-Ring F) / ({p} -Ideal)) implies o in rng (emb p) )assume
o in the
carrier of
((Polynom-Ring F) / ({p} -Ideal))
;
o in rng (emb p)then consider q being
Element of the
carrier of
(Polynom-Ring F) such that E1:
o = Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
q)
by RING_1:11;
consider r being
constant Element of the
carrier of
(Polynom-Ring F) such that E2:
Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
q)
= Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
r)
by B;
consider a being
Element of
F such that E3:
a | F = r
by RING_4:20;
E4:
(emb p) . a = o
by E1, E2, E3, FIELD_1:39;
dom (emb p) = the
carrier of
F
by FUNCT_2:def 1;
hence
o in rng (emb p)
by E4, FUNCT_1:def 3;
verum end;
then C:
rng (emb p) = the carrier of ((Polynom-Ring F) / ({p} -Ideal))
by E, TARSKI:2;
X:
( [#] F = the carrier of F & [#] ((Polynom-Ring F) / ({p} -Ideal)) = the carrier of ((Polynom-Ring F) / ({p} -Ideal)) )
;
thus the carrier of (embField (emb p)) =
carr (emb p)
by FIELD_2:def 7
.=
( the carrier of ((Polynom-Ring F) / ({p} -Ideal)) \ (rng (emb p))) \/ the carrier of F
by X, FIELD_2:def 2
.=
{} \/ the carrier of F
by C, XBOOLE_1:37
.=
the carrier of F
; verum