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

theorem Th1: :: POLYNOM3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable LoopStr
for p being FinSequence of the carrier of L st ( for i being Nat st i in dom p holds
p . i = 0. L ) holds
Sum p = 0. L
proof end;

theorem Th2: :: POLYNOM3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty Abelian add-associative right_zeroed LoopStr
for p being FinSequence of the carrier of V holds Sum p = Sum (Rev p)
proof end;

theorem Th3: :: POLYNOM3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence of REAL holds Sum p = Sum (Rev p)
proof end;

theorem Th4: :: POLYNOM3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence of NAT
for i being Nat st i in dom p holds
Sum p >= p . i
proof end;

definition
let D be non empty set ;
let i be Nat;
let p be FinSequence of D;
:: original: Del
redefine func Del p,i -> FinSequence of D;
coherence
Del p,i is FinSequence of D
by FINSEQ_3:114;
end;

definition
let D be non empty set ;
let a, b be Element of D;
:: original: <*
redefine func <*a,b*> -> Element of 2 -tuples_on D;
coherence
<*a,b*> is Element of 2 -tuples_on D
by FINSEQ_2:121;
end;

definition
let D be non empty set ;
let k, n be Nat;
let p be Element of k -tuples_on D;
let q be Element of n -tuples_on D;
:: original: ^
redefine func p ^ q -> Element of (k + n) -tuples_on D;
coherence
p ^ q is Element of (k + n) -tuples_on D
by FINSEQ_2:127;
end;

registration
let D be non empty set ;
let n be Nat;
cluster -> FinSequence-yielding FinSequence of n -tuples_on D;
coherence
for b1 being FinSequence of n -tuples_on D holds b1 is FinSequence-yielding
proof end;
end;

definition
let D be non empty set ;
let k, n be Nat;
let p be FinSequence of k -tuples_on D;
let q be FinSequence of n -tuples_on D;
:: original: ^^
redefine func p ^^ q -> Element of ((k + n) -tuples_on D) * ;
coherence
p ^^ q is Element of ((k + n) -tuples_on D) *
proof end;
end;

scheme :: POLYNOM3:sch 1
SeqOfSeqLambdaD{ F1() -> non empty set , F2() -> Nat, F3( Nat) -> Nat, F4( set , set ) -> Element of F1() } :
ex p being FinSequence of F1() * st
( len p = F2() & ( for k being Nat st k in Seg F2() holds
( len (p /. k) = F3(k) & ( for n being Nat st n in dom (p /. k) holds
(p /. k) . n = F4(k,n) ) ) ) )
proof end;

definition
let n be Nat;
let p, q be Element of n -tuples_on NAT ;
pred p < q means :Def1: :: POLYNOM3:def 1
ex i being Nat st
( i in Seg n & p . i < q . i & ( for k being Nat st 1 <= k & k < i holds
p . k = q . k ) );
asymmetry
for p, q being Element of n -tuples_on NAT st ex i being Nat st
( i in Seg n & p . i < q . i & ( for k being Nat st 1 <= k & k < i holds
p . k = q . k ) ) holds
for i being Nat holds
( not i in Seg n or not q . i < p . i or ex k being Nat st
( 1 <= k & k < i & not q . k = p . k ) )
proof end;
end;

:: deftheorem Def1 defines < POLYNOM3:def 1 :
for n being Nat
for p, q being Element of n -tuples_on NAT holds
( p < q iff ex i being Nat st
( i in Seg n & p . i < q . i & ( for k being Nat st 1 <= k & k < i holds
p . k = q . k ) ) );

notation
let n be Nat;
let p, q be Element of n -tuples_on NAT ;
synonym q > p for p < q;
end;

definition
let n be Nat;
let p, q be Element of n -tuples_on NAT ;
pred p <= q means :Def2: :: POLYNOM3:def 2
( p < q or p = q );
reflexivity
for p being Element of n -tuples_on NAT holds
( p < p or p = p )
;
end;

:: deftheorem Def2 defines <= POLYNOM3:def 2 :
for n being Nat
for p, q being Element of n -tuples_on NAT holds
( p <= q iff ( p < q or p = q ) );

notation
let n be Nat;
let p, q be Element of n -tuples_on NAT ;
synonym q >= p for p <= q;
end;

theorem Th5: :: POLYNOM3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for p, q, r being Element of n -tuples_on NAT holds
( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) )
proof end;

