:: The Ring of Polynomials
:: by Robert Milewski
::
:: Received April 17, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem Th1: :: POLYNOM3:1
theorem Th2: :: POLYNOM3:2
theorem Th3: :: POLYNOM3:3
theorem Th4: :: POLYNOM3:4
:: deftheorem Def1 defines < POLYNOM3:def 1 :
:: deftheorem Def2 defines <= POLYNOM3:def 2 :
theorem Th5: :: POLYNOM3:5
theorem Th6: :: POLYNOM3:6
theorem Th7: :: POLYNOM3:7
:: deftheorem Def3 defines TuplesOrder POLYNOM3:def 3 :
:: deftheorem Def4 defines Decomp POLYNOM3:def 4 :
theorem Th8: :: POLYNOM3:8
theorem Th9: :: POLYNOM3:9
theorem :: POLYNOM3:10
theorem Th11: :: POLYNOM3:11
theorem Th12: :: POLYNOM3:12
theorem Th13: :: POLYNOM3:13
theorem Th14: :: POLYNOM3:14
:: deftheorem Def5 defines prodTuples POLYNOM3:def 5 :
theorem Th15: :: POLYNOM3:15
theorem Th16: :: POLYNOM3:16
theorem :: POLYNOM3:17
theorem Th18: :: POLYNOM3:18
theorem :: POLYNOM3:19
theorem Th20: :: POLYNOM3:20
theorem Th21: :: POLYNOM3:21
theorem Th22: :: POLYNOM3:22
theorem Th23: :: POLYNOM3:23
theorem Th24: :: POLYNOM3:24
theorem :: POLYNOM3:25
theorem Th26: :: POLYNOM3:26
Lm1:
for L being non empty addLoopStr
for p, q being sequence of L holds p - q = p + (- q)
:: deftheorem POLYNOM3:def 6 :
canceled;
:: deftheorem POLYNOM3:def 7 :
canceled;
:: deftheorem defines - POLYNOM3:def 8 :
theorem :: POLYNOM3:27
:: deftheorem defines 0_. POLYNOM3:def 9 :
theorem :: POLYNOM3:28
canceled;
theorem Th29: :: POLYNOM3:29
theorem Th30: :: POLYNOM3:30
:: deftheorem defines 1_. POLYNOM3:def 10 :
theorem Th31: :: POLYNOM3:31
:: deftheorem Def11 defines *' POLYNOM3:def 11 :
theorem Th32: :: POLYNOM3:32
theorem Th33: :: POLYNOM3:33
theorem Th34: :: POLYNOM3:34
theorem :: POLYNOM3:35
theorem Th36: :: POLYNOM3:36
definition
let L be non
empty right_complementable add-associative right_zeroed distributive doubleLoopStr ;
func Polynom-Ring L -> non
empty strict doubleLoopStr means :
Def12:
:: POLYNOM3:def 12
( ( for
x being
set holds
(
x in the
carrier of
it iff
x is
Polynomial of
L ) ) & ( for
x,
y being
Element of
it for
p,
q being
sequence of
L st
x = p &
y = q holds
x + y = p + q ) & ( for
x,
y being
Element of
it for
p,
q being
sequence of
L st
x = p &
y = q holds
x * y = p *' q ) &
0. it = 0_. L &
1. it = 1_. 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 L ) ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b1 = 0_. L & 1. b1 = 1_. 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 L ) ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b1 = 0_. L & 1. b1 = 1_. L & ( for x being set holds
( x in the carrier of b2 iff x is Polynomial of L ) ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b2 = 0_. L & 1. b2 = 1_. L holds
b1 = b2
end;
:: deftheorem Def12 defines Polynom-Ring POLYNOM3:def 12 :
theorem :: POLYNOM3:37