:: Multivariate polynomials with arbitrary number of variables
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received September 22, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

registration
cluster non empty degenerated right_complementable right-distributive right_unital add-associative right_zeroed -> non empty trivial right_complementable right-distributive right_unital add-associative right_zeroed for doubleLoopStr ;
coherence
for b1 being non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr st b1 is degenerated holds
b1 is trivial
proof end;
end;

registration
cluster non empty non trivial right_complementable right-distributive right_unital add-associative right_zeroed -> non empty non degenerated right_complementable right-distributive right_unital add-associative right_zeroed for doubleLoopStr ;
coherence
for b1 being non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr st not b1 is trivial holds
not b1 is degenerated
;
end;

theorem Th1: :: POLYNOM1:1
for K being non empty addLoopStr
for p1, p2 being FinSequence of the carrier of K st dom p1 = dom p2 holds
dom (p1 + p2) = dom p1
proof end;

theorem Th2: :: POLYNOM1:2
for L being non empty addLoopStr
for F being FinSequence of the carrier of L * holds dom (Sum F) = dom F
proof end;

theorem Th3: :: POLYNOM1:3
for L being non empty addLoopStr
for F being FinSequence of the carrier of L * holds Sum (<*> ( the carrier of L *)) = <*> the carrier of L
proof end;

theorem Th4: :: POLYNOM1:4
for L being non empty addLoopStr
for p being Element of the carrier of L * holds <*(Sum p)*> = Sum <*p*>
proof end;

theorem Th5: :: POLYNOM1:5
for L being non empty addLoopStr
for F, G being FinSequence of the carrier of L * holds Sum (F ^ G) = (Sum F) ^ (Sum G)
proof end;

definition
let L be non empty multMagma ;
let p be FinSequence of the carrier of L;
let a be Element of L;
redefine func a * p means :Def1: :: POLYNOM1:def 1
( dom it = dom p & ( for i being set st i in dom p holds
it /. i = a * (p /. i) ) );
compatibility
for b1 being FinSequence of the carrier of L holds
( b1 = a * p iff ( dom b1 = dom p & ( for i being set st i in dom p holds
b1 /. i = a * (p /. i) ) ) )
proof end;
end;

:: deftheorem Def1 defines * POLYNOM1:def 1 :
for L being non empty multMagma
for p being FinSequence of the carrier of L
for a being Element of L
for b4 being FinSequence of the carrier of L holds
( b4 = a * p iff ( dom b4 = dom p & ( for i being set st i in dom p holds
b4 /. i = a * (p /. i) ) ) );

