let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
for b being bag of n st b in Support g holds
b <= HT (f,T),T
let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
for b being bag of n st b in Support g holds
b <= HT (f,T),T
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
for b being bag of n st b in Support g holds
b <= HT (f,T),T
let f, p, g be Polynomial of n,L; :: thesis: ( f reduces_to g,p,T implies for b being bag of n st b in Support g holds
b <= HT (f,T),T )
A1: T is_connected_in field T by RELAT_2:def 14;
assume f reduces_to g,p,T ; :: thesis: for b being bag of n st b in Support g holds
b <= HT (f,T),T
then consider b being bag of n such that
A2: f reduces_to g,p,b,T ;
b in Support f by A2;
then A3: b <= HT (f,T),T by TERMORD:def 6;
now :: thesis: for u being bag of n st u in Support g holds
u <= HT (f,T),T
let u be bag of n; :: thesis: ( u in Support g implies u <= HT (f,T),T )
assume A4: u in Support g ; :: thesis: u <= HT (f,T),T
now :: thesis: ( ( u = b & contradiction ) or ( u <> b & u <= HT (f,T),T ) )
per cases ( u = b or u <> b ) ;
case A5: u <> b ; :: thesis: u <= HT (f,T),T
b <= b,T by TERMORD:6;
then [b,b] in T by TERMORD:def 2;
then A6: b in field T by RELAT_1:15;
u <= u,T by TERMORD:6;
then [u,u] in T by TERMORD:def 2;
then u in field T by RELAT_1:15;
then A7: ( [u,b] in T or [b,u] in T ) by A1, A5, A6, RELAT_2:def 6;
now :: thesis: ( ( u <= b,T & u <= HT (f,T),T ) or ( b <= u,T & u <= HT (f,T),T ) )
per cases ( u <= b,T or b <= u,T ) by A7, TERMORD:def 2;
case u <= b,T ; :: thesis: u <= HT (f,T),T
hence u <= HT (f,T),T by A3, TERMORD:8; :: thesis: verum
end;
case b <= u,T ; :: thesis: u <= HT (f,T),T
then b < u,T by A5, TERMORD:def 3;
then ( u in Support f iff u in Support g ) by A2, Th40;
hence u <= HT (f,T),T by A4, TERMORD:def 6; :: thesis: verum
end;
end;
end;
hence u <= HT (f,T),T ; :: thesis: verum
end;
end;
end;
hence u <= HT (f,T),T ; :: thesis: verum
end;
hence for b being bag of n st b in Support g holds
b <= HT (f,T),T ; :: thesis: verum