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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
g < f,T
let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
g < f,T
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
g < f,T
let f, p, g be Polynomial of n,L; :: thesis: ( f reduces_to g,p,T implies g < f,T )
set R = RelStr(# (Bags n),T #);
defpred S₁[ Nat] means for f, p, g being Polynomial of n,L st card (Support f) = $1 & f reduces_to g,p,T holds
[(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #);
A1: ex k being Nat st card (Support f) = k ;
assume A2: f reduces_to g,p,T ; :: thesis: g < f,T
then consider b being bag of n such that
A3: f reduces_to g,p,b,T by Def6;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: for f, p, g being Polynomial of n,L st card (Support f) = k & f reduces_to g,p,T holds
[(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) ; :: thesis: S₁[k + 1]

now

A6: T is_connected_in field T by RELAT_2:def 14;
let f, p, g be Polynomial of n,L; :: thesis: ( card (Support f) = k + 1 & f reduces_to g,p,T implies [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) )
assume that
A7: card (Support f) = k + 1 and
A8: f reduces_to g,p,T ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)
consider b being bag of n such that
A9: f reduces_to g,p,b,T by A8, Def6;
consider s being bag of n such that
A10: s + (HT p,T) = b and
A11: g = f - (((f . b) / (HC p,T)) * (s *' p)) by A9, Def5;
A12: b in Support f by A9, Def5;
A13: f <> 0_ n,L by A9, Def5;

now

per cases ( HT f,T <> HT g,T or HT g,T = HT f,T ) ;

case A14: HT f,T <> HT g,T ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)

HT g,T <= HT g,T,T by TERMORD:6;
then [(HT g,T),(HT g,T)] in T by TERMORD:def 2;
then A15: HT g,T in field T by RELAT_1:30;
HT f,T <= HT f,T,T by TERMORD:6;
then [(HT f,T),(HT f,T)] in T by TERMORD:def 2;
then HT f,T in field T by RELAT_1:30;
then A16: ( [(HT f,T),(HT g,T)] in T or [(HT g,T),(HT f,T)] in T ) by A6, A14, A15, RELAT_2:def 6;

now

per cases ( HT f,T <= HT g,T,T or HT g,T <= HT f,T,T ) by A16, TERMORD:def 2;

case A17: HT f,T <= HT g,T,T ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)

now

assume not HT g,T in Support g ; :: thesis: contradiction
then HT g,T = EmptyBag n by TERMORD:def 6;
then [(HT g,T),(HT f,T)] in T by BAGORDER:def 7;
then HT g,T <= HT f,T,T by TERMORD:def 2;
hence contradiction by A14, A17, TERMORD:7; :: thesis: verum

end;

then HT g,T <= HT f,T,T by A8, Th42;
hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) by A14, A17, TERMORD:7; :: thesis: verum

end;

case HT g,T <= HT f,T,T ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)

then HT g,T < HT f,T,T by A14, TERMORD:def 3;
then g < f,T by Lm15;
then g <= f,T by Def3;
hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) by Def2; :: thesis: verum

end;

end;

end;

hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) ; :: thesis: verum

end;

case A18: HT g,T = HT f,T ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)

now

per cases ( b = HT f,T or b <> HT f,T ) ;

case b = HT f,T ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)

then not HT g,T in Support g by A9, A18, Lm17;
then Support g = {} by TERMORD:def 6;
then g = 0_ n,L by POLYNOM7:1;
then g <= f,T by Lm12;
hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) by Def2; :: thesis: verum

end;

case A19: b <> HT f,T ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)