definition
let L be non empty multMagma ;
let p be FinSequence of the carrier of L;
let a be Element of L;
func p * a -> FinSequence of the carrier of L means :Def2: :: POLYNOM1:def 2
( dom it = dom p & ( for i being set st i in dom p holds
it /. i = (p /. i) * a ) );
existence
ex b1 being FinSequence of the carrier of L st
( dom b1 = dom p & ( for i being set st i in dom p holds
b1 /. i = (p /. i) * a ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of L st dom b1 = dom p & ( for i being set st i in dom p holds
b1 /. i = (p /. i) * a ) & dom b2 = dom p & ( for i being set st i in dom p holds
b2 /. i = (p /. i) * a ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines * POLYNOM1:def 2 :
for L being non empty multMagma
for p being FinSequence of the carrier of L
for a being Element of L
for b4 being FinSequence of the carrier of L holds
( b4 = p * a iff ( dom b4 = dom p & ( for i being set st i in dom p holds
b4 /. i = (p /. i) * a ) ) );

theorem Th6: :: POLYNOM1:6
for L being non empty multMagma
for a being Element of L holds a * (<*> the carrier of L) = <*> the carrier of L
proof end;

theorem Th7: :: POLYNOM1:7
for L being non empty multMagma
for a being Element of L holds (<*> the carrier of L) * a = <*> the carrier of L
proof end;

theorem Th8: :: POLYNOM1:8
for L being non empty multMagma
for a, b being Element of L holds a * <*b*> = <*(a * b)*>
proof end;

theorem Th9: :: POLYNOM1:9
for L being non empty multMagma
for a, b being Element of L holds <*b*> * a = <*(b * a)*>
proof end;

theorem Th10: :: POLYNOM1:10
for L being non empty multMagma
for a being Element of L
for p, q being FinSequence of the carrier of L holds a * (p ^ q) = (a * p) ^ (a * q)
proof end;

theorem Th11: :: POLYNOM1:11
for L being non empty multMagma
for a being Element of L
for p, q being FinSequence of the carrier of L holds (p ^ q) * a = (p * a) ^ (q * a)
proof end;

registration
cluster non empty strict right_unital for multLoopStr_0 ;
existence
ex b1 being non empty strict multLoopStr_0 st b1 is right_unital
proof end;
end;

registration
cluster non empty non trivial right_complementable almost_left_invertible strict associative commutative well-unital distributive Abelian add-associative right_zeroed for doubleLoopStr ;
existence
ex b1 being non empty doubleLoopStr st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is associative & b1 is commutative & b1 is distributive & b1 is almost_left_invertible & b1 is well-unital & not b1 is trivial )
proof end;
end;

theorem Th12: :: POLYNOM1:12
for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for a being Element of L
for p being FinSequence of the carrier of L holds Sum (a * p) = a * (Sum p)
proof end;

theorem Th13: :: POLYNOM1:13
for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for a being Element of L
for p being FinSequence of the carrier of L holds Sum (p * a) = (Sum p) * a
proof end;

begin

theorem Th14: :: POLYNOM1:14
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for F being FinSequence of the carrier of L * holds Sum (FlattenSeq F) = Sum (Sum F)
proof end;

definition
let X be non empty set ;
let S be ZeroStr ;
let f be Function of X,S;
func Support f -> Subset of X means :Def3: :: POLYNOM1:def 3
for x being Element of X holds
( x in it iff f . x <> 0. S );
existence
ex b1 being Subset of X st
for x being Element of X holds
( x in b1 iff f . x <> 0. S )
proof end;
uniqueness
for b1, b2 being Subset of X st ( for x being Element of X holds
( x in b1 iff f . x <> 0. S ) ) & ( for x being Element of X holds
( x in b2 iff f . x <> 0. S ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Support POLYNOM1:def 3 :
for X being non empty set
for S being ZeroStr
for f being Function of X,S
for b4 being Subset of X holds
( b4 = Support f iff for x being Element of X holds
( x in b4 iff f . x <> 0. S ) );

definition
let X be non empty set ;
let S be ZeroStr ;
let p be Function of X,S;
attr p is finite-Support means :Def4: :: POLYNOM1:def 4
Support p is finite ;
end;

:: deftheorem Def4 defines finite-Support POLYNOM1:def 4 :
for X being non empty set
for S being ZeroStr
for p being Function of X,S holds
( p is finite-Support iff Support p is finite );

definition
let n be set ;
let L be non empty 1-sorted ;
let p be Function of (Bags n),L;
let x be bag of n;
:: original: .
redefine func p . x -> Element of L;
coherence
p . x is Element of L
proof end;
end;

begin

definition
let X be set ;
let S be 1-sorted ;
mode Series of X,S is Function of (Bags X),S;
end;

definition
let n be set ;
let L be non empty addLoopStr ;
let p, q be Series of n,L;
func p + q -> Series of n,L equals :: POLYNOM1:def 5
p + q;
coherence
p + q is Series of n,L
;
end;

:: deftheorem defines + POLYNOM1:def 5 :
for n being set
for L being non empty addLoopStr
for p, q being Series of n,L holds p + q = p + q;

theorem Th15: :: POLYNOM1:15
for n being set
for L being non empty addLoopStr
for p, q being Series of n,L
for x being bag of n holds (p + q) . x = (p . x) + (q . x)
proof end;

theorem :: POLYNOM1:16
for n being set
for L being non empty addLoopStr
for p, q, r being Series of n,L st ( for x being bag of n holds r . x = (p . x) + (q . x) ) holds
r = p + q
proof end;

theorem Th17: :: POLYNOM1:17
for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L
for x being bag of n holds (- p) . x = - (p . x)
proof end;

theorem :: POLYNOM1:18
for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, r being Series of n,L st ( for x being bag of n holds r . x = - (p . x) ) holds
r = - p
proof end;

theorem :: POLYNOM1:19
for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L holds p = - (- p)
proof end;

theorem Th20: :: POLYNOM1:20
for n being set
for L being non empty right_zeroed addLoopStr
for p, q being Series of n,L holds Support (p + q) c= (Support p) \/ (Support q)
proof end;

definition
let n be set ;
let L be non empty Abelian right_zeroed addLoopStr ;
let p, q be Series of n,L;
:: original: +
redefine func p + q -> Series of n,L;
commutativity
for p, q being Series of n,L holds p + q = q + p
proof end;
end;

theorem Th21: :: POLYNOM1:21
for n being set
for L being non empty add-associative right_zeroed doubleLoopStr
for p, q, r being Series of n,L holds (p + q) + r = p + (q + r)
proof end;

definition
let n be set ;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p, q be Series of n,L;
func p - q -> Series of n,L equals :: POLYNOM1:def 6
p + (- q);
coherence
p + (- q) is Series of n,L
;
end;

:: deftheorem defines - POLYNOM1:def 6 :
for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, q being Series of n,L holds p - q = p + (- q);

definition
let n be set ;
let S be non empty ZeroStr ;
func 0_ (n,S) -> Series of n,S equals :: POLYNOM1:def 7
(Bags n) --> (0. S);
coherence
(Bags n) --> (0. S) is Series of n,S
;
end;

:: deftheorem defines 0_ POLYNOM1:def 7 :
for n being set
for S being non empty ZeroStr holds 0_ (n,S) = (Bags n) --> (0. S);

theorem Th22: :: POLYNOM1:22
for n being set
for S being non empty ZeroStr
for b being bag of n holds (0_ (n,S)) . b = 0. S
proof end;

theorem Th23: :: POLYNOM1:23
for n being set
for L being non empty right_zeroed addLoopStr
for p being Series of n,L holds p + (0_ (n,L)) = p
proof end;

definition
let n be set ;
let L be non empty right_unital multLoopStr_0 ;
func 1_ (n,L) -> Series of n,L equals :: POLYNOM1:def 8
(0_ (n,L)) +* ((EmptyBag n),(1. L));
coherence
(0_ (n,L)) +* ((EmptyBag n),(1. L)) is Series of n,L
;
end;

:: deftheorem defines 1_ POLYNOM1:def 8 :
for n being set
for L being non empty right_unital multLoopStr_0 holds 1_ (n,L) = (0_ (n,L)) +* ((EmptyBag n),(1. L));

theorem Th24: :: POLYNOM1:24
for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L holds p - p = 0_ (n,L)
proof end;

theorem Th25: :: POLYNOM1:25
for n being set
for L being non empty right_unital multLoopStr_0 holds
( (1_ (n,L)) . (EmptyBag n) = 1. L & ( for b being bag of n st b <> EmptyBag n holds
(1_ (n,L)) . b = 0. L ) )
proof end;

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;
func p *' q -> Series of n,L means :Def9: :: POLYNOM1:def 9
for b being bag of n ex s being FinSequence of the carrier of L st
( it . 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) ) ) );
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) ) ) )
proof end;
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
proof end;
end;

