begin
begin
begin
definition
let n be
Ordinal;
let L be non
empty right_complementable add-associative right_zeroed doubleLoopStr ;
let p,
q be
Series of
n,
L;
existence
ex b1 being Series of n,L st
for b being bag of n ex s being FinSequence of the carrier of L st
( b1 . 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 n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) )
uniqueness
for b1, b2 being Series of n,L st ( for b being bag of n ex s being FinSequence of the carrier of L st
( b1 . 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 n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ) & ( for b being bag of n ex s being FinSequence of the carrier of L st
( b2 . 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 n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ) holds
b1 = b2
end;
begin
begin
definition
let n be
Ordinal;
let L be non
trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;
func Polynom-Ring (
n,
L)
-> non
empty strict doubleLoopStr means :
Def10:
( ( for
x being
set holds
(
x in the
carrier of
it iff
x is
Polynomial of
n,
L ) ) & ( for
x,
y being
Element of
it for
p,
q being
Polynomial of
n,
L st
x = p &
y = q holds
x + y = p + q ) & ( for
x,
y being
Element of
it for
p,
q being
Polynomial of
n,
L st
x = p &
y = q holds
x * y = p *' q ) &
0. it = 0_ (
n,
L) &
1. it = 1_ (
n,
L) );
existence
ex b1 being non empty strict doubleLoopStr st
( ( for x being set holds
( x in the carrier of b1 iff x is Polynomial of n,L ) ) & ( for x, y being Element of b1
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. b1 = 0_ (n,L) & 1. b1 = 1_ (n,L) )
uniqueness
for b1, b2 being non empty strict doubleLoopStr st ( for x being set holds
( x in the carrier of b1 iff x is Polynomial of n,L ) ) & ( for x, y being Element of b1
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. b1 = 0_ (n,L) & 1. b1 = 1_ (n,L) & ( for x being set holds
( x in the carrier of b2 iff x is Polynomial of n,L ) ) & ( for x, y being Element of b2
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b2
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. b2 = 0_ (n,L) & 1. b2 = 1_ (n,L) holds
b1 = b2
end;
::
deftheorem Def10 defines
Polynom-Ring POLYNOM1:def 10 :
for n being Ordinal
for L being non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for b3 being non empty strict doubleLoopStr holds
( b3 = Polynom-Ring (n,L) iff ( ( for x being set holds
( x in the carrier of b3 iff x is Polynomial of n,L ) ) & ( for x, y being Element of b3
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b3
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. b3 = 0_ (n,L) & 1. b3 = 1_ (n,L) ) );
Lm1:
now for n being Ordinal
for L being non empty non trivial right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for x, e being Element of (Polynom-Ring (n,L)) st e = 1. (Polynom-Ring (n,L)) holds
( x * e = x & e * x = x )
let n be
Ordinal;
for L being non empty non trivial right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for x, e being Element of (Polynom-Ring (n,L)) st e = 1. (Polynom-Ring (n,L)) holds
( x * e = x & e * x = x )let L be non
empty non
trivial right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
for x, e being Element of (Polynom-Ring (n,L)) st e = 1. (Polynom-Ring (n,L)) holds
( x * e = x & e * x = x )set Pm =
Polynom-Ring (
n,
L);
let x,
e be
Element of
(Polynom-Ring (n,L));
( e = 1. (Polynom-Ring (n,L)) implies ( x * e = x & e * x = x ) )reconsider p =
x as
Polynomial of
n,
L by Def10;
assume A1:
e = 1. (Polynom-Ring (n,L))
;
( x * e = x & e * x = x )A2:
1. (Polynom-Ring (n,L)) = 1_ (
n,
L)
by Def10;
hence x * e =
p *' (1_ (n,L))
by A1, Def10
.=
x
by Th29
;
e * x = xthus e * x =
(1_ (n,L)) *' p
by A1, A2, Def10
.=
x
by Th30
;
verum
end;