let n be Ordinal; for R being non degenerated comRing holds Polynom-Ring (n,R) is Subring of Formal-Series (n,R)
let R be non degenerated comRing; Polynom-Ring (n,R) is Subring of Formal-Series (n,R)
set PR = Polynom-Ring (n,R);
set FS = Formal-Series (n,R);
set X = [: the carrier of (Polynom-Ring (n,R)), the carrier of (Polynom-Ring (n,R)):];
set Y = [: the carrier of (Formal-Series (n,R)), the carrier of (Formal-Series (n,R)):];
A1:
for o being object st o in the carrier of (Polynom-Ring (n,R)) holds
o in the carrier of (Formal-Series (n,R))
A2:
the carrier of (Polynom-Ring (n,R)) c= the carrier of (Formal-Series (n,R))
by A1;
A3:
the addF of (Polynom-Ring (n,R)) = the addF of (Formal-Series (n,R)) || the carrier of (Polynom-Ring (n,R))
proof
A4:
dom the
addF of
(Polynom-Ring (n,R)) = [: the carrier of (Polynom-Ring (n,R)), the carrier of (Polynom-Ring (n,R)):]
by FUNCT_2:def 1;
dom the
addF of
(Formal-Series (n,R)) = [: the carrier of (Formal-Series (n,R)), the carrier of (Formal-Series (n,R)):]
by FUNCT_2:def 1;
then A5:
(dom the addF of (Formal-Series (n,R))) /\ [: the carrier of (Polynom-Ring (n,R)), the carrier of (Polynom-Ring (n,R)):] = [: the carrier of (Polynom-Ring (n,R)), the carrier of (Polynom-Ring (n,R)):]
by XBOOLE_1:28, A2, ZFMISC_1:96;
for
o being
object st
o in dom the
addF of
(Polynom-Ring (n,R)) holds
the
addF of
(Polynom-Ring (n,R)) . o = the
addF of
(Formal-Series (n,R)) . o
proof
let o be
object ;
( o in dom the addF of (Polynom-Ring (n,R)) implies the addF of (Polynom-Ring (n,R)) . o = the addF of (Formal-Series (n,R)) . o )
assume
o in dom the
addF of
(Polynom-Ring (n,R))
;
the addF of (Polynom-Ring (n,R)) . o = the addF of (Formal-Series (n,R)) . o
then consider o1,
o2 being
object such that A6:
(
o1 in the
carrier of
(Polynom-Ring (n,R)) &
o2 in the
carrier of
(Polynom-Ring (n,R)) &
o = [o1,o2] )
by ZFMISC_1:def 2;
reconsider x =
o1,
y =
o2 as
Element of the
carrier of
(Polynom-Ring (n,R)) by A6;
reconsider s1 =
x,
s2 =
y as
finite-Support Series of
n,
R by POLYNOM1:def 11;
reconsider x1 =
x,
y1 =
y as
Element of the
carrier of
(Formal-Series (n,R)) by A1;
the
addF of
(Polynom-Ring (n,R)) . [x,y] =
x + y
.=
s1 + s2
by POLYNOM1:def 11
.=
x1 + y1
by Def3
.=
the
addF of
(Formal-Series (n,R)) . [x1,y1]
;
hence
the
addF of
(Polynom-Ring (n,R)) . o = the
addF of
(Formal-Series (n,R)) . o
by A6;
verum
end;
hence
the
addF of
(Polynom-Ring (n,R)) = the
addF of
(Formal-Series (n,R)) || the
carrier of
(Polynom-Ring (n,R))
by A4, A5, FUNCT_1:46;
verum
end;
A7:
the multF of (Polynom-Ring (n,R)) = the multF of (Formal-Series (n,R)) || the carrier of (Polynom-Ring (n,R))
proof
A8:
dom the
multF of
(Formal-Series (n,R)) = [: the carrier of (Formal-Series (n,R)), the carrier of (Formal-Series (n,R)):]
by FUNCT_2:def 1;
A9:
dom the
multF of
(Polynom-Ring (n,R)) = [: the carrier of (Polynom-Ring (n,R)), the carrier of (Polynom-Ring (n,R)):]
by FUNCT_2:def 1;
A10:
(dom the multF of (Formal-Series (n,R))) /\ [: the carrier of (Polynom-Ring (n,R)), the carrier of (Polynom-Ring (n,R)):] = [: the carrier of (Polynom-Ring (n,R)), the carrier of (Polynom-Ring (n,R)):]
by A8, XBOOLE_1:28, A2, ZFMISC_1:96;
for
o being
object st
o in dom the
multF of
(Polynom-Ring (n,R)) holds
the
multF of
(Polynom-Ring (n,R)) . o = the
multF of
(Formal-Series (n,R)) . o
proof
let o be
object ;
( o in dom the multF of (Polynom-Ring (n,R)) implies the multF of (Polynom-Ring (n,R)) . o = the multF of (Formal-Series (n,R)) . o )
assume
o in dom the
multF of
(Polynom-Ring (n,R))
;
the multF of (Polynom-Ring (n,R)) . o = the multF of (Formal-Series (n,R)) . o
then consider o1,
o2 being
object such that A11:
(
o1 in the
carrier of
(Polynom-Ring (n,R)) &
o2 in the
carrier of
(Polynom-Ring (n,R)) &
o = [o1,o2] )
by ZFMISC_1:def 2;
reconsider x =
o1,
y =
o2 as
Element of the
carrier of
(Polynom-Ring (n,R)) by A11;
reconsider s1 =
x,
s2 =
y as
finite-Support Series of
n,
R by POLYNOM1:def 11;
reconsider x1 =
x,
y1 =
y as
Element of the
carrier of
(Formal-Series (n,R)) by A1;
the
multF of
(Polynom-Ring (n,R)) . [x,y] =
x * y
.=
s1 *' s2
by POLYNOM1:def 11
.=
x1 * y1
by Def3
.=
the
multF of
(Formal-Series (n,R)) . [x1,y1]
;
hence
the
multF of
(Polynom-Ring (n,R)) . o = the
multF of
(Formal-Series (n,R)) . o
by A11;
verum
end;
hence
the
multF of
(Polynom-Ring (n,R)) = the
multF of
(Formal-Series (n,R)) || the
carrier of
(Polynom-Ring (n,R))
by A9, A10, FUNCT_1:46;
verum
end;
A12: 0. (Polynom-Ring (n,R)) =
0_ (n,R)
by POLYNOM1:def 11
.=
0. (Formal-Series (n,R))
by Def3
;
1. (Polynom-Ring (n,R)) =
1_ (n,R)
by POLYNOM1:def 11
.=
1. (Formal-Series (n,R))
by Def3
;
hence
Polynom-Ring (n,R) is Subring of Formal-Series (n,R)
by A1, TARSKI:def 3, A3, A7, A12, C0SP1:def 3; verum