set n = {} ;
let L be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; Polynom-Ring ({},L) is_ringisomorph_to L
set PL = Polynom-Ring ({},L);
defpred S1[ set , set ] means ex p being Polynomial of {},L st
( p = $1 & p . {} = $2 );
A1:
dom (0_ ({},L)) = Bags {}
by FUNCT_2:def 1;
A2:
EmptyBag {} in dom ((EmptyBag {}) .--> (1_ L))
by TARSKI:def 1;
A3:
for b being bag of {} holds b = {}
then A4:
EmptyBag {} = {}
;
then reconsider i = {} as bag of {} ;
A5:
for x being Element of (Polynom-Ring ({},L)) ex y being Element of L st S1[x,y]
consider f being Function of the carrier of (Polynom-Ring ({},L)), the carrier of L such that
A7:
for x being Element of (Polynom-Ring ({},L)) holds S1[x,f . x]
from FUNCT_2:sch 3(A5);
A8:
dom f = the carrier of (Polynom-Ring ({},L))
by FUNCT_2:def 1;
reconsider f = f as Function of (Polynom-Ring ({},L)),L ;
consider p being Polynomial of {},L such that
A9:
p = 1_ (Polynom-Ring ({},L))
and
A10:
p . {} = f . (1. (Polynom-Ring ({},L)))
by A7;
A11: p =
1_ ({},L)
by A9, POLYNOM1:31
.=
(0_ ({},L)) +* ((EmptyBag {}),(1_ L))
by POLYNOM1:def 9
;
for x, y being Element of (Polynom-Ring ({},L)) holds f . (x * y) = (f . x) * (f . y)
proof
let x,
y be
Element of
(Polynom-Ring ({},L));
f . (x * y) = (f . x) * (f . y)
consider p being
Polynomial of
{},
L such that A12:
(
p = x &
p . {} = f . x )
by A7;
consider q being
Polynomial of
{},
L such that A13:
(
q = y &
q . {} = f . y )
by A7;
A14:
(p *' q) . {} = (p . i) * (q . i)
proof
A15:
decomp (EmptyBag {}) = <*<*(EmptyBag {}),(EmptyBag {})*>*>
by PRE_POLY:73;
then A16:
len (decomp (EmptyBag {})) = 1
by FINSEQ_1:39;
set z =
(p . i) * (q . i);
consider s being
FinSequence of the
carrier of
L such that A17:
(p *' q) . (EmptyBag {}) = Sum s
and A18:
len s = len (decomp (EmptyBag {}))
and A19:
for
k being
Element of
NAT st
k in dom s holds
ex
b1,
b2 being
bag of
{} st
(
(decomp (EmptyBag {})) /. k = <*b1,b2*> &
s /. k = (p . b1) * (q . b2) )
by POLYNOM1:def 10;
len s = 1
by A15, A18, FINSEQ_1:39;
then
Seg 1
= dom s
by FINSEQ_1:def 3;
then A20:
1
in dom s
by FINSEQ_1:2, TARSKI:def 1;
then consider b1,
b2 being
bag of
{} such that
(decomp (EmptyBag {})) /. 1
= <*b1,b2*>
and A21:
s /. 1
= (p . b1) * (q . b2)
by A19;
s . 1 =
(p . b1) * (q . b2)
by A20, A21, PARTFUN1:def 6
.=
(p . i) * (q . b2)
by A3
.=
(p . i) * (q . i)
by A3
;
then
s = <*((p . i) * (q . i))*>
by A16, A18, FINSEQ_1:40;
then
Sum s = (p . i) * (q . i)
by RLVECT_1:44;
hence
(p *' q) . {} = (p . i) * (q . i)
by A3, A17;
verum
end;
ex
pq being
Polynomial of
{},
L st
(
pq = x * y &
pq . {} = f . (x * y) )
by A7;
hence
f . (x * y) = (f . x) * (f . y)
by A12, A13, A14, POLYNOM1:def 11;
verum
end;
then A22:
f is multiplicative
by GROUP_6:def 6;
for x, y being Element of (Polynom-Ring ({},L)) holds f . (x + y) = (f . x) + (f . y)
proof
let x,
y be
Element of
(Polynom-Ring ({},L));
f . (x + y) = (f . x) + (f . y)
consider p being
Polynomial of
{},
L such that A23:
p = x
and A24:
p . {} = f . x
by A7;
consider q being
Polynomial of
{},
L such that A25:
q = y
and A26:
q . {} = f . y
by A7;
consider a being
Element of
L such that A27:
p = {(EmptyBag {})} --> a
by Lm1;
A28:
ex
pq being
Polynomial of
{},
L st
(
pq = x + y &
pq . {} = f . (x + y) )
by A7;
consider b being
Element of
L such that A29:
q = {(EmptyBag {})} --> b
by Lm1;
A30:
p . {} = a
by A4, A27;
A31:
(p + q) . {} =
(p . i) + (q . i)
by POLYNOM1:15
.=
a + b
by A4, A30, A29
;
q . {} = b
by A4, A29;
then
(f . x) + (f . y) = a + b
by A4, A24, A26, A27;
hence
f . (x + y) = (f . x) + (f . y)
by A23, A25, A28, A31, POLYNOM1:def 11;
verum
end;
then A32:
f is additive
by VECTSP_1:def 20;
p . i =
p . (EmptyBag {})
by A3
.=
((0_ ({},L)) +* ((EmptyBag {}) .--> (1_ L))) . (EmptyBag {})
by A11, A1, FUNCT_7:def 3
.=
((EmptyBag {}) .--> (1_ L)) . (EmptyBag {})
by A2, FUNCT_4:13
.=
1_ L
by FUNCOP_1:72
;
then
f is unity-preserving
by A9, A10, GROUP_1:def 13;
then A33:
f is RingHomomorphism
by A32, A22;
A34:
for u being object st u in the carrier of L holds
u in rng f
proof
let u be
object ;
( u in the carrier of L implies u in rng f )
assume
u in the
carrier of
L
;
u in rng f
then reconsider u =
u as
Element of
L ;
set p =
(EmptyBag {}) .--> u;
reconsider p =
(EmptyBag {}) .--> u as
Function ;
(
rng p = {u} &
dom p = Bags {} )
by FUNCOP_1:8, PRE_POLY:51, TARSKI:def 1;
then reconsider p =
p as
Function of
(Bags {}), the
carrier of
L by FUNCT_2:2;
reconsider p =
p as
Function of
(Bags {}),
L ;
reconsider p =
p as
Series of
{},
L ;
then reconsider p =
p as
Polynomial of
{},
L by POLYNOM1:def 5;
reconsider p9 =
p as
Element of
(Polynom-Ring ({},L)) by POLYNOM1:def 11;
consider q being
Polynomial of
{},
L such that A40:
q = p9
and A41:
q . {} = f . p9
by A7;
q . {} =
p . (EmptyBag {})
by A3, A40
.=
u
by FUNCOP_1:72
;
hence
u in rng f
by A8, A41, FUNCT_1:3;
verum
end;
rng f c= the carrier of L
by RELAT_1:def 19;
then
for u being object st u in rng f holds
u in the carrier of L
;
then
rng f = the carrier of L
by A34, TARSKI:2;
then
f is onto
;
then A42:
f is RingEpimorphism
by A33;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that A43:
(
x1 in dom f &
x2 in dom f )
and A44:
f . x1 = f . x2
;
x1 = x2
reconsider x1 =
x1,
x2 =
x2 as
Element of
(Polynom-Ring ({},L)) by A43;
consider p being
Polynomial of
{},
L such that A45:
(
p = x1 &
p . {} = f . x1 )
by A7;
consider q being
Polynomial of
{},
L such that A46:
(
q = x2 &
q . {} = f . x2 )
by A7;
consider a2 being
Element of
L such that A47:
q = {(EmptyBag {})} --> a2
by Lm1;
A48:
q . (EmptyBag {}) = a2
by A47;
A49:
p . {} = p . (EmptyBag {})
by A3;
consider a1 being
Element of
L such that A50:
p = {(EmptyBag {})} --> a1
by Lm1;
thus
x1 = x2
by A3, A44, A45, A46, A50, A47, A48, A49;
verum
end;
then
f is one-to-one
by FUNCT_1:def 4;
then
f is RingMonomorphism
by A33;
then
f is RingIsomorphism
by A42;
hence
Polynom-Ring ({},L) is_ringisomorph_to L
by QUOFIELD:def 23; verum