:: deftheorem Def9 defines *' POLYNOM1:def 9 :
for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed doubleLoopStr
for p, q, b5 being Series of n,L holds
( b5 = p *' q iff for b being bag of n ex s being FinSequence of the carrier of L st
( b5 . 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) ) ) ) );

theorem Th26: :: POLYNOM1:26
for n being Ordinal
for L being non empty right_complementable associative distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being Series of n,L holds p *' (q + r) = (p *' q) + (p *' r)
proof end;

theorem Th27: :: POLYNOM1:27
for n being Ordinal
for L being non empty right_complementable associative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being Series of n,L holds (p *' q) *' r = p *' (q *' r)
proof end;

definition
let n be Ordinal;
let L be non empty right_complementable commutative Abelian add-associative right_zeroed doubleLoopStr ;
let p, q be Series of n,L;
:: original: *'
redefine func p *' q -> Series of n,L;
commutativity
for p, q being Series of n,L holds p *' q = q *' p
proof end;
end;

theorem :: POLYNOM1:28
for n being Ordinal
for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds p *' (0_ (n,L)) = 0_ (n,L)
proof end;

theorem Th29: :: POLYNOM1:29
for n being Ordinal
for L being non empty non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds p *' (1_ (n,L)) = p
proof end;

theorem Th30: :: POLYNOM1:30
for n being Ordinal
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds (1_ (n,L)) *' p = p
proof end;

begin

registration
let n be set ;
let S be non empty ZeroStr ;
cluster Relation-like Bags n -defined the carrier of S -valued Function-like non empty total quasi_total finite-Support for Element of bool [:(Bags n), the carrier of S:];
existence
ex b1 being Series of n,S st b1 is finite-Support
proof end;
end;

definition
let n be Ordinal;
let S be non empty ZeroStr ;
mode Polynomial of n,S is finite-Support Series of n,S;
end;

registration
let n be Ordinal;
let L be non empty right_zeroed addLoopStr ;
let p, q be Polynomial of n,L;
cluster p + q -> finite-Support ;
coherence
p + q is finite-Support
proof end;
end;

registration
let n be Ordinal;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p be Polynomial of n,L;
cluster - p -> finite-Support ;
coherence
- p is finite-Support
proof end;
end;

registration
let n be Element of NAT ;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p, q be Polynomial of n,L;
cluster p - q -> finite-Support ;
coherence
p - q is finite-Support
;
end;

registration
let n be Ordinal;
let S be non empty ZeroStr ;
cluster 0_ (n,S) -> finite-Support ;
coherence
0_ (n,S) is finite-Support
proof end;
end;

registration
let n be Ordinal;
let L be non trivial right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr ;
cluster 1_ (n,L) -> finite-Support ;
coherence
1_ (n,L) is finite-Support
proof end;
end;

registration
let n be Ordinal;
let L be non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;
let p, q be Polynomial of n,L;
cluster p *' q -> finite-Support ;
coherence
p *' q is finite-Support
proof end;
end;

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: :: POLYNOM1:def 10
( ( 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) )
proof end;
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
proof end;
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) ) );

