:: TERMORD semantic presentation
begin
registration
cluster non trivial for addLoopStr ;
existence
not for b1 being addLoopStr holds b1 is trivial
proof
take the Field ; ::_thesis: not the Field is trivial
thus not the Field is trivial ; ::_thesis: verum
end;
end;
registration
cluster non empty non trivial right_complementable add-associative right_zeroed for addLoopStr ;
existence
ex b1 being non trivial addLoopStr st
( b1 is add-associative & b1 is right_complementable & b1 is right_zeroed )
proof
set F = the Field;
take the Field ; ::_thesis: ( the Field is add-associative & the Field is right_complementable & the Field is right_zeroed )
thus ( the Field is add-associative & the Field is right_complementable & the Field is right_zeroed ) ; ::_thesis: verum
end;
end;
definition
let X be set ;
let b be bag of X;
attrb is zero means :: TERMORD:def 1
b = EmptyBag X;
end;
:: deftheorem defines zero TERMORD:def_1_:_
for X being set
for b being bag of X holds
( b is zero iff b = EmptyBag X );
theorem Th1: :: TERMORD:1
for X being set
for b1, b2 being bag of X holds
( b1 divides b2 iff ex b being bag of X st b2 = b1 + b )
proof
let n be set ; ::_thesis: for b1, b2 being bag of n holds
( b1 divides b2 iff ex b being bag of n st b2 = b1 + b )
let b1, b2 be bag of n; ::_thesis: ( b1 divides b2 iff ex b being bag of n st b2 = b1 + b )
now__::_thesis:_(_b1_divides_b2_implies_ex_b_being_bag_of_n_st_b2_=_b1_+_b_)
assume A1: b1 divides b2 ; ::_thesis: ex b being bag of n st b2 = b1 + b
A2: now__::_thesis:_for_k_being_set_holds_0_<=_(b2_._k)_-_(b1_._k)
let k be set ; ::_thesis: 0 <= (b2 . k) - (b1 . k)
b1 . k <= b2 . k by A1, PRE_POLY:def_11;
then (b1 . k) - (b1 . k) <= (b2 . k) - (b1 . k) by XREAL_1:9;
hence 0 <= (b2 . k) - (b1 . k) ; ::_thesis: verum
end;
now__::_thesis:_(_(_n_=_{}_&_ex_b_being_bag_of_n_st_b2_=_b1_+_b_)_or_(_n_<>_{}_&_ex_b,_b_being_bag_of_n_st_b2_=_b1_+_b_)_)
percases ( n = {} or n <> {} ) ;
caseA3: n = {} ; ::_thesis: ex b being bag of n st b2 = b1 + b
then b1 + (EmptyBag n) = EmptyBag n by POLYNOM7:3
.= b2 by A3, POLYNOM7:3 ;
hence ex b being bag of n st b2 = b1 + b ; ::_thesis: verum
end;
case n <> {} ; ::_thesis: ex b, b being bag of n st b2 = b1 + b
then reconsider n9 = n as non empty set ;
set b = { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } ;
A4: now__::_thesis:_for_x_being_set_st_x_in__{__[k,((b2_._k)_-'_(b1_._k))]_where_k_is_Element_of_n9_:_verum__}__holds_
ex_y,_z_being_set_st_x_=_[y,z]
let x be set ; ::_thesis: ( x in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } implies ex y, z being set st x = [y,z] )
assume x in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } ; ::_thesis: ex y, z being set st x = [y,z]
then ex k being Element of n9 st x = [k,((b2 . k) -' (b1 . k))] ;
hence ex y, z being set st x = [y,z] ; ::_thesis: verum
end;
now__::_thesis:_for_x,_y1,_y2_being_set_st_[x,y1]_in__{__[k,((b2_._k)_-'_(b1_._k))]_where_k_is_Element_of_n9_:_verum__}__&_[x,y2]_in__{__[k,((b2_._k)_-'_(b1_._k))]_where_k_is_Element_of_n9_:_verum__}__holds_
y1_=_y2
let x, y1, y2 be set ; ::_thesis: ( [x,y1] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } & [x,y2] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } implies y1 = y2 )
assume that
A5: [x,y1] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } and
A6: [x,y2] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } ; ::_thesis: y1 = y2
consider k being Element of n9 such that
A7: [x,y1] = [k,((b2 . k) -' (b1 . k))] by A5;
consider k9 being Element of n9 such that
A8: [x,y2] = [k9,((b2 . k9) -' (b1 . k9))] by A6;
k = x by A7, XTUPLE_0:1
.= k9 by A8, XTUPLE_0:1 ;
hence y1 = y2 by A7, A8, XTUPLE_0:1; ::_thesis: verum
end;
then reconsider b = { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } as Function by A4, FUNCT_1:def_1, RELAT_1:def_1;
A9: now__::_thesis:_for_x_being_set_st_x_in_dom_b_holds_
x_in_n9
let x be set ; ::_thesis: ( x in dom b implies x in n9 )
assume x in dom b ; ::_thesis: x in n9
then consider y being set such that
A10: [x,y] in b by XTUPLE_0:def_12;
consider k being Element of n9 such that
A11: [x,y] = [k,((b2 . k) -' (b1 . k))] by A10;
x = k by A11, XTUPLE_0:1;
hence x in n9 ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_n9_holds_
x_in_dom_b
let x be set ; ::_thesis: ( x in n9 implies x in dom b )
assume x in n9 ; ::_thesis: x in dom b
then reconsider k = x as Element of n9 ;
[k,((b2 . k) -' (b1 . k))] in b ;
hence x in dom b by XTUPLE_0:def_12; ::_thesis: verum
end;
then A12: dom b = n9 by A9, TARSKI:1;
then reconsider b = b as ManySortedSet of n9 by PARTFUN1:def_2, RELAT_1:def_18;
A13: now__::_thesis:_for_k_being_set_st_k_in_n_holds_
b_._k_=_(b2_._k)_-'_(b1_._k)
let k be set ; ::_thesis: ( k in n implies b . k = (b2 . k) -' (b1 . k) )
assume k in n ; ::_thesis: b . k = (b2 . k) -' (b1 . k)
then consider u being set such that
A14: [k,u] in b by A12, XTUPLE_0:def_12;
consider k9 being Element of n9 such that
A15: [k,u] = [k9,((b2 . k9) -' (b1 . k9))] by A14;
A16: u = (b2 . k9) -' (b1 . k9) by A15, XTUPLE_0:1;
k = k9 by A15, XTUPLE_0:1;
hence b . k = (b2 . k) -' (b1 . k) by A14, A16, FUNCT_1:1; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_support_b_holds_
x_in_support_b2
let x be set ; ::_thesis: ( x in support b implies x in support b2 )
A17: support b c= dom b by PRE_POLY:37;
assume A18: x in support b ; ::_thesis: x in support b2
then A19: b . x <> 0 by PRE_POLY:def_7;
now__::_thesis:_x_in_support_b2
assume not x in support b2 ; ::_thesis: contradiction
then b2 . x = 0 by PRE_POLY:def_7;
then 0 = (b2 . x) -' (b1 . x) by NAT_2:8;
hence contradiction by A12, A13, A18, A19, A17; ::_thesis: verum
end;
hence x in support b2 ; ::_thesis: verum
end;
then A20: support b c= support b2 by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_rng_b_holds_
x_in_NAT
let x be set ; ::_thesis: ( x in rng b implies x in NAT )
assume x in rng b ; ::_thesis: x in NAT
then consider y being set such that
A21: [y,x] in b by XTUPLE_0:def_13;
consider k being Element of n9 such that
A22: [y,x] = [k,((b2 . k) -' (b1 . k))] by A21;
x = (b2 . k) -' (b1 . k) by A22, XTUPLE_0:1;
hence x in NAT ; ::_thesis: verum
end;
then rng b c= NAT by TARSKI:def_3;
then reconsider b = b as bag of n by A20, PRE_POLY:def_8, VALUED_0:def_6;
take b = b; ::_thesis: ex b being bag of n st b2 = b1 + b
now__::_thesis:_for_k_being_set_st_k_in_n_holds_
(b1_._k)_+_(b_._k)_=_b2_._k
let k be set ; ::_thesis: ( k in n implies (b1 . k) + (b . k) = b2 . k )
A23: 0 <= (b2 . k) - (b1 . k) by A2;
assume k in n ; ::_thesis: (b1 . k) + (b . k) = b2 . k
hence (b1 . k) + (b . k) = (b1 . k) + ((b2 . k) -' (b1 . k)) by A13
.= (b1 . k) + ((b2 . k) + (- (b1 . k))) by A23, XREAL_0:def_2
.= b2 . k ;
::_thesis: verum
end;
then b2 = b1 + b by PRE_POLY:33;
hence ex b being bag of n st b2 = b1 + b ; ::_thesis: verum
end;
end;
end;
hence ex b being bag of n st b2 = b1 + b ; ::_thesis: verum
end;
hence ( b1 divides b2 iff ex b being bag of n st b2 = b1 + b ) by PRE_POLY:50; ::_thesis: verum
end;
theorem Th2: :: TERMORD:2
for n being Ordinal
for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds (0_ (n,L)) *' p = 0_ (n,L)
proof
let n be Ordinal; ::_thesis: for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds (0_ (n,L)) *' p = 0_ (n,L)
let L be non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Series of n,L holds (0_ (n,L)) *' p = 0_ (n,L)
let p be Series of n,L; ::_thesis: (0_ (n,L)) *' p = 0_ (n,L)
set Z = 0_ (n,L);
now__::_thesis:_for_b_being_Element_of_Bags_n_holds_((0__(n,L))_*'_p)_._b_=_(0__(n,L))_._b
let b be Element of Bags n; ::_thesis: ((0_ (n,L)) *' p) . b = (0_ (n,L)) . b
consider s being FinSequence of L such that
A1: ((0_ (n,L)) *' p) . b = Sum s and
len s = len (decomp b) and
A2: 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 = ((0_ (n,L)) . b1) * (p . b2) ) by POLYNOM1:def_9;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_s_holds_
s_/._k_=_0._L
let k be Nat; ::_thesis: ( k in dom s implies s /. k = 0. L )
assume k in dom s ; ::_thesis: s /. k = 0. L
then consider b1, b2 being bag of n such that
(decomp b) /. k = <*b1,b2*> and
A3: s /. k = ((0_ (n,L)) . b1) * (p . b2) by A2;
thus s /. k = (0. L) * (p . b2) by A3, POLYNOM1:22
.= 0. L by VECTSP_1:7 ; ::_thesis: verum
end;
then Sum s = 0. L by MATRLIN:11;
hence ((0_ (n,L)) *' p) . b = (0_ (n,L)) . b by A1, POLYNOM1:22; ::_thesis: verum
end;
hence (0_ (n,L)) *' p = 0_ (n,L) by FUNCT_2:63; ::_thesis: verum
end;
registration
let n be Ordinal;
let L be non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;
let m1, m2 be Monomial of n,L;
clusterm1 *' m2 -> monomial-like ;
coherence
m1 *' m2 is monomial-like
proof
percases ( Support (m1 *' m2) = {} or Support (m1 *' m2) <> {} ) ;
suppose Support (m1 *' m2) = {} ; ::_thesis: m1 *' m2 is monomial-like
hence m1 *' m2 is monomial-like by POLYNOM7:6; ::_thesis: verum
end;
supposeA1: Support (m1 *' m2) <> {} ; ::_thesis: m1 *' m2 is monomial-like
now__::_thesis:_(_(_Support_m1_<>_{}_&_Support_m2_<>_{}_&_m1_*'_m2_is_monomial-like_)_or_(_(_Support_m1_=_{}_or_Support_m2_=_{}_)_&_m1_*'_m2_is_monomial-like_)_)
percases ( ( Support m1 <> {} & Support m2 <> {} ) or Support m1 = {} or Support m2 = {} ) ;
caseA2: ( Support m1 <> {} & Support m2 <> {} ) ; ::_thesis: m1 *' m2 is monomial-like
then consider mb2 being bag of n such that
A3: Support m2 = {mb2} by POLYNOM7:6;
mb2 in Support m2 by A3, TARSKI:def_1;
then A4: m2 . mb2 <> 0. L by POLYNOM1:def_3;
A5: now__::_thesis:_for_b_being_bag_of_n_st_b_<>_mb2_holds_
m2_._b_=_0._L
let b be bag of n; ::_thesis: ( b <> mb2 implies m2 . b = 0. L )
assume A6: b <> mb2 ; ::_thesis: m2 . b = 0. L
consider b9 being bag of n such that
A7: for b being bag of n st b <> b9 holds
m2 . b = 0. L by POLYNOM7:def_3;
b9 = mb2 by A4, A7;
hence m2 . b = 0. L by A6, A7; ::_thesis: verum
end;
consider mb1 being bag of n such that
A8: Support m1 = {mb1} by A2, POLYNOM7:6;
mb1 in Support m1 by A8, TARSKI:def_1;
then A9: m1 . mb1 <> 0. L by POLYNOM1:def_3;
A10: now__::_thesis:_for_b_being_bag_of_n_st_b_<>_mb1_holds_
m1_._b_=_0._L
let b be bag of n; ::_thesis: ( b <> mb1 implies m1 . b = 0. L )
assume A11: b <> mb1 ; ::_thesis: m1 . b = 0. L
consider b9 being bag of n such that
A12: for b being bag of n st b <> b9 holds
m1 . b = 0. L by POLYNOM7:def_3;
b9 = mb1 by A9, A12;
hence m1 . b = 0. L by A11, A12; ::_thesis: verum
end;
set b = the Element of Support (m1 *' m2);
A13: the Element of Support (m1 *' m2) in Support (m1 *' m2) by A1;
then the Element of Support (m1 *' m2) is Element of Bags n ;
then reconsider b = the Element of Support (m1 *' m2) as bag of n ;
consider s being FinSequence of L such that
A14: (m1 *' m2) . b = Sum s and
A15: len s = len (decomp b) and
A16: 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 = (m1 . b1) * (m2 . b2) ) by POLYNOM1:def_9;
A17: dom s = Seg (len (decomp b)) by A15, FINSEQ_1:def_3
.= dom (decomp b) by FINSEQ_1:def_3 ;
A18: now__::_thesis:_not_b_<>_mb1_+_mb2
assume A19: b <> mb1 + mb2 ; ::_thesis: contradiction
A20: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_s_holds_
s_/._k_=_0._L
let k be Element of NAT ; ::_thesis: ( k in dom s implies s /. k = 0. L )
assume A21: k in dom s ; ::_thesis: s /. k = 0. L
then consider b1, b2 being bag of n such that
A22: (decomp b) /. k = <*b1,b2*> and
A23: s /. k = (m1 . b1) * (m2 . b2) by A16;
consider b19, b29 being bag of n such that
A24: (decomp b) /. k = <*b19,b29*> and
A25: b = b19 + b29 by A17, A21, PRE_POLY:68;
A26: b2 = <*b19,b29*> . 2 by A22, A24, FINSEQ_1:44
.= b29 by FINSEQ_1:44 ;
A27: b1 = <*b19,b29*> . 1 by A22, A24, FINSEQ_1:44
.= b19 by FINSEQ_1:44 ;
now__::_thesis:_(_(_b1_<>_mb1_&_(m1_._b1)_*_(m2_._b2)_=_0._L_)_or_(_b2_<>_mb2_&_(m1_._b1)_*_(m2_._b2)_=_0._L_)_)
percases ( b1 <> mb1 or b2 <> mb2 ) by A19, A25, A27, A26;
case b1 <> mb1 ; ::_thesis: (m1 . b1) * (m2 . b2) = 0. L
then m1 . b1 = 0. L by A10;
hence (m1 . b1) * (m2 . b2) = 0. L by BINOM:1; ::_thesis: verum
end;
case b2 <> mb2 ; ::_thesis: (m1 . b1) * (m2 . b2) = 0. L
then m2 . b2 = 0. L by A5;
hence (m1 . b1) * (m2 . b2) = 0. L by BINOM:2; ::_thesis: verum
end;
end;
end;
hence s /. k = 0. L by A23; ::_thesis: verum
end;
now__::_thesis:_(_(_dom_s_=_{}_&_(m1_*'_m2)_._b_=_0._L_)_or_(_dom_s_<>_{}_&_(m1_*'_m2)_._b_=_0._L_)_)
percases ( dom s = {} or dom s <> {} ) ;
case dom s = {} ; ::_thesis: (m1 *' m2) . b = 0. L
then s = <*> the carrier of L by RELAT_1:41;
hence (m1 *' m2) . b = 0. L by A15; ::_thesis: verum
end;
caseA28: dom s <> {} ; ::_thesis: (m1 *' m2) . b = 0. L
set k = the Element of dom s;
A29: the Element of dom s in dom s by A28;
for k9 being Element of NAT st k9 in dom s & k9 <> the Element of dom s holds
s /. k9 = 0. L by A20;
then s /. the Element of dom s = (m1 *' m2) . b by A14, A29, POLYNOM2:3;
hence (m1 *' m2) . b = 0. L by A20, A29; ::_thesis: verum
end;
end;
end;
hence contradiction by A13, POLYNOM1:def_3; ::_thesis: verum
end;
now__::_thesis:_for_b9_being_bag_of_n_st_b9_<>_b_holds_
(m1_*'_m2)_._b9_=_0._L
let b9 be bag of n; ::_thesis: ( b9 <> b implies (m1 *' m2) . b9 = 0. L )
assume A30: b9 <> b ; ::_thesis: (m1 *' m2) . b9 = 0. L
consider s being FinSequence of L such that
A31: (m1 *' m2) . b9 = Sum s and
A32: len s = len (decomp b9) and
A33: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b9) /. k = <*b1,b2*> & s /. k = (m1 . b1) * (m2 . b2) ) by POLYNOM1:def_9;
A34: dom s = Seg (len (decomp b9)) by A32, FINSEQ_1:def_3
.= dom (decomp b9) by FINSEQ_1:def_3 ;
A35: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_s_holds_
s_/._k_=_0._L
let k be Element of NAT ; ::_thesis: ( k in dom s implies s /. k = 0. L )
assume A36: k in dom s ; ::_thesis: s /. k = 0. L
then consider b1, b2 being bag of n such that
A37: (decomp b9) /. k = <*b1,b2*> and
A38: s /. k = (m1 . b1) * (m2 . b2) by A33;
consider b19, b29 being bag of n such that
A39: (decomp b9) /. k = <*b19,b29*> and
A40: b9 = b19 + b29 by A34, A36, PRE_POLY:68;
A41: b2 = <*b19,b29*> . 2 by A37, A39, FINSEQ_1:44
.= b29 by FINSEQ_1:44 ;
A42: b1 = <*b19,b29*> . 1 by A37, A39, FINSEQ_1:44
.= b19 by FINSEQ_1:44 ;
now__::_thesis:_(_(_b1_<>_mb1_&_(m1_._b1)_*_(m2_._b2)_=_0._L_)_or_(_b2_<>_mb2_&_(m1_._b1)_*_(m2_._b2)_=_0._L_)_)
percases ( b1 <> mb1 or b2 <> mb2 ) by A18, A30, A40, A42, A41;
case b1 <> mb1 ; ::_thesis: (m1 . b1) * (m2 . b2) = 0. L
then m1 . b1 = 0. L by A10;
hence (m1 . b1) * (m2 . b2) = 0. L by BINOM:1; ::_thesis: verum
end;
case b2 <> mb2 ; ::_thesis: (m1 . b1) * (m2 . b2) = 0. L
then m2 . b2 = 0. L by A5;
hence (m1 . b1) * (m2 . b2) = 0. L by BINOM:2; ::_thesis: verum
end;
end;
end;
hence s /. k = 0. L by A38; ::_thesis: verum
end;
now__::_thesis:_(_(_dom_s_=_{}_&_(m1_*'_m2)_._b9_=_0._L_)_or_(_dom_s_<>_{}_&_(m1_*'_m2)_._b9_=_0._L_)_)
percases ( dom s = {} or dom s <> {} ) ;
case dom s = {} ; ::_thesis: (m1 *' m2) . b9 = 0. L
then s = <*> the carrier of L by RELAT_1:41;
hence (m1 *' m2) . b9 = 0. L by A32; ::_thesis: verum
end;
caseA43: dom s <> {} ; ::_thesis: (m1 *' m2) . b9 = 0. L
set k = the Element of dom s;
A44: the Element of dom s in dom s by A43;
for k9 being Element of NAT st k9 in dom s & k9 <> the Element of dom s holds
s /. k9 = 0. L by A35;
then s /. the Element of dom s = (m1 *' m2) . b9 by A31, A44, POLYNOM2:3;
hence (m1 *' m2) . b9 = 0. L by A35, A44; ::_thesis: verum
end;
end;
end;
hence (m1 *' m2) . b9 = 0. L ; ::_thesis: verum
end;
hence m1 *' m2 is monomial-like by POLYNOM7:def_3; ::_thesis: verum
end;
caseA45: ( Support m1 = {} or Support m2 = {} ) ; ::_thesis: m1 *' m2 is monomial-like
now__::_thesis:_(_(_Support_m1_=_{}_&_m1_*'_m2_is_monomial-like_)_or_(_Support_m2_=_{}_&_m1_*'_m2_is_monomial-like_)_)
percases ( Support m1 = {} or Support m2 = {} ) by A45;
case Support m1 = {} ; ::_thesis: m1 *' m2 is monomial-like
then m1 = 0_ (n,L) by POLYNOM7:1;
hence m1 *' m2 is monomial-like by Th2; ::_thesis: verum
end;
case Support m2 = {} ; ::_thesis: m1 *' m2 is monomial-like
then m2 = 0_ (n,L) by POLYNOM7:1;
hence m1 *' m2 is monomial-like by POLYNOM1:28; ::_thesis: verum
end;
end;
end;
hence m1 *' m2 is monomial-like ; ::_thesis: verum
end;
end;
end;
hence m1 *' m2 is monomial-like ; ::_thesis: verum
end;
end;
end;
end;
registration
let n be Ordinal;
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
let c1, c2 be ConstPoly of n,L;
clusterc1 *' c2 -> Constant ;
coherence
c1 *' c2 is Constant
proof
set p = c1 *' c2;
now__::_thesis:_for_b_being_bag_of_n_st_b_<>_EmptyBag_n_holds_
(c1_*'_c2)_._b_=_0._L
let b be bag of n; ::_thesis: ( b <> EmptyBag n implies (c1 *' c2) . b = 0. L )
assume A1: b <> EmptyBag n ; ::_thesis: (c1 *' c2) . b = 0. L
consider s being FinSequence of L such that
A2: (c1 *' c2) . b = Sum s and
A3: len s = len (decomp b) and
A4: 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 = (c1 . b1) * (c2 . b2) ) by POLYNOM1:def_9;
A5: dom s = Seg (len (decomp b)) by A3, FINSEQ_1:def_3
.= dom (decomp b) by FINSEQ_1:def_3 ;
A6: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_s_holds_
s_/._k_=_0._L
let k be Element of NAT ; ::_thesis: ( k in dom s implies s /. k = 0. L )
assume A7: k in dom s ; ::_thesis: s /. k = 0. L
then consider b1, b2 being bag of n such that
A8: (decomp b) /. k = <*b1,b2*> and
A9: s /. k = (c1 . b1) * (c2 . b2) by A4;
consider b19, b29 being bag of n such that
A10: (decomp b) /. k = <*b19,b29*> and
A11: b = b19 + b29 by A5, A7, PRE_POLY:68;
A12: b2 = <*b19,b29*> . 2 by A8, A10, FINSEQ_1:44
.= b29 by FINSEQ_1:44 ;
b1 = <*b19,b29*> . 1 by A8, A10, FINSEQ_1:44
.= b19 by FINSEQ_1:44 ;
then A13: ( b1 <> EmptyBag n or b2 <> EmptyBag n ) by A1, A11, A12, PRE_POLY:53;
now__::_thesis:_(_(_c1_._b1_=_0._L_&_s_/._k_=_0._L_)_or_(_c2_._b2_=_0._L_&_s_/._k_=_0._L_)_)
percases ( c1 . b1 = 0. L or c2 . b2 = 0. L ) by A13, POLYNOM7:def_7;
case c1 . b1 = 0. L ; ::_thesis: s /. k = 0. L
hence s /. k = 0. L by A9, BINOM:1; ::_thesis: verum
end;
case c2 . b2 = 0. L ; ::_thesis: s /. k = 0. L
hence s /. k = 0. L by A9, BINOM:2; ::_thesis: verum
end;
end;
end;
hence s /. k = 0. L ; ::_thesis: verum
end;
now__::_thesis:_(_(_dom_s_=_{}_&_(c1_*'_c2)_._b_=_0._L_)_or_(_dom_s_<>_{}_&_(c1_*'_c2)_._b_=_0._L_)_)
percases ( dom s = {} or dom s <> {} ) ;
case dom s = {} ; ::_thesis: (c1 *' c2) . b = 0. L
then s = <*> the carrier of L by RELAT_1:41;
hence (c1 *' c2) . b = 0. L by A3; ::_thesis: verum
end;
caseA14: dom s <> {} ; ::_thesis: (c1 *' c2) . b = 0. L
set k = the Element of dom s;
A15: the Element of dom s in dom s by A14;
for k9 being Element of NAT st k9 in dom s & k9 <> the Element of dom s holds
s /. k9 = 0. L by A6;
then Sum s = s /. the Element of dom s by A15, POLYNOM2:3;
hence (c1 *' c2) . b = 0. L by A2, A6, A15; ::_thesis: verum
end;
end;
end;
hence (c1 *' c2) . b = 0. L ; ::_thesis: verum
end;
hence c1 *' c2 is Constant by POLYNOM7:def_7; ::_thesis: verum
end;
end;
theorem Th3: :: TERMORD:3
for n being Ordinal
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for b, b9 being bag of n
for a, a9 being non zero Element of L holds Monom ((a * a9),(b + b9)) = (Monom (a,b)) *' (Monom (a9,b9))
proof
let n be Ordinal; ::_thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for b, b9 being bag of n
for a, a9 being non zero Element of L holds Monom ((a * a9),(b + b9)) = (Monom (a,b)) *' (Monom (a9,b9))
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for b, b9 being bag of n
for a, a9 being non zero Element of L holds Monom ((a * a9),(b + b9)) = (Monom (a,b)) *' (Monom (a9,b9))
let b, b9 be bag of n; ::_thesis: for a, a9 being non zero Element of L holds Monom ((a * a9),(b + b9)) = (Monom (a,b)) *' (Monom (a9,b9))
let a, a9 be non zero Element of L; ::_thesis: Monom ((a * a9),(b + b9)) = (Monom (a,b)) *' (Monom (a9,b9))
set m1 = Monom (a,b);
set m2 = Monom (a9,b9);
set m = Monom ((a * a9),(b + b9));
set m3 = (Monom (a,b)) *' (Monom (a9,b9));
consider s being FinSequence of L such that
A1: ((Monom (a,b)) *' (Monom (a9,b9))) . (b + b9) = Sum s and
A2: len s = len (decomp (b + b9)) and
A3: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp (b + b9)) /. k = <*b1,b2*> & s /. k = ((Monom (a,b)) . b1) * ((Monom (a9,b9)) . b2) ) by POLYNOM1:def_9;
set u = b + b9;
consider k9 being Element of NAT such that
A4: k9 in dom (decomp (b + b9)) and
A5: (decomp (b + b9)) /. k9 = <*b,b9*> by PRE_POLY:69;
A6: dom s = Seg (len (decomp (b + b9))) by A2, FINSEQ_1:def_3
.= dom (decomp (b + b9)) by FINSEQ_1:def_3 ;
then consider b1, b2 being bag of n such that
A7: (decomp (b + b9)) /. k9 = <*b1,b2*> and
A8: s /. k9 = ((Monom (a,b)) . b1) * ((Monom (a9,b9)) . b2) by A3, A4;
A9: b1 = <*b,b9*> . 1 by A5, A7, FINSEQ_1:44
.= b by FINSEQ_1:44 ;
A10: b2 = <*b,b9*> . 2 by A5, A7, FINSEQ_1:44
.= b9 by FINSEQ_1:44 ;
A11: (Monom (a9,b9)) . b9 = (Monom (a9,b9)) . (term (Monom (a9,b9))) by POLYNOM7:10
.= coefficient (Monom (a9,b9)) by POLYNOM7:def_6
.= a9 by POLYNOM7:9 ;
A12: now__::_thesis:_for_u_being_bag_of_n_st_u_<>_b9_holds_
not_(Monom_(a9,b9))_._u_<>_0._L
A13: (Monom (a9,b9)) . b9 <> 0. L by A11;
let u be bag of n; ::_thesis: ( u <> b9 implies not (Monom (a9,b9)) . u <> 0. L )
assume A14: u <> b9 ; ::_thesis: not (Monom (a9,b9)) . u <> 0. L
consider v being bag of n such that
A15: for b9 being bag of n st b9 <> v holds
(Monom (a9,b9)) . b9 = 0. L by POLYNOM7:def_3;
assume (Monom (a9,b9)) . u <> 0. L ; ::_thesis: contradiction
then u = v by A15;
hence contradiction by A14, A15, A13; ::_thesis: verum
end;
a * a9 <> 0. L by VECTSP_2:def_1;
then A16: not a * a9 is zero by STRUCT_0:def_12;
A17: (Monom (a,b)) . b = (Monom (a,b)) . (term (Monom (a,b))) by POLYNOM7:10
.= coefficient (Monom (a,b)) by POLYNOM7:def_6
.= a by POLYNOM7:9 ;
A18: now__::_thesis:_for_u_being_bag_of_n_st_u_<>_b_holds_
not_(Monom_(a,b))_._u_<>_0._L
A19: (Monom (a,b)) . b <> 0. L by A17;
let u be bag of n; ::_thesis: ( u <> b implies not (Monom (a,b)) . u <> 0. L )
assume A20: u <> b ; ::_thesis: not (Monom (a,b)) . u <> 0. L
consider v being bag of n such that
A21: for b9 being bag of n st b9 <> v holds
(Monom (a,b)) . b9 = 0. L by POLYNOM7:def_3;
assume (Monom (a,b)) . u <> 0. L ; ::_thesis: contradiction
then u = v by A21;
hence contradiction by A20, A21, A19; ::_thesis: verum
end;
A22: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_s_&_k_<>_k9_holds_
s_/._k_=_0._L
let k be Element of NAT ; ::_thesis: ( k in dom s & k <> k9 implies s /. k = 0. L )
assume that
A23: k in dom s and
A24: k <> k9 ; ::_thesis: s /. k = 0. L
consider b1, b2 being bag of n such that
A25: (decomp (b + b9)) /. k = <*b1,b2*> and
A26: s /. k = ((Monom (a,b)) . b1) * ((Monom (a9,b9)) . b2) by A3, A23;
A27: now__::_thesis:_(_b1_=_b_implies_not_b2_=_b9_)
assume A28: ( b1 = b & b2 = b9 ) ; ::_thesis: contradiction
(decomp (b + b9)) . k = (decomp (b + b9)) /. k by A6, A23, PARTFUN1:def_6
.= (decomp (b + b9)) . k9 by A4, A5, A25, A28, PARTFUN1:def_6 ;
hence contradiction by A6, A4, A23, A24, FUNCT_1:def_4; ::_thesis: verum
end;
now__::_thesis:_(_(_b1_<>_b_&_((Monom_(a,b))_._b1)_*_((Monom_(a9,b9))_._b2)_=_0._L_)_or_(_b2_<>_b9_&_((Monom_(a,b))_._b1)_*_((Monom_(a9,b9))_._b2)_=_0._L_)_)
percases ( b1 <> b or b2 <> b9 ) by A27;
case b1 <> b ; ::_thesis: ((Monom (a,b)) . b1) * ((Monom (a9,b9)) . b2) = 0. L
then (Monom (a,b)) . b1 = 0. L by A18;
hence ((Monom (a,b)) . b1) * ((Monom (a9,b9)) . b2) = 0. L by BINOM:1; ::_thesis: verum
end;
case b2 <> b9 ; ::_thesis: ((Monom (a,b)) . b1) * ((Monom (a9,b9)) . b2) = 0. L
then (Monom (a9,b9)) . b2 = 0. L by A12;
hence ((Monom (a,b)) . b1) * ((Monom (a9,b9)) . b2) = 0. L by BINOM:2; ::_thesis: verum
end;
end;
end;
hence s /. k = 0. L by A26; ::_thesis: verum
end;
then Sum s = s /. k9 by A6, A4, POLYNOM2:3;
then A29: ((Monom (a,b)) *' (Monom (a9,b9))) . (b + b9) <> 0. L by A17, A11, A1, A8, A9, A10, VECTSP_2:def_1;
then A30: term ((Monom (a,b)) *' (Monom (a9,b9))) = b + b9 by POLYNOM7:def_5
.= term (Monom ((a * a9),(b + b9))) by A16, POLYNOM7:10 ;
A31: coefficient ((Monom (a,b)) *' (Monom (a9,b9))) = ((Monom (a,b)) *' (Monom (a9,b9))) . (term ((Monom (a,b)) *' (Monom (a9,b9)))) by POLYNOM7:def_6
.= ((Monom (a,b)) *' (Monom (a9,b9))) . (b + b9) by A29, POLYNOM7:def_5
.= a * a9 by A17, A11, A1, A6, A4, A8, A9, A10, A22, POLYNOM2:3
.= coefficient (Monom ((a * a9),(b + b9))) by POLYNOM7:9 ;
thus Monom ((a * a9),(b + b9)) = Monom ((coefficient (Monom ((a * a9),(b + b9)))),(term (Monom ((a * a9),(b + b9))))) by POLYNOM7:11
.= (Monom (a,b)) *' (Monom (a9,b9)) by A30, A31, POLYNOM7:11 ; ::_thesis: verum
end;
theorem :: TERMORD:4
for n being Ordinal
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for a, a9 being Element of L holds (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L))
proof
let n be Ordinal; ::_thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for a, a9 being Element of L holds (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L))
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for a, a9 being Element of L holds (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L))
let a, a9 be Element of L; ::_thesis: (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L))
percases ( ( not a is zero & not a9 is zero ) or a is zero or a9 is zero ) ;
supposeA1: ( not a is zero & not a9 is zero ) ; ::_thesis: (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L))
( term ((a * a9) | (n,L)) = EmptyBag n & coefficient ((a * a9) | (n,L)) = a * a9 ) by POLYNOM7:23;
then A2: (a * a9) | (n,L) = Monom ((a * a9),(EmptyBag n)) by POLYNOM7:11;
( term (a9 | (n,L)) = EmptyBag n & coefficient (a9 | (n,L)) = a9 ) by POLYNOM7:23;
then A3: a9 | (n,L) = Monom (a9,(EmptyBag n)) by POLYNOM7:11;
( term (a | (n,L)) = EmptyBag n & coefficient (a | (n,L)) = a ) by POLYNOM7:23;
then A4: a | (n,L) = Monom (a,(EmptyBag n)) by POLYNOM7:11;
(EmptyBag n) + (EmptyBag n) = EmptyBag n by PRE_POLY:53;
hence (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) by A1, A2, A4, A3, Th3; ::_thesis: verum
end;
supposeA5: ( a is zero or a9 is zero ) ; ::_thesis: (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L))
now__::_thesis:_(_(_a_=_0._L_&_(a_*_a9)_|_(n,L)_=_(a_|_(n,L))_*'_(a9_|_(n,L))_)_or_(_a9_=_0._L_&_(a_*_a9)_|_(n,L)_=_(a_|_(n,L))_*'_(a9_|_(n,L))_)_)
percases ( a = 0. L or a9 = 0. L ) by A5, STRUCT_0:def_12;
caseA6: a = 0. L ; ::_thesis: (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L))
then a * a9 = 0. L by BINOM:1;
then A7: (a * a9) | (n,L) = 0_ (n,L) by POLYNOM7:19;
a | (n,L) = 0_ (n,L) by A6, POLYNOM7:19;
hence (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) by A7, Th2; ::_thesis: verum
end;
caseA8: a9 = 0. L ; ::_thesis: (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L))
then a * a9 = 0. L by BINOM:2;
then A9: (a * a9) | (n,L) = 0_ (n,L) by POLYNOM7:19;
a9 | (n,L) = 0_ (n,L) by A8, POLYNOM7:19;
hence (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) by A9, POLYNOM1:28; ::_thesis: verum
end;
end;
end;
hence (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) ; ::_thesis: verum
end;
end;
end;
begin
Lm1: for n being Ordinal
for T being TermOrder of n
for b being set st b in field T holds
b is bag of n
proof
let n be Ordinal; ::_thesis: for T being TermOrder of n
for b being set st b in field T holds
b is bag of n
let T be TermOrder of n; ::_thesis: for b being set st b in field T holds
b is bag of n
let b be set ; ::_thesis: ( b in field T implies b is bag of n )
assume b in field T ; ::_thesis: b is bag of n
then A1: b in (dom T) \/ (rng T) by RELAT_1:def_6;
percases ( b in dom T or b in rng T ) by A1, XBOOLE_0:def_3;
suppose b in dom T ; ::_thesis: b is bag of n
then b is Element of Bags n ;
hence b is bag of n ; ::_thesis: verum
end;
suppose b in rng T ; ::_thesis: b is bag of n
then b is Element of Bags n ;
hence b is bag of n ; ::_thesis: verum
end;
end;
end;
registration
let n be Ordinal;
cluster Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric connected transitive admissible for Element of K19(K20((Bags n),(Bags n)));
existence
ex b1 being TermOrder of n st
( b1 is admissible & b1 is connected )
proof
set T = LexOrder n;
take LexOrder n ; ::_thesis: ( LexOrder n is admissible & LexOrder n is connected )
now__::_thesis:_for_x,_y_being_set_st_x_in_field_(LexOrder_n)_&_y_in_field_(LexOrder_n)_&_x_<>_y_&_not_[x,y]_in_LexOrder_n_holds_
[y,x]_in_LexOrder_n
let x, y be set ; ::_thesis: ( x in field (LexOrder n) & y in field (LexOrder n) & x <> y & not [x,y] in LexOrder n implies [y,x] in LexOrder n )
assume that
A1: ( x in field (LexOrder n) & y in field (LexOrder n) ) and
x <> y ; ::_thesis: ( [x,y] in LexOrder n or [y,x] in LexOrder n )
reconsider b1 = x, b2 = y as bag of n by A1, Lm1;
( b1 <=' b2 or b2 <=' b1 ) by PRE_POLY:45;
hence ( [x,y] in LexOrder n or [y,x] in LexOrder n ) by PRE_POLY:def_14; ::_thesis: verum
end;
then LexOrder n is_connected_in field (LexOrder n) by RELAT_2:def_6;
hence ( LexOrder n is admissible & LexOrder n is connected ) by RELAT_2:def_14; ::_thesis: verum
end;
end;
registration
let n be Nat;
cluster total reflexive antisymmetric transitive admissible -> well_founded admissible for Element of K19(K20((Bags n),(Bags n)));
coherence
for b1 being admissible TermOrder of n holds b1 is well_founded
proof
let T be admissible TermOrder of n; ::_thesis: T is well_founded
T is well-ordering by BAGORDER:34;
hence T is well_founded by WELLORD1:def_4; ::_thesis: verum
end;
end;
definition
let n be Ordinal;
let T be TermOrder of n;
let b, b9 be bag of n;
predb <= b9,T means :Def2: :: TERMORD:def 2
[b,b9] in T;
end;
:: deftheorem Def2 defines <= TERMORD:def_2_:_
for n being Ordinal
for T being TermOrder of n
for b, b9 being bag of n holds
( b <= b9,T iff [b,b9] in T );
definition
let n be Ordinal;
let T be TermOrder of n;
let b, b9 be bag of n;
predb < b9,T means :Def3: :: TERMORD:def 3
( b <= b9,T & b <> b9 );
end;
:: deftheorem Def3 defines < TERMORD:def_3_:_
for n being Ordinal
for T being TermOrder of n
for b, b9 being bag of n holds
( b < b9,T iff ( b <= b9,T & b <> b9 ) );
definition
let n be Ordinal;
let T be TermOrder of n;
let b1, b2 be bag of n;
func min (b1,b2,T) -> bag of n equals :Def4: :: TERMORD:def 4
b1 if b1 <= b2,T
otherwise b2;
correctness
coherence
( ( b1 <= b2,T implies b1 is bag of n ) & ( not b1 <= b2,T implies b2 is bag of n ) );
consistency
for b1 being bag of n holds verum;
;
func max (b1,b2,T) -> bag of n equals :Def5: :: TERMORD:def 5
b1 if b2 <= b1,T
otherwise b2;
correctness
coherence
( ( b2 <= b1,T implies b1 is bag of n ) & ( not b2 <= b1,T implies b2 is bag of n ) );
consistency
for b1 being bag of n holds verum;
;
end;
:: deftheorem Def4 defines min TERMORD:def_4_:_
for n being Ordinal
for T being TermOrder of n
for b1, b2 being bag of n holds
( ( b1 <= b2,T implies min (b1,b2,T) = b1 ) & ( not b1 <= b2,T implies min (b1,b2,T) = b2 ) );
:: deftheorem Def5 defines max TERMORD:def_5_:_
for n being Ordinal
for T being TermOrder of n
for b1, b2 being bag of n holds
( ( b2 <= b1,T implies max (b1,b2,T) = b1 ) & ( not b2 <= b1,T implies max (b1,b2,T) = b2 ) );
Lm2: for n being Ordinal
for T being TermOrder of n
for b being bag of n holds b <= b,T
proof
let n be Ordinal; ::_thesis: for T being TermOrder of n
for b being bag of n holds b <= b,T
let T be TermOrder of n; ::_thesis: for b being bag of n holds b <= b,T
let b be bag of n; ::_thesis: b <= b,T
field T = Bags n by ORDERS_1:12;
then A1: T is_reflexive_in Bags n by RELAT_2:def_9;
b is Element of Bags n by PRE_POLY:def_12;
then [b,b] in T by A1, RELAT_2:def_1;
hence b <= b,T by Def2; ::_thesis: verum
end;
Lm3: for n being Ordinal
for T being TermOrder of n
for b1, b2 being bag of n st b1 <= b2,T & b2 <= b1,T holds
b1 = b2
proof
let n be Ordinal; ::_thesis: for T being TermOrder of n
for b1, b2 being bag of n st b1 <= b2,T & b2 <= b1,T holds
b1 = b2
let T be TermOrder of n; ::_thesis: for b1, b2 being bag of n st b1 <= b2,T & b2 <= b1,T holds
b1 = b2
let b1, b2 be bag of n; ::_thesis: ( b1 <= b2,T & b2 <= b1,T implies b1 = b2 )
field T = Bags n by ORDERS_1:12;
then A1: T is_antisymmetric_in Bags n by RELAT_2:def_12;
assume ( b1 <= b2,T & b2 <= b1,T ) ; ::_thesis: b1 = b2
then A2: ( [b1,b2] in T & [b2,b1] in T ) by Def2;
( b1 is Element of Bags n & b2 is Element of Bags n ) by PRE_POLY:def_12;
hence b1 = b2 by A2, A1, RELAT_2:def_4; ::_thesis: verum
end;
Lm4: for n being Ordinal
for T being TermOrder of n
for b being bag of n holds b in field T
proof
let n be Ordinal; ::_thesis: for T being TermOrder of n
for b being bag of n holds b in field T
let T be TermOrder of n; ::_thesis: for b being bag of n holds b in field T
let b be bag of n; ::_thesis: b in field T
field T = Bags n by ORDERS_1:12;
then A1: T is_reflexive_in Bags n by RELAT_2:def_9;
b is Element of Bags n by PRE_POLY:def_12;
then [b,b] in T by A1, RELAT_2:def_1;
hence b in field T by RELAT_1:15; ::_thesis: verum
end;
theorem Th5: :: TERMORD:5
for n being Ordinal
for T being connected TermOrder of n
for b1, b2 being bag of n holds
( b1 <= b2,T iff not b2 < b1,T )
proof
let n be Ordinal; ::_thesis: for T being connected TermOrder of n
for b1, b2 being bag of n holds
( b1 <= b2,T iff not b2 < b1,T )
let T be connected TermOrder of n; ::_thesis: for b1, b2 being bag of n holds
( b1 <= b2,T iff not b2 < b1,T )
let b1, b2 be bag of n; ::_thesis: ( b1 <= b2,T iff not b2 < b1,T )
A1: T is_connected_in field T by RELAT_2:def_14;
percases ( b1 = b2 or b1 <> b2 ) ;
suppose b1 = b2 ; ::_thesis: ( b1 <= b2,T iff not b2 < b1,T )
hence ( b1 <= b2,T iff not b2 < b1,T ) by Def3, Lm2; ::_thesis: verum
end;
supposeA2: b1 <> b2 ; ::_thesis: ( b1 <= b2,T iff not b2 < b1,T )
A3: ( not b2 < b1,T implies b1 <= b2,T )
proof
assume A4: not b2 < b1,T ; ::_thesis: b1 <= b2,T
now__::_thesis:_(_(_not_b2_<=_b1,T_&_b1_<=_b2,T_)_or_(_b1_=_b2_&_b1_<=_b2,T_)_)
percases ( not b2 <= b1,T or b1 = b2 ) by A4, Def3;
caseA5: not b2 <= b1,T ; ::_thesis: b1 <= b2,T
A6: ( b1 in field T & b2 in field T ) by Lm4;
not [b2,b1] in T by A5, Def2;
then [b1,b2] in T by A1, A2, A6, RELAT_2:def_6;
hence b1 <= b2,T by Def2; ::_thesis: verum
end;
case b1 = b2 ; ::_thesis: b1 <= b2,T
hence b1 <= b2,T by A2; ::_thesis: verum
end;
end;
end;
hence b1 <= b2,T ; ::_thesis: verum
end;
( b1 <= b2,T implies not b2 < b1,T )
proof
assume A7: b1 <= b2,T ; ::_thesis: not b2 < b1,T
assume b2 < b1,T ; ::_thesis: contradiction
then ( b2 <= b1,T & b1 <> b2 ) by Def3;
hence contradiction by A7, Lm3; ::_thesis: verum
end;
hence ( b1 <= b2,T iff not b2 < b1,T ) by A3; ::_thesis: verum
end;
end;
end;
Lm5: for n being Ordinal
for T being connected TermOrder of n
for b1, b2 being bag of n holds
( b1 <= b2,T or b2 <= b1,T )
proof
let n be Ordinal; ::_thesis: for T being connected TermOrder of n
for b1, b2 being bag of n holds
( b1 <= b2,T or b2 <= b1,T )
let T be connected TermOrder of n; ::_thesis: for b1, b2 being bag of n holds
( b1 <= b2,T or b2 <= b1,T )
let b1, b2 be bag of n; ::_thesis: ( b1 <= b2,T or b2 <= b1,T )
A1: T is_connected_in field T by RELAT_2:def_14;
percases ( b1 = b2 or b1 <> b2 ) ;
supposeA2: b1 = b2 ; ::_thesis: ( b1 <= b2,T or b2 <= b1,T )
field T = Bags n by ORDERS_1:12;
then A3: T is_reflexive_in Bags n by RELAT_2:def_9;
b1 is Element of Bags n by PRE_POLY:def_12;
then [b1,b2] in T by A2, A3, RELAT_2:def_1;
hence ( b1 <= b2,T or b2 <= b1,T ) by Def2; ::_thesis: verum
end;
supposeA4: b1 <> b2 ; ::_thesis: ( b1 <= b2,T or b2 <= b1,T )
assume not b1 <= b2,T ; ::_thesis: b2 <= b1,T
then A5: not [b1,b2] in T by Def2;
( b1 in field T & b2 in field T ) by Lm4;
then [b2,b1] in T by A1, A4, A5, RELAT_2:def_6;
hence b2 <= b1,T by Def2; ::_thesis: verum
end;
end;
end;
theorem :: TERMORD:6
for n being Ordinal
for T being TermOrder of n
for b being bag of n holds b <= b,T by Lm2;
theorem :: TERMORD:7
for n being Ordinal
for T being TermOrder of n
for b1, b2 being bag of n st b1 <= b2,T & b2 <= b1,T holds
b1 = b2 by Lm3;
theorem Th8: :: TERMORD:8
for n being Ordinal
for T being TermOrder of n
for b1, b2, b3 being bag of n st b1 <= b2,T & b2 <= b3,T holds
b1 <= b3,T
proof
let n be Ordinal; ::_thesis: for T being TermOrder of n
for b1, b2, b3 being bag of n st b1 <= b2,T & b2 <= b3,T holds
b1 <= b3,T
let T be TermOrder of n; ::_thesis: for b1, b2, b3 being bag of n st b1 <= b2,T & b2 <= b3,T holds
b1 <= b3,T
let b1, b2, b3 be bag of n; ::_thesis: ( b1 <= b2,T & b2 <= b3,T implies b1 <= b3,T )
A1: b3 is Element of Bags n by PRE_POLY:def_12;
field T = Bags n by ORDERS_1:12;
then A2: T is_transitive_in Bags n by RELAT_2:def_16;
assume ( b1 <= b2,T & b2 <= b3,T ) ; ::_thesis: b1 <= b3,T
then A3: ( [b1,b2] in T & [b2,b3] in T ) by Def2;
( b1 is Element of Bags n & b2 is Element of Bags n ) by PRE_POLY:def_12;
then [b1,b3] in T by A3, A2, A1, RELAT_2:def_8;
hence b1 <= b3,T by Def2; ::_thesis: verum
end;
theorem Th9: :: TERMORD:9
for n being Ordinal
for T being admissible TermOrder of n
for b being bag of n holds EmptyBag n <= b,T
proof
let n be Ordinal; ::_thesis: for T being admissible TermOrder of n
for b being bag of n holds EmptyBag n <= b,T
let T be admissible TermOrder of n; ::_thesis: for b being bag of n holds EmptyBag n <= b,T
let b be bag of n; ::_thesis: EmptyBag n <= b,T
[(EmptyBag n),b] in T by BAGORDER:def_5;
hence EmptyBag n <= b,T by Def2; ::_thesis: verum
end;
theorem :: TERMORD:10
for n being Ordinal
for T being admissible TermOrder of n
for b1, b2 being bag of n st b1 divides b2 holds
b1 <= b2,T
proof
let n be Ordinal; ::_thesis: for T being admissible TermOrder of n
for b1, b2 being bag of n st b1 divides b2 holds
b1 <= b2,T
let T be admissible TermOrder of n; ::_thesis: for b1, b2 being bag of n st b1 divides b2 holds
b1 <= b2,T
let b1, b2 be bag of n; ::_thesis: ( b1 divides b2 implies b1 <= b2,T )
assume b1 divides b2 ; ::_thesis: b1 <= b2,T
then consider b3 being bag of n such that
A1: b2 = b1 + b3 by Th1;
EmptyBag n <= b3,T by Th9;
then [(EmptyBag n),b3] in T by Def2;
then [((EmptyBag n) + b1),b2] in T by A1, BAGORDER:def_5;
then [b1,b2] in T by PRE_POLY:53;
hence b1 <= b2,T by Def2; ::_thesis: verum
end;
theorem Th11: :: TERMORD:11
for n being Ordinal
for T being TermOrder of n
for b1, b2 being bag of n holds
( min (b1,b2,T) = b1 or min (b1,b2,T) = b2 )
proof
let n be Ordinal; ::_thesis: for T being TermOrder of n
for b1, b2 being bag of n holds
( min (b1,b2,T) = b1 or min (b1,b2,T) = b2 )
let T be TermOrder of n; ::_thesis: for b1, b2 being bag of n holds
( min (b1,b2,T) = b1 or min (b1,b2,T) = b2 )
let b1, b2 be bag of n; ::_thesis: ( min (b1,b2,T) = b1 or min (b1,b2,T) = b2 )
assume A1: min (b1,b2,T) <> b1 ; ::_thesis: min (b1,b2,T) = b2
now__::_thesis:_(_(_not_b1_<=_b2,T_&_min_(b1,b2,T)_=_b2_)_or_(_b1_=_b2_&_contradiction_)_)
percases ( not b1 <= b2,T or b1 = b2 ) by A1, Def4;
case not b1 <= b2,T ; ::_thesis: min (b1,b2,T) = b2
hence min (b1,b2,T) = b2 by Def4; ::_thesis: verum
end;
case b1 = b2 ; ::_thesis: contradiction
then b1 <= b2,T by Lm2;
hence contradiction by A1, Def4; ::_thesis: verum
end;
end;
end;
hence min (b1,b2,T) = b2 ; ::_thesis: verum
end;
theorem Th12: :: TERMORD:12
for n being Ordinal
for T being TermOrder of n
for b1, b2 being bag of n holds
( max (b1,b2,T) = b1 or max (b1,b2,T) = b2 )
proof
let n be Ordinal; ::_thesis: for T being TermOrder of n
for b1, b2 being bag of n holds
( max (b1,b2,T) = b1 or max (b1,b2,T) = b2 )
let T be TermOrder of n; ::_thesis: for b1, b2 being bag of n holds
( max (b1,b2,T) = b1 or max (b1,b2,T) = b2 )
let b1, b2 be bag of n; ::_thesis: ( max (b1,b2,T) = b1 or max (b1,b2,T) = b2 )
assume A1: max (b1,b2,T) <> b1 ; ::_thesis: max (b1,b2,T) = b2
now__::_thesis:_(_(_not_b2_<=_b1,T_&_max_(b1,b2,T)_=_b2_)_or_(_b1_=_b2_&_contradiction_)_)
percases ( not b2 <= b1,T or b1 = b2 ) by A1, Def5;
case not b2 <= b1,T ; ::_thesis: max (b1,b2,T) = b2
hence max (b1,b2,T) = b2 by Def5; ::_thesis: verum
end;
case b1 = b2 ; ::_thesis: contradiction
then b2 <= b1,T by Lm2;
hence contradiction by A1, Def5; ::_thesis: verum
end;
end;
end;
hence max (b1,b2,T) = b2 ; ::_thesis: verum
end;
Lm6: for n being Ordinal
for T being TermOrder of n
for b being bag of n holds
( min (b,b,T) = b & max (b,b,T) = b )
proof
let n be Ordinal; ::_thesis: for T being TermOrder of n
for b being bag of n holds
( min (b,b,T) = b & max (b,b,T) = b )
let T be TermOrder of n; ::_thesis: for b being bag of n holds
( min (b,b,T) = b & max (b,b,T) = b )
let b be bag of n; ::_thesis: ( min (b,b,T) = b & max (b,b,T) = b )
thus min (b,b,T) = b by Def4; ::_thesis: max (b,b,T) = b
thus max (b,b,T) = b by Def5; ::_thesis: verum
end;
theorem :: TERMORD:13
for n being Ordinal
for T being connected TermOrder of n
for b1, b2 being bag of n holds
( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T )
proof
let n be Ordinal; ::_thesis: for T being connected TermOrder of n
for b1, b2 being bag of n holds
( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T )
let T be connected TermOrder of n; ::_thesis: for b1, b2 being bag of n holds
( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T )
let b1, b2 be bag of n; ::_thesis: ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T )
percases ( b1 <= b2,T or b2 <= b1,T ) by Lm5;
supposeA1: b1 <= b2,T ; ::_thesis: ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T )
then min (b1,b2,T) = b1 by Def4;
hence ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T ) by A1, Lm2; ::_thesis: verum
end;
supposeA2: b2 <= b1,T ; ::_thesis: ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T )
now__::_thesis:_(_(_b1_=_b2_&_min_(b1,b2,T)_<=_b1,T_&_min_(b1,b2,T)_<=_b2,T_)_or_(_b1_<>_b2_&_min_(b1,b2,T)_<=_b1,T_&_min_(b1,b2,T)_<=_b2,T_)_)
percases ( b1 = b2 or b1 <> b2 ) ;
caseA3: b1 = b2 ; ::_thesis: ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T )
then min (b1,b2,T) = b1 by Lm6;
hence ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T ) by A3, Lm2; ::_thesis: verum
end;
case b1 <> b2 ; ::_thesis: ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T )
then b2 < b1,T by A2, Def3;
then not b1 <= b2,T by Th5;
then min (b1,b2,T) = b2 by Def4;
hence ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T ) by A2, Lm2; ::_thesis: verum
end;
end;
end;
hence ( min (b1,b2,T) <= b1,T & min (b1,b2,T) <= b2,T ) ; ::_thesis: verum
end;
end;
end;
theorem Th14: :: TERMORD:14
for n being Ordinal
for T being connected TermOrder of n
for b1, b2 being bag of n holds
( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T )
proof
let n be Ordinal; ::_thesis: for T being connected TermOrder of n
for b1, b2 being bag of n holds
( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T )
let T be connected TermOrder of n; ::_thesis: for b1, b2 being bag of n holds
( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T )
let b1, b2 be bag of n; ::_thesis: ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T )
percases ( b2 <= b1,T or b1 <= b2,T ) by Lm5;
supposeA1: b2 <= b1,T ; ::_thesis: ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T )
then max (b1,b2,T) = b1 by Def5;
hence ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) by A1, Lm2; ::_thesis: verum
end;
supposeA2: b1 <= b2,T ; ::_thesis: ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T )
now__::_thesis:_(_(_b1_=_b2_&_b1_<=_max_(b1,b2,T),T_&_b2_<=_max_(b1,b2,T),T_)_or_(_b1_<>_b2_&_b1_<=_max_(b1,b2,T),T_&_b2_<=_max_(b1,b2,T),T_)_)
percases ( b1 = b2 or b1 <> b2 ) ;
caseA3: b1 = b2 ; ::_thesis: ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T )
then max (b1,b2,T) = b1 by Lm6;
hence ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) by A3, Lm2; ::_thesis: verum
end;
case b1 <> b2 ; ::_thesis: ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T )
then b1 < b2,T by A2, Def3;
then not b2 <= b1,T by Th5;
then max (b1,b2,T) = b2 by Def5;
hence ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) by A2, Lm2; ::_thesis: verum
end;
end;
end;
hence ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) ; ::_thesis: verum
end;
end;
end;
theorem Th15: :: TERMORD:15
for n being Ordinal
for T being connected TermOrder of n
for b1, b2 being bag of n holds
( min (b1,b2,T) = min (b2,b1,T) & max (b1,b2,T) = max (b2,b1,T) )
proof
let n be Ordinal; ::_thesis: for T being connected TermOrder of n
for b1, b2 being bag of n holds
( min (b1,b2,T) = min (b2,b1,T) & max (b1,b2,T) = max (b2,b1,T) )
let T be connected TermOrder of n; ::_thesis: for b1, b2 being bag of n holds
( min (b1,b2,T) = min (b2,b1,T) & max (b1,b2,T) = max (b2,b1,T) )
let b1, b2 be bag of n; ::_thesis: ( min (b1,b2,T) = min (b2,b1,T) & max (b1,b2,T) = max (b2,b1,T) )
now__::_thesis:_(_(_min_(b1,b2,T)_=_b1_&_min_(b1,b2,T)_=_min_(b2,b1,T)_)_or_(_min_(b1,b2,T)_<>_b1_&_min_(b1,b2,T)_=_min_(b2,b1,T)_)_)
percases ( min (b1,b2,T) = b1 or min (b1,b2,T) <> b1 ) ;
caseA1: min (b1,b2,T) = b1 ; ::_thesis: min (b1,b2,T) = min (b2,b1,T)
now__::_thesis:_(_(_b1_<=_b2,T_&_min_(b1,b2,T)_=_min_(b2,b1,T)_)_or_(_b1_=_b2_&_min_(b2,b1,T)_=_min_(b1,b2,T)_)_)
percases ( b1 <= b2,T or b1 = b2 ) by A1, Def4;
caseA2: b1 <= b2,T ; ::_thesis: min (b1,b2,T) = min (b2,b1,T)
now__::_thesis:_(_(_b1_=_b2_&_min_(b2,b1,T)_=_min_(b1,b2,T)_)_or_(_b1_<>_b2_&_min_(b2,b1,T)_=_min_(b1,b2,T)_)_)
percases ( b1 = b2 or b1 <> b2 ) ;
case b1 = b2 ; ::_thesis: min (b2,b1,T) = min (b1,b2,T)
hence min (b2,b1,T) = min (b1,b2,T) ; ::_thesis: verum
end;
case b1 <> b2 ; ::_thesis: min (b2,b1,T) = min (b1,b2,T)
then not b2 <= b1,T by A2, Lm3;
hence min (b2,b1,T) = min (b1,b2,T) by A1, Def4; ::_thesis: verum
end;
end;
end;
hence min (b1,b2,T) = min (b2,b1,T) ; ::_thesis: verum
end;
case b1 = b2 ; ::_thesis: min (b2,b1,T) = min (b1,b2,T)
hence min (b2,b1,T) = min (b1,b2,T) ; ::_thesis: verum
end;
end;
end;
hence min (b1,b2,T) = min (b2,b1,T) ; ::_thesis: verum
end;
caseA3: min (b1,b2,T) <> b1 ; ::_thesis: min (b1,b2,T) = min (b2,b1,T)
A4: now__::_thesis:_b2_<=_b1,T
assume not b2 <= b1,T ; ::_thesis: contradiction
then b1 <= b2,T by Lm5;
hence contradiction by A3, Def4; ::_thesis: verum
end;
thus min (b1,b2,T) = b2 by A3, Th11
.= min (b2,b1,T) by A4, Def4 ; ::_thesis: verum
end;
end;
end;
hence min (b1,b2,T) = min (b2,b1,T) ; ::_thesis: max (b1,b2,T) = max (b2,b1,T)
now__::_thesis:_(_(_max_(b1,b2,T)_=_b1_&_max_(b1,b2,T)_=_max_(b2,b1,T)_)_or_(_max_(b1,b2,T)_<>_b1_&_max_(b2,b1,T)_=_max_(b1,b2,T)_)_)
percases ( max (b1,b2,T) = b1 or max (b1,b2,T) <> b1 ) ;
caseA5: max (b1,b2,T) = b1 ; ::_thesis: max (b1,b2,T) = max (b2,b1,T)
now__::_thesis:_(_(_b2_<=_b1,T_&_max_(b1,b2,T)_=_max_(b2,b1,T)_)_or_(_b1_=_b2_&_max_(b2,b1,T)_=_max_(b1,b2,T)_)_)
percases ( b2 <= b1,T or b1 = b2 ) by A5, Def5;
caseA6: b2 <= b1,T ; ::_thesis: max (b1,b2,T) = max (b2,b1,T)
now__::_thesis:_(_(_b1_=_b2_&_max_(b2,b1,T)_=_max_(b1,b2,T)_)_or_(_b1_<>_b2_&_max_(b2,b1,T)_=_max_(b1,b2,T)_)_)
percases ( b1 = b2 or b1 <> b2 ) ;
case b1 = b2 ; ::_thesis: max (b2,b1,T) = max (b1,b2,T)
hence max (b2,b1,T) = max (b1,b2,T) ; ::_thesis: verum
end;
case b1 <> b2 ; ::_thesis: max (b2,b1,T) = max (b1,b2,T)
then not b1 <= b2,T by A6, Lm3;
hence max (b2,b1,T) = max (b1,b2,T) by A5, Def5; ::_thesis: verum
end;
end;
end;
hence max (b1,b2,T) = max (b2,b1,T) ; ::_thesis: verum
end;
case b1 = b2 ; ::_thesis: max (b2,b1,T) = max (b1,b2,T)
hence max (b2,b1,T) = max (b1,b2,T) ; ::_thesis: verum
end;
end;
end;
hence max (b1,b2,T) = max (b2,b1,T) ; ::_thesis: verum
end;
caseA7: max (b1,b2,T) <> b1 ; ::_thesis: max (b2,b1,T) = max (b1,b2,T)
now__::_thesis:_(_(_b1_<=_b2,T_&_max_(b2,b1,T)_=_max_(b1,b2,T)_)_or_(_b2_<=_b1,T_&_max_(b2,b1,T)_=_max_(b1,b2,T)_)_)
percases ( b1 <= b2,T or b2 <= b1,T ) by Lm5;
case b1 <= b2,T ; ::_thesis: max (b2,b1,T) = max (b1,b2,T)
hence max (b2,b1,T) = b2 by Def5
.= max (b1,b2,T) by A7, Th12 ;
::_thesis: verum
end;
case b2 <= b1,T ; ::_thesis: max (b2,b1,T) = max (b1,b2,T)
hence max (b2,b1,T) = max (b1,b2,T) by A7, Def5; ::_thesis: verum
end;
end;
end;
hence max (b2,b1,T) = max (b1,b2,T) ; ::_thesis: verum
end;
end;
end;
hence max (b1,b2,T) = max (b2,b1,T) ; ::_thesis: verum
end;
theorem :: TERMORD:16
for n being Ordinal
for T being connected TermOrder of n
for b1, b2 being bag of n holds
( min (b1,b2,T) = b1 iff max (b1,b2,T) = b2 )
proof
let n be Ordinal; ::_thesis: for T being connected TermOrder of n
for b1, b2 being bag of n holds
( min (b1,b2,T) = b1 iff max (b1,b2,T) = b2 )
let T be connected TermOrder of n; ::_thesis: for b1, b2 being bag of n holds
( min (b1,b2,T) = b1 iff max (b1,b2,T) = b2 )
let b1, b2 be bag of n; ::_thesis: ( min (b1,b2,T) = b1 iff max (b1,b2,T) = b2 )
A1: now__::_thesis:_(_max_(b1,b2,T)_=_b2_implies_min_(b1,b2,T)_=_b1_)
assume A2: max (b1,b2,T) = b2 ; ::_thesis: min (b1,b2,T) = b1
now__::_thesis:_(_(_not_b2_<=_b1,T_&_min_(b1,b2,T)_=_b1_)_or_(_b1_=_b2_&_min_(b1,b2,T)_=_b1_)_)
percases ( not b2 <= b1,T or b1 = b2 ) by A2, Def5;
case not b2 <= b1,T ; ::_thesis: min (b1,b2,T) = b1
then b1 <= b2,T by Lm5;
hence min (b1,b2,T) = b1 by Def4; ::_thesis: verum
end;
case b1 = b2 ; ::_thesis: min (b1,b2,T) = b1
hence min (b1,b2,T) = b1 by Th11; ::_thesis: verum
end;
end;
end;
hence min (b1,b2,T) = b1 ; ::_thesis: verum
end;
now__::_thesis:_(_min_(b1,b2,T)_=_b1_implies_max_(b1,b2,T)_=_b2_)
assume A3: min (b1,b2,T) = b1 ; ::_thesis: max (b1,b2,T) = b2
now__::_thesis:_(_(_b1_<=_b2,T_&_max_(b1,b2,T)_=_b2_)_or_(_b1_=_b2_&_max_(b1,b2,T)_=_b2_)_)
percases ( b1 <= b2,T or b1 = b2 ) by A3, Def4;
case b1 <= b2,T ; ::_thesis: max (b1,b2,T) = b2
then max (b2,b1,T) = b2 by Def5;
hence max (b1,b2,T) = b2 by Th15; ::_thesis: verum
end;
case b1 = b2 ; ::_thesis: max (b1,b2,T) = b2
hence max (b1,b2,T) = b2 by Th12; ::_thesis: verum
end;
end;
end;
hence max (b1,b2,T) = b2 ; ::_thesis: verum
end;
hence ( min (b1,b2,T) = b1 iff max (b1,b2,T) = b2 ) by A1; ::_thesis: verum
end;
begin
definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty ZeroStr ;
let p be Polynomial of n,L;
func HT (p,T) -> Element of Bags n means :Def6: :: TERMORD:def 6
( ( Support p = {} & it = EmptyBag n ) or ( it in Support p & ( for b being bag of n st b in Support p holds
b <= it,T ) ) );
existence
ex b1 being Element of Bags n st
( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds
b <= b1,T ) ) )
proof
set O = T;
percases ( Support p = {} or Support p <> {} ) ;
suppose Support p = {} ; ::_thesis: ex b1 being Element of Bags n st
( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds
b <= b1,T ) ) )
hence ex b1 being Element of Bags n st
( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds
b <= b1,T ) ) ) ; ::_thesis: verum
end;
supposeA1: Support p <> {} ; ::_thesis: ex b1 being Element of Bags n st
( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds
b <= b1,T ) ) )
reconsider sp = Support p as finite set by POLYNOM1:def_4;
card sp is finite ;
then consider m being Nat such that
A2: card (Support p) = card m by CARD_1:48;
reconsider sp = Support p as finite Subset of (Bags n) by POLYNOM1:def_4;
defpred S1[ Nat] means for B being finite Subset of (Bags n) st card B = $1 holds
ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) );
A3: for k being Nat st 1 <= k & S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( 1 <= k & S1[k] implies S1[k + 1] )
assume A4: 1 <= k ; ::_thesis: ( not S1[k] or S1[k + 1] )
thus ( S1[k] implies S1[k + 1] ) ::_thesis: verum
proof
assume A5: S1[k] ; ::_thesis: S1[k + 1]
thus S1[k + 1] ::_thesis: verum
proof
let B be finite Subset of (Bags n); ::_thesis: ( card B = k + 1 implies ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) ) )
assume A6: card B = k + 1 ; ::_thesis: ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) )
then reconsider B = B as non empty finite Subset of (Bags n) ;
set x = the Element of B;
reconsider x = the Element of B as Element of Bags n ;
reconsider x = x as bag of n ;
set X = B \ {x};
now__::_thesis:_for_u_being_set_st_u_in_{x}_holds_
u_in_B
let u be set ; ::_thesis: ( u in {x} implies u in B )
assume u in {x} ; ::_thesis: u in B
then u = x by TARSKI:def_1;
hence u in B ; ::_thesis: verum
end;
then {x} c= B by TARSKI:def_3;
then A7: B = {x} \/ B by XBOOLE_1:12
.= {x} \/ (B \ {x}) by XBOOLE_1:39 ;
( x in B \ {x} iff ( x in B & not x in {x} ) ) by XBOOLE_0:def_5;
then A8: (card (B \ {x})) + 1 = k + 1 by A6, A7, CARD_2:41, TARSKI:def_1;
then reconsider X = B \ {x} as non empty set by A4;
consider b9 being bag of n such that
A9: b9 in X and
A10: for b being bag of n st b in X holds
[b,b9] in T by A5, A8;
A11: T is_connected_in field T by RELAT_2:def_14;
now__::_thesis:_(_(_x_=_b9_&_ex_b9,_b9_being_bag_of_n_st_
(_b9_in_B_&_(_for_b_being_bag_of_n_st_b_in_B_holds_
[b,b9]_in_T_)_)_)_or_(_x_<>_b9_&_ex_b9_being_bag_of_n_st_
(_b9_in_B_&_(_for_b_being_bag_of_n_st_b_in_B_holds_
[b,b9]_in_T_)_)_)_)
percases ( x = b9 or x <> b9 ) ;
caseA12: x = b9 ; ::_thesis: ex b9, b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) )
A13: now__::_thesis:_for_b_being_bag_of_n_st_b_in_B_holds_
[b,b9]_in_T
let b be bag of n; ::_thesis: ( b in B implies [b,b9] in T )
assume A14: b in B ; ::_thesis: [b,b9] in T
now__::_thesis:_(_(_b_in_X_&_[b,b9]_in_T_)_or_(_not_b_in_X_&_[b,b9]_in_T_)_)
percases ( b in X or not b in X ) ;
case b in X ; ::_thesis: [b,b9] in T
hence [b,b9] in T by A10; ::_thesis: verum
end;
case not b in X ; ::_thesis: [b,b9] in T
then b in {x} by A7, A14, XBOOLE_0:def_3;
then b = x by TARSKI:def_1;
hence [b,b9] in T by A12, ORDERS_1:3; ::_thesis: verum
end;
end;
end;
hence [b,b9] in T ; ::_thesis: verum
end;
take b9 = b9; ::_thesis: ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) )
X c= B by XBOOLE_1:36;
hence ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) ) by A9, A13; ::_thesis: verum
end;
caseA15: x <> b9 ; ::_thesis: ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) )
b9 is Element of Bags n by PRE_POLY:def_12;
then [b9,b9] in T by ORDERS_1:3;
then A16: b9 in field T by RELAT_1:15;
[x,x] in T by ORDERS_1:3;
then A17: x in field T by RELAT_1:15;
now__::_thesis:_(_(_[x,b9]_in_T_&_ex_b9_being_bag_of_n_st_
(_b9_in_B_&_(_for_b_being_bag_of_n_st_b_in_B_holds_
[b,b9]_in_T_)_)_)_or_(_[b9,x]_in_T_&_ex_b9_being_bag_of_n_st_
(_b9_in_B_&_(_for_b_being_bag_of_n_st_b_in_B_holds_
[b,b9]_in_T_)_)_)_)
percases ( [x,b9] in T or [b9,x] in T ) by A11, A15, A17, A16, RELAT_2:def_6;
caseA18: [x,b9] in T ; ::_thesis: ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) )
thus ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) ) ::_thesis: verum
proof
take b9 ; ::_thesis: ( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) )
for b being bag of n st b in B holds
[b,b9] in T
proof
let b be bag of n; ::_thesis: ( b in B implies [b,b9] in T )
assume A19: b in B ; ::_thesis: [b,b9] in T
now__::_thesis:_(_(_b_<>_x_&_[b,b9]_in_T_)_or_(_b_=_x_&_[b,b9]_in_T_)_)
percases ( b <> x or b = x ) ;
case b <> x ; ::_thesis: [b,b9] in T
then not b in {x} by TARSKI:def_1;
then b in X by A19, XBOOLE_0:def_5;
hence [b,b9] in T by A10; ::_thesis: verum
end;
case b = x ; ::_thesis: [b,b9] in T
hence [b,b9] in T by A18; ::_thesis: verum
end;
end;
end;
hence [b,b9] in T ; ::_thesis: verum
end;
hence ( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) ) by A9, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
caseA20: [b9,x] in T ; ::_thesis: ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) )
thus ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) ) ::_thesis: verum
proof
take x ; ::_thesis: ( x in B & ( for b being bag of n st b in B holds
[b,x] in T ) )
for b being bag of n st b in B holds
[b,x] in T
proof
let b be bag of n; ::_thesis: ( b in B implies [b,x] in T )
assume A21: b in B ; ::_thesis: [b,x] in T
now__::_thesis:_(_(_b_<>_x_&_[b,x]_in_T_)_or_(_b_=_x_&_[b,x]_in_T_)_)
percases ( b <> x or b = x ) ;
case b <> x ; ::_thesis: [b,x] in T
then not b in {x} by TARSKI:def_1;
then b in X by A21, XBOOLE_0:def_5;
then A22: [b,b9] in T by A10;
( b is Element of Bags n & b9 is Element of Bags n ) by PRE_POLY:def_12;
hence [b,x] in T by A20, A22, ORDERS_1:5; ::_thesis: verum
end;
case b = x ; ::_thesis: [b,x] in T
hence [b,x] in T by ORDERS_1:3; ::_thesis: verum
end;
end;
end;
hence [b,x] in T ; ::_thesis: verum
end;
hence ( x in B & ( for b being bag of n st b in B holds
[b,x] in T ) ) ; ::_thesis: verum
end;
end;
end;
end;
hence ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) ) ; ::_thesis: verum
end;
end;
end;
hence ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) ) ; ::_thesis: verum
end;
end;
end;
m <> 0 by A1, A2;
then A23: 1 <= m by NAT_1:14;
A24: card (Support p) = m by A2, CARD_1:def_2;
A25: S1[1]
proof
let B be finite Subset of (Bags n); ::_thesis: ( card B = 1 implies ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) ) )
assume card B = 1 ; ::_thesis: ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) )
then card {{}} = card B by CARD_1:30;
then consider b being set such that
A26: B = {b} by CARD_1:29;
A27: b in B by A26, TARSKI:def_1;
then reconsider b = b as Element of Bags n ;
reconsider b = b as bag of n ;
now__::_thesis:_for_b9_being_bag_of_n_st_b9_in_B_holds_
[b9,b]_in_T
let b9 be bag of n; ::_thesis: ( b9 in B implies [b9,b] in T )
assume b9 in B ; ::_thesis: [b9,b] in T
then b9 = b by A26, TARSKI:def_1;
hence [b9,b] in T by ORDERS_1:3; ::_thesis: verum
end;
hence ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) ) by A27; ::_thesis: verum
end;
for k being Nat st 1 <= k holds
S1[k] from NAT_1:sch_8(A25, A3);
then consider b9 being bag of n such that
A28: b9 in sp and
A29: for b being bag of n st b in sp holds
[b,b9] in T by A24, A23;
take b9 ; ::_thesis: ( b9 is Element of Bags n & b9 is Element of Bags n & not ( not ( Support p = {} & b9 = EmptyBag n ) & not ( b9 in Support p & ( for b being bag of n st b in Support p holds
b <= b9,T ) ) ) )
now__::_thesis:_for_b_being_bag_of_n_st_b_in_sp_holds_
b_<=_b9,T
let b be bag of n; ::_thesis: ( b in sp implies b <= b9,T )
assume b in sp ; ::_thesis: b <= b9,T
then [b,b9] in T by A29;
hence b <= b9,T by Def2; ::_thesis: verum
end;
hence ( b9 is Element of Bags n & b9 is Element of Bags n & not ( not ( Support p = {} & b9 = EmptyBag n ) & not ( b9 in Support p & ( for b being bag of n st b in Support p holds
b <= b9,T ) ) ) ) by A28; ::_thesis: verum
end;
end;
end;
uniqueness
for b1, b2 being Element of Bags n st ( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds
b <= b1,T ) ) ) & ( ( Support p = {} & b2 = EmptyBag n ) or ( b2 in Support p & ( for b being bag of n st b in Support p holds
b <= b2,T ) ) ) holds
b1 = b2
proof
let b1, b2 be Element of Bags n; ::_thesis: ( ( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds
b <= b1,T ) ) ) & ( ( Support p = {} & b2 = EmptyBag n ) or ( b2 in Support p & ( for b being bag of n st b in Support p holds
b <= b2,T ) ) ) implies b1 = b2 )
set O = T;
assume A30: ( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds
b <= b1,T ) ) ) ; ::_thesis: ( ( not ( Support p = {} & b2 = EmptyBag n ) & not ( b2 in Support p & ( for b being bag of n st b in Support p holds
b <= b2,T ) ) ) or b1 = b2 )
assume A31: ( ( Support p = {} & b2 = EmptyBag n ) or ( b2 in Support p & ( for b being bag of n st b in Support p holds
b <= b2,T ) ) ) ; ::_thesis: b1 = b2
percases ( Support p = {} or Support p <> {} ) ;
suppose Support p = {} ; ::_thesis: b1 = b2
hence b1 = b2 by A30, A31; ::_thesis: verum
end;
supposeA32: Support p <> {} ; ::_thesis: b1 = b2
then b1 <= b2,T by A30, A31;
then A33: [b1,b2] in T by Def2;
b2 <= b1,T by A30, A31, A32;
then [b2,b1] in T by Def2;
hence b1 = b2 by A33, ORDERS_1:4; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem Def6 defines HT TERMORD:def_6_:_
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L
for b5 being Element of Bags n holds
( b5 = HT (p,T) iff ( ( Support p = {} & b5 = EmptyBag n ) or ( b5 in Support p & ( for b being bag of n st b in Support p holds
b <= b5,T ) ) ) );
definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty ZeroStr ;
let p be Polynomial of n,L;
func HC (p,T) -> Element of L equals :: TERMORD:def 7
p . (HT (p,T));
correctness
coherence
p . (HT (p,T)) is Element of L;
;
end;
:: deftheorem defines HC TERMORD:def_7_:_
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds HC (p,T) = p . (HT (p,T));
definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty ZeroStr ;
let p be Polynomial of n,L;
func HM (p,T) -> Monomial of n,L equals :: TERMORD:def 8
Monom ((HC (p,T)),(HT (p,T)));
correctness
coherence
Monom ((HC (p,T)),(HT (p,T))) is Monomial of n,L;
;
end;
:: deftheorem defines HM TERMORD:def_8_:_
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds HM (p,T) = Monom ((HC (p,T)),(HT (p,T)));
Lm7: for n being Ordinal
for O being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds
( HC (p,O) = 0. L iff p = 0_ (n,L) )
proof
let n be Ordinal; ::_thesis: for O being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds
( HC (p,O) = 0. L iff p = 0_ (n,L) )
let O be connected TermOrder of n; ::_thesis: for L being non empty ZeroStr
for p being Polynomial of n,L holds
( HC (p,O) = 0. L iff p = 0_ (n,L) )
let L be non empty ZeroStr ; ::_thesis: for p being Polynomial of n,L holds
( HC (p,O) = 0. L iff p = 0_ (n,L) )
let p be Polynomial of n,L; ::_thesis: ( HC (p,O) = 0. L iff p = 0_ (n,L) )
now__::_thesis:_(_HC_(p,O)_=_0._L_implies_p_=_0__(n,L)_)
assume HC (p,O) = 0. L ; ::_thesis: p = 0_ (n,L)
then not HT (p,O) in Support p by POLYNOM1:def_3;
then Support p = {} by Def6;
hence p = 0_ (n,L) by POLYNOM7:1; ::_thesis: verum
end;
hence ( HC (p,O) = 0. L iff p = 0_ (n,L) ) by POLYNOM1:22; ::_thesis: verum
end;
Lm8: for n being Ordinal
for O being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds (HM (p,O)) . (HT (p,O)) = p . (HT (p,O))
proof
let n be Ordinal; ::_thesis: for O being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds (HM (p,O)) . (HT (p,O)) = p . (HT (p,O))
let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr
for p being Polynomial of n,L holds (HM (p,O)) . (HT (p,O)) = p . (HT (p,O))
let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L holds (HM (p,O)) . (HT (p,O)) = p . (HT (p,O))
let p be Polynomial of n,L; ::_thesis: (HM (p,O)) . (HT (p,O)) = p . (HT (p,O))
A1: now__::_thesis:_(_(_HC_(p,O)_<>_0._L_&_term_(HM_(p,O))_=_HT_(p,O)_)_or_(_HC_(p,O)_=_0._L_&_term_(HM_(p,O))_=_HT_(p,O)_)_)
percases ( HC (p,O) <> 0. L or HC (p,O) = 0. L ) ;
case HC (p,O) <> 0. L ; ::_thesis: term (HM (p,O)) = HT (p,O)
then not HC (p,O) is zero by STRUCT_0:def_12;
hence term (HM (p,O)) = HT (p,O) by POLYNOM7:10; ::_thesis: verum
end;
caseA2: HC (p,O) = 0. L ; ::_thesis: term (HM (p,O)) = HT (p,O)
then p = 0_ (n,L) by Lm7;
then Support p = {} by POLYNOM7:1;
then HT (p,O) = EmptyBag n by Def6;
hence term (HM (p,O)) = HT (p,O) by A2, POLYNOM7:8; ::_thesis: verum
end;
end;
end;
p . (HT (p,O)) = coefficient (HM (p,O)) by POLYNOM7:9
.= (HM (p,O)) . (term (HM (p,O))) by POLYNOM7:def_6 ;
hence (HM (p,O)) . (HT (p,O)) = p . (HT (p,O)) by A1; ::_thesis: verum
end;
Lm9: for n being Ordinal
for O being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L st HC (p,O) <> 0. L holds
HT (p,O) in Support (HM (p,O))
proof
let n be Ordinal; ::_thesis: for O being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L st HC (p,O) <> 0. L holds
HT (p,O) in Support (HM (p,O))
let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr
for p being Polynomial of n,L st HC (p,O) <> 0. L holds
HT (p,O) in Support (HM (p,O))
let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L st HC (p,O) <> 0. L holds
HT (p,O) in Support (HM (p,O))
let p be Polynomial of n,L; ::_thesis: ( HC (p,O) <> 0. L implies HT (p,O) in Support (HM (p,O)) )
assume HC (p,O) <> 0. L ; ::_thesis: HT (p,O) in Support (HM (p,O))
then (HM (p,O)) . (HT (p,O)) <> 0. L by Lm8;
hence HT (p,O) in Support (HM (p,O)) by POLYNOM1:def_3; ::_thesis: verum
end;
Lm10: for n being Ordinal
for O being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L st HC (p,O) = 0. L holds
Support (HM (p,O)) = {}
proof
let n be Ordinal; ::_thesis: for O being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L st HC (p,O) = 0. L holds
Support (HM (p,O)) = {}
let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr
for p being Polynomial of n,L st HC (p,O) = 0. L holds
Support (HM (p,O)) = {}
let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L st HC (p,O) = 0. L holds
Support (HM (p,O)) = {}
let p be Polynomial of n,L; ::_thesis: ( HC (p,O) = 0. L implies Support (HM (p,O)) = {} )
assume A1: HC (p,O) = 0. L ; ::_thesis: Support (HM (p,O)) = {}
then p = 0_ (n,L) by Lm7;
then Support p = {} by POLYNOM7:1;
then A2: HT (p,O) = EmptyBag n by Def6;
A3: term (HM (p,O)) = EmptyBag n by A1, POLYNOM7:8;
now__::_thesis:_not_Support_(HM_(p,O))_<>_{}
assume Support (HM (p,O)) <> {} ; ::_thesis: contradiction
then Support (HM (p,O)) = {(term (HM (p,O)))} by POLYNOM7:7;
then term (HM (p,O)) in Support (HM (p,O)) by TARSKI:def_1;
then (HM (p,O)) . (EmptyBag n) <> 0. L by A3, POLYNOM1:def_3;
hence contradiction by A1, A2, Lm8; ::_thesis: verum
end;
hence Support (HM (p,O)) = {} ; ::_thesis: verum
end;
registration
let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial ZeroStr ;
let p be non-zero Polynomial of n,L;
cluster HM (p,T) -> non-zero ;
coherence
HM (p,T) is non-zero
proof
set O = T;
now__::_thesis:_(_(_HC_(p,T)_<>_0._L_&_HM_(p,T)_is_non-zero_)_or_(_HC_(p,T)_=_0._L_&_HM_(p,T)_is_non-zero_)_)
percases ( HC (p,T) <> 0. L or HC (p,T) = 0. L ) ;
case HC (p,T) <> 0. L ; ::_thesis: HM (p,T) is non-zero
then HT (p,T) in Support (HM (p,T)) by Lm9;
then HM (p,T) <> 0_ (n,L) by POLYNOM7:1;
hence HM (p,T) is non-zero by POLYNOM7:def_1; ::_thesis: verum
end;
case HC (p,T) = 0. L ; ::_thesis: HM (p,T) is non-zero
then p = 0_ (n,L) by Lm7;
hence HM (p,T) is non-zero by POLYNOM7:def_1; ::_thesis: verum
end;
end;
end;
hence HM (p,T) is non-zero ; ::_thesis: verum
end;
cluster HC (p,T) -> non zero ;
coherence
not HC (p,T) is zero
proof
set O = T;
set a = HC (p,T);
now__::_thesis:_not_HC_(p,T)_=_0._L
assume HC (p,T) = 0. L ; ::_thesis: contradiction
then not HT (p,T) in Support p by POLYNOM1:def_3;
then Support p = {} by Def6;
then p = 0_ (n,L) by POLYNOM7:1;
hence contradiction by POLYNOM7:def_1; ::_thesis: verum
end;
hence not HC (p,T) is zero by STRUCT_0:def_12; ::_thesis: verum
end;
end;
Lm11: for n being Ordinal
for O being connected TermOrder of n
for L being non empty ZeroStr
for m being Monomial of n,L holds
( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m )
proof
let n be Ordinal; ::_thesis: for O being connected TermOrder of n
for L being non empty ZeroStr
for m being Monomial of n,L holds
( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m )
let O be connected TermOrder of n; ::_thesis: for L being non empty ZeroStr
for m being Monomial of n,L holds
( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m )
let L be non empty ZeroStr ; ::_thesis: for m being Monomial of n,L holds
( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m )
let m be Monomial of n,L; ::_thesis: ( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m )
percases ( Support m = {} or ex b being bag of n st Support m = {b} ) by POLYNOM7:6;
supposeA1: Support m = {} ; ::_thesis: ( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m )
hence A2: term m = EmptyBag n by POLYNOM7:def_5
.= HT (m,O) by A1, Def6 ;
::_thesis: ( HC (m,O) = coefficient m & HM (m,O) = m )
hence HC (m,O) = coefficient m by POLYNOM7:def_6; ::_thesis: HM (m,O) = m
hence HM (m,O) = m by A2, POLYNOM7:11; ::_thesis: verum
end;
supposeA3: ex b being bag of n st Support m = {b} ; ::_thesis: ( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m )
then consider b being bag of n such that
A4: Support m = {b} ;
b in Support m by A4, TARSKI:def_1;
then A5: m . b <> 0. L by POLYNOM1:def_3;
HT (m,O) in Support m by A3, Def6;
hence A6: HT (m,O) = b by A4, TARSKI:def_1
.= term m by A5, POLYNOM7:def_5 ;
::_thesis: ( HC (m,O) = coefficient m & HM (m,O) = m )
hence HC (m,O) = coefficient m by POLYNOM7:def_6; ::_thesis: HM (m,O) = m
hence HM (m,O) = m by A6, POLYNOM7:11; ::_thesis: verum
end;
end;
end;
theorem :: TERMORD:17
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds
( HC (p,T) = 0. L iff p = 0_ (n,L) ) by Lm7;
theorem :: TERMORD:18
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds (HM (p,T)) . (HT (p,T)) = p . (HT (p,T)) by Lm8;
theorem Th19: :: TERMORD:19
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L
for b being bag of n st b <> HT (p,T) holds
(HM (p,T)) . b = 0. L
proof
let n be Ordinal; ::_thesis: for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L
for b being bag of n st b <> HT (p,T) holds
(HM (p,T)) . b = 0. L
let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr
for p being Polynomial of n,L
for b being bag of n st b <> HT (p,O) holds
(HM (p,O)) . b = 0. L
let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L
for b being bag of n st b <> HT (p,O) holds
(HM (p,O)) . b = 0. L
let p be Polynomial of n,L; ::_thesis: for b being bag of n st b <> HT (p,O) holds
(HM (p,O)) . b = 0. L
let b be bag of n; ::_thesis: ( b <> HT (p,O) implies (HM (p,O)) . b = 0. L )
assume A1: b <> HT (p,O) ; ::_thesis: (HM (p,O)) . b = 0. L
percases ( Support (HM (p,O)) = {} or ex b being bag of n st Support (HM (p,O)) = {b} ) by POLYNOM7:6;
suppose Support (HM (p,O)) = {} ; ::_thesis: (HM (p,O)) . b = 0. L
then HM (p,O) = 0_ (n,L) by POLYNOM7:1;
hence (HM (p,O)) . b = 0. L by POLYNOM1:22; ::_thesis: verum
end;
suppose ex b being bag of n st Support (HM (p,O)) = {b} ; ::_thesis: (HM (p,O)) . b = 0. L
then consider b1 being bag of n such that
A2: Support (HM (p,O)) = {b1} ;
A3: b is Element of Bags n by PRE_POLY:def_12;
now__::_thesis:_(_(_HC_(p,O)_<>_0._L_&_(HM_(p,O))_._b_=_0._L_)_or_(_HC_(p,O)_=_0._L_&_(HM_(p,O))_._b_=_0._L_)_)
percases ( HC (p,O) <> 0. L or HC (p,O) = 0. L ) ;
case HC (p,O) <> 0. L ; ::_thesis: (HM (p,O)) . b = 0. L
then HT (p,O) in {b1} by A2, Lm9;
then b1 <> b by A1, TARSKI:def_1;
then not b in {b1} by TARSKI:def_1;
hence (HM (p,O)) . b = 0. L by A2, A3, POLYNOM1:def_3; ::_thesis: verum
end;
case HC (p,O) = 0. L ; ::_thesis: (HM (p,O)) . b = 0. L
then Support (HM (p,O)) = {} by Lm10;
then HM (p,O) = 0_ (n,L) by POLYNOM7:1;
hence (HM (p,O)) . b = 0. L by POLYNOM1:22; ::_thesis: verum
end;
end;
end;
hence (HM (p,O)) . b = 0. L ; ::_thesis: verum
end;
end;
end;
Lm12: for n being Ordinal
for O being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds
( Support (HM (p,O)) = {} or Support (HM (p,O)) = {(HT (p,O))} )
proof
let n be Ordinal; ::_thesis: for O being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds
( Support (HM (p,O)) = {} or Support (HM (p,O)) = {(HT (p,O))} )
let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr
for p being Polynomial of n,L holds
( Support (HM (p,O)) = {} or Support (HM (p,O)) = {(HT (p,O))} )
let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L holds
( Support (HM (p,O)) = {} or Support (HM (p,O)) = {(HT (p,O))} )
let p be Polynomial of n,L; ::_thesis: ( Support (HM (p,O)) = {} or Support (HM (p,O)) = {(HT (p,O))} )
assume A1: not Support (HM (p,O)) = {} ; ::_thesis: Support (HM (p,O)) = {(HT (p,O))}
then A2: ex b being bag of n st Support (HM (p,O)) = {b} by POLYNOM7:6;
now__::_thesis:_(_(_HC_(p,O)_=_0._L_&_Support_(HM_(p,O))_=_{(HT_(p,O))}_)_or_(_HC_(p,O)_<>_0._L_&_Support_(HM_(p,O))_=_{(HT_(p,O))}_)_)
percases ( HC (p,O) = 0. L or HC (p,O) <> 0. L ) ;
case HC (p,O) = 0. L ; ::_thesis: Support (HM (p,O)) = {(HT (p,O))}
hence Support (HM (p,O)) = {(HT (p,O))} by A1, Lm10; ::_thesis: verum
end;
case HC (p,O) <> 0. L ; ::_thesis: Support (HM (p,O)) = {(HT (p,O))}
then HT (p,O) in Support (HM (p,O)) by Lm9;
hence Support (HM (p,O)) = {(HT (p,O))} by A2, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence Support (HM (p,O)) = {(HT (p,O))} ; ::_thesis: verum
end;
theorem :: TERMORD:20
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds Support (HM (p,T)) c= Support p
proof
let n be Ordinal; ::_thesis: for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds Support (HM (p,T)) c= Support p
let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr
for p being Polynomial of n,L holds Support (HM (p,O)) c= Support p
let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L holds Support (HM (p,O)) c= Support p
let p be Polynomial of n,L; ::_thesis: Support (HM (p,O)) c= Support p
now__::_thesis:_for_u_being_set_st_u_in_Support_(HM_(p,O))_holds_
u_in_Support_p
let u be set ; ::_thesis: ( u in Support (HM (p,O)) implies u in Support p )
assume A1: u in Support (HM (p,O)) ; ::_thesis: u in Support p
now__::_thesis:_(_(_u_in_{}_&_u_in_Support_p_)_or_(_u_in_{(HT_(p,O))}_&_u_in_Support_p_)_)
percases ( u in {} or u in {(HT (p,O))} ) by A1, Lm12;
case u in {} ; ::_thesis: u in Support p
hence u in Support p ; ::_thesis: verum
end;
case u in {(HT (p,O))} ; ::_thesis: u in Support p
then A2: u = HT (p,O) by TARSKI:def_1;
now__::_thesis:_(_(_HC_(p,O)_=_0._L_&_contradiction_)_or_(_HC_(p,O)_<>_0._L_&_u_in_Support_p_)_)
percases ( HC (p,O) = 0. L or HC (p,O) <> 0. L ) ;
case HC (p,O) = 0. L ; ::_thesis: contradiction
then (HM (p,O)) . (HT (p,O)) = 0. L by Lm8;
hence contradiction by A1, A2, POLYNOM1:def_3; ::_thesis: verum
end;
case HC (p,O) <> 0. L ; ::_thesis: u in Support p
hence u in Support p by A2, POLYNOM1:def_3; ::_thesis: verum
end;
end;
end;
hence u in Support p ; ::_thesis: verum
end;
end;
end;
hence u in Support p ; ::_thesis: verum
end;
hence Support (HM (p,O)) c= Support p by TARSKI:def_3; ::_thesis: verum
end;
theorem :: TERMORD:21
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds
( Support (HM (p,T)) = {} or Support (HM (p,T)) = {(HT (p,T))} ) by Lm12;
theorem :: TERMORD:22
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds
( term (HM (p,T)) = HT (p,T) & coefficient (HM (p,T)) = HC (p,T) )
proof
let n be Ordinal; ::_thesis: for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds
( term (HM (p,T)) = HT (p,T) & coefficient (HM (p,T)) = HC (p,T) )
let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr
for p being Polynomial of n,L holds
( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) )
let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L holds
( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) )
let p be Polynomial of n,L; ::_thesis: ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) )
percases ( not HC (p,O) is zero or HC (p,O) is zero ) ;
suppose not HC (p,O) is zero ; ::_thesis: ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) )
then reconsider a = HC (p,O) as non zero Element of L ;
term (Monom (a,(HT (p,O)))) = HT (p,O) by POLYNOM7:10;
hence ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) ) by POLYNOM7:9; ::_thesis: verum
end;
supposeA1: HC (p,O) is zero ; ::_thesis: ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) )
now__::_thesis:_(_(_not_p_is_non-zero_&_term_(HM_(p,O))_=_HT_(p,O)_&_coefficient_(HM_(p,O))_=_HC_(p,O)_)_or_(_p_is_non-zero_&_term_(HM_(p,O))_=_HT_(p,O)_&_coefficient_(HM_(p,O))_=_HC_(p,O)_)_)
percases ( not p is non-zero or p is non-zero ) ;
case not p is non-zero ; ::_thesis: ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) )
then p = 0_ (n,L) by POLYNOM7:def_1;
then Support p = {} by POLYNOM7:1;
then HT (p,O) = EmptyBag n by Def6
.= term (Monom ((0. L),(HT (p,O)))) by POLYNOM7:8
.= term (HM (p,O)) by A1, STRUCT_0:def_12 ;
hence ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) ) by POLYNOM7:9; ::_thesis: verum
end;
case p is non-zero ; ::_thesis: ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) )
then reconsider p = p as non-zero Polynomial of n,L ;
not HC (p,O) is zero ;
hence ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) ) by A1; ::_thesis: verum
end;
end;
end;
hence ( term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) ) ; ::_thesis: verum
end;
end;
end;
theorem :: TERMORD:23
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for m being Monomial of n,L holds
( HT (m,T) = term m & HC (m,T) = coefficient m & HM (m,T) = m ) by Lm11;
theorem :: TERMORD:24
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for c being ConstPoly of n,L holds
( HT (c,T) = EmptyBag n & HC (c,T) = c . (EmptyBag n) )
proof
let n be Ordinal; ::_thesis: for T being connected TermOrder of n
for L being non empty ZeroStr
for c being ConstPoly of n,L holds
( HT (c,T) = EmptyBag n & HC (c,T) = c . (EmptyBag n) )
let O be connected TermOrder of n; ::_thesis: for L being non empty ZeroStr
for c being ConstPoly of n,L holds
( HT (c,O) = EmptyBag n & HC (c,O) = c . (EmptyBag n) )
let L be non empty ZeroStr ; ::_thesis: for c being ConstPoly of n,L holds
( HT (c,O) = EmptyBag n & HC (c,O) = c . (EmptyBag n) )
let c be ConstPoly of n,L; ::_thesis: ( HT (c,O) = EmptyBag n & HC (c,O) = c . (EmptyBag n) )
thus HT (c,O) = term c by Lm11
.= EmptyBag n by POLYNOM7:16 ; ::_thesis: HC (c,O) = c . (EmptyBag n)
thus HC (c,O) = coefficient c by Lm11
.= c . (EmptyBag n) by POLYNOM7:16 ; ::_thesis: verum
end;
theorem :: TERMORD:25
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for a being Element of L holds
( HT ((a | (n,L)),T) = EmptyBag n & HC ((a | (n,L)),T) = a )
proof
let n be Ordinal; ::_thesis: for T being connected TermOrder of n
for L being non empty ZeroStr
for a being Element of L holds
( HT ((a | (n,L)),T) = EmptyBag n & HC ((a | (n,L)),T) = a )
let O be connected TermOrder of n; ::_thesis: for L being non empty ZeroStr
for a being Element of L holds
( HT ((a | (n,L)),O) = EmptyBag n & HC ((a | (n,L)),O) = a )
let L be non empty ZeroStr ; ::_thesis: for a being Element of L holds
( HT ((a | (n,L)),O) = EmptyBag n & HC ((a | (n,L)),O) = a )
let a be Element of L; ::_thesis: ( HT ((a | (n,L)),O) = EmptyBag n & HC ((a | (n,L)),O) = a )
set p = a | (n,L);
thus HT ((a | (n,L)),O) = term (a | (n,L)) by Lm11
.= EmptyBag n by POLYNOM7:23 ; ::_thesis: HC ((a | (n,L)),O) = a
thus HC ((a | (n,L)),O) = coefficient (a | (n,L)) by Lm11
.= a by POLYNOM7:23 ; ::_thesis: verum
end;
theorem Th26: :: TERMORD:26
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds HT ((HM (p,T)),T) = HT (p,T)
proof
let n be Ordinal; ::_thesis: for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds HT ((HM (p,T)),T) = HT (p,T)
let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr
for p being Polynomial of n,L holds HT ((HM (p,O)),O) = HT (p,O)
let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L holds HT ((HM (p,O)),O) = HT (p,O)
let p be Polynomial of n,L; ::_thesis: HT ((HM (p,O)),O) = HT (p,O)
percases ( not HC (p,O) is zero or HC (p,O) is zero ) ;
suppose not HC (p,O) is zero ; ::_thesis: HT ((HM (p,O)),O) = HT (p,O)
then reconsider a = HC (p,O) as non zero Element of L ;
thus HT ((HM (p,O)),O) = term (Monom (a,(HT (p,O)))) by Lm11
.= HT (p,O) by POLYNOM7:10 ; ::_thesis: verum
end;
supposeA1: HC (p,O) is zero ; ::_thesis: HT ((HM (p,O)),O) = HT (p,O)
now__::_thesis:_(_(_not_p_is_non-zero_&_HT_((HM_(p,O)),O)_=_HT_(p,O)_)_or_(_p_is_non-zero_&_HT_((HM_(p,O)),O)_=_HT_(p,O)_)_)
percases ( not p is non-zero or p is non-zero ) ;
case not p is non-zero ; ::_thesis: HT ((HM (p,O)),O) = HT (p,O)
then p = 0_ (n,L) by POLYNOM7:def_1;
then Support p = {} by POLYNOM7:1;
then HT (p,O) = EmptyBag n by Def6
.= term (Monom ((0. L),(HT (p,O)))) by POLYNOM7:8
.= term (HM (p,O)) by A1, STRUCT_0:def_12 ;
hence HT ((HM (p,O)),O) = HT (p,O) by Lm11; ::_thesis: verum
end;
case p is non-zero ; ::_thesis: HT ((HM (p,O)),O) = HT (p,O)
then reconsider p = p as non-zero Polynomial of n,L ;
not HC (p,O) is zero ;
hence HT ((HM (p,O)),O) = HT (p,O) by A1; ::_thesis: verum
end;
end;
end;
hence HT ((HM (p,O)),O) = HT (p,O) ; ::_thesis: verum
end;
end;
end;
theorem :: TERMORD:27
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds HC ((HM (p,T)),T) = HC (p,T)
proof
let n be Ordinal; ::_thesis: for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds HC ((HM (p,T)),T) = HC (p,T)
let O be connected TermOrder of n; ::_thesis: for L being non trivial ZeroStr
for p being Polynomial of n,L holds HC ((HM (p,O)),O) = HC (p,O)
let L be non trivial ZeroStr ; ::_thesis: for p being Polynomial of n,L holds HC ((HM (p,O)),O) = HC (p,O)
let p be Polynomial of n,L; ::_thesis: HC ((HM (p,O)),O) = HC (p,O)
thus HC ((HM (p,O)),O) = (HM (p,O)) . (HT (p,O)) by Th26
.= HC (p,O) by Lm8 ; ::_thesis: verum
end;
theorem :: TERMORD:28
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds HM ((HM (p,T)),T) = HM (p,T) by Lm11;
Lm13: for X being set
for S being Subset of X
for R being Order of X st R is being_linear-order holds
R linearly_orders S
proof
let X be set ; ::_thesis: for S being Subset of X
for R being Order of X st R is being_linear-order holds
R linearly_orders S
let S be Subset of X; ::_thesis: for R being Order of X st R is being_linear-order holds
R linearly_orders S
let R be Order of X; ::_thesis: ( R is being_linear-order implies R linearly_orders S )
S c= X ;
then A1: S c= field R by ORDERS_1:15;
assume R is being_linear-order ; ::_thesis: R linearly_orders S
hence R linearly_orders S by A1, ORDERS_1:37, ORDERS_1:38; ::_thesis: verum
end;
Lm14: for n being Ordinal
for O being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr
for p, q being non-zero Polynomial of n,L holds (p *' q) . ((HT (p,O)) + (HT (q,O))) = (p . (HT (p,O))) * (q . (HT (q,O)))
proof
let n be Ordinal; ::_thesis: for O being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr
for p, q being non-zero Polynomial of n,L holds (p *' q) . ((HT (p,O)) + (HT (q,O))) = (p . (HT (p,O))) * (q . (HT (q,O)))
let O be connected admissible TermOrder of n; ::_thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr
for p, q being non-zero Polynomial of n,L holds (p *' q) . ((HT (p,O)) + (HT (q,O))) = (p . (HT (p,O))) * (q . (HT (q,O)))
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr ; ::_thesis: for p, q being non-zero Polynomial of n,L holds (p *' q) . ((HT (p,O)) + (HT (q,O))) = (p . (HT (p,O))) * (q . (HT (q,O)))
let p, q be non-zero Polynomial of n,L; ::_thesis: (p *' q) . ((HT (p,O)) + (HT (q,O))) = (p . (HT (p,O))) * (q . (HT (q,O)))
set b = (HT (p,O)) + (HT (q,O));
consider s being FinSequence of L such that
A1: (p *' q) . ((HT (p,O)) + (HT (q,O))) = Sum s and
A2: len s = len (decomp ((HT (p,O)) + (HT (q,O)))) and
A3: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp ((HT (p,O)) + (HT (q,O)))) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by POLYNOM1:def_9;
consider S being non empty finite Subset of (Bags n) such that
A4: divisors ((HT (p,O)) + (HT (q,O))) = SgmX ((BagOrder n),S) and
A5: for p being bag of n holds
( p in S iff p divides (HT (p,O)) + (HT (q,O)) ) by PRE_POLY:def_16;
set sgm = SgmX ((BagOrder n),S);
A6: BagOrder n linearly_orders S by Lm13;
HT (p,O) divides (HT (p,O)) + (HT (q,O)) by PRE_POLY:50;
then HT (p,O) in S by A5;
then HT (p,O) in rng (SgmX ((BagOrder n),S)) by A6, PRE_POLY:def_2;
then consider i being set such that
A7: i in dom (SgmX ((BagOrder n),S)) and
A8: (SgmX ((BagOrder n),S)) . i = HT (p,O) by FUNCT_1:def_3;
A9: i in dom (decomp ((HT (p,O)) + (HT (q,O)))) by A4, A7, PRE_POLY:def_17;
(divisors ((HT (p,O)) + (HT (q,O)))) /. i = HT (p,O) by A4, A7, A8, PARTFUN1:def_6;
then A10: (decomp ((HT (p,O)) + (HT (q,O)))) /. i = <*(HT (p,O)),(((HT (p,O)) + (HT (q,O))) -' (HT (p,O)))*> by A9, PRE_POLY:def_17;
then A11: (decomp ((HT (p,O)) + (HT (q,O)))) /. i = <*(HT (p,O)),(HT (q,O))*> by PRE_POLY:48;
A12: dom s = Seg (len (decomp ((HT (p,O)) + (HT (q,O))))) by A2, FINSEQ_1:def_3
.= dom (decomp ((HT (p,O)) + (HT (q,O)))) by FINSEQ_1:def_3 ;
then A13: i in dom s by A4, A7, PRE_POLY:def_17;
reconsider i = i as Element of NAT by A7;
consider b1, b2 being bag of n such that
A14: (decomp ((HT (p,O)) + (HT (q,O)))) /. i = <*b1,b2*> and
A15: s /. i = (p . b1) * (q . b2) by A3, A13;
A16: b2 = <*(HT (p,O)),(HT (q,O))*> . 2 by A11, A14, FINSEQ_1:44
.= HT (q,O) by FINSEQ_1:44 ;
A17: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_s_&_k_<>_i_holds_
s_/._k_=_0._L
let k be Element of NAT ; ::_thesis: ( k in dom s & k <> i implies s /. k = 0. L )
assume that
A18: k in dom s and
A19: k <> i ; ::_thesis: s /. k = 0. L
consider b1, b2 being bag of n such that
A20: (decomp ((HT (p,O)) + (HT (q,O)))) /. k = <*b1,b2*> and
A21: s /. k = (p . b1) * (q . b2) by A3, A18;
consider b19, b29 being bag of n such that
A22: (decomp ((HT (p,O)) + (HT (q,O)))) /. k = <*b19,b29*> and
A23: (HT (p,O)) + (HT (q,O)) = b19 + b29 by A12, A18, PRE_POLY:68;
A24: b2 = <*b19,b29*> . 2 by A22, A20, FINSEQ_1:44
.= b29 by FINSEQ_1:44 ;
A25: b1 = <*b19,b29*> . 1 by A22, A20, FINSEQ_1:44
.= b19 by FINSEQ_1:44 ;
A26: now__::_thesis:_(_p_._b1_<>_0._L_implies_not_q_._b2_<>_0._L_)
assume that
A27: p . b1 <> 0. L and
A28: q . b2 <> 0. L ; ::_thesis: contradiction
b1 is Element of Bags n by PRE_POLY:def_12;
then b1 in Support p by A27, POLYNOM1:def_3;
then b1 <= HT (p,O),O by Def6;
then A29: [b1,(HT (p,O))] in O by Def2;
b2 is Element of Bags n by PRE_POLY:def_12;
then b2 in Support q by A28, POLYNOM1:def_3;
then b2 <= HT (q,O),O by Def6;
then A30: [b2,(HT (q,O))] in O by Def2;
A31: now__::_thesis:_(_b1_=_HT_(p,O)_implies_not_b2_=_HT_(q,O)_)
assume ( b1 = HT (p,O) & b2 = HT (q,O) ) ; ::_thesis: contradiction
then (decomp ((HT (p,O)) + (HT (q,O)))) . k = <*(HT (p,O)),(HT (q,O))*> by A12, A18, A20, PARTFUN1:def_6
.= (decomp ((HT (p,O)) + (HT (q,O)))) /. i by A10, PRE_POLY:48
.= (decomp ((HT (p,O)) + (HT (q,O)))) . i by A9, PARTFUN1:def_6 ;
hence contradiction by A9, A12, A18, A19, FUNCT_1:def_4; ::_thesis: verum
end;
now__::_thesis:_(_(_b1_<>_HT_(p,O)_&_contradiction_)_or_(_b2_<>_HT_(q,O)_&_contradiction_)_)
percases ( b1 <> HT (p,O) or b2 <> HT (q,O) ) by A31;
caseA32: b1 <> HT (p,O) ; ::_thesis: contradiction
A33: now__::_thesis:_not_b1_+_b2_=_(HT_(p,O))_+_b2
assume b1 + b2 = (HT (p,O)) + b2 ; ::_thesis: contradiction
then b1 = ((HT (p,O)) + b2) -' b2 by PRE_POLY:48;
hence contradiction by A32, PRE_POLY:48; ::_thesis: verum
end;
A34: ( (HT (p,O)) + b2 is Element of Bags n & (HT (p,O)) + (HT (q,O)) is Element of Bags n ) by PRE_POLY:def_12;
( [((HT (p,O)) + (HT (q,O))),((HT (p,O)) + b2)] in O & [((HT (p,O)) + b2),((HT (p,O)) + (HT (q,O)))] in O ) by A23, A25, A24, A29, A30, BAGORDER:def_5;
hence contradiction by A23, A25, A24, A33, A34, ORDERS_1:4; ::_thesis: verum
end;
caseA35: b2 <> HT (q,O) ; ::_thesis: contradiction
A36: now__::_thesis:_not_b2_+_b1_=_(HT_(q,O))_+_b1
assume b2 + b1 = (HT (q,O)) + b1 ; ::_thesis: contradiction
then b2 = ((HT (q,O)) + b1) -' b1 by PRE_POLY:48;
hence contradiction by A35, PRE_POLY:48; ::_thesis: verum
end;
A37: ( (HT (q,O)) + b1 is Element of Bags n & (HT (p,O)) + (HT (q,O)) is Element of Bags n ) by PRE_POLY:def_12;
( [((HT (p,O)) + (HT (q,O))),((HT (q,O)) + b1)] in O & [((HT (q,O)) + b1),((HT (p,O)) + (HT (q,O)))] in O ) by A23, A25, A24, A29, A30, BAGORDER:def_5;
hence contradiction by A23, A25, A24, A36, A37, ORDERS_1:4; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
now__::_thesis:_(_(_p_._b1_=_0._L_&_(p_._b1)_*_(q_._b2)_=_0._L_)_or_(_q_._b2_=_0._L_&_(p_._b1)_*_(q_._b2)_=_0._L_)_)
percases ( p . b1 = 0. L or q . b2 = 0. L ) by A26;
case p . b1 = 0. L ; ::_thesis: (p . b1) * (q . b2) = 0. L
hence (p . b1) * (q . b2) = 0. L by BINOM:1; ::_thesis: verum
end;
case q . b2 = 0. L ; ::_thesis: (p . b1) * (q . b2) = 0. L
hence (p . b1) * (q . b2) = 0. L by BINOM:2; ::_thesis: verum
end;
end;
end;
hence s /. k = 0. L by A21; ::_thesis: verum
end;
b1 = <*(HT (p,O)),(HT (q,O))*> . 1 by A11, A14, FINSEQ_1:44
.= HT (p,O) by FINSEQ_1:44 ;
hence (p *' q) . ((HT (p,O)) + (HT (q,O))) = (p . (HT (p,O))) * (q . (HT (q,O))) by A1, A13, A17, A15, A16, POLYNOM2:3; ::_thesis: verum
end;
theorem Th29: :: TERMORD:29
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr
for p, q being non-zero Polynomial of n,L holds (HT (p,T)) + (HT (q,T)) in Support (p *' q)
proof
let n be Ordinal; ::_thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr
for p, q being non-zero Polynomial of n,L holds (HT (p,T)) + (HT (q,T)) in Support (p *' q)
let O be connected admissible TermOrder of n; ::_thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr
for p, q being non-zero Polynomial of n,L holds (HT (p,O)) + (HT (q,O)) in Support (p *' q)
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr ; ::_thesis: for p, q being non-zero Polynomial of n,L holds (HT (p,O)) + (HT (q,O)) in Support (p *' q)
let p, q be non-zero Polynomial of n,L; ::_thesis: (HT (p,O)) + (HT (q,O)) in Support (p *' q)
set b = (HT (p,O)) + (HT (q,O));
assume A1: not (HT (p,O)) + (HT (q,O)) in Support (p *' q) ; ::_thesis: contradiction
p <> 0_ (n,L) by POLYNOM7:def_1;
then Support p <> {} by POLYNOM7:1;
then HT (p,O) in Support p by Def6;
then A2: p . (HT (p,O)) <> 0. L by POLYNOM1:def_3;
q <> 0_ (n,L) by POLYNOM7:def_1;
then Support q <> {} by POLYNOM7:1;
then HT (q,O) in Support q by Def6;
then A3: q . (HT (q,O)) <> 0. L by POLYNOM1:def_3;
(HT (p,O)) + (HT (q,O)) is Element of Bags n by PRE_POLY:def_12;
then (p *' q) . ((HT (p,O)) + (HT (q,O))) = 0. L by A1, POLYNOM1:def_3;
then (p . (HT (p,O))) * (q . (HT (q,O))) = 0. L by Lm14;
hence contradiction by A2, A3, VECTSP_2:def_1; ::_thesis: verum
end;
theorem Th30: :: TERMORD:30
for n being Ordinal
for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of n,L holds Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) }
proof
let n be Ordinal; ::_thesis: for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of n,L holds Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) }
let L be non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of n,L holds Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) }
let p, q be Polynomial of n,L; ::_thesis: Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) }
A1: now__::_thesis:_for_b_being_bag_of_n_st_b_in_Support_(p_*'_q)_holds_
ex_s,_t_being_bag_of_n_st_
(_s_in_Support_p_&_t_in_Support_q_&_b_=_s_+_t_)
let b be bag of n; ::_thesis: ( b in Support (p *' q) implies ex s, t being bag of n st
( s in Support p & t in Support q & b = s + t ) )
consider s being FinSequence of L such that
A2: (p *' q) . b = Sum s and
A3: len s = len (decomp b) and
A4: 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) ) by POLYNOM1:def_9;
A5: dom s = Seg (len (decomp b)) by A3, FINSEQ_1:def_3
.= dom (decomp b) by FINSEQ_1:def_3 ;
assume A6: b in Support (p *' q) ; ::_thesis: ex s, t being bag of n st
( s in Support p & t in Support q & b = s + t )
now__::_thesis:_(_(_dom_s_=_{}_&_contradiction_)_or_(_dom_s_<>_{}_&_ex_s,_t_being_bag_of_n_st_
(_s_in_Support_p_&_t_in_Support_q_&_b_=_s_+_t_)_)_)
percases ( dom s = {} or dom s <> {} ) ;
case dom s = {} ; ::_thesis: contradiction
then Seg (len s) = {} by FINSEQ_1:def_3;
then len s = 0 ;
hence contradiction by A3; ::_thesis: verum
end;
caseA7: dom s <> {} ; ::_thesis: ex s, t being bag of n st
( s in Support p & t in Support q & b = s + t )
set k = the Element of dom s;
the Element of dom s in dom s by A7;
then reconsider k = the Element of dom s as Element of NAT ;
now__::_thesis:_ex_k_being_Element_of_dom_(decomp_b)_ex_b1,_b2_being_bag_of_n_st_
(_(decomp_b)_/._k_=_<*b1,b2*>_&_p_._b1_<>_0._L_&_q_._b2_<>_0._L_)
assume A8: for k being Element of dom (decomp b)
for b1, b2 being bag of n holds
( not (decomp b) /. k = <*b1,b2*> or not p . b1 <> 0. L or not q . b2 <> 0. L ) ; ::_thesis: contradiction
A9: for k being Nat st k in dom s holds
s /. k = 0. L
proof
let k be Nat; ::_thesis: ( k in dom s implies s /. k = 0. L )
assume A10: k in dom s ; ::_thesis: s /. k = 0. L
then consider b1, b2 being bag of n such that
A11: (decomp b) /. k = <*b1,b2*> and
A12: s /. k = (p . b1) * (q . b2) by A4;
now__::_thesis:_(_(_p_._b1_=_0._L_&_s_/._k_=_0._L_)_or_(_q_._b2_=_0._L_&_s_/._k_=_0._L_)_)
percases ( p . b1 = 0. L or q . b2 = 0. L ) by A5, A8, A10, A11;
case p . b1 = 0. L ; ::_thesis: s /. k = 0. L
hence s /. k = 0. L by A12, BINOM:1; ::_thesis: verum
end;
case q . b2 = 0. L ; ::_thesis: s /. k = 0. L
hence s /. k = 0. L by A12, BINOM:2; ::_thesis: verum
end;
end;
end;
hence s /. k = 0. L ; ::_thesis: verum
end;
then for k9 being Element of NAT st k9 in dom s & k9 <> k holds
s /. k9 = 0. L ;
then Sum s = s /. k by A7, POLYNOM2:3
.= 0. L by A7, A9 ;
hence contradiction by A6, A2, POLYNOM1:def_3; ::_thesis: verum
end;
then consider k being Element of dom (decomp b), b1, b2 being bag of n such that
A13: (decomp b) /. k = <*b1,b2*> and
A14: p . b1 <> 0. L and
A15: q . b2 <> 0. L ;
k in dom (decomp b) by A5, A7;
then reconsider k = k as Element of NAT ;
consider b19, b29 being bag of n such that
A16: (decomp b) /. k = <*b19,b29*> and
A17: b = b19 + b29 by A5, A7, PRE_POLY:68;
A18: b29 = <*b1,b2*> . 2 by A13, A16, FINSEQ_1:44
.= b2 by FINSEQ_1:44 ;
b2 is Element of Bags n by PRE_POLY:def_12;
then A19: b2 in Support q by A15, POLYNOM1:def_3;
b1 is Element of Bags n by PRE_POLY:def_12;
then A20: b1 in Support p by A14, POLYNOM1:def_3;
b19 = <*b1,b2*> . 1 by A13, A16, FINSEQ_1:44
.= b1 by FINSEQ_1:44 ;
hence ex s, t being bag of n st
( s in Support p & t in Support q & b = s + t ) by A20, A19, A17, A18; ::_thesis: verum
end;
end;
end;
hence ex s, t being bag of n st
( s in Support p & t in Support q & b = s + t ) ; ::_thesis: verum
end;
now__::_thesis:_for_u_being_set_st_u_in_Support_(p_*'_q)_holds_
u_in__{__(s9_+_t9)_where_s9,_t9_is_Element_of_Bags_n_:_(_s9_in_Support_p_&_t9_in_Support_q_)__}_
let u be set ; ::_thesis: ( u in Support (p *' q) implies u in { (s9 + t9) where s9, t9 is Element of Bags n : ( s9 in Support p & t9 in Support q ) } )
assume A21: u in Support (p *' q) ; ::_thesis: u in { (s9 + t9) where s9, t9 is Element of Bags n : ( s9 in Support p & t9 in Support q ) }
then reconsider u9 = u as Element of Bags n ;
ex s, t being bag of n st
( s in Support p & t in Support q & u9 = s + t ) by A1, A21;
hence u in { (s9 + t9) where s9, t9 is Element of Bags n : ( s9 in Support p & t9 in Support q ) } ; ::_thesis: verum
end;
hence Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) } by TARSKI:def_3; ::_thesis: verum
end;
theorem Th31: :: TERMORD:31
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HT ((p *' q),T) = (HT (p,T)) + (HT (q,T))
proof
let n be Ordinal; ::_thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HT ((p *' q),T) = (HT (p,T)) + (HT (q,T))
let O be connected admissible TermOrder of n; ::_thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HT ((p *' q),O) = (HT (p,O)) + (HT (q,O))
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p, q being non-zero Polynomial of n,L holds HT ((p *' q),O) = (HT (p,O)) + (HT (q,O))
let p, q be non-zero Polynomial of n,L; ::_thesis: HT ((p *' q),O) = (HT (p,O)) + (HT (q,O))
A1: (HT (p,O)) + (HT (q,O)) is Element of Bags n by PRE_POLY:def_12;
(HT (p,O)) + (HT (q,O)) in Support (p *' q) by Th29;
then (HT (p,O)) + (HT (q,O)) <= HT ((p *' q),O),O by Def6;
then A2: [((HT (p,O)) + (HT (q,O))),(HT ((p *' q),O))] in O by Def2;
Support (p *' q) <> {} by Th29;
then A3: HT ((p *' q),O) in Support (p *' q) by Def6;
Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) } by Th30;
then HT ((p *' q),O) in { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) } by A3;
then consider s, t being Element of Bags n such that
A4: HT ((p *' q),O) = s + t and
A5: s in Support p and
A6: t in Support q ;
s <= HT (p,O),O by A5, Def6;
then [s,(HT (p,O))] in O by Def2;
then A7: [(s + t),((HT (p,O)) + t)] in O by BAGORDER:def_5;
t <= HT (q,O),O by A6, Def6;
then [t,(HT (q,O))] in O by Def2;
then A8: [(t + (HT (p,O))),((HT (p,O)) + (HT (q,O)))] in O by BAGORDER:def_5;
( s + t is Element of Bags n & (HT (p,O)) + t is Element of Bags n ) by PRE_POLY:def_12;
then [(s + t),((HT (p,O)) + (HT (q,O)))] in O by A1, A7, A8, ORDERS_1:5;
hence HT ((p *' q),O) = (HT (p,O)) + (HT (q,O)) by A2, A4, A1, ORDERS_1:4; ::_thesis: verum
end;
theorem Th32: :: TERMORD:32
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HC ((p *' q),T) = (HC (p,T)) * (HC (q,T))
proof
let n be Ordinal; ::_thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HC ((p *' q),T) = (HC (p,T)) * (HC (q,T))
let O be connected admissible TermOrder of n; ::_thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HC ((p *' q),O) = (HC (p,O)) * (HC (q,O))
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p, q being non-zero Polynomial of n,L holds HC ((p *' q),O) = (HC (p,O)) * (HC (q,O))
let p, q be non-zero Polynomial of n,L; ::_thesis: HC ((p *' q),O) = (HC (p,O)) * (HC (q,O))
thus HC ((p *' q),O) = (p *' q) . ((HT (p,O)) + (HT (q,O))) by Th31
.= (HC (p,O)) * (HC (q,O)) by Lm14 ; ::_thesis: verum
end;
theorem :: TERMORD:33
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HM ((p *' q),T) = (HM (p,T)) *' (HM (q,T))
proof
let n be Ordinal; ::_thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HM ((p *' q),T) = (HM (p,T)) *' (HM (q,T))
let O be connected admissible TermOrder of n; ::_thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HM ((p *' q),O) = (HM (p,O)) *' (HM (q,O))
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p, q being non-zero Polynomial of n,L holds HM ((p *' q),O) = (HM (p,O)) *' (HM (q,O))
let p, q be non-zero Polynomial of n,L; ::_thesis: HM ((p *' q),O) = (HM (p,O)) *' (HM (q,O))
thus HM ((p *' q),O) = Monom (((HC (p,O)) * (HC (q,O))),(HT ((p *' q),O))) by Th32
.= Monom (((HC (p,O)) * (HC (q,O))),((HT (p,O)) + (HT (q,O)))) by Th31
.= (HM (p,O)) *' (HM (q,O)) by Th3 ; ::_thesis: verum
end;
theorem :: TERMORD:34
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of n,L holds HT ((p + q),T) <= max ((HT (p,T)),(HT (q,T)),T),T
proof
let n be Ordinal; ::_thesis: for T being connected admissible TermOrder of n
for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of n,L holds HT ((p + q),T) <= max ((HT (p,T)),(HT (q,T)),T),T
let O be connected admissible TermOrder of n; ::_thesis: for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of n,L holds HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O
let L be non empty right_zeroed addLoopStr ; ::_thesis: for p, q being Polynomial of n,L holds HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O
let p, q be Polynomial of n,L; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O
percases ( HT ((p + q),O) in Support (p + q) or not HT ((p + q),O) in Support (p + q) ) ;
supposeA1: HT ((p + q),O) in Support (p + q) ; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O
A2: Support (p + q) c= (Support p) \/ (Support q) by POLYNOM1:20;
now__::_thesis:_(_(_HT_((p_+_q),O)_in_Support_p_&_HT_((p_+_q),O)_<=_max_((HT_(p,O)),(HT_(q,O)),O),O_)_or_(_HT_((p_+_q),O)_in_Support_q_&_HT_((p_+_q),O)_<=_max_((HT_(p,O)),(HT_(q,O)),O),O_)_)
percases ( HT ((p + q),O) in Support p or HT ((p + q),O) in Support q ) by A1, A2, XBOOLE_0:def_3;
caseA3: HT ((p + q),O) in Support p ; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O
then A4: HT ((p + q),O) <= HT (p,O),O by Def6;
now__::_thesis:_(_(_max_((HT_(p,O)),(HT_(q,O)),O)_=_HT_(p,O)_&_HT_((p_+_q),O)_<=_max_((HT_(p,O)),(HT_(q,O)),O),O_)_or_(_max_((HT_(p,O)),(HT_(q,O)),O)_=_HT_(q,O)_&_HT_((p_+_q),O)_<=_max_((HT_(p,O)),(HT_(q,O)),O),O_)_)
percases ( max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) or max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) ) by Th12;
case max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) ; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O
hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O by A3, Def6; ::_thesis: verum
end;
caseA5: max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) ; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O
then HT (p,O) <= HT (q,O),O by Th14;
hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O by A4, A5, Th8; ::_thesis: verum
end;
end;
end;
hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ; ::_thesis: verum
end;
caseA6: HT ((p + q),O) in Support q ; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O
then A7: HT ((p + q),O) <= HT (q,O),O by Def6;
now__::_thesis:_(_(_max_((HT_(p,O)),(HT_(q,O)),O)_=_HT_(q,O)_&_HT_((p_+_q),O)_<=_max_((HT_(p,O)),(HT_(q,O)),O),O_)_or_(_max_((HT_(p,O)),(HT_(q,O)),O)_=_HT_(p,O)_&_HT_((p_+_q),O)_<=_max_((HT_(p,O)),(HT_(q,O)),O),O_)_)
percases ( max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) or max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) ) by Th12;
case max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) ; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O
hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O by A6, Def6; ::_thesis: verum
end;
caseA8: max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) ; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O
then HT (q,O) <= HT (p,O),O by Th14;
hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O by A7, A8, Th8; ::_thesis: verum
end;
end;
end;
hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ; ::_thesis: verum
end;
end;
end;
hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ; ::_thesis: verum
end;
suppose not HT ((p + q),O) in Support (p + q) ; ::_thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O
then HT ((p + q),O) = EmptyBag n by Def6;
then [(HT ((p + q),O)),(max ((HT (p,O)),(HT (q,O)),O))] in O by BAGORDER:def_5;
hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O by Def2; ::_thesis: verum
end;
end;
end;
begin
definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p be Polynomial of n,L;
func Red (p,T) -> Polynomial of n,L equals :: TERMORD:def 9
p - (HM (p,T));
coherence
p - (HM (p,T)) is Polynomial of n,L ;
end;
:: deftheorem defines Red TERMORD:def_9_:_
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Red (p,T) = p - (HM (p,T));
Lm15: for n being Ordinal
for O being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds not HT (p,O) in Support (Red (p,O))
proof
let n be Ordinal; ::_thesis: for O being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds not HT (p,O) in Support (Red (p,O))
let O be connected TermOrder of n; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds not HT (p,O) in Support (Red (p,O))
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of n,L holds not HT (p,O) in Support (Red (p,O))
let p be Polynomial of n,L; ::_thesis: not HT (p,O) in Support (Red (p,O))
assume HT (p,O) in Support (Red (p,O)) ; ::_thesis: contradiction
then (Red (p,O)) . (HT (p,O)) <> 0. L by POLYNOM1:def_3;
then (p + (- (HM (p,O)))) . (HT (p,O)) <> 0. L by POLYNOM1:def_6;
then (p . (HT (p,O))) + ((- (HM (p,O))) . (HT (p,O))) <> 0. L by POLYNOM1:15;
then A1: (p . (HT (p,O))) + (- ((HM (p,O)) . (HT (p,O)))) <> 0. L by POLYNOM1:17;
(HM (p,O)) . (HT (p,O)) = p . (HT (p,O)) by Lm8;
hence contradiction by A1, RLVECT_1:def_10; ::_thesis: verum
end;
Lm16: for n being Ordinal
for O being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for b being bag of n st b in Support p & b <> HT (p,O) holds
b in Support (Red (p,O))
proof
let n be Ordinal; ::_thesis: for O being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for b being bag of n st b in Support p & b <> HT (p,O) holds
b in Support (Red (p,O))
let O be connected TermOrder of n; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for b being bag of n st b in Support p & b <> HT (p,O) holds
b in Support (Red (p,O))
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of n,L
for b being bag of n st b in Support p & b <> HT (p,O) holds
b in Support (Red (p,O))
let p be Polynomial of n,L; ::_thesis: for b being bag of n st b in Support p & b <> HT (p,O) holds
b in Support (Red (p,O))
let b be bag of n; ::_thesis: ( b in Support p & b <> HT (p,O) implies b in Support (Red (p,O)) )
assume that
A1: b in Support p and
A2: b <> HT (p,O) ; ::_thesis: b in Support (Red (p,O))
(Red (p,O)) . b = (p + (- (HM (p,O)))) . b by POLYNOM1:def_6
.= (p . b) + ((- (HM (p,O))) . b) by POLYNOM1:15
.= (p . b) + (- ((HM (p,O)) . b)) by POLYNOM1:17
.= (p . b) + (- (0. L)) by A2, Th19
.= (p . b) + (0. L) by RLVECT_1:12
.= p . b by RLVECT_1:4 ;
then ( b is Element of Bags n & (Red (p,O)) . b <> 0. L ) by A1, POLYNOM1:def_3;
hence b in Support (Red (p,O)) by POLYNOM1:def_3; ::_thesis: verum
end;
Lm17: for n being Ordinal
for O being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Support (Red (p,O)) = (Support p) \ {(HT (p,O))}
proof
let n be Ordinal; ::_thesis: for O being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Support (Red (p,O)) = (Support p) \ {(HT (p,O))}
let O be connected TermOrder of n; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Support (Red (p,O)) = (Support p) \ {(HT (p,O))}
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of n,L holds Support (Red (p,O)) = (Support p) \ {(HT (p,O))}
let p be Polynomial of n,L; ::_thesis: Support (Red (p,O)) = (Support p) \ {(HT (p,O))}
A1: now__::_thesis:_for_u_being_set_st_u_in_Support_(Red_(p,O))_holds_
u_in_(Support_p)_\_{(HT_(p,O))}
let u be set ; ::_thesis: ( u in Support (Red (p,O)) implies u in (Support p) \ {(HT (p,O))} )
assume A2: u in Support (Red (p,O)) ; ::_thesis: u in (Support p) \ {(HT (p,O))}
then reconsider u9 = u as Element of Bags n ;
reconsider u9 = u9 as bag of n ;
A3: (p - (HM (p,O))) . u9 <> 0. L by A2, POLYNOM1:def_3;
A4: not u9 = HT (p,O) by A2, Lm15;
(p + (- (HM (p,O)))) . u9 = (p . u9) + ((- (HM (p,O))) . u9) by POLYNOM1:15
.= (p . u9) + (- ((HM (p,O)) . u9)) by POLYNOM1:17 ;
then (p + (- (HM (p,O)))) . u9 = (p . u9) + (- (0. L)) by A4, Th19
.= (p . u9) + (0. L) by RLVECT_1:12
.= p . u9 by RLVECT_1:4 ;
then p . u9 <> 0. L by A3, POLYNOM1:def_6;
then A5: u9 in Support p by POLYNOM1:def_3;
not u9 in {(HT (p,O))} by A4, TARSKI:def_1;
hence u in (Support p) \ {(HT (p,O))} by A5, XBOOLE_0:def_5; ::_thesis: verum
end;
now__::_thesis:_for_u_being_set_st_u_in_(Support_p)_\_{(HT_(p,O))}_holds_
u_in_Support_(Red_(p,O))
let u be set ; ::_thesis: ( u in (Support p) \ {(HT (p,O))} implies u in Support (Red (p,O)) )
assume A6: u in (Support p) \ {(HT (p,O))} ; ::_thesis: u in Support (Red (p,O))
then reconsider u9 = u as Element of Bags n ;
reconsider u9 = u9 as bag of n ;
not u in {(HT (p,O))} by A6, XBOOLE_0:def_5;
then A7: u9 <> HT (p,O) by TARSKI:def_1;
u in Support p by A6, XBOOLE_0:def_5;
hence u in Support (Red (p,O)) by A7, Lm16; ::_thesis: verum
end;
hence Support (Red (p,O)) = (Support p) \ {(HT (p,O))} by A1, TARSKI:1; ::_thesis: verum
end;
theorem :: TERMORD:35
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Support (Red (p,T)) c= Support p
proof
let n be Ordinal; ::_thesis: for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Support (Red (p,T)) c= Support p
let O be connected TermOrder of n; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Support (Red (p,O)) c= Support p
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of n,L holds Support (Red (p,O)) c= Support p
let p be Polynomial of n,L; ::_thesis: Support (Red (p,O)) c= Support p
Support (Red (p,O)) = (Support p) \ {(HT (p,O))} by Lm17;
hence Support (Red (p,O)) c= Support p by XBOOLE_1:36; ::_thesis: verum
end;
theorem :: TERMORD:36
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Support (Red (p,T)) = (Support p) \ {(HT (p,T))} by Lm17;
Lm18: for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds (Red (p,T)) . (HT (p,T)) = 0. L
proof
let n be Ordinal; ::_thesis: for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds (Red (p,T)) . (HT (p,T)) = 0. L
let O be connected TermOrder of n; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds (Red (p,O)) . (HT (p,O)) = 0. L
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of n,L holds (Red (p,O)) . (HT (p,O)) = 0. L
let p be Polynomial of n,L; ::_thesis: (Red (p,O)) . (HT (p,O)) = 0. L
( HT (p,O) in {(HT (p,O))} & Support (Red (p,O)) = (Support p) \ {(HT (p,O))} ) by Lm17, TARSKI:def_1;
then not HT (p,O) in Support (Red (p,O)) by XBOOLE_0:def_5;
hence (Red (p,O)) . (HT (p,O)) = 0. L by POLYNOM1:def_3; ::_thesis: verum
end;
Lm19: for n being Ordinal
for O being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for b being bag of n st b <> HT (p,O) holds
(Red (p,O)) . b = p . b
proof
let n be Ordinal; ::_thesis: for O being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for b being bag of n st b <> HT (p,O) holds
(Red (p,O)) . b = p . b
let O be connected TermOrder of n; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for b being bag of n st b <> HT (p,O) holds
(Red (p,O)) . b = p . b
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of n,L
for b being bag of n st b <> HT (p,O) holds
(Red (p,O)) . b = p . b
let p be Polynomial of n,L; ::_thesis: for b being bag of n st b <> HT (p,O) holds
(Red (p,O)) . b = p . b
let b be bag of n; ::_thesis: ( b <> HT (p,O) implies (Red (p,O)) . b = p . b )
A1: b is Element of Bags n by PRE_POLY:def_12;
assume b <> HT (p,O) ; ::_thesis: (Red (p,O)) . b = p . b
then not b in {(HT (p,O))} by TARSKI:def_1;
then A2: not b in Support (HM (p,O)) by Lm12;
thus (Red (p,O)) . b = (p + (- (HM (p,O)))) . b by POLYNOM1:def_6
.= (p . b) + ((- (HM (p,O))) . b) by POLYNOM1:15
.= (p . b) + (- ((HM (p,O)) . b)) by POLYNOM1:17
.= (p . b) + (- (0. L)) by A2, A1, POLYNOM1:def_3
.= (p . b) + (0. L) by RLVECT_1:12
.= p . b by RLVECT_1:4 ; ::_thesis: verum
end;
theorem :: TERMORD:37
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Support ((HM (p,T)) + (Red (p,T))) = Support p
proof
let n be Ordinal; ::_thesis: for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Support ((HM (p,T)) + (Red (p,T))) = Support p
let O be connected TermOrder of n; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Support ((HM (p,O)) + (Red (p,O))) = Support p
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of n,L holds Support ((HM (p,O)) + (Red (p,O))) = Support p
let p be Polynomial of n,L; ::_thesis: Support ((HM (p,O)) + (Red (p,O))) = Support p
A1: now__::_thesis:_for_u_being_set_st_u_in_Support_p_holds_
u_in_Support_((HM_(p,O))_+_(Red_(p,O)))
let u be set ; ::_thesis: ( u in Support p implies u in Support ((HM (p,O)) + (Red (p,O))) )
assume A2: u in Support p ; ::_thesis: u in Support ((HM (p,O)) + (Red (p,O)))
then reconsider u9 = u as Element of Bags n ;
reconsider u9 = u9 as bag of n ;
A3: p . u9 <> 0. L by A2, POLYNOM1:def_3;
now__::_thesis:_(_(_u9_=_HT_(p,O)_&_u9_in_Support_((HM_(p,O))_+_(Red_(p,O)))_)_or_(_u9_<>_HT_(p,O)_&_u9_in_Support_((HM_(p,O))_+_(Red_(p,O)))_)_)
percases ( u9 = HT (p,O) or u9 <> HT (p,O) ) ;
caseA4: u9 = HT (p,O) ; ::_thesis: u9 in Support ((HM (p,O)) + (Red (p,O)))
then A5: p . (HT (p,O)) <> 0. L by A2, POLYNOM1:def_3;
((HM (p,O)) + (Red (p,O))) . u9 = ((HM (p,O)) . u9) + ((Red (p,O)) . u9) by POLYNOM1:15
.= ((HM (p,O)) . u9) + (0. L) by A4, Lm18
.= (HM (p,O)) . u9 by RLVECT_1:4
.= HC (p,O) by A4, Lm8 ;
hence u9 in Support ((HM (p,O)) + (Red (p,O))) by A5, POLYNOM1:def_3; ::_thesis: verum
end;
caseA6: u9 <> HT (p,O) ; ::_thesis: u9 in Support ((HM (p,O)) + (Red (p,O)))
((HM (p,O)) + (Red (p,O))) . u9 = ((HM (p,O)) . u9) + ((Red (p,O)) . u9) by POLYNOM1:15
.= ((HM (p,O)) . u9) + (p . u9) by A6, Lm19
.= (0. L) + (p . u9) by A6, Th19
.= p . u9 by RLVECT_1:4 ;
hence u9 in Support ((HM (p,O)) + (Red (p,O))) by A3, POLYNOM1:def_3; ::_thesis: verum
end;
end;
end;
hence u in Support ((HM (p,O)) + (Red (p,O))) ; ::_thesis: verum
end;
now__::_thesis:_for_u_being_set_st_u_in_Support_((HM_(p,O))_+_(Red_(p,O)))_holds_
u_in_Support_p
let u be set ; ::_thesis: ( u in Support ((HM (p,O)) + (Red (p,O))) implies u in Support p )
assume A7: u in Support ((HM (p,O)) + (Red (p,O))) ; ::_thesis: u in Support p
then reconsider u9 = u as Element of Bags n ;
reconsider u9 = u9 as bag of n ;
A8: ((HM (p,O)) + (Red (p,O))) . u9 <> 0. L by A7, POLYNOM1:def_3;
now__::_thesis:_(_(_u9_=_HT_(p,O)_&_u9_in_Support_p_)_or_(_u9_<>_HT_(p,O)_&_u9_in_Support_p_)_)
percases ( u9 = HT (p,O) or u9 <> HT (p,O) ) ;
caseA9: u9 = HT (p,O) ; ::_thesis: u9 in Support p
((HM (p,O)) + (Red (p,O))) . u9 = ((HM (p,O)) . u9) + ((Red (p,O)) . u9) by POLYNOM1:15
.= ((HM (p,O)) . (HT (p,O))) + (0. L) by A9, Lm18
.= (HM (p,O)) . (HT (p,O)) by RLVECT_1:4
.= p . u9 by A9, Lm8 ;
hence u9 in Support p by A8, POLYNOM1:def_3; ::_thesis: verum
end;
caseA10: u9 <> HT (p,O) ; ::_thesis: u9 in Support p
((HM (p,O)) + (Red (p,O))) . u9 = ((HM (p,O)) . u9) + ((Red (p,O)) . u9) by POLYNOM1:15
.= (0. L) + ((Red (p,O)) . u9) by A10, Th19
.= (Red (p,O)) . u9 by RLVECT_1:4
.= p . u by A10, Lm19 ;
hence u9 in Support p by A8, POLYNOM1:def_3; ::_thesis: verum
end;
end;
end;
hence u in Support p ; ::_thesis: verum
end;
hence Support ((HM (p,O)) + (Red (p,O))) = Support p by A1, TARSKI:1; ::_thesis: verum
end;
theorem :: TERMORD:38
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds (HM (p,T)) + (Red (p,T)) = p
proof
let n be Ordinal; ::_thesis: for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds (HM (p,T)) + (Red (p,T)) = p
let O be connected TermOrder of n; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds (HM (p,O)) + (Red (p,O)) = p
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of n,L holds (HM (p,O)) + (Red (p,O)) = p
let p be Polynomial of n,L; ::_thesis: (HM (p,O)) + (Red (p,O)) = p
A1: now__::_thesis:_for_x_being_set_st_x_in_Bags_n_holds_
p_._x_=_((HM_(p,O))_+_(Red_(p,O)))_._x
let x be set ; ::_thesis: ( x in Bags n implies p . x = ((HM (p,O)) + (Red (p,O))) . x )
assume x in Bags n ; ::_thesis: p . x = ((HM (p,O)) + (Red (p,O))) . x
then reconsider x9 = x as Element of Bags n ;
now__::_thesis:_(_(_x_=_HT_(p,O)_&_((HM_(p,O))_+_(Red_(p,O)))_._x_=_p_._x_)_or_(_x_<>_HT_(p,O)_&_p_._x_=_((HM_(p,O))_+_(Red_(p,O)))_._x_)_)
percases ( x = HT (p,O) or x <> HT (p,O) ) ;
caseA2: x = HT (p,O) ; ::_thesis: ((HM (p,O)) + (Red (p,O))) . x = p . x
hence ((HM (p,O)) + (Red (p,O))) . x = ((HM (p,O)) . (HT (p,O))) + ((Red (p,O)) . (HT (p,O))) by POLYNOM1:15
.= ((HM (p,O)) . (HT (p,O))) + (0. L) by Lm18
.= (HM (p,O)) . (HT (p,O)) by RLVECT_1:4
.= p . x by A2, Lm8 ;
::_thesis: verum
end;
caseA3: x <> HT (p,O) ; ::_thesis: p . x = ((HM (p,O)) + (Red (p,O))) . x
((HM (p,O)) + (Red (p,O))) . x9 = ((HM (p,O)) . x9) + ((Red (p,O)) . x9) by POLYNOM1:15
.= ((HM (p,O)) . x9) + (p . x9) by A3, Lm19
.= (0. L) + (p . x9) by A3, Th19
.= p . x9 by RLVECT_1:4 ;
hence p . x = ((HM (p,O)) + (Red (p,O))) . x ; ::_thesis: verum
end;
end;
end;
hence p . x = ((HM (p,O)) + (Red (p,O))) . x ; ::_thesis: verum
end;
( dom p = Bags n & dom ((HM (p,O)) + (Red (p,O))) = Bags n ) by FUNCT_2:def_1;
hence (HM (p,O)) + (Red (p,O)) = p by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem :: TERMORD:39
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds (Red (p,T)) . (HT (p,T)) = 0. L by Lm18;
theorem :: TERMORD:40
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for b being bag of n st b in Support p & b <> HT (p,T) holds
(Red (p,T)) . b = p . b by Lm19;