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 being Element of (Polynom-Ring n,L) st f,g are_convertible_wrt PolyRedRel P,T holds
f,g are_congruent_mod P -Ideal
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 being Element of (Polynom-Ring n,L) st f,g are_convertible_wrt PolyRedRel P,T holds
f,g are_congruent_mod P -Ideal
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 being Element of (Polynom-Ring n,L) st f,g are_convertible_wrt PolyRedRel P,T holds
f,g are_congruent_mod P -Ideal
let P be Subset of (Polynom-Ring n,L); :: thesis: for f, g being Element of (Polynom-Ring n,L) st f,g are_convertible_wrt PolyRedRel P,T holds
f,g are_congruent_mod P -Ideal
let f, g be Element of (Polynom-Ring n,L); :: thesis: ( f,g are_convertible_wrt PolyRedRel P,T implies f,g are_congruent_mod P -Ideal )
set R = PolyRedRel P,T;
set PR = Polynom-Ring n,L;
X:
0_ n,L = 0. (Polynom-Ring n,L)
by POLYNOM1:def 27;
assume A1:
f,g are_convertible_wrt PolyRedRel P,T
; :: thesis: f,g are_congruent_mod P -Ideal
defpred S1[ Nat] means for f, g being Element of (Polynom-Ring n,L) st (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) reduces f,g holds
for p being RedSequence of (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) st p . 1 = f & p . (len p) = g & len p = $1 holds
f,g are_congruent_mod P -Ideal ;
A2:
S1[1]
proof
let f,
g be
Element of
(Polynom-Ring n,L);
:: thesis: ( (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) reduces f,g implies for p being RedSequence of (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) st p . 1 = f & p . (len p) = g & len p = 1 holds
f,g are_congruent_mod P -Ideal )
assume
(PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) reduces f,
g
;
:: thesis: for p being RedSequence of (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) st p . 1 = f & p . (len p) = g & len p = 1 holds
f,g are_congruent_mod P -Ideal
let p be
RedSequence of
(PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ );
:: thesis: ( p . 1 = f & p . (len p) = g & len p = 1 implies f,g are_congruent_mod P -Ideal )
assume
(
p . 1
= f &
p . (len p) = g &
len p = 1 )
;
:: thesis: f,g are_congruent_mod P -Ideal
then A3:
f - g = 0. (Polynom-Ring n,L)
by RLVECT_1:28;
0. (Polynom-Ring n,L) in P -Ideal
by IDEAL_1:3;
hence
f,
g are_congruent_mod P -Ideal
by A3, Def14;
:: thesis: verum
end;
A4:
now let k be
Nat;
:: thesis: ( 1 <= k & S1[k] implies S1[k + 1] )assume A5:
1
<= k
;
:: thesis: ( S1[k] implies S1[k + 1] )thus
(
S1[
k] implies
S1[
k + 1] )
:: thesis: verumproof
assume A6:
S1[
k]
;
:: thesis: S1[k + 1]
now let f,
g be
Element of
(Polynom-Ring n,L);
:: thesis: ( (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) reduces f,g implies for p being RedSequence of (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) st p . 1 = f & p . (len p) = g & len p = k + 1 holds
f,g are_congruent_mod P -Ideal )assume
(PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) reduces f,
g
;
:: thesis: for p being RedSequence of (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) st p . 1 = f & p . (len p) = g & len p = k + 1 holds
f,g are_congruent_mod P -Ideal let p be
RedSequence of
(PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ );
:: thesis: ( p . 1 = f & p . (len p) = g & len p = k + 1 implies f,g are_congruent_mod P -Ideal )assume A7:
(
p . 1
= f &
p . (len p) = g &
len p = k + 1 )
;
:: thesis: f,g are_congruent_mod P -Ideal then A8:
dom p = Seg (k + 1)
by FINSEQ_1:def 3;
A9:
k <= k + 1
by NAT_1:11;
then A10:
k in dom p
by A5, A8, FINSEQ_1:3;
k + 1
in dom p
by A8, FINSEQ_1:6;
then A11:
[(p . k),(p . (k + 1))] in (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ )
by A10, REWRITE1:def 2;
set q =
p | (Seg k);
reconsider q =
p | (Seg k) as
FinSequence by FINSEQ_1:19;
set h =
q . (len q);
A12:
len q = k
by A7, A9, FINSEQ_1:21;
A13:
dom q = Seg k
by A7, A9, FINSEQ_1:21;
then
k in dom q
by A5, FINSEQ_1:3;
then
[(q . (len q)),g] in (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ )
by A7, A11, A12, FUNCT_1:70;
then A14:
(
[(q . (len q)),g] in PolyRedRel P,
T or
[(q . (len q)),g] in (PolyRedRel P,T) ~ )
by XBOOLE_0:def 3;
now per cases
( [(q . (len q)),g] in PolyRedRel P,T or [g,(q . (len q))] in PolyRedRel P,T )
by A14, RELAT_1:def 7;
case
[(q . (len q)),g] in PolyRedRel P,
T
;
:: thesis: ( q . (len q) in the carrier of (Polynom-Ring n,L) \ {(0_ n,L)} & q . (len q) in the carrier of (Polynom-Ring n,L) & g in the carrier of (Polynom-Ring n,L) )then consider h',
g' being
set such that A15:
(
[(q . (len q)),g] = [h',g'] &
h' in NonZero (Polynom-Ring n,L) &
g' in the
carrier of
(Polynom-Ring n,L) )
by RELSET_1:6;
q . (len q) =
[h',g'] `1
by A15, MCART_1:def 1
.=
h'
by MCART_1:def 1
;
hence
(
q . (len q) in the
carrier of
(Polynom-Ring n,L) \ {(0_ n,L)} &
q . (len q) in the
carrier of
(Polynom-Ring n,L) &
g in the
carrier of
(Polynom-Ring n,L) )
by A15, X;
:: thesis: verum end; case
[g,(q . (len q))] in PolyRedRel P,
T
;
:: thesis: ( g in the carrier of (Polynom-Ring n,L) \ {(0_ n,L)} & g in the carrier of (Polynom-Ring n,L) & q . (len q) in the carrier of (Polynom-Ring n,L) )then consider h',
g' being
set such that A16:
(
[g,(q . (len q))] = [h',g'] &
h' in NonZero (Polynom-Ring n,L) &
g' in the
carrier of
(Polynom-Ring n,L) )
by RELSET_1:6;
A17:
g =
[h',g'] `1
by A16, MCART_1:def 1
.=
h'
by MCART_1:def 1
;
q . (len q) =
[h',g'] `2
by A16, MCART_1:def 2
.=
g'
by MCART_1:def 2
;
hence
(
g in the
carrier of
(Polynom-Ring n,L) \ {(0_ n,L)} &
g in the
carrier of
(Polynom-Ring n,L) &
q . (len q) in the
carrier of
(Polynom-Ring n,L) )
by A16, A17, X;
:: thesis: verum end; then reconsider h =
q . (len q) as
Polynomial of
n,
L by POLYNOM1:def 27;
reconsider h' =
h as
Element of
(Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider h' =
h' as
Element of
(Polynom-Ring n,L) ;
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) \/ ((PolyRedRel P,T) ~ ) )assume A18:
(
i in dom q &
i + 1
in dom q )
;
:: thesis: [(q . i),(q . (i + 1))] in (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ )then A19:
( 1
<= i &
i <= k & 1
<= i + 1 &
i + 1
<= k )
by A13, FINSEQ_1:3;
then A20:
(
i <= k + 1 &
i + 1
<= k + 1 )
by A9, XXREAL_0:2;
then A21:
i in dom p
by A8, A19, FINSEQ_1:3;
i + 1
in dom p
by A8, A19, A20, FINSEQ_1:3;
then A22:
[(p . i),(p . (i + 1))] in (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ )
by A21, REWRITE1:def 2;
p . i = q . i
by A18, FUNCT_1:70;
hence
[(q . i),(q . (i + 1))] in (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ )
by A18, A22, FUNCT_1:70;
:: thesis: verum end; then reconsider q =
q as
RedSequence of
(PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) by A5, A12, REWRITE1:def 2;
1
in dom q
by A5, A13, FINSEQ_1:3;
then A23:
q . 1
= f
by A7, FUNCT_1:70;
then
(PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) reduces f,
h
by REWRITE1:def 3;
then A24:
f,
h' are_congruent_mod P -Ideal
by A6, A12, A23;
now per cases
( [h,g] in PolyRedRel P,T or [g,h] in PolyRedRel P,T )
by A14, RELAT_1:def 7;
case A25:
[h,g] in PolyRedRel P,
T
;
:: thesis: f - g in P -Ideal then consider h',
g' being
set such that A26:
(
[h,g] = [h',g'] &
h' in NonZero (Polynom-Ring n,L) &
g' in the
carrier of
(Polynom-Ring n,L) )
by RELSET_1:6;
A27:
h =
[h',g'] `1
by A26, MCART_1:def 1
.=
h'
by MCART_1:def 1
;
A28:
g =
[h',g'] `2
by A26, MCART_1:def 2
.=
g'
by MCART_1:def 2
;
not
h' in {(0_ n,L)}
by A26, X, XBOOLE_0:def 5;
then
h' <> 0_ n,
L
by TARSKI:def 1;
then reconsider h =
h as
non-zero Polynomial of
n,
L by A27, POLYNOM7:def 2;
reconsider h' =
h as
Element of
(Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider h' =
h' as
Element of
(Polynom-Ring n,L) ;
reconsider g' =
g' as
Polynomial of
n,
L by A26, POLYNOM1:def 27;
h reduces_to g',
P,
T
by A25, A28, Def13;
then
h',
g are_congruent_mod P -Ideal
by A28, Lm19;
then
f,
g are_congruent_mod P -Ideal
by A24, Th54;
hence
f - g in P -Ideal
by Def14;
:: thesis: verum end; case A29:
[g,h] in PolyRedRel P,
T
;
:: thesis: f - g in P -Ideal then consider g',
h' being
set such that A30:
(
[g,h] = [g',h'] &
g' in NonZero (Polynom-Ring n,L) &
h' in the
carrier of
(Polynom-Ring n,L) )
by RELSET_1:6;
A31:
g =
[g',h'] `1
by A30, MCART_1:def 1
.=
g'
by MCART_1:def 1
;
A32:
h =
[g',h'] `2
by A30, MCART_1:def 2
.=
h'
by MCART_1:def 2
;
not
g' in {(0_ n,L)}
by A30, X, XBOOLE_0:def 5;
then
g' <> 0_ n,
L
by TARSKI:def 1;
then reconsider g' =
g as
non-zero Polynomial of
n,
L by A31, POLYNOM1:def 27, POLYNOM7:def 2;
reconsider gg =
g' as
Element of
(Polynom-Ring n,L) ;
reconsider gg =
gg as
Element of
(Polynom-Ring n,L) ;
reconsider h' =
h' as
Polynomial of
n,
L by A32;
reconsider h =
h as
Element of
(Polynom-Ring n,L) by A30, A32;
reconsider h =
h as
Element of
(Polynom-Ring n,L) ;
g' reduces_to h',
P,
T
by A29, A32, Def13;
then
h,
gg are_congruent_mod P -Ideal
by A32, Lm19, Th53;
then
f,
gg are_congruent_mod P -Ideal
by A24, Th54;
hence
f - g in P -Ideal
by Def14;
:: thesis: verum end; hence
f,
g are_congruent_mod P -Ideal
by Def14;
:: thesis: verum end;
hence
S1[
k + 1]
;
:: thesis: verum
end; end;
A33:
for k being Nat st 1 <= k holds
S1[k]
from NAT_1:sch 8(A2, A4);
A34:
(PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) reduces f,g
by A1, REWRITE1:def 4;
then consider p being RedSequence of (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) such that
A35:
( p . 1 = f & p . (len p) = g )
by REWRITE1:def 3;
consider k being Nat such that
A36:
len p = k
;
k > 0
by A36;
then
1 <= k
by NAT_1:14;
hence
f,g are_congruent_mod P -Ideal
by A33, A34, A35, A36; :: thesis: verum