:: Multivariate polynomials with arbitrary number of variables
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received September 22, 1999
:: Copyright (c) 1999-2011 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 doubleLoopStr ;
coherence
for b₁ being non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr st b₁ is degenerated holds
b₁ 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 doubleLoopStr ;
coherence
for b₁ being non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr st not b₁ is trivial holds
not b₁ is degenerated ;

end;

theorem :: POLYNOM1:1

canceled;

theorem :: POLYNOM1:2

canceled;

theorem :: POLYNOM1:3

canceled;

theorem :: POLYNOM1:4

canceled;

theorem Th5: :: POLYNOM1:5

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 :: POLYNOM1:6

canceled;

theorem :: POLYNOM1:7

canceled;

theorem :: POLYNOM1:8

canceled;

theorem :: POLYNOM1:9

canceled;

theorem :: POLYNOM1:10

canceled;

theorem :: POLYNOM1:11

canceled;

theorem :: POLYNOM1:12

canceled;

theorem :: POLYNOM1:13

canceled;

theorem :: POLYNOM1:14

canceled;

theorem Th15: :: POLYNOM1:15

for L being non empty addLoopStr
for F being FinSequence of the carrier of L * holds dom (Sum F) = dom F

proof end;

theorem Th16: :: POLYNOM1:16

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 Th17: :: POLYNOM1:17

for L being non empty addLoopStr
for p being Element of the carrier of L * holds <*(Sum p)*> = Sum <*p*>

proof end;

theorem Th18: :: POLYNOM1:18

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;
canceled;
redefine func a * p means :Def2: :: POLYNOM1:def 2
( dom it = dom p & ( for i being set st i in dom p holds
it /. i = a * (p /. i) ) );
compatibility
for b₁ being FinSequence of the carrier of L holds
( b₁ = a * p iff ( dom b₁ = dom p & ( for i being set st i in dom p holds
b₁ /. i = a * (p /. i) ) ) )

proof end;

end;

:: deftheorem POLYNOM1:def 1 :
canceled;

