:: POLYNOM7 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
cluster non empty non trivial ZeroStr ;
existence
not for b1 being non empty ZeroStr holds b1 is trivial
proof end;
end;

registration
cluster non trivial -> non empty ZeroStr ;
coherence
for b1 being ZeroStr st not b1 is trivial holds
not b1 is empty
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
ex b1 being non trivial doubleLoopStr st
( b1 is Abelian & b1 is left_zeroed & b1 is right_zeroed & b1 is add-associative & b1 is right_complementable & b1 is unital & b1 is associative & b1 is commutative & b1 is distributive & b1 is domRing-like )
proof end;
end;

registration
let R be non trivial ZeroStr ;
cluster non-zero Element of the carrier of R;
existence
ex b1 being Element of R st b1 is non-zero
proof end;
end;

definition
let X be set ;
let R be non empty ZeroStr ;
let p be Series of X,R;
canceled;
attr p is non-zero means :Def2: :: POLYNOM7:def 2
p <> 0_ X,R;
end;

:: deftheorem POLYNOM7:def 1 :
canceled;

:: deftheorem Def2 defines non-zero POLYNOM7:def 2 :
for X being set
for R being non empty ZeroStr
for p being Series of X,R holds
( p is non-zero iff p <> 0_ X,R );

registration
let X be set ;
let R be non trivial ZeroStr ;
cluster non-zero Relation of Bags X,the carrier of R;
existence
ex b1 being Series of X,R st b1 is non-zero
proof end;
end;

registration
let n be Ordinal;
let R be non trivial ZeroStr ;
cluster non-zero Relation of Bags n,the carrier of R;
existence
ex b1 being Polynomial of n,R st b1 is non-zero
proof end;
end;

theorem Th1: :: POLYNOM7:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for R being non empty ZeroStr
for s being Series of X,R holds
( s = 0_ X,R iff Support s = {} )
proof end;

theorem :: POLYNOM7:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for R being non empty ZeroStr holds
( not R is trivial iff ex s being Series of X,R st Support s <> {} )
proof end;

definition
let X be set ;
let b be bag of X;
attr b is univariate means :Def3: :: POLYNOM7:def 3
ex u being Element of X st support b = {u};
end;

:: deftheorem Def3 defines univariate POLYNOM7:def 3 :
for X being set
for b being bag of X holds
( b is univariate iff ex u being Element of X st support b = {u} );

registration
let X be non empty set ;
cluster univariate M32(X);
existence
ex b1 being bag of X st b1 is univariate
proof end;
end;

registration
let X be non empty set ;
cluster univariate -> non empty M32(X);
coherence
for b1 being bag of X st b1 is univariate holds
not b1 is empty
proof end;
end;

theorem :: POLYNOM7:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b being bag of {} holds b = EmptyBag {}
proof end;

Lm1: for L being non empty doubleLoopStr
for p being Polynomial of {} ,L ex a being Element of L st p = {(EmptyBag {} )} --> a
proof end;

theorem :: POLYNOM7:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for p being Polynomial of {} ,L
for x being Function of {} ,L holds eval p,x = p . (EmptyBag {} )
proof end;

theorem :: POLYNOM7:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Abelian add-associative right_zeroed right_complementable unital associative distributive non trivial doubleLoopStr holds Polynom-Ring {} ,L is_ringisomorph_to L
proof end;

definition
let X be set ;
let L be non empty ZeroStr ;
let p be Series of X,L;
attr p is monomial-like means :Def4: :: POLYNOM7:def 4
ex b being bag of X st
for b' being bag of X st b' <> b holds
p . b' = 0. L;
end;

