deffunc H1( object ) -> Element of bool [:(Bags {}),{$1}:] = (Bags {}) --> $1;
let R be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; ex P being Function of R,(Polynom-Ring (0,R)) st P is RingIsomorphism
consider P being Function such that
A1:
dom P = the carrier of R
and
A2:
for x being object st x in the carrier of R holds
P . x = H1(x)
from FUNCT_1:sch 3();
then A7:
rng P = the carrier of (Polynom-Ring (0,R))
by TARSKI:2;
then reconsider P = P as Function of R,(Polynom-Ring (0,R)) by A1, FUNCT_2:1;
A8:
P is onto
by A7;
A9:
EmptyBag {} = {} --> 0
;
then A13:
P is additive
;
now for x, y being Element of R holds (P . x) * (P . y) = P . (x * y)let x,
y be
Element of
R;
(P . x) * (P . y) = P . (x * y)reconsider Px =
P . x,
Py =
P . y,
Pxy =
P . (x * y) as
Polynomial of
0,
R by POLYNOM1:def 11;
now for b being bag of 0 ex s being FinSequence of the carrier of R st
( Pxy . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 0 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ) )reconsider s =
<*(x * y)*> as
FinSequence of the
carrier of
R ;
let b be
bag of
0 ;
ex s being FinSequence of the carrier of R st
( Pxy . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 0 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ) )take s =
s;
( Pxy . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 0 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ) )A14:
b in Bags {}
by PRE_POLY:def 12;
thus Pxy . b =
((Bags {}) --> (x * y)) . b
by A2
.=
x * y
by A14, FUNCOP_1:7
.=
Sum s
by RLVECT_1:44
;
( len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 0 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ) )A15:
decomp b = <*<*{},{}*>*>
by Th2;
A16:
len s = 1
by FINSEQ_1:39;
hence
len s = len (decomp b)
by A15, FINSEQ_1:39;
for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 0 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )A17:
len (decomp b) = 1
by A15, FINSEQ_1:39;
now for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 0 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )set b1 =
{} ;
set b2 =
{} ;
let k be
Element of
NAT ;
( k in dom s implies ex b1, b2 being bag of 0 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) )A18:
{} in Bags {}
by PRE_POLY:51, TARSKI:def 1;
then reconsider b1 =
{} ,
b2 =
{} as
bag of
0 ;
A19:
Px . b1 =
((Bags {}) --> x) . b1
by A2
.=
x
by A18, FUNCOP_1:7
;
A20:
Py . b2 =
((Bags {}) --> y) . b2
by A2
.=
y
by A18, FUNCOP_1:7
;
assume A21:
k in dom s
;
ex b1, b2 being bag of 0 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )then A22:
( 1
<= k &
k <= 1 )
by A16, FINSEQ_3:25;
then A23:
k = 1
by XXREAL_0:1;
take b1 =
b1;
ex b2 being bag of 0 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )take b2 =
b2;
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )
k in dom (decomp b)
by A17, A22, FINSEQ_3:25;
hence (decomp b) /. k =
(decomp b) . 1
by A23, PARTFUN1:def 6
.=
<*b1,b2*>
by A15, FINSEQ_1:40
;
s /. k = (Px . b1) * (Py . b2)thus s /. k =
s . 1
by A21, A23, PARTFUN1:def 6
.=
(Px . b1) * (Py . b2)
by A19, A20, FINSEQ_1:40
;
verum end; hence
for
k being
Element of
NAT st
k in dom s holds
ex
b1,
b2 being
bag of
0 st
(
(decomp b) /. k = <*b1,b2*> &
s /. k = (Px . b1) * (Py . b2) )
;
verum end; then
Pxy = Px *' Py
by POLYNOM1:def 10;
hence
(P . x) * (P . y) = P . (x * y)
by POLYNOM1:def 11;
verum end;
then A24:
P is multiplicative
;
take
P
; P is RingIsomorphism
reconsider f0 = {{}} --> (0. R), f1 = {{}} --> (1_ R) as Function of {{}}, the carrier of R ;
A25:
dom f1 = {{}}
;
A26:
dom f0 = {{}}
;
A27:
{} in dom ({{}} --> (0. R))
by TARSKI:def 1;
1_ (Polynom-Ring (0,R)) =
1_ (0,R)
by POLYNOM1:31
.=
(0_ (0,R)) +* ({},(1_ R))
by A9, POLYNOM1:def 9
.=
({{}} --> (0. R)) +* ({},(1_ R))
by POLYNOM1:def 8, PRE_POLY:51
.=
({{}} --> (0. R)) +* ({} .--> (1_ R))
by A27, FUNCT_7:def 3
.=
{{}} --> (1_ R)
by A26, A25, FUNCT_4:19
.=
P . (1_ R)
by A2, PRE_POLY:51
;
then
P is unity-preserving
by GROUP_1:def 13;
then A28:
P is RingHomomorphism
by A13, A24;
then A29:
P is RingEpimorphism
by A8;
then
P is one-to-one
by FUNCT_1:def 4;
then
P is RingMonomorphism
by A28;
hence
P is RingIsomorphism
by A29; verum