:: 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 b₄ being FinSequence of the carrier of L holds
( b₄ = a * p iff ( dom b₄ = dom p & ( for i being set st i in dom p holds
b₄ /. 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 :Def3: :: POLYNOM1:def 3
( dom it = dom p & ( for i being set st i in dom p holds
it /. i = (p /. i) * a ) );
existence
ex b₁ being FinSequence of the carrier of L st
( dom b₁ = dom p & ( for i being set st i in dom p holds
b₁ /. i = (p /. i) * a ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of the carrier of L st dom b₁ = dom p & ( for i being set st i in dom p holds
b₁ /. i = (p /. i) * a ) & dom b₂ = dom p & ( for i being set st i in dom p holds
b₂ /. i = (p /. i) * a ) holds
b₁ = b₂

proof end;

end;

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

theorem Th19: :: POLYNOM1:19

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 Th20: :: POLYNOM1:20

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 Th21: :: POLYNOM1:21

for L being non empty multMagma
for a, b being Element of L holds a * <*b*> = <*(a * b)*>

proof end;

theorem Th22: :: POLYNOM1:22

for L being non empty multMagma
for a, b being Element of L holds <*b*> * a = <*(b * a)*>

proof end;

theorem Th23: :: POLYNOM1:23

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 Th24: :: POLYNOM1:24

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 multLoopStr_0 ;
existence
ex b₁ being non empty strict multLoopStr_0 st b₁ 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 doubleLoopStr ;
existence
ex b₁ being non empty doubleLoopStr st
( b₁ is strict & b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is associative & b₁ is commutative & b₁ is distributive & b₁ is almost_left_invertible & b₁ is well-unital & not b₁ is trivial )

proof end;

end;

theorem :: POLYNOM1:25

canceled;

theorem :: POLYNOM1:26

canceled;

theorem :: POLYNOM1:27

canceled;

theorem Th28: :: POLYNOM1:28

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 Th29: :: POLYNOM1:29

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 :: POLYNOM1:30

canceled;

theorem :: POLYNOM1:31

canceled;

theorem :: POLYNOM1:32

canceled;

theorem :: POLYNOM1:33

canceled;

theorem Th34: :: POLYNOM1:34

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

canceled;
canceled;
canceled;
canceled;
canceled;
let X be non empty set ;
let S be ZeroStr ;
let f be Function of X,S;
func Support f -> Subset of X means :Def9: :: POLYNOM1:def 9
for x being Element of X holds
( x in it iff f . x <> 0. S );
existence
ex b₁ being Subset of X st
for x being Element of X holds
( x in b₁ iff f . x <> 0. S )

proof end;

uniqueness
for b₁, b₂ being Subset of X st ( for x being Element of X holds
( x in b₁ iff f . x <> 0. S ) ) & ( for x being Element of X holds
( x in b₂ iff f . x <> 0. S ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem POLYNOM1:def 4 :
canceled;

:: deftheorem POLYNOM1:def 5 :
canceled;

:: deftheorem POLYNOM1:def 6 :
canceled;

:: deftheorem POLYNOM1:def 7 :
canceled;

:: deftheorem POLYNOM1:def 8 :
canceled;

:: deftheorem Def9 defines Support POLYNOM1:def 9 :
for X being non empty set
for S being ZeroStr
for f being Function of X,S
for b₄ being Subset of X holds
( b₄ = Support f iff for x being Element of X holds
( x in b₄ 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 :Def10: :: POLYNOM1:def 10
Support p is finite ;

end;

:: deftheorem Def10 defines finite-Support POLYNOM1:def 10 :
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

canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
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 21
p + q;
coherence
p + q is Series of n,L

proof end;

end;

:: deftheorem POLYNOM1:def 11 :
canceled;

:: deftheorem POLYNOM1:def 12 :
canceled;

:: deftheorem POLYNOM1:def 13 :
canceled;

:: deftheorem POLYNOM1:def 14 :
canceled;

:: deftheorem POLYNOM1:def 15 :
canceled;

:: deftheorem POLYNOM1:def 16 :
canceled;

:: deftheorem POLYNOM1:def 17 :
canceled;

:: deftheorem POLYNOM1:def 18 :
canceled;

:: deftheorem POLYNOM1:def 19 :
canceled;

:: deftheorem POLYNOM1:def 20 :
canceled;

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

theorem TDef21: :: POLYNOM1:35

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:36

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 TDef22: :: POLYNOM1:37

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:38

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:39

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 :: POLYNOM1:40

canceled;

theorem :: POLYNOM1:41

canceled;

theorem :: POLYNOM1:42

canceled;

theorem :: POLYNOM1:43

canceled;

theorem :: POLYNOM1:44

canceled;

theorem :: POLYNOM1:45

canceled;

theorem :: POLYNOM1:46

canceled;

theorem :: POLYNOM1:47

canceled;

theorem :: POLYNOM1:48

canceled;

theorem :: POLYNOM1:49

canceled;

theorem :: POLYNOM1:50

canceled;

theorem :: POLYNOM1:51

canceled;

theorem :: POLYNOM1:52

canceled;

theorem :: POLYNOM1:53

canceled;

theorem :: POLYNOM1:54

canceled;

theorem :: POLYNOM1:55

canceled;

theorem :: POLYNOM1:56

canceled;

theorem :: POLYNOM1:57

canceled;

theorem :: POLYNOM1:58

canceled;

theorem :: POLYNOM1:59

canceled;

theorem :: POLYNOM1:60

canceled;

theorem :: POLYNOM1:61

canceled;

theorem :: POLYNOM1:62

canceled;

theorem :: POLYNOM1:63

canceled;

theorem :: POLYNOM1:64

canceled;

theorem :: POLYNOM1:65

canceled;

theorem :: POLYNOM1:66

canceled;

theorem :: POLYNOM1:67

canceled;

theorem :: POLYNOM1:68

canceled;

theorem :: POLYNOM1:69

canceled;

theorem :: POLYNOM1:70

canceled;

theorem :: POLYNOM1:71

canceled;

theorem :: POLYNOM1:72

canceled;

theorem :: POLYNOM1:73

canceled;

theorem :: POLYNOM1:74

canceled;

theorem :: POLYNOM1:75

canceled;

theorem :: POLYNOM1:76

canceled;

theorem :: POLYNOM1:77

canceled;

theorem :: POLYNOM1:78

canceled;

theorem Th79: :: POLYNOM1:79

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 Th80: :: POLYNOM1:80

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

canceled;
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 23
p + (- q);
coherence
p + (- q) is Series of n,L ;

end;

:: deftheorem POLYNOM1:def 22 :
canceled;

:: deftheorem defines - POLYNOM1:def 23 :
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 24
(Bags n) --> (0. S);
coherence
(Bags n) --> (0. S) is Series of n,S ;

end;

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

theorem Th81: :: POLYNOM1:81

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 Th82: :: POLYNOM1:82

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 25
(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 25 :
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 Th83: :: POLYNOM1:83

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 Th84: :: POLYNOM1:84

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 :Def26: :: POLYNOM1:def 26
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 b₁ being Series of n,L st
for b being bag of n ex s being FinSequence of the carrier of L st
( b₁ . 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 b₁, b₂ being Series of n,L st ( for b being bag of n ex s being FinSequence of the carrier of L st
( b₁ . 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
( b₂ . 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
b₁ = b₂

proof end;

end;

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

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 Th86: :: POLYNOM1:86

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:87

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 Th88: :: POLYNOM1:88

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 Th89: :: POLYNOM1:89

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 Element of bool [:(Bags n), the carrier of S:];
existence
ex b₁ being Series of n,S st b₁ 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 empty 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 empty non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;
func Polynom-Ring (n,L) -> non empty strict doubleLoopStr means :Def27: :: POLYNOM1:def 27
( ( 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 b₁ being non empty strict doubleLoopStr st
( ( for x being set holds
( x in the carrier of b₁ iff x is Polynomial of n,L ) ) & ( for x, y being Element of b₁
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₁
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. b₁ = 0_ (n,L) & 1. b₁ = 1_ (n,L) )

proof end;

uniqueness
for b₁, b₂ being non empty strict doubleLoopStr st ( for x being set holds
( x in the carrier of b₁ iff x is Polynomial of n,L ) ) & ( for x, y being Element of b₁
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₁
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. b₁ = 0_ (n,L) & 1. b₁ = 1_ (n,L) & ( for x being set holds
( x in the carrier of b₂ iff x is Polynomial of n,L ) ) & ( for x, y being Element of b₂
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₂
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. b₂ = 0_ (n,L) & 1. b₂ = 1_ (n,L) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def27 defines Polynom-Ring POLYNOM1:def 27 :
for n being Ordinal
for L being non empty non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for b₃ being non empty strict doubleLoopStr holds
( b₃ = Polynom-Ring (n,L) iff ( ( for x being set holds
( x in the carrier of b₃ iff x is Polynomial of n,L ) ) & ( for x, y being Element of b₃
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₃
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. b₃ = 0_ (n,L) & 1. b₃ = 1_ (n,L) ) );

registration

let n be Ordinal;
let L be non empty 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 empty 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 empty 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 empty 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

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 Def27;
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 Def27;
hence x * e = p *' (1_ (n,L)) by A1, Def27
.= x by Th88 ;
:: thesis: e * x = x
thus e * x = (1_ (n,L)) *' p by A1, A2, Def27
.= x by Th89 ; :: 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:90

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 Def27;