set n = {} ;
let L be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis:
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 (() .--> (1_ L)) by TARSKI:def 1;
A3: for b being bag of {} holds b = {}
proof
let b be bag of {} ; :: thesis: b = {}
b in Bags {} by PRE_POLY:def 12;
hence b = {} by ; :: thesis: verum
end;
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]
proof
let x be Element of (Polynom-Ring ({},L)); :: thesis: ex y being Element of L st S1[x,y]
reconsider p = x as Polynomial of {},L by POLYNOM1:def 11;
take p . {} ; :: thesis: ( p . {} is Element of L & S1[x,p . {}] )
dom p = Bags {} by FUNCT_2:def 1;
then A6: p . {} in rng p by ;
rng p c= the carrier of L by RELAT_1:def 19;
hence ( p . {} is Element of L & S1[x,p . {}] ) by A6; :: thesis: verum
end;
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 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
.= (0_ ({},L)) +* ((),(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)); :: thesis: 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 () = <*<*(),()*>*> by PRE_POLY:73;
then A16: len () = 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) . () = Sum s and
A18: len s = len () and
A19: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of {} st
( () /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by POLYNOM1:def 10;
len s = 1 by ;
then Seg 1 = dom s by FINSEQ_1:def 3;
then A20: 1 in dom s by ;
then consider b1, b2 being bag of {} such that
(decomp ()) /. 1 = <*b1,b2*> and
A21: s /. 1 = (p . b1) * (q . b2) by A19;
s . 1 = (p . b1) * (q . b2) by
.= (p . i) * (q . b2) by A3
.= (p . i) * (q . i) by A3 ;
then s = <*((p . i) * (q . i))*> by ;
then Sum s = (p . i) * (q . i) by RLVECT_1:44;
hence (p *' q) . {} = (p . i) * (q . i) by ; :: thesis: 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 ; :: thesis: 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)); :: thesis: 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 = {()} --> 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 = {()} --> b by Lm1;
A30: p . {} = a by ;
A31: (p + q) . {} = (p . i) + (q . i) by POLYNOM1:15
.= a + b by A4, A30, A29 ;
q . {} = b by ;
then (f . x) + (f . y) = a + b by A4, A24, A26, A27;
hence f . (x + y) = (f . x) + (f . y) by ; :: thesis: verum
end;
then A32: f is additive by VECTSP_1:def 20;
p . i = p . () by A3
.= ((0_ ({},L)) +* (() .--> (1_ L))) . () by
.= (() .--> (1_ L)) . () by
.= 1_ L by FUNCOP_1:72 ;
then f is unity-preserving by ;
then A33: f is RingHomomorphism by ;
A34: for u being object st u in the carrier of L holds
u in rng f
proof
let u be object ; :: thesis: ( u in the carrier of L implies u in rng f )
assume u in the carrier of L ; :: thesis: u in rng f
then reconsider u = u as Element of L ;
set p = () .--> u;
reconsider p = () .--> u as Function ;
( rng p = {u} & dom p = Bags {} ) by ;
then reconsider p = p as Function of (), the carrier of L by FUNCT_2:2;
reconsider p = p as Function of (),L ;
reconsider p = p as Series of {},L ;
now :: thesis: ( ( u = 0. L & Support p is finite ) or ( u <> 0. L & Support p is finite ) )
per cases ( u = 0. L or u <> 0. L ) ;
case A35: u = 0. L ; :: thesis:
Support p = {}
proof
set v = the Element of Support p;
assume Support p <> {} ; :: thesis: contradiction
then A36: the Element of Support p in Support p ;
then the Element of Support p is bag of {} ;
then p . the Element of Support p = p . () by A3, A4
.= u by FUNCOP_1:72 ;
hence contradiction by A35, A36, POLYNOM1:def 4; :: thesis: verum
end;
hence Support p is finite ; :: thesis: verum
end;
case A37: u <> 0. L ; :: thesis:
A38: for v being object st v in {()} holds
v in Support p
proof
let v be object ; :: thesis: ( v in {()} implies v in Support p )
assume A39: v in {()} ; :: thesis:
then reconsider v = v as Element of Bags {} ;
p . v = p . () by
.= u by FUNCOP_1:72 ;
hence v in Support p by ; :: thesis: verum
end;
for v being object st v in Support p holds
v in {()}
proof
let v be object ; :: thesis: ( v in Support p implies v in {()} )
assume v in Support p ; :: thesis: v in {()}
then reconsider v = v as bag of {} ;
v = EmptyBag {} by A3, A4;
hence v in {()} by TARSKI:def 1; :: thesis: verum
end;
hence Support p is finite by ; :: thesis: verum
end;
end;
end;
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 . () by
.= u by FUNCOP_1:72 ;
hence u in rng f by ; :: thesis: 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 ;
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 ; :: thesis: ( 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 ; :: thesis: 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 = {()} --> a2 by Lm1;
A48: q . () = a2 by A47;
A49: p . {} = p . () by A3;
consider a1 being Element of L such that
A50: p = {()} --> a1 by Lm1;
thus x1 = x2 by A3, A44, A45, A46, A50, A47, A48, A49; :: thesis: 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; :: thesis: verum