let n be Ordinal; for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, g being Polynomial of n,L
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
( g <= f,T & ( g = 0_ (n,L) or HT (g,T) <= HT (f,T),T ) )
let T be connected admissible TermOrder of n; for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, g being Polynomial of n,L
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
( g <= f,T & ( g = 0_ (n,L) or HT (g,T) <= HT (f,T),T ) )
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; for f, g being Polynomial of n,L
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
( g <= f,T & ( g = 0_ (n,L) or HT (g,T) <= HT (f,T),T ) )
let f, g be Polynomial of n,L; for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
( g <= f,T & ( g = 0_ (n,L) or HT (g,T) <= HT (f,T),T ) )
let P be Subset of (Polynom-Ring (n,L)); ( PolyRedRel (P,T) reduces f,g implies ( g <= f,T & ( g = 0_ (n,L) or HT (g,T) <= HT (f,T),T ) ) )
set R = PolyRedRel (P,T);
defpred S1[ Nat] means for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds
for p being RedSequence of PolyRedRel (P,T) st p . 1 = f & p . (len p) = g & len p = $1 holds
g <= f,T;
assume A1:
PolyRedRel (P,T) reduces f,g
; ( g <= f,T & ( g = 0_ (n,L) or HT (g,T) <= HT (f,T),T ) )
then consider p being RedSequence of PolyRedRel (P,T) such that
A2:
( p . 1 = f & p . (len p) = g )
by REWRITE1:def 3;
A3:
now for k being Nat st 1 <= k & S1[k] holds
S1[k + 1]let k be
Nat;
( 1 <= k & S1[k] implies S1[k + 1] )assume A4:
1
<= k
;
( S1[k] implies S1[k + 1] )thus
(
S1[
k] implies
S1[
k + 1] )
verumproof
assume A5:
S1[
k]
;
S1[k + 1]
now for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds
for p being RedSequence of PolyRedRel (P,T) st p . 1 = f & p . (len p) = g & len p = k + 1 holds
g <= f,Tlet f,
g be
Polynomial of
n,
L;
( PolyRedRel (P,T) reduces f,g implies for p being RedSequence of PolyRedRel (P,T) st p . 1 = f & p . (len p) = g & len p = k + 1 holds
g <= f,T )assume
PolyRedRel (
P,
T)
reduces f,
g
;
for p being RedSequence of PolyRedRel (P,T) st p . 1 = f & p . (len p) = g & len p = k + 1 holds
g <= f,Tlet p be
RedSequence of
PolyRedRel (
P,
T);
( p . 1 = f & p . (len p) = g & len p = k + 1 implies g <= f,T )assume that A6:
p . 1
= f
and A7:
p . (len p) = g
and A8:
len p = k + 1
;
g <= f,TA9:
dom p = Seg (k + 1)
by A8, FINSEQ_1:def 3;
then A10:
k + 1
in dom p
by FINSEQ_1:4;
set q =
p | (Seg k);
reconsider q =
p | (Seg k) as
FinSequence by FINSEQ_1:15;
A11:
k <= k + 1
by NAT_1:11;
then A12:
dom q = Seg k
by A8, FINSEQ_1:17;
then A13:
k in dom q
by A4, FINSEQ_1:1;
set h =
q . (len q);
A14:
len q = k
by A8, A11, FINSEQ_1:17;
k in dom p
by A4, A9, A11, FINSEQ_1:1;
then
[(p . k),(p . (k + 1))] in PolyRedRel (
P,
T)
by A10, REWRITE1:def 2;
then A15:
[(q . (len q)),g] in PolyRedRel (
P,
T)
by A7, A8, A14, A13, FUNCT_1:47;
then consider h9,
g9 being
object such that A16:
[(q . (len q)),g] = [h9,g9]
and A17:
h9 in NonZero (Polynom-Ring (n,L))
and
g9 in the
carrier of
(Polynom-Ring (n,L))
by RELSET_1:2;
A18:
q . (len q) = h9
by A16, XTUPLE_0:1;
A19:
now for i being Nat st i in dom q & i + 1 in dom q holds
[(q . i),(q . (i + 1))] in PolyRedRel (P,T)let i be
Nat;
( i in dom q & i + 1 in dom q implies [(q . i),(q . (i + 1))] in PolyRedRel (P,T) )assume that A20:
i in dom q
and A21:
i + 1
in dom q
;
[(q . i),(q . (i + 1))] in PolyRedRel (P,T)
i + 1
<= k
by A12, A21, FINSEQ_1:1;
then A22:
i + 1
<= k + 1
by A11, XXREAL_0:2;
i <= k
by A12, A20, FINSEQ_1:1;
then A23:
i <= k + 1
by A11, XXREAL_0:2;
1
<= i + 1
by A12, A21, FINSEQ_1:1;
then A24:
i + 1
in dom p
by A9, A22, FINSEQ_1:1;
1
<= i
by A12, A20, FINSEQ_1:1;
then
i in dom p
by A9, A23, FINSEQ_1:1;
then A25:
[(p . i),(p . (i + 1))] in PolyRedRel (
P,
T)
by A24, REWRITE1:def 2;
p . i = q . i
by A20, FUNCT_1:47;
hence
[(q . i),(q . (i + 1))] in PolyRedRel (
P,
T)
by A21, A25, FUNCT_1:47;
verum end;
0_ (
n,
L)
= 0. (Polynom-Ring (n,L))
by POLYNOM1:def 11;
then
not
h9 in {(0_ (n,L))}
by A17, XBOOLE_0:def 5;
then
h9 <> 0_ (
n,
L)
by TARSKI:def 1;
then reconsider h =
q . (len q) as
non-zero Polynomial of
n,
L by A17, A18, POLYNOM1:def 11, POLYNOM7:def 1;
reconsider q =
q as
RedSequence of
PolyRedRel (
P,
T)
by A4, A14, A19, REWRITE1:def 2;
1
in dom q
by A4, A12, FINSEQ_1:1;
then A26:
q . 1
= f
by A6, FUNCT_1:47;
then
PolyRedRel (
P,
T)
reduces f,
h
by REWRITE1:def 3;
then A27:
h <= f,
T
by A5, A8, A11, A26, FINSEQ_1:17;
h reduces_to g,
P,
T
by A15, Def13;
then A28:
ex
r being
Polynomial of
n,
L st
(
r in P &
h reduces_to g,
r,
T )
;
reconsider h =
h as
non-zero Polynomial of
n,
L ;
g < h,
T
by A28, Th43;
then
g <= h,
T
;
hence
g <= f,
T
by A27, Th27;
verum end;
hence
S1[
k + 1]
;
verum
end; end;
A29:
S1[1]
by Th25;
A30:
for k being Nat st 1 <= k holds
S1[k]
from NAT_1:sch 8(A29, A3);
consider k being Nat such that
A31:
len p = k
;
1 <= k
by A31, NAT_1:14;
hence A32:
g <= f,T
by A1, A30, A2, A31; ( g = 0_ (n,L) or HT (g,T) <= HT (f,T),T )
now ( g <> 0_ (n,L) implies HT (g,T) <= HT (f,T),T )assume
g <> 0_ (
n,
L)
;
HT (g,T) <= HT (f,T),Tthen
Support g <> {}
by POLYNOM7:1;
then A33:
HT (
g,
T)
in Support g
by TERMORD:def 6;
assume A34:
not
HT (
g,
T)
<= HT (
f,
T),
T
;
contradictionnow ( ( HT (f,T) = HT (g,T) & contradiction ) or ( HT (f,T) <> HT (g,T) & contradiction ) )per cases
( HT (f,T) = HT (g,T) or HT (f,T) <> HT (g,T) )
;
case A35:
HT (
f,
T)
<> HT (
g,
T)
;
contradiction
HT (
g,
T)
<= HT (
g,
T),
T
by TERMORD:6;
then
[(HT (g,T)),(HT (g,T))] in T
by TERMORD:def 2;
then A36:
HT (
g,
T)
in field T
by RELAT_1:15;
HT (
f,
T)
<= HT (
f,
T),
T
by TERMORD:6;
then
[(HT (f,T)),(HT (f,T))] in T
by TERMORD:def 2;
then
(
T is_connected_in field T &
HT (
f,
T)
in field T )
by RELAT_1:15, RELAT_2:def 14;
then
(
[(HT (f,T)),(HT (g,T))] in T or
[(HT (g,T)),(HT (f,T))] in T )
by A35, A36, RELAT_2:def 6;
then
HT (
f,
T)
<= HT (
g,
T),
T
by A34, TERMORD:def 2;
then A37:
HT (
f,
T)
< HT (
g,
T),
T
by A35, TERMORD:def 3;
then
f < g,
T
by Lm15;
then
f <= g,
T
;
then
Support f = Support g
by A32, Th26;
then
HT (
g,
T)
<= HT (
f,
T),
T
by A33, TERMORD:def 6;
hence
contradiction
by A37, TERMORD:5;
verum end; end; end; hence
contradiction
;
verum end;
hence
( g = 0_ (n,L) or HT (g,T) <= HT (f,T),T )
; verum