:: On polynomials with coefficients in a ring of polynomials
:: by Barbara Dzienis
::
:: Received August 10, 2001
:: Copyright (c) 2001 Association of Mizar Users
theorem Th1: :: POLYNOM6:1
theorem Th2: :: POLYNOM6:2
:: deftheorem Def1 defines +^ POLYNOM6:def 1 :
theorem Th3: :: POLYNOM6:3
theorem :: POLYNOM6:4
theorem Th5: :: POLYNOM6:5
theorem Th6: :: POLYNOM6:6
theorem Th7: :: POLYNOM6:7
theorem Th8: :: POLYNOM6:8
definition
let o1,
o2 be non
empty Ordinal;
let L be non
empty non
trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;
let P be
Polynomial of
o1,
(Polynom-Ring o2,L);
func Compress P -> Polynomial of
(o1 +^ o2),
L means :
Def2:
:: POLYNOM6:def 2
for
b being
Element of
Bags (o1 +^ o2) ex
b1 being
Element of
Bags o1 ex
b2 being
Element of
Bags o2 ex
Q1 being
Polynomial of
o2,
L st
(
Q1 = P . b1 &
b = b1 +^ b2 &
it . b = Q1 . b2 );
existence
ex b1 being Polynomial of (o1 +^ o2),L st
for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & b1 . b = Q1 . b2 )
uniqueness
for b1, b2 being Polynomial of (o1 +^ o2),L st ( for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & b1 . b = Q1 . b2 ) ) & ( for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & b2 . b = Q1 . b2 ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines Compress POLYNOM6:def 2 :
theorem Th9: :: POLYNOM6:9
theorem Th10: :: POLYNOM6:10
theorem Th11: :: POLYNOM6:11
theorem Th12: :: POLYNOM6:12
theorem Th13: :: POLYNOM6:13
theorem Th14: :: POLYNOM6:14
theorem :: POLYNOM6:15