registration
let n be Ordinal;
let L be non trivial right_complementable right_unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) -> non empty strict Abelian ;
coherence
Polynom-Ring (n,L) is Abelian
proof end;
end;

registration
let n be Ordinal;
let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) -> non empty strict add-associative ;
coherence
Polynom-Ring (n,L) is add-associative
proof end;
end;

registration
let n be Ordinal;
let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) -> non empty strict right_zeroed ;
coherence
Polynom-Ring (n,L) is right_zeroed
proof end;
end;

registration
let n be Ordinal;
let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) -> non empty right_complementable strict ;
coherence
Polynom-Ring (n,L) is right_complementable
proof end;
end;

registration
let n be Ordinal;
let L be non empty non trivial right_complementable commutative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) -> non empty strict commutative ;
coherence
Polynom-Ring (n,L) is commutative
proof end;
end;

registration
let n be Ordinal;
let L be non empty non trivial right_complementable associative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) -> non empty strict associative ;
coherence
Polynom-Ring (n,L) is associative
proof end;
end;

Lm1: now :: thesis: 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; :: thesis: 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 ; :: thesis: 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)); :: thesis: ( 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)) ; :: thesis: ( 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 ;
:: thesis: e * x = x
thus e * x = (1_ (n,L)) *' p by A1, A2, Def10
.= x by Th30 ; :: thesis: verum
end;

registration
let n be Ordinal;
let L be non empty non trivial right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) -> non empty strict right-distributive well-unital ;
coherence
( Polynom-Ring (n,L) is well-unital & Polynom-Ring (n,L) is right-distributive )
proof end;
end;

theorem :: POLYNOM1:31
for n being Ordinal
for L being non empty non trivial right_complementable associative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr holds 1. (Polynom-Ring (n,L)) = 1_ (n,L) by Def10;