let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for f, g, h, h1 being Polynomial of n,L st f - g = h & PolyRedRel P,T reduces h,h1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 )
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for f, g, h, h1 being Polynomial of n,L st f - g = h & PolyRedRel P,T reduces h,h1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 )
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for P being Subset of (Polynom-Ring n,L)
for f, g, h, h1 being Polynomial of n,L st f - g = h & PolyRedRel P,T reduces h,h1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 )
let P be Subset of (Polynom-Ring n,L); :: thesis: for f, g, h, h1 being Polynomial of n,L st f - g = h & PolyRedRel P,T reduces h,h1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 )
let f, g, h, h1 be Polynomial of n,L; :: thesis: ( f - g = h & PolyRedRel P,T reduces h,h1 implies ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 ) )
assume A1:
( f - g = h & PolyRedRel P,T reduces h,h1 )
; :: thesis: ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 )
defpred S1[ Nat] means for f, g, h being Polynomial of n,L st f - g = h holds
for h1 being Polynomial of n,L
for p being RedSequence of PolyRedRel P,T st p . 1 = h & p . (len p) = h1 & len p = $1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 );
A2:
S1[1]
proof
let f,
g,
h be
Polynomial of
n,
L;
:: thesis: ( f - g = h implies for h1 being Polynomial of n,L
for p being RedSequence of PolyRedRel P,T st p . 1 = h & p . (len p) = h1 & len p = 1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 ) )
assume A3:
f - g = h
;
:: thesis: for h1 being Polynomial of n,L
for p being RedSequence of PolyRedRel P,T st p . 1 = h & p . (len p) = h1 & len p = 1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 )
let h1 be
Polynomial of
n,
L;
:: thesis: for p being RedSequence of PolyRedRel P,T st p . 1 = h & p . (len p) = h1 & len p = 1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 )let p be
RedSequence of
PolyRedRel P,
T;
:: thesis: ( p . 1 = h & p . (len p) = h1 & len p = 1 implies ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 ) )
assume A4:
(
p . 1
= h &
p . (len p) = h1 &
len p = 1 )
;
:: thesis: ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 )
take
f
;
:: thesis: ex g1 being Polynomial of n,L st
( f - g1 = h1 & PolyRedRel P,T reduces f,f & PolyRedRel P,T reduces g,g1 )
take
g
;
:: thesis: ( f - g = h1 & PolyRedRel P,T reduces f,f & PolyRedRel P,T reduces g,g )
thus
(
f - g = h1 &
PolyRedRel P,
T reduces f,
f &
PolyRedRel P,
T reduces g,
g )
by A3, A4, REWRITE1:13;
:: thesis: verum
end;
A5:
now let k be
Nat;
:: thesis: ( 1 <= k & S1[k] implies S1[k + 1] )assume A6:
1
<= k
;
:: thesis: ( S1[k] implies S1[k + 1] )assume A7:
S1[
k]
;
:: thesis: S1[k + 1]thus
S1[
k + 1]
:: thesis: verumproof
let f,
g,
h be
Polynomial of
n,
L;
:: thesis: ( f - g = h implies for h1 being Polynomial of n,L
for p being RedSequence of PolyRedRel P,T st p . 1 = h & p . (len p) = h1 & len p = k + 1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 ) )
assume A8:
f - g = h
;
:: thesis: for h1 being Polynomial of n,L
for p being RedSequence of PolyRedRel P,T st p . 1 = h & p . (len p) = h1 & len p = k + 1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 )
let h1 be
Polynomial of
n,
L;
:: thesis: for p being RedSequence of PolyRedRel P,T st p . 1 = h & p . (len p) = h1 & len p = k + 1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 )let r be
RedSequence of
PolyRedRel P,
T;
:: thesis: ( r . 1 = h & r . (len r) = h1 & len r = k + 1 implies ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 ) )
assume A9:
(
r . 1
= h &
r . (len r) = h1 &
len r = k + 1 )
;
:: thesis: ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 )
then A10:
dom r = Seg (k + 1)
by FINSEQ_1:def 3;
set h2 =
r . k;
1
<= k + 1
by NAT_1:11;
then A11:
k + 1
in dom r
by A10, FINSEQ_1:3;
k <= k + 1
by NAT_1:11;
then
k in dom r
by A6, A10, FINSEQ_1:3;
then A12:
[(r . k),(r . (k + 1))] in PolyRedRel P,
T
by A11, REWRITE1:def 2;
then consider x,
y being
set such that A13:
(
x in NonZero (Polynom-Ring n,L) &
y in the
carrier of
(Polynom-Ring n,L) &
[(r . k),(r . (k + 1))] = [x,y] )
by ZFMISC_1:def 2;
A14:
r . k =
[x,y] `1
by A13, MCART_1:def 1
.=
x
by MCART_1:def 1
;
then reconsider h2 =
r . k as
Polynomial of
n,
L by A13, POLYNOM1:def 27;
0_ n,
L = 0. (Polynom-Ring n,L)
by POLYNOM1:def 27;
then
not
r . k in {(0_ n,L)}
by A13, A14, XBOOLE_0:def 5;
then
r . k <> 0_ n,
L
by TARSKI:def 1;
then reconsider h2 =
h2 as
non-zero Polynomial of
n,
L by POLYNOM7:def 2;
set q =
r | (Seg k);
reconsider q =
r | (Seg k) as
FinSequence by FINSEQ_1:19;
A15:
dom r = Seg (k + 1)
by A9, FINSEQ_1:def 3;
A16:
k <= k + 1
by NAT_1:11;
then A17:
len q = k
by A9, FINSEQ_1:21;
A18:
dom q = Seg k
by A9, A16, FINSEQ_1:21;
now let i be
Element of
NAT ;
:: thesis: ( i in dom q & i + 1 in dom q implies [(q . i),(q . (i + 1))] in PolyRedRel P,T )assume A19:
(
i in dom q &
i + 1
in dom q )
;
:: thesis: [(q . i),(q . (i + 1))] in PolyRedRel P,Tthen A20:
( 1
<= i &
i <= k & 1
<= i + 1 &
i + 1
<= k )
by A18, FINSEQ_1:3;
then A21:
(
i <= k + 1 &
i + 1
<= k + 1 )
by A16, XXREAL_0:2;
then A22:
i in dom r
by A15, A20, FINSEQ_1:3;
i + 1
in dom r
by A15, A20, A21, FINSEQ_1:3;
then A23:
[(r . i),(r . (i + 1))] in PolyRedRel P,
T
by A22, REWRITE1:def 2;
r . i = q . i
by A19, FUNCT_1:70;
hence
[(q . i),(q . (i + 1))] in PolyRedRel P,
T
by A19, A23, FUNCT_1:70;
:: thesis: verum end;
then reconsider q =
q as
RedSequence of
PolyRedRel P,
T by A6, A17, REWRITE1:def 2;
1
in dom q
by A6, A18, FINSEQ_1:3;
then A24:
q . 1
= h
by A9, FUNCT_1:70;
A25:
k in dom q
by A6, A18, FINSEQ_1:3;
q . (len q) =
q . k
by A9, A16, FINSEQ_1:21
.=
h2
by A25, FUNCT_1:70
;
then consider f2,
g2 being
Polynomial of
n,
L such that A26:
(
f2 - g2 = h2 &
PolyRedRel P,
T reduces f,
f2 &
PolyRedRel P,
T reduces g,
g2 )
by A7, A8, A17, A24;
h2 reduces_to h1,
P,
T
by A9, A12, Def13;
then consider p being
Polynomial of
n,
L such that A27:
(
p in P &
h2 reduces_to h1,
p,
T )
by Def7;
consider b being
bag of
such that A28:
h2 reduces_to h1,
p,
b,
T
by A27, Def6;
consider s being
bag of
such that A29:
(
s + (HT p,T) = b &
h1 = h2 - (((h2 . b) / (HC p,T)) * (s *' p)) )
by A28, Def5;
set f1 =
f2 - (((f2 . b) / (HC p,T)) * (s *' p));
set g1 =
g2 - (((g2 . b) / (HC p,T)) * (s *' p));
A30:
((f2 . b) / (HC p,T)) + (- ((g2 . b) / (HC p,T))) =
((f2 . b) * ((HC p,T) " )) + (- ((g2 . b) / (HC p,T)))
by VECTSP_1:def 23
.=
((f2 . b) * ((HC p,T) " )) + (- ((g2 . b) * ((HC p,T) " )))
by VECTSP_1:def 23
.=
((f2 . b) * ((HC p,T) " )) + ((- (g2 . b)) * ((HC p,T) " ))
by VECTSP_1:41
.=
((f2 . b) + (- (g2 . b))) * ((HC p,T) " )
by VECTSP_1:def 18
.=
((f2 . b) + ((- g2) . b)) * ((HC p,T) " )
by POLYNOM1:def 22
.=
((f2 + (- g2)) . b) * ((HC p,T) " )
by POLYNOM1:def 21
.=
((f2 - g2) . b) * ((HC p,T) " )
by POLYNOM1:def 23
.=
((f2 - g2) . b) / (HC p,T)
by VECTSP_1:def 23
;
A31:
(f2 - (((f2 . b) / (HC p,T)) * (s *' p))) - (g2 - (((g2 . b) / (HC p,T)) * (s *' p))) =
(f2 - (((f2 . b) / (HC p,T)) * (s *' p))) + (- (g2 - (((g2 . b) / (HC p,T)) * (s *' p))))
by POLYNOM1:def 23
.=
(f2 + (- (((f2 . b) / (HC p,T)) * (s *' p)))) + (- (g2 - (((g2 . b) / (HC p,T)) * (s *' p))))
by POLYNOM1:def 23
.=
(f2 + (- (((f2 . b) / (HC p,T)) * (s *' p)))) + (- (g2 + (- (((g2 . b) / (HC p,T)) * (s *' p)))))
by POLYNOM1:def 23
.=
(f2 + (- (((f2 . b) / (HC p,T)) * (s *' p)))) + ((- g2) + (- (- (((g2 . b) / (HC p,T)) * (s *' p)))))
by Th1
.=
((f2 + (- (((f2 . b) / (HC p,T)) * (s *' p)))) + (- g2)) + (((g2 . b) / (HC p,T)) * (s *' p))
by POLYNOM1:80
.=
((- (((f2 . b) / (HC p,T)) * (s *' p))) + (f2 + (- g2))) + (((g2 . b) / (HC p,T)) * (s *' p))
by POLYNOM1:80
.=
(f2 + (- g2)) + ((- (((f2 . b) / (HC p,T)) * (s *' p))) + (((g2 . b) / (HC p,T)) * (s *' p)))
by POLYNOM1:80
.=
(f2 - g2) + ((- (((f2 . b) / (HC p,T)) * (s *' p))) + (((g2 . b) / (HC p,T)) * (s *' p)))
by POLYNOM1:def 23
.=
(f2 - g2) + (((- ((f2 . b) / (HC p,T))) * (s *' p)) + (((g2 . b) / (HC p,T)) * (s *' p)))
by Th9
.=
(f2 - g2) + (- (- (((- ((f2 . b) / (HC p,T))) + ((g2 . b) / (HC p,T))) * (s *' p))))
by Th10
.=
(f2 - g2) + (- ((- ((- ((f2 . b) / (HC p,T))) + ((g2 . b) / (HC p,T)))) * (s *' p)))
by Th9
.=
(f2 - g2) - ((- ((- ((f2 . b) / (HC p,T))) + ((g2 . b) / (HC p,T)))) * (s *' p))
by POLYNOM1:def 23
.=
(f2 - g2) - (((- (- ((f2 . b) / (HC p,T)))) + (- ((g2 . b) / (HC p,T)))) * (s *' p))
by RLVECT_1:45
.=
h1
by A26, A29, A30, RLVECT_1:30
;
A32:
now per cases
( not b in Support f2 or b in Support f2 )
;
case A34:
b in Support f2
;
:: thesis: PolyRedRel P,T reduces f,f2 - (((f2 . b) / (HC p,T)) * (s *' p))then
f2 <> 0_ n,
L
by POLYNOM7:1;
then reconsider f2 =
f2 as
non-zero Polynomial of
n,
L by POLYNOM7:def 2;
(
f2 <> 0_ n,
L &
p <> 0_ n,
L )
by A27, Lm18, POLYNOM7:def 2;
then
f2 reduces_to f2 - (((f2 . b) / (HC p,T)) * (s *' p)),
p,
b,
T
by A29, A34, Def5;
then
f2 reduces_to f2 - (((f2 . b) / (HC p,T)) * (s *' p)),
p,
T
by Def6;
then
f2 reduces_to f2 - (((f2 . b) / (HC p,T)) * (s *' p)),
P,
T
by A27, Def7;
then
[f2,(f2 - (((f2 . b) / (HC p,T)) * (s *' p)))] in PolyRedRel P,
T
by Def13;
then
PolyRedRel P,
T reduces f2,
f2 - (((f2 . b) / (HC p,T)) * (s *' p))
by REWRITE1:16;
hence
PolyRedRel P,
T reduces f,
f2 - (((f2 . b) / (HC p,T)) * (s *' p))
by A26, REWRITE1:17;
:: thesis: verum end;
now per cases
( not b in Support g2 or b in Support g2 )
;
case A36:
b in Support g2
;
:: thesis: PolyRedRel P,T reduces g,g2 - (((g2 . b) / (HC p,T)) * (s *' p))then
g2 <> 0_ n,
L
by POLYNOM7:1;
then reconsider g2 =
g2 as
non-zero Polynomial of
n,
L by POLYNOM7:def 2;
(
g2 <> 0_ n,
L &
p <> 0_ n,
L )
by A27, Lm18, POLYNOM7:def 2;
then
g2 reduces_to g2 - (((g2 . b) / (HC p,T)) * (s *' p)),
p,
b,
T
by A29, A36, Def5;
then
g2 reduces_to g2 - (((g2 . b) / (HC p,T)) * (s *' p)),
p,
T
by Def6;
then
g2 reduces_to g2 - (((g2 . b) / (HC p,T)) * (s *' p)),
P,
T
by A27, Def7;
then
[g2,(g2 - (((g2 . b) / (HC p,T)) * (s *' p)))] in PolyRedRel P,
T
by Def13;
then
PolyRedRel P,
T reduces g2,
g2 - (((g2 . b) / (HC p,T)) * (s *' p))
by REWRITE1:16;
hence
PolyRedRel P,
T reduces g,
g2 - (((g2 . b) / (HC p,T)) * (s *' p))
by A26, REWRITE1:17;
:: thesis: verum end;
hence
ex
f1,
g1 being
Polynomial of
n,
L st
(
f1 - g1 = h1 &
PolyRedRel P,
T reduces f,
f1 &
PolyRedRel P,
T reduces g,
g1 )
by A31, A32;
:: thesis: verum
end; end;
A37:
for k being Nat st 1 <= k holds
S1[k]
from NAT_1:sch 8(A2, A5);
consider p being RedSequence of PolyRedRel P,T such that
A38:
( p . 1 = h & p . (len p) = h1 )
by A1, REWRITE1:def 3;
consider k being Nat such that
A39:
len p = k
;
k > 0
by A39;
then
1 <= k
by NAT_1:14;
hence
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel P,T reduces f,f1 & PolyRedRel P,T reduces g,g1 )
by A1, A37, A38, A39; :: thesis: verum