theorem Th6: :: POLYNOM3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for p, q being Element of n -tuples_on NAT st p <> q holds
ex i being Nat st
( i in Seg n & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds
p . k = q . k ) )
proof end;

theorem Th7: :: POLYNOM3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for p, q being Element of n -tuples_on NAT holds
( p <= q or p > q )
proof end;

definition
let n be Nat;
func TuplesOrder n -> Order of n -tuples_on NAT means :Def3: :: POLYNOM3:def 3
for p, q being Element of n -tuples_on NAT holds
( [p,q] in it iff p <= q );
existence
ex b1 being Order of n -tuples_on NAT st
for p, q being Element of n -tuples_on NAT holds
( [p,q] in b1 iff p <= q )
proof end;
uniqueness
for b1, b2 being Order of n -tuples_on NAT st ( for p, q being Element of n -tuples_on NAT holds
( [p,q] in b1 iff p <= q ) ) & ( for p, q being Element of n -tuples_on NAT holds
( [p,q] in b2 iff p <= q ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines TuplesOrder POLYNOM3:def 3 :
for n being Nat
for b2 being Order of n -tuples_on NAT holds
( b2 = TuplesOrder n iff for p, q being Element of n -tuples_on NAT holds
( [p,q] in b2 iff p <= q ) );

registration
let n be Nat;
cluster TuplesOrder n -> being_linear-order ;
coherence
TuplesOrder n is being_linear-order
proof end;
end;

definition
let i be non empty Nat;
let n be Nat;
func Decomp n,i -> FinSequence of i -tuples_on NAT means :Def4: :: POLYNOM3:def 4
ex A being finite Subset of (i -tuples_on NAT ) st
( it = SgmX (TuplesOrder i),A & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) );
existence
ex b1 being FinSequence of i -tuples_on NAT ex A being finite Subset of (i -tuples_on NAT ) st
( b1 = SgmX (TuplesOrder i),A & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of i -tuples_on NAT st ex A being finite Subset of (i -tuples_on NAT ) st
( b1 = SgmX (TuplesOrder i),A & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) & ex A being finite Subset of (i -tuples_on NAT ) st
( b2 = SgmX (TuplesOrder i),A & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Decomp POLYNOM3:def 4 :
for i being non empty Nat
for n being Nat
for b3 being FinSequence of i -tuples_on NAT holds
( b3 = Decomp n,i iff ex A being finite Subset of (i -tuples_on NAT ) st
( b3 = SgmX (TuplesOrder i),A & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) );

registration
let i be non empty Nat;
let n be Nat;
cluster Decomp n,i -> non empty one-to-one FinSequence-yielding ;
coherence
( not Decomp n,i is empty & Decomp n,i is one-to-one & Decomp n,i is FinSequence-yielding )
proof end;
end;

theorem Th8: :: POLYNOM3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds len (Decomp n,1) = 1
proof end;

theorem Th9: :: POLYNOM3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds len (Decomp n,2) = n + 1
proof end;

theorem :: POLYNOM3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds Decomp n,1 = <*<*n*>*>
proof end;

theorem Th11: :: POLYNOM3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, n, k1, k2 being Nat st (Decomp n,2) . i = <*k1,(n -' k1)*> & (Decomp n,2) . j = <*k2,(n -' k2)*> holds
( i < j iff k1 < k2 )
proof end;

theorem Th12: :: POLYNOM3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n, k1, k2 being Nat st (Decomp n,2) . i = <*k1,(n -' k1)*> & (Decomp n,2) . (i + 1) = <*k2,(n -' k2)*> holds
k2 = k1 + 1
proof end;

theorem Th13: :: POLYNOM3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds (Decomp n,2) . 1 = <*0,n*>
proof end;

theorem Th14: :: POLYNOM3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat st i in Seg (n + 1) holds
(Decomp n,2) . i = <*(i -' 1),((n + 1) -' i)*>
proof end;

definition
let L be non empty HGrStr ;
let p, q, r be sequence of L;
let t be FinSequence of 3 -tuples_on NAT ;
func prodTuples p,q,r,t -> Element of the carrier of L * means :Def5: :: POLYNOM3:def 5
( len it = len t & ( for k being Nat st k in dom t holds
it . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) );
existence
ex b1 being Element of the carrier of L * st
( len b1 = len t & ( for k being Nat st k in dom t holds
b1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) )
proof end;
uniqueness
for b1, b2 being Element of the carrier of L * st len b1 = len t & ( for k being Nat st k in dom t holds
b1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) & len b2 = len t & ( for k being Nat st k in dom t holds
b2 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines prodTuples POLYNOM3:def 5 :
for L being non empty HGrStr
for p, q, r being sequence of L
for t being FinSequence of 3 -tuples_on NAT
for b6 being Element of the carrier of L * holds
( b6 = prodTuples p,q,r,t iff ( len b6 = len t & ( for k being Nat st k in dom t holds
b6 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) ) );

theorem Th15: :: POLYNOM3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty HGrStr
for p, q, r being sequence of L
for t being FinSequence of 3 -tuples_on NAT
for P being Permutation of dom t
for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds
prodTuples p,q,r,t1 = (prodTuples p,q,r,t) * P
proof end;

theorem Th16: :: POLYNOM3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being set
for f being FinSequence of D *
for i being Nat holds Card (f | i) = (Card f) | i
proof end;

theorem Th17: :: POLYNOM3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence of REAL
for q being FinSequence of NAT st p = q holds
for i being Nat holds p | i = q | i
proof end;

theorem Th18: :: POLYNOM3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence of NAT
for i, j being Nat st i <= j holds
Sum (p | i) <= Sum (p | j)
proof end;

theorem Th19: :: POLYNOM3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being set
for p being FinSequence of D
for i being Nat st i < len p holds
p | (i + 1) = (p | i) ^ <*(p . (i + 1))*>
proof end;

theorem Th20: :: POLYNOM3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence of REAL
for i being Nat st i < len p holds
Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1))
proof end;

theorem Th21: :: POLYNOM3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence of NAT
for i, j, k1, k2 being Nat st i < len p & j < len p & 1 <= k1 & 1 <= k2 & k1 <= p . (i + 1) & k2 <= p . (j + 1) & (Sum (p | i)) + k1 = (Sum (p | j)) + k2 holds
( i = j & k1 = k2 )
proof end;

theorem Th22: :: POLYNOM3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D1, D2 being set
for f1 being FinSequence of D1 *
for f2 being FinSequence of D2 *
for i1, i2, j1, j2 being Nat st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds
( i1 = i2 & j1 = j2 )
proof end;

definition
let L be non empty ZeroStr ;
mode Polynomial of L is AlgSequence of L;
end;

theorem Th23: :: POLYNOM3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ZeroStr
for p being Polynomial of L
for n being Nat holds
( n >= len p iff n is_at_least_length_of p )
proof end;

scheme :: POLYNOM3:sch 2
PolynomialLambdaF{ F1() -> non empty LoopStr , F2() -> Nat, F3( Nat) -> Element of F1() } :
ex p being Polynomial of F1() st
( len p <= F2() & ( for n being Nat st n < F2() holds
p . n = F3(n) ) )
proof end;

definition
let L be non empty LoopStr ;
let p, q be sequence of L;
func p + q -> sequence of L means :Def6: :: POLYNOM3:def 6
for n being Nat holds it . n = (p . n) + (q . n);
existence
ex b1 being sequence of L st
for n being Nat holds b1 . n = (p . n) + (q . n)
proof end;
uniqueness
for b1, b2 being sequence of L st ( for n being Nat holds b1 . n = (p . n) + (q . n) ) & ( for n being Nat holds b2 . n = (p . n) + (q . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines + POLYNOM3:def 6 :
for L being non empty LoopStr
for p, q, b4 being sequence of L holds
( b4 = p + q iff for n being Nat holds b4 . n = (p . n) + (q . n) );

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

theorem Th24: :: POLYNOM3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty right_zeroed LoopStr
for p, q being Polynomial of L
for n being Nat st n is_at_least_length_of p & n is_at_least_length_of q holds
n is_at_least_length_of p + q
proof end;

theorem :: POLYNOM3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty right_zeroed LoopStr
for p, q being Polynomial of L holds support (p + q) c= (support p) \/ (support q)
proof end;

definition
let L be non empty Abelian LoopStr ;
let p, q be sequence of L;
:: original: +
redefine func p + q -> sequence of L;
commutativity
for p, q being sequence of L holds p + q = q + p
proof end;
end;

theorem Th26: :: POLYNOM3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative LoopStr
for p, q, r being sequence of L holds (p + q) + r = p + (q + r)
proof end;

definition
let L be non empty LoopStr ;
let p be sequence of L;
func - p -> sequence of L means :Def7: :: POLYNOM3:def 7
for n being Nat holds it . n = - (p . n);
existence
ex b1 being sequence of L st
for n being Nat holds b1 . n = - (p . n)
proof end;
uniqueness
for b1, b2 being sequence of L st ( for n being Nat holds b1 . n = - (p . n) ) & ( for n being Nat holds b2 . n = - (p . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines - POLYNOM3:def 7 :
for L being non empty LoopStr
for p, b3 being sequence of L holds
( b3 = - p iff for n being Nat holds b3 . n = - (p . n) );

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

definition
let L be non empty LoopStr ;
let p, q be sequence of L;
func p - q -> sequence of L equals :: POLYNOM3:def 8
p + (- q);
coherence
p + (- q) is sequence of L
;
end;

:: deftheorem defines - POLYNOM3:def 8 :
for L being non empty LoopStr
for p, q being sequence of L holds p - q = p + (- q);

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

theorem Th27: :: POLYNOM3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty LoopStr
for p, q being sequence of L
for n being Nat holds (p - q) . n = (p . n) - (q . n)
proof end;

definition
let L be non empty ZeroStr ;
func 0_. L -> sequence of L equals :: POLYNOM3:def 9
NAT --> (0. L);
coherence
NAT --> (0. L) is sequence of L
;
end;

:: deftheorem defines 0_. POLYNOM3:def 9 :
for L being non empty ZeroStr holds 0_. L = NAT --> (0. L);

registration
let L be non empty ZeroStr ;
cluster 0_. L -> finite-Support ;
coherence
0_. L is finite-Support
proof end;
end;

theorem Th28: :: POLYNOM3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ZeroStr
for n being Nat holds (0_. L) . n = 0. L by FUNCOP_1:13;

theorem Th29: :: POLYNOM3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty right_zeroed LoopStr
for p being sequence of L holds p + (0_. L) = p
proof end;

theorem Th30: :: POLYNOM3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable LoopStr
for p being sequence of L holds p - p = 0_. L
proof end;

definition
let L be non empty multLoopStr_0 ;
func 1_. L -> sequence of L equals :: POLYNOM3:def 10
(0_. L) +* 0,(1. L);
coherence
(0_. L) +* 0,(1. L) is sequence of L
;
end;

:: deftheorem defines 1_. POLYNOM3:def 10 :
for L being non empty multLoopStr_0 holds 1_. L = (0_. L) +* 0,(1. L);

registration
let L be non empty multLoopStr_0 ;
cluster 1_. L -> finite-Support ;
coherence
1_. L is finite-Support
proof end;
end;

theorem Th31: :: POLYNOM3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty multLoopStr_0 holds
( (1_. L) . 0 = 1. L & ( for n being Nat st n <> 0 holds
(1_. L) . n = 0. L ) )
proof end;

definition
let L be non empty doubleLoopStr ;
let p, q be sequence of L;
func p *' q -> sequence of L means :Def11: :: POLYNOM3:def 11
for i being Nat ex r being FinSequence of the carrier of L st
( len r = i + 1 & it . i = Sum r & ( for k being Nat st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) );
existence
ex b1 being sequence of L st
for i being Nat ex r being FinSequence of the carrier of L st
( len r = i + 1 & b1 . i = Sum r & ( for k being Nat st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) )
proof end;
uniqueness
for b1, b2 being sequence of L st ( for i being Nat ex r being FinSequence of the carrier of L st
( len r = i + 1 & b1 . i = Sum r & ( for k being Nat st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) & ( for i being Nat ex r being FinSequence of the carrier of L st
( len r = i + 1 & b2 . i = Sum r & ( for k being Nat st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines *' POLYNOM3:def 11 :
for L being non empty doubleLoopStr
for p, q, b4 being sequence of L holds
( b4 = p *' q iff for i being Nat ex r being FinSequence of the carrier of L st
( len r = i + 1 & b4 . i = Sum r & ( for k being Nat st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) );

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

theorem Th32: :: POLYNOM3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Abelian add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for p, q, r being sequence of L holds p *' (q + r) = (p *' q) + (p *' r)
proof end;

theorem Th33: :: POLYNOM3:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Abelian add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for p, q, r being sequence of L holds (p + q) *' r = (p *' r) + (q *' r)
proof end;

theorem Th34: :: POLYNOM3:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Abelian add-associative right_zeroed right_complementable unital associative distributive doubleLoopStr
for p, q, r being sequence of L holds (p *' q) *' r = p *' (q *' r)
proof end;

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

theorem :: POLYNOM3:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for p being sequence of L holds p *' (0_. L) = 0_. L
proof end;

theorem Th36: :: POLYNOM3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable right-distributive right_unital doubleLoopStr
for p being sequence of L holds p *' (1_. L) = p
proof end;

definition
let L be non empty add-associative right_zeroed right_complementable distributive doubleLoopStr ;
func Polynom-Ring L -> non empty strict doubleLoopStr means :Def12: :: POLYNOM3:def 12
( ( for x being set holds
( x in the carrier of it iff x is Polynomial of L ) ) & ( for x, y being Element of it
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of it
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. it = 0_. L & 1_ it = 1_. 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 L ) ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b1 = 0_. L & 1_ b1 = 1_. 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 L ) ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b1 = 0_. L & 1_ b1 = 1_. L & ( for x being set holds
( x in the carrier of b2 iff x is Polynomial of L ) ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b2 = 0_. L & 1_ b2 = 1_. L holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines Polynom-Ring POLYNOM3:def 12 :
for L being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b2 being non empty strict doubleLoopStr holds
( b2 = Polynom-Ring L iff ( ( for x being set holds
( x in the carrier of b2 iff x is Polynomial of L ) ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b2 = 0_. L & 1_ b2 = 1_. L ) );

registration
let L be non empty Abelian add-associative right_zeroed right_complementable distributive doubleLoopStr ;
cluster Polynom-Ring L -> non empty Abelian strict ;
coherence
Polynom-Ring L is Abelian
proof end;
end;

registration
let L be non empty add-associative right_zeroed right_complementable distributive doubleLoopStr ;
cluster Polynom-Ring L -> non empty add-associative strict ;
coherence
Polynom-Ring L is add-associative
proof end;
cluster Polynom-Ring L -> non empty right_zeroed strict ;
coherence
Polynom-Ring L is right_zeroed
proof end;
cluster Polynom-Ring L -> non empty right_complementable strict ;
coherence
Polynom-Ring L is right_complementable
proof end;
end;

registration
let L be non empty Abelian add-associative right_zeroed right_complementable commutative distributive doubleLoopStr ;
cluster Polynom-Ring L -> non empty Abelian add-associative right_zeroed right_complementable commutative strict ;
coherence
Polynom-Ring L is commutative
proof end;
end;

registration
let L be non empty Abelian add-associative right_zeroed right_complementable unital associative distributive doubleLoopStr ;
cluster Polynom-Ring L -> non empty Abelian add-associative right_zeroed right_complementable associative strict ;
coherence
Polynom-Ring L is associative
proof end;
end;

Lm1: now
let L be non empty Abelian add-associative right_zeroed right_complementable commutative right_unital distributive doubleLoopStr ; :: thesis: for x, e being Element of (Polynom-Ring L) st e = 1_ (Polynom-Ring L) holds
( x * e = x & e * x = x )

set Pm = Polynom-Ring L;
let x, e be Element of (Polynom-Ring L); :: thesis: ( e = 1_ (Polynom-Ring L) implies ( x * e = x & e * x = x ) )
assume A1: e = 1_ (Polynom-Ring L) ; :: thesis: ( x * e = x & e * x = x )
reconsider p = x as Polynomial of L by Def12;
A2: 1_ (Polynom-Ring L) = 1_. L by Def12;
hence x * e = p *' (1_. L) by A1, Def12
.= x by Th36 ;
:: thesis: e * x = x
reconsider p1 = x, q1 = e as sequence of L by Def12;
thus e * x = q1 *' p1 by Def12
.= p *' (1_. L) by A2, A1
.= x by Th36 ; :: thesis: verum
end;

registration
let L be non empty Abelian add-associative right_zeroed right_complementable commutative right_unital distributive doubleLoopStr ;
cluster Polynom-Ring L -> non empty Abelian add-associative right_zeroed right_complementable unital commutative strict ;
coherence
Polynom-Ring L is unital
proof end;
end;

registration
let L be non empty Abelian add-associative right_zeroed right_complementable distributive doubleLoopStr ;
cluster Polynom-Ring L -> non empty Abelian add-associative right_zeroed right_complementable strict distributive ;
coherence
Polynom-Ring L is distributive
proof end;
end;

theorem :: POLYNOM3:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Abelian add-associative right_zeroed right_complementable commutative right_unital distributive doubleLoopStr holds 1. (Polynom-Ring L) = 1_. L
proof end;