:: deftheorem Def4 defines monomial-like POLYNOM7:def 4 :
for X being set
for L being non empty ZeroStr
for p being Series of X,L holds
( p is monomial-like iff ex b being bag of X st
for b' being bag of X st b' <> b holds
p . b' = 0. L );

registration
let X be set ;
let L be non empty ZeroStr ;
cluster monomial-like Relation of Bags X,the carrier of L;
existence
ex b1 being Series of X,L st b1 is monomial-like
proof end;
end;

definition
let X be set ;
let L be non empty ZeroStr ;
mode Monomial of X,L is monomial-like Series of X,L;
end;

registration
let X be set ;
let L be non empty ZeroStr ;
cluster monomial-like -> finite-Support Relation of Bags X,the carrier of L;
coherence
for b1 being Series of X,L st b1 is monomial-like holds
b1 is finite-Support
proof end;
end;

theorem Th6: :: POLYNOM7:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty ZeroStr
for p being Series of X,L holds
( p is Monomial of X,L iff ( Support p = {} or ex b being bag of X st Support p = {b} ) )
proof end;

definition
let X be set ;
let L be non empty ZeroStr ;
let a be Element of L;
let b be bag of X;
func Monom a,b -> Monomial of X,L equals :: POLYNOM7:def 5
(0_ X,L) +* b,a;
coherence
(0_ X,L) +* b,a is Monomial of X,L
proof end;
end;

:: deftheorem defines Monom POLYNOM7:def 5 :
for X being set
for L being non empty ZeroStr
for a being Element of L
for b being bag of X holds Monom a,b = (0_ X,L) +* b,a;

definition
let X be set ;
let L be non empty ZeroStr ;
let m be Monomial of X,L;
func term m -> bag of X means :Def6: :: POLYNOM7:def 6
( m . it <> 0. L or ( Support m = {} & it = EmptyBag X ) );
existence
ex b1 being bag of X st
( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) )
proof end;
uniqueness
for b1, b2 being bag of X st ( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) ) & ( m . b2 <> 0. L or ( Support m = {} & b2 = EmptyBag X ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines term POLYNOM7:def 6 :
for X being set
for L being non empty ZeroStr
for m being Monomial of X,L
for b4 being bag of X holds
( b4 = term m iff ( m . b4 <> 0. L or ( Support m = {} & b4 = EmptyBag X ) ) );

definition
let X be set ;
let L be non empty ZeroStr ;
let m be Monomial of X,L;
func coefficient m -> Element of L equals :: POLYNOM7:def 7
m . (term m);
coherence
m . (term m) is Element of L
;
end;

:: deftheorem defines coefficient POLYNOM7:def 7 :
for X being set
for L being non empty ZeroStr
for m being Monomial of X,L holds coefficient m = m . (term m);

theorem Th7: :: POLYNOM7:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty ZeroStr
for m being Monomial of X,L holds
( Support m = {} or Support m = {(term m)} )
proof end;

theorem Th8: :: POLYNOM7:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty ZeroStr
for b being bag of X holds
( coefficient (Monom (0. L),b) = 0. L & term (Monom (0. L),b) = EmptyBag X )
proof end;

theorem Th9: :: POLYNOM7:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty ZeroStr
for a being Element of L
for b being bag of X holds coefficient (Monom a,b) = a
proof end;

theorem Th10: :: POLYNOM7:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non trivial ZeroStr
for a being non-zero Element of L
for b being bag of X holds term (Monom a,b) = b
proof end;

theorem :: POLYNOM7:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty ZeroStr
for m being Monomial of X,L holds Monom (coefficient m),(term m) = m
proof end;

theorem Th12: :: POLYNOM7:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for m being Monomial of n,L
for x being Function of n,L holds eval m,x = (coefficient m) * (eval (term m),x)
proof end;

theorem :: POLYNOM7:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for a being Element of L
for b being bag of n
for x being Function of n,L holds eval (Monom a,b),x = a * (eval b,x)
proof end;

definition
let X be set ;
let L be non empty ZeroStr ;
let p be Series of X,L;
attr p is Constant means :Def8: :: POLYNOM7:def 8
for b being bag of X st b <> EmptyBag X holds
p . b = 0. L;
end;

:: deftheorem Def8 defines Constant POLYNOM7:def 8 :
for X being set
for L being non empty ZeroStr
for p being Series of X,L holds
( p is Constant iff for b being bag of X st b <> EmptyBag X holds
p . b = 0. L );

registration
let X be set ;
let L be non empty ZeroStr ;
cluster Constant Relation of Bags X,the carrier of L;
existence
ex b1 being Series of X,L st b1 is Constant
proof end;
end;

definition
let X be set ;
let L be non empty ZeroStr ;
mode ConstPoly of X,L is Constant Series of X,L;
end;

registration
let X be set ;
let L be non empty ZeroStr ;
cluster Constant -> finite-Support monomial-like Relation of Bags X,the carrier of L;
coherence
for b1 being Series of X,L st b1 is Constant holds
b1 is monomial-like
proof end;
end;

theorem Th14: :: POLYNOM7:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty ZeroStr
for p being Series of X,L holds
( p is ConstPoly of X,L iff ( p = 0_ X,L or Support p = {(EmptyBag X)} ) )
proof end;

registration
let X be set ;
let L be non empty ZeroStr ;
cluster 0_ X,L -> finite-Support monomial-like Constant ;
coherence
0_ X,L is Constant
proof end;
end;

registration
let X be set ;
let L be non empty unital doubleLoopStr ;
cluster 1_ X,L -> finite-Support monomial-like Constant ;
coherence
1_ X,L is Constant
proof end;
end;

Lm2: for X being set
for L being non empty ZeroStr
for c being ConstPoly of X,L holds
( term c = EmptyBag X & coefficient c = c . (EmptyBag X) )
proof end;

theorem Th15: :: POLYNOM7:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty ZeroStr
for c being ConstPoly of X,L holds
( Support c = {} or Support c = {(EmptyBag X)} )
proof end;

theorem :: POLYNOM7:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty ZeroStr
for c being ConstPoly of X,L holds
( term c = EmptyBag X & coefficient c = c . (EmptyBag X) ) by Lm2;

definition
let X be set ;
let L be non empty ZeroStr ;
let a be Element of L;
func a | X,L -> Series of X,L equals :: POLYNOM7:def 9
(0_ X,L) +* (EmptyBag X),a;
coherence
(0_ X,L) +* (EmptyBag X),a is Series of X,L
;
end;

:: deftheorem defines | POLYNOM7:def 9 :
for X being set
for L being non empty ZeroStr
for a being Element of L holds a | X,L = (0_ X,L) +* (EmptyBag X),a;

registration
let X be set ;
let L be non empty ZeroStr ;
let a be Element of L;
cluster a | X,L -> finite-Support monomial-like Constant ;
coherence
a | X,L is Constant
proof end;
end;

Lm3: for X being set
for L being non empty ZeroStr holds (0. L) | X,L = 0_ X,L
proof end;

theorem :: POLYNOM7:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty ZeroStr
for p being Series of X,L holds
( p is ConstPoly of X,L iff ex a being Element of L st p = a | X,L )
proof end;

theorem Th18: :: POLYNOM7:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty multLoopStr_0
for a being Element of L holds
( (a | X,L) . (EmptyBag X) = a & ( for b being bag of X st b <> EmptyBag X holds
(a | X,L) . b = 0. L ) )
proof end;

theorem :: POLYNOM7:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty ZeroStr holds (0. L) | X,L = 0_ X,L by Lm3;

theorem :: POLYNOM7:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty unital multLoopStr_0 holds (1. L) | X,L = 1_ X,L
proof end;

theorem :: POLYNOM7:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty ZeroStr
for a, b being Element of L holds
( a | X,L = b | X,L iff a = b )
proof end;

theorem :: POLYNOM7:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty ZeroStr
for a being Element of L holds
( Support (a | X,L) = {} or Support (a | X,L) = {(EmptyBag X)} ) by Th15;

theorem Th23: :: POLYNOM7:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty ZeroStr
for a being Element of L holds
( term (a | X,L) = EmptyBag X & coefficient (a | X,L) = a )
proof end;

theorem Th24: :: POLYNOM7:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for c being ConstPoly of n,L
for x being Function of n,L holds eval c,x = coefficient c
proof end;

theorem Th25: :: POLYNOM7:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for a being Element of L
for x being Function of n,L holds eval (a | n,L),x = a
proof end;

definition
let X be set ;
let L be non empty multLoopStr_0 ;
let p be Series of X,L;
let a be Element of L;
func a * p -> Series of X,L means :Def10: :: POLYNOM7:def 10
for b being bag of X holds it . b = a * (p . b);
existence
ex b1 being Series of X,L st
for b being bag of X holds b1 . b = a * (p . b)
proof end;
uniqueness
for b1, b2 being Series of X,L st ( for b being bag of X holds b1 . b = a * (p . b) ) & ( for b being bag of X holds b2 . b = a * (p . b) ) holds
b1 = b2
proof end;
func p * a -> Series of X,L means :Def11: :: POLYNOM7:def 11
for b being bag of X holds it . b = (p . b) * a;
existence
ex b1 being Series of X,L st
for b being bag of X holds b1 . b = (p . b) * a
proof end;
uniqueness
for b1, b2 being Series of X,L st ( for b being bag of X holds b1 . b = (p . b) * a ) & ( for b being bag of X holds b2 . b = (p . b) * a ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines * POLYNOM7:def 10 :
for X being set
for L being non empty multLoopStr_0
for p being Series of X,L
for a being Element of L
for b5 being Series of X,L holds
( b5 = a * p iff for b being bag of X holds b5 . b = a * (p . b) );

:: deftheorem Def11 defines * POLYNOM7:def 11 :
for X being set
for L being non empty multLoopStr_0
for p being Series of X,L
for a being Element of L
for b5 being Series of X,L holds
( b5 = p * a iff for b being bag of X holds b5 . b = (p . b) * a );

registration
let X be set ;
let L be non empty right_zeroed distributive left_zeroed add-cancelable doubleLoopStr ;
let p be finite-Support Series of X,L;
let a be Element of L;
cluster a * p -> finite-Support ;
coherence
a * p is finite-Support
proof end;
cluster p * a -> finite-Support ;
coherence
p * a is finite-Support
proof end;
end;

theorem :: POLYNOM7:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty commutative multLoopStr_0
for p being Series of X,L
for a being Element of L holds a * p = p * a
proof end;

theorem Th27: :: POLYNOM7:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for p being Series of n,L
for a being Element of L holds a * p = (a | n,L) *' p
proof end;

theorem Th28: :: POLYNOM7:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for p being Series of n,L
for a being Element of L holds p * a = p *' (a | n,L)
proof end;

Lm4: for n being Ordinal
for L being Abelian add-associative right_zeroed right_complementable unital associative commutative distributive left_zeroed non trivial doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval ((a | n,L) *' p),x = a * (eval p,x)
proof end;

Lm5: for n being Ordinal
for L being Abelian add-associative right_zeroed right_complementable unital associative commutative distributive left_zeroed non trivial doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval (p *' (a | n,L)),x = (eval p,x) * a
proof end;

theorem :: POLYNOM7:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being Abelian add-associative right_zeroed right_complementable unital associative commutative distributive left_zeroed non trivial doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval (a * p),x = a * (eval p,x)
proof end;

theorem :: POLYNOM7:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being add-associative right_zeroed right_complementable unital associative distributive left_zeroed add-left-cancelable domRing-like non trivial doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval (a * p),x = a * (eval p,x)
proof end;

theorem :: POLYNOM7:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being Abelian add-associative right_zeroed right_complementable unital associative commutative distributive left_zeroed non trivial doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval (p * a),x = (eval p,x) * a
proof end;

theorem :: POLYNOM7:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being add-associative right_zeroed right_complementable unital associative commutative distributive left_zeroed add-left-cancelable domRing-like non trivial doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval (p * a),x = (eval p,x) * a
proof end;

theorem :: POLYNOM7:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being Abelian add-associative right_zeroed right_complementable unital associative commutative distributive left_zeroed non trivial doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval ((a | n,L) *' p),x = a * (eval p,x) by Lm4;

theorem :: POLYNOM7:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being Abelian add-associative right_zeroed right_complementable unital associative commutative distributive left_zeroed non trivial doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval (p *' (a | n,L)),x = (eval p,x) * a
proof end;