let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of n,L st HT p1,T, HT p2,T are_disjoint holds
for b1, b2 being bag of st b1 in Support p1 & b2 in Support p2 & ( not b1 = HT p1,T or not b2 = HT p2,T ) holds
not (HT p1,T) + b2 = (HT p2,T) + b1
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of n,L st HT p1,T, HT p2,T are_disjoint holds
for b1, b2 being bag of st b1 in Support p1 & b2 in Support p2 & ( not b1 = HT p1,T or not b2 = HT p2,T ) holds
not (HT p1,T) + b2 = (HT p2,T) + b1
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p1, p2 being Polynomial of n,L st HT p1,T, HT p2,T are_disjoint holds
for b1, b2 being bag of st b1 in Support p1 & b2 in Support p2 & ( not b1 = HT p1,T or not b2 = HT p2,T ) holds
not (HT p1,T) + b2 = (HT p2,T) + b1
let p1, p2 be Polynomial of n,L; :: thesis: ( HT p1,T, HT p2,T are_disjoint implies for b1, b2 being bag of st b1 in Support p1 & b2 in Support p2 & ( not b1 = HT p1,T or not b2 = HT p2,T ) holds
not (HT p1,T) + b2 = (HT p2,T) + b1 )
assume A1:
HT p1,T, HT p2,T are_disjoint
; :: thesis: for b1, b2 being bag of st b1 in Support p1 & b2 in Support p2 & ( not b1 = HT p1,T or not b2 = HT p2,T ) holds
not (HT p1,T) + b2 = (HT p2,T) + b1
let b1, b2 be bag of ; :: thesis: ( b1 in Support p1 & b2 in Support p2 & ( not b1 = HT p1,T or not b2 = HT p2,T ) implies not (HT p1,T) + b2 = (HT p2,T) + b1 )
assume
( b1 in Support p1 & b2 in Support p2 )
; :: thesis: ( ( b1 = HT p1,T & b2 = HT p2,T ) or not (HT p1,T) + b2 = (HT p2,T) + b1 )
then
( b1 <= HT p1,T,T & b2 <= HT p2,T,T )
by TERMORD:def 6;
then A2:
( (HT p2,T) + b1 <= (HT p1,T) + (HT p2,T),T & (HT p1,T) + b2 <= (HT p1,T) + (HT p2,T),T )
by Th2;
assume A3:
( not b1 = HT p1,T or not b2 = HT p2,T )
; :: thesis: not (HT p1,T) + b2 = (HT p2,T) + b1
assume
(HT p1,T) + b2 = (HT p2,T) + b1
; :: thesis: contradiction
then A4:
( HT p2,T divides (HT p1,T) + b2 & HT p1,T divides (HT p2,T) + b1 )
by POLYNOM1:54;
now per cases
( not b1 = HT p1,T or not b2 = HT p2,T )
by A3;
case A5:
not
b1 = HT p1,
T
;
:: thesis: contradiction
HT p2,
T divides (HT p2,T) + b1
by POLYNOM1:54;
then
lcm (HT p1,T),
(HT p2,T) divides (HT p2,T) + b1
by A4, GROEB_2:8;
then
(HT p1,T) + (HT p2,T) divides (HT p2,T) + b1
by A1, GROEB_2:9;
then
(HT p1,T) + (HT p2,T) <= (HT p2,T) + b1,
T
by TERMORD:10;
then A6:
(HT p1,T) + (HT p2,T) = (HT p2,T) + b1
by A2, TERMORD:7;
HT p1,
T = ((HT p1,T) + (HT p2,T)) -' (HT p2,T)
by POLYNOM1:52;
hence
contradiction
by A5, A6, POLYNOM1:52;
:: thesis: verum end; case A7:
not
b2 = HT p2,
T
;
:: thesis: contradiction
HT p1,
T divides (HT p1,T) + b2
by POLYNOM1:54;
then
lcm (HT p1,T),
(HT p2,T) divides (HT p1,T) + b2
by A4, GROEB_2:8;
then
(HT p1,T) + (HT p2,T) divides (HT p1,T) + b2
by A1, GROEB_2:9;
then
(HT p1,T) + (HT p2,T) <= (HT p1,T) + b2,
T
by TERMORD:10;
then A8:
(HT p1,T) + (HT p2,T) = (HT p1,T) + b2
by A2, TERMORD:7;
HT p2,
T = ((HT p1,T) + (HT p2,T)) -' (HT p1,T)
by POLYNOM1:52;
hence
contradiction
by A7, A8, POLYNOM1:52;
:: thesis: verum end;
hence
contradiction
; :: thesis: verum