:: POLYNOM7 semantic presentation

registration

cluster non empty non trivial ZeroStr ;
existence

proof end;

end;

registration

cluster non trivial -> non empty ZeroStr ;
coherence

proof end;

end;

registration

cluster non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive left_zeroed domRing-like non trivial doubleLoopStr ;
existence

proof end;

end;

registration

let c₁ be non trivial ZeroStr ;
cluster non-zero Element of the carrier of a₁;
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be non empty ZeroStr ;
let c₃ be Series of c₁,c₂;
canceled;
attr a₃ is non-zero means :Def2: :: POLYNOM7:def 2
a₃ <> 0_ a₁,a₂;

end;

:: deftheorem Def1 POLYNOM7:def 1 :

:: deftheorem Def2 defines non-zero POLYNOM7:def 2 :

registration

let c₁ be set ;
let c₂ be non trivial ZeroStr ;
cluster non-zero Relation of Bags a₁,the carrier of a₂;
existence

proof end;

end;

registration

let c₁ be Ordinal;
let c₂ be non trivial ZeroStr ;
cluster non-zero Relation of Bags a₁,the carrier of a₂;
existence

proof end;

end;

theorem Th1: :: POLYNOM7:1

for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being Series of b₁,b₂ holds
( b₃ = 0_ b₁,b₂ iff Support b₃ = {} )

proof end;

theorem Th2: :: POLYNOM7:2

for b₁ being set
for b₂ being non empty ZeroStr holds
( not b₂ is trivial iff ex b₃ being Series of b₁,b₂ st Support b₃ <> {} )

proof end;

definition

let c₁ be set ;
let c₂ be bag of c₁;
attr a₂ is univariate means :Def3: :: POLYNOM7:def 3
ex b₁ being Element of a₁ st support a₂ = {b₁};

end;

:: deftheorem Def3 defines univariate POLYNOM7:def 3 :

registration

let c₁ be non empty set ;
cluster univariate M32(a₁);
existence

proof end;

end;

registration

let c₁ be non empty set ;
cluster univariate -> non empty M32(a₁);
coherence

proof end;

end;

theorem Th3: :: POLYNOM7:3

for b₁ being bag of {} holds b₁ = EmptyBag {}

proof end;

Lemma4: for b₁ being non empty doubleLoopStr
for b₂ being Polynomial of {} ,b₁ ex b₃ being Element of b₁ st b₂ = {(EmptyBag {} )} --> b₃

proof end;

theorem Th4: :: POLYNOM7:4

for b₁ being add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for b₂ being Polynomial of {} ,b₁
for b₃ being Function of {} ,b₁ holds eval b₂,b₃ = b₂ . (EmptyBag {} )

proof end;

theorem Th5: :: POLYNOM7:5

for b₁ being Abelian add-associative right_zeroed right_complementable unital associative distributive non trivial doubleLoopStr holds Polynom-Ring {} ,b₁ is_ringisomorph_to b₁

proof end;

definition

let c₁ be set ;
let c₂ be non empty ZeroStr ;
let c₃ be Series of c₁,c₂;
attr a₃ is monomial-like means :Def4: :: POLYNOM7:def 4
ex b₁ being bag of a₁ st
for b₂ being bag of a₁ st b₂ <> b₁ holds
a₃ . b₂ = 0. a₂;

end;

:: deftheorem Def4 defines monomial-like POLYNOM7:def 4 :

registration

let c₁ be set ;
let c₂ be non empty ZeroStr ;
cluster monomial-like Relation of Bags a₁,the carrier of a₂;
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be non empty ZeroStr ;
mode Monomial of a₁,a₂ is monomial-like Series of a₁,a₂;

end;

registration

let c₁ be set ;
let c₂ be non empty ZeroStr ;
cluster monomial-like -> finite-Support Relation of Bags a₁,the carrier of a₂;
coherence

proof end;

end;

theorem Th6: :: POLYNOM7:6

for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being Series of b₁,b₂ holds
( b₃ is Monomial of b₁,b₂ iff ( Support b₃ = {} or ex b₄ being bag of b₁ st Support b₃ = {b₄} ) )