HT f,T in Support f by A12, TERMORD:def 6;
then for u being set st u in {(HT f,T)} holds
u in Support f by TARSKI:def 1;
then A20: {(HT f,T)} c= Support f by TARSKI:def 3;
A21: Support (Red f,T) = (Support f) \ {(HT f,T)} by TERMORD:36;
not b in {(HT f,T)} by A19, TARSKI:def 1;
then A22: b in Support (Red f,T) by A12, A21, XBOOLE_0:def 5;
then Red f,T <> 0_ n,L by POLYNOM7:1;
then reconsider rf = Red f,T as non-zero Polynomial of n,L by POLYNOM7:def 2;
A23: ( rf <> 0_ n,L & p <> 0_ n,L ) by A9, Def5, POLYNOM7:def 2;
b <= HT f,T,T by A12, TERMORD:def 6;
then b < HT f,T,T by A19, TERMORD:def 3;
then f . (HT f,T) = g . (HT g,T) by A9, A18, Th41;
then HC f,T = g . (HT g,T) by TERMORD:def 7
.= HC g,T by TERMORD:def 7 ;
then HM f,T = Monom (HC g,T),(HT g,T) by A18, TERMORD:def 8
.= HM g,T by TERMORD:def 8 ;
then Red g,T = (f - (((f . b) / (HC p,T)) * (s *' p))) - (HM f,T) by A11, TERMORD:def 9
.= (((HM f,T) + rf) - (((f . b) / (HC p,T)) * (s *' p))) - (HM f,T) by TERMORD:38
.= (((HM f,T) + rf) - (((rf . b) / (HC p,T)) * (s *' p))) - (HM f,T) by A12, A19, TERMORD:40
.= (((HM f,T) + rf) + (- (((rf . b) / (HC p,T)) * (s *' p)))) - (HM f,T) by POLYNOM1:def 23
.= ((HM f,T) + (rf + (- (((rf . b) / (HC p,T)) * (s *' p))))) - (HM f,T) by POLYNOM1:80
.= ((HM f,T) + (rf + (- (((rf . b) / (HC p,T)) * (s *' p))))) + (- (HM f,T)) by POLYNOM1:def 23
.= (rf + (- (((rf . b) / (HC p,T)) * (s *' p)))) + ((HM f,T) + (- (HM f,T))) by POLYNOM1:80
.= (rf - (((rf . b) / (HC p,T)) * (s *' p))) + ((HM f,T) + (- (HM f,T))) by POLYNOM1:def 23
.= (rf - (((rf . b) / (HC p,T)) * (s *' p))) + ((HM f,T) - (HM f,T)) by POLYNOM1:def 23
.= (rf - (((rf . b) / (HC p,T)) * (s *' p))) + (0_ n,L) by POLYNOM1:83
.= rf - (((rf . b) / (HC p,T)) * (s *' p)) by POLYNOM1:82 ;
then rf reduces_to Red g,T,p,b,T by A10, A22, A23, Def5;
then A24: rf reduces_to Red g,T,p,T by Def6;
HT f,T in {(HT f,T)} by TARSKI:def 1;
then A25: not HT f,T in Support (Red f,T) by A21, XBOOLE_0:def 5;
(Support (Red f,T)) \/ {(HT f,T)} = (Support f) \/ {(HT f,T)} by A21, XBOOLE_1:39
.= Support f by A20, XBOOLE_1:12 ;
then (card (Support (Red f,T))) + 1 = k + 1 by A7, A25, CARD_2:54;
then [(Support (Red g,T)),(Support rf)] in FinOrd RelStr(# (Bags n),T #) by A5, A24, XCMPLX_1:2;
then Red g,T <= Red f,T,T by Def2;
then g <= f,T by A13, A18, Lm16;
hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) by Def2; :: thesis: verum

end;

end;

end;

hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) ; :: thesis: verum

end;

end;

end;

hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A26: S₁[ 0 ]

proof

let f, p, g be Polynomial of n,L; :: thesis: ( card (Support f) = 0 & f reduces_to g,p,T implies [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) )
assume that
A27: card (Support f) = 0 and
A28: f reduces_to g,p,T ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)
Support f = {} by A27;
then f = 0_ n,L by POLYNOM7:1;
then f is_irreducible_wrt p,T by Th37;
hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) by A28, Def8; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A26, A4);
then [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) by A2, A1;
then A29: g <= f,T by Def2;
b in Support f by A3, Def5;
then Support f <> Support g by A3, Lm17;
hence g < f,T by A29, Def3; :: thesis: verum