proof end;

definition

let c₁ be set ;
let c₂ be non empty ZeroStr ;
let c₃ be Element of c₂;
let c₄ be bag of c₁;
func Monom c₃,c₄ -> Monomial of a₁,a₂ equals :: POLYNOM7:def 5
(0_ a₁,a₂) +* a₄,a₃;
coherence

proof end;

end;

:: deftheorem Def5 defines Monom POLYNOM7:def 5 :

definition

let c₁ be set ;
let c₂ be non empty ZeroStr ;
let c₃ be Monomial of c₁,c₂;
func term c₃ -> bag of a₁ means :Def6: :: POLYNOM7:def 6
( a₃ . a₄ <> 0. a₂ or ( Support a₃ = {} & a₄ = EmptyBag a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines term POLYNOM7:def 6 :

definition

let c₁ be set ;
let c₂ be non empty ZeroStr ;
let c₃ be Monomial of c₁,c₂;
func coefficient c₃ -> Element of a₂ equals :: POLYNOM7:def 7
a₃ . (term a₃);
coherence ;

end;

:: deftheorem Def7 defines coefficient POLYNOM7:def 7 :

theorem Th7: :: POLYNOM7:7

for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being Monomial of b₁,b₂ holds
( Support b₃ = {} or Support b₃ = {(term b₃)} )

proof end;

theorem Th8: :: POLYNOM7:8

for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being bag of b₁ holds
( coefficient (Monom (0. b₂),b₃) = 0. b₂ & term (Monom (0. b₂),b₃) = EmptyBag b₁ )

proof end;

theorem Th9: :: POLYNOM7:9

for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being Element of b₂
for b₄ being bag of b₁ holds coefficient (Monom b₃,b₄) = b₃

proof end;

theorem Th10: :: POLYNOM7:10

for b₁ being set
for b₂ being non trivial ZeroStr
for b₃ being non-zero Element of b₂
for b₄ being bag of b₁ holds term (Monom b₃,b₄) = b₄

proof end;

theorem Th11: :: POLYNOM7:11

for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being Monomial of b₁,b₂ holds Monom (coefficient b₃),(term b₃) = b₃

proof end;

theorem Th12: :: POLYNOM7:12

for b₁ being Ordinal
for b₂ being add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for b₃ being Monomial of b₁,b₂
for b₄ being Function of b₁,b₂ holds eval b₃,b₄ = (coefficient b₃) * (eval (term b₃),b₄)

proof end;

theorem Th13: :: POLYNOM7:13

for b₁ being Ordinal
for b₂ being add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for b₃ being Element of b₂
for b₄ being bag of b₁
for b₅ being Function of b₁,b₂ holds eval (Monom b₃,b₄),b₅ = b₃ * (eval b₄,b₅)

proof end;

definition

let c₁ be set ;
let c₂ be non empty ZeroStr ;
let c₃ be Series of c₁,c₂;
attr a₃ is Constant means :Def8: :: POLYNOM7:def 8
for b₁ being bag of a₁ st b₁ <> EmptyBag a₁ holds
a₃ . b₁ = 0. a₂;

end;

:: deftheorem Def8 defines Constant POLYNOM7:def 8 :

registration

let c₁ be set ;
let c₂ be non empty ZeroStr ;
cluster Constant Relation of Bags a₁,the carrier of a₂;
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be non empty ZeroStr ;
mode ConstPoly of a₁,a₂ is Constant Series of a₁,a₂;

end;

registration

let c₁ be set ;
let c₂ be non empty ZeroStr ;
cluster Constant -> finite-Support monomial-like Relation of Bags a₁,the carrier of a₂;
coherence

proof end;

end;

theorem Th14: :: POLYNOM7:14

for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being Series of b₁,b₂ holds
( b₃ is ConstPoly of b₁,b₂ iff ( b₃ = 0_ b₁,b₂ or Support b₃ = {(EmptyBag b₁)} ) )

proof end;

registration

let c₁ be set ;
let c₂ be non empty ZeroStr ;
cluster 0_ a₁,a₂ -> finite-Support monomial-like Constant ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be non empty unital doubleLoopStr ;
cluster 1_ a₁,a₂ -> finite-Support monomial-like Constant ;
coherence

proof end;

end;

Lemma15: for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being ConstPoly of b₁,b₂ holds
( term b₃ = EmptyBag b₁ & coefficient b₃ = b₃ . (EmptyBag b₁) )

proof end;

theorem Th15: :: POLYNOM7:15

for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being ConstPoly of b₁,b₂ holds
( Support b₃ = {} or Support b₃ = {(EmptyBag b₁)} )

proof end;

theorem Th16: :: POLYNOM7:16

for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being ConstPoly of b₁,b₂ holds
( term b₃ = EmptyBag b₁ & coefficient b₃ = b₃ . (EmptyBag b₁) ) by Lemma15;

definition

let c₁ be set ;
let c₂ be non empty ZeroStr ;
let c₃ be Element of c₂;
func c₃ | c₁,c₂ -> Series of a₁,a₂ equals :: POLYNOM7:def 9
(0_ a₁,a₂) +* (EmptyBag a₁),a₃;
coherence ;

end;

:: deftheorem Def9 defines | POLYNOM7:def 9 :

registration

let c₁ be set ;
let c₂ be non empty ZeroStr ;
let c₃ be Element of c₂;
cluster a₃ | a₁,a₂ -> finite-Support monomial-like Constant ;
coherence

proof end;

end;

Lemma17: for b₁ being set
for b₂ being non empty ZeroStr holds (0. b₂) | b₁,b₂ = 0_ b₁,b₂

proof end;

theorem Th17: :: POLYNOM7:17

for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being Series of b₁,b₂ holds
( b₃ is ConstPoly of b₁,b₂ iff ex b₄ being Element of b₂ st b₃ = b₄ | b₁,b₂ )

proof end;

theorem Th18: :: POLYNOM7:18

for b₁ being set
for b₂ being non empty multLoopStr_0
for b₃ being Element of b₂ holds
( (b₃ | b₁,b₂) . (EmptyBag b₁) = b₃ & ( for b₄ being bag of b₁ st b₄ <> EmptyBag b₁ holds
(b₃ | b₁,b₂) . b₄ = 0. b₂ ) )

proof end;

theorem Th19: :: POLYNOM7:19

for b₁ being set
for b₂ being non empty ZeroStr holds (0. b₂) | b₁,b₂ = 0_ b₁,b₂ by Lemma17;

theorem Th20: :: POLYNOM7:20

for b₁ being set
for b₂ being non empty unital multLoopStr_0 holds (1. b₂) | b₁,b₂ = 1_ b₁,b₂

proof end;

theorem Th21: :: POLYNOM7:21

for b₁ being set
for b₂ being non empty ZeroStr
for b₃, b₄ being Element of b₂ holds
( b₃ | b₁,b₂ = b₄ | b₁,b₂ iff b₃ = b₄ )

proof end;

theorem Th22: :: POLYNOM7:22

for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being Element of b₂ holds
( Support (b₃ | b₁,b₂) = {} or Support (b₃ | b₁,b₂) = {(EmptyBag b₁)} ) by Th15;

theorem Th23: :: POLYNOM7:23

for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being Element of b₂ holds
( term (b₃ | b₁,b₂) = EmptyBag b₁ & coefficient (b₃ | b₁,b₂) = b₃ )

proof end;

theorem Th24: :: POLYNOM7:24

for b₁ being Ordinal
for b₂ being add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for b₃ being ConstPoly of b₁,b₂
for b₄ being Function of b₁,b₂ holds eval b₃,b₄ = coefficient b₃

proof end;

theorem Th25: :: POLYNOM7:25

for b₁ being Ordinal
for b₂ being add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for b₃ being Element of b₂
for b₄ being Function of b₁,b₂ holds eval (b₃ | b₁,b₂),b₄ = b₃

proof end;

definition

let c₁ be set ;
let c₂ be non empty multLoopStr_0 ;
let c₃ be Series of c₁,c₂;
let c₄ be Element of c₂;
func c₄ * c₃ -> Series of a₁,a₂ means :Def10: :: POLYNOM7:def 10
for b₁ being bag of a₁ holds a₅ . b₁ = a₄ * (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

func c₃ * c₄ -> Series of a₁,a₂ means :Def11: :: POLYNOM7:def 11
for b₁ being bag of a₁ holds a₅ . b₁ = (a₃ . b₁) * a₄;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines * POLYNOM7:def 10 :

:: deftheorem Def11 defines * POLYNOM7:def 11 :

registration

let c₁ be set ;
let c₂ be non empty right_zeroed distributive left_zeroed add-cancelable doubleLoopStr ;
let c₃ be finite-Support Series of c₁,c₂;
let c₄ be Element of c₂;
cluster a₄ * a₃ -> finite-Support ;
coherence

proof end;

cluster a₃ * a₄ -> finite-Support ;
coherence

proof end;

end;

theorem Th26: :: POLYNOM7:26

for b₁ being set
for b₂ being non empty commutative multLoopStr_0
for b₃ being Series of b₁,b₂
for b₄ being Element of b₂ holds b₄ * b₃ = b₃ * b₄

proof end;

theorem Th27: :: POLYNOM7:27

for b₁ being Ordinal
for b₂ being non empty add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b₃ being Series of b₁,b₂
for b₄ being Element of b₂ holds b₄ * b₃ = (b₄ | b₁,b₂) *' b₃

proof end;

theorem Th28: :: POLYNOM7:28

for b₁ being Ordinal
for b₂ being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b₃ being Series of b₁,b₂
for b₄ being Element of b₂ holds b₃ * b₄ = b₃ *' (b₄ | b₁,b₂)

proof end;

Lemma26: for b₁ being Ordinal
for b₂ being Abelian add-associative right_zeroed right_complementable unital associative commutative distributive left_zeroed non trivial doubleLoopStr
for b₃ being Polynomial of b₁,b₂
for b₄ being Element of b₂
for b₅ being Function of b₁,b₂ holds eval ((b₄ | b₁,b₂) *' b₃),b₅ = b₄ * (eval b₃,b₅)

proof end;

Lemma27: for b₁ being Ordinal
for b₂ being Abelian add-associative right_zeroed right_complementable unital associative commutative distributive left_zeroed non trivial doubleLoopStr
for b₃ being Polynomial of b₁,b₂
for b₄ being Element of b₂
for b₅ being Function of b₁,b₂ holds eval (b₃ *' (b₄ | b₁,b₂)),b₅ = (eval b₃,b₅) * b₄

proof end;

theorem Th29: :: POLYNOM7:29

for b₁ being Ordinal
for b₂ being Abelian add-associative right_zeroed right_complementable unital associative commutative distributive left_zeroed non trivial doubleLoopStr
for b₃ being Polynomial of b₁,b₂
for b₄ being Element of b₂
for b₅ being Function of b₁,b₂ holds eval (b₄ * b₃),b₅ = b₄ * (eval b₃,b₅)

proof end;

theorem Th30: :: POLYNOM7:30

for b₁ being Ordinal
for b₂ being add-associative right_zeroed right_complementable unital associative distributive left_zeroed add-left-cancelable domRing-like non trivial doubleLoopStr
for b₃ being Polynomial of b₁,b₂
for b₄ being Element of b₂
for b₅ being Function of b₁,b₂ holds eval (b₄ * b₃),b₅ = b₄ * (eval b₃,b₅)

proof end;

theorem Th31: :: POLYNOM7:31

proof end;

theorem Th32: :: POLYNOM7:32

for b₁ being Ordinal
for b₂ being add-associative right_zeroed right_complementable unital associative commutative distributive left_zeroed add-left-cancelable domRing-like non trivial doubleLoopStr
for b₃ being Polynomial of b₁,b₂
for b₄ being Element of b₂
for b₅ being Function of b₁,b₂ holds eval (b₃ * b₄),b₅ = (eval b₃,b₅) * b₄

proof end;

theorem Th33: :: POLYNOM7:33

theorem Th34: :: POLYNOM7:34

proof end;