let n be Ordinal; for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative 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; for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 P be 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 f, g be Element of (Polynom-Ring (n,L)); ( 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);
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 ;
assume
f,g are_convertible_wrt PolyRedRel (P,T)
; f,g are_congruent_mod P -Ideal
then A1:
(PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) reduces f,g
by REWRITE1:def 4;
then consider p being RedSequence of (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) such that
A2:
( p . 1 = f & p . (len p) = g )
by REWRITE1:def 3;
A3:
0_ (n,L) = 0. (Polynom-Ring (n,L))
by POLYNOM1:def 11;
A4:
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 A5:
1
<= k
;
( S1[k] implies S1[k + 1] )thus
(
S1[
k] implies
S1[
k + 1] )
verumproof
assume A6:
S1[
k]
;
S1[k + 1]
now 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 = k + 1 holds
f,g are_congruent_mod P -Ideal let f,
g be
Element of
(Polynom-Ring (n,L));
( (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
;
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)) ~);
( p . 1 = f & p . (len p) = g & len p = k + 1 implies f,g are_congruent_mod P -Ideal )assume that A7:
p . 1
= f
and A8:
p . (len p) = g
and A9:
len p = k + 1
;
f,g are_congruent_mod P -Ideal A10:
dom p = Seg (k + 1)
by A9, FINSEQ_1:def 3;
then A11:
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;
A12:
k <= k + 1
by NAT_1:11;
then A13:
dom q = Seg k
by A9, FINSEQ_1:17;
then A14:
k in dom q
by A5, FINSEQ_1:1;
set h =
q . (len q);
A15:
len q = k
by A9, A12, FINSEQ_1:17;
k in dom p
by A5, A10, A12, FINSEQ_1:1;
then
[(p . k),(p . (k + 1))] in (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~)
by A11, REWRITE1:def 2;
then
[(q . (len q)),g] in (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~)
by A8, A9, A15, A14, FUNCT_1:47;
then A16:
(
[(q . (len q)),g] in PolyRedRel (
P,
T) or
[(q . (len q)),g] in (PolyRedRel (P,T)) ~ )
by XBOOLE_0:def 3;
A17:
now ( ( [(q . (len q)),g] in PolyRedRel (P,T) & 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)) ) or ( [g,(q . (len q))] in PolyRedRel (P,T) & 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)) ) )per cases
( [(q . (len q)),g] in PolyRedRel (P,T) or [g,(q . (len q))] in PolyRedRel (P,T) )
by A16, RELAT_1:def 7;
case
[(q . (len q)),g] in PolyRedRel (
P,
T)
;
( 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 h9,
g9 being
object such that A18:
[(q . (len q)),g] = [h9,g9]
and A19:
h9 in NonZero (Polynom-Ring (n,L))
and
g9 in the
carrier of
(Polynom-Ring (n,L))
by RELSET_1:2;
q . (len q) = h9
by A18, XTUPLE_0: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 A19, POLYNOM1:def 11;
verum end; case
[g,(q . (len q))] in PolyRedRel (
P,
T)
;
( 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 h9,
g9 being
object such that A20:
[g,(q . (len q))] = [h9,g9]
and A21:
(
h9 in NonZero (Polynom-Ring (n,L)) &
g9 in the
carrier of
(Polynom-Ring (n,L)) )
by RELSET_1:2;
A22:
q . (len q) = g9
by A20, XTUPLE_0:1;
g = h9
by A20, XTUPLE_0:1;
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 A21, A22, POLYNOM1:def 11;
verum end; end; end; 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)) \/ ((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)) \/ ((PolyRedRel (P,T)) ~) )assume that A23:
i in dom q
and A24:
i + 1
in dom q
;
[(q . i),(q . (i + 1))] in (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~)
i + 1
<= k
by A13, A24, FINSEQ_1:1;
then A25:
i + 1
<= k + 1
by A12, XXREAL_0:2;
i <= k
by A13, A23, FINSEQ_1:1;
then A26:
i <= k + 1
by A12, XXREAL_0:2;
1
<= i + 1
by A13, A24, FINSEQ_1:1;
then A27:
i + 1
in dom p
by A10, A25, FINSEQ_1:1;
1
<= i
by A13, A23, FINSEQ_1:1;
then
i in dom p
by A10, A26, FINSEQ_1:1;
then A28:
[(p . i),(p . (i + 1))] in (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~)
by A27, REWRITE1:def 2;
p . i = q . i
by A23, FUNCT_1:47;
hence
[(q . i),(q . (i + 1))] in (PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~)
by A24, A28, FUNCT_1:47;
verum end; then reconsider q =
q as
RedSequence of
(PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) by A5, A15, REWRITE1:def 2;
reconsider h =
q . (len q) as
Polynomial of
n,
L by A17, POLYNOM1:def 11;
reconsider h9 =
h as
Element of
(Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider h9 =
h9 as
Element of
(Polynom-Ring (n,L)) ;
1
in dom q
by A5, A13, FINSEQ_1:1;
then A29:
q . 1
= f
by A7, FUNCT_1:47;
then
(PolyRedRel (P,T)) \/ ((PolyRedRel (P,T)) ~) reduces f,
h
by REWRITE1:def 3;
then A30:
f,
h9 are_congruent_mod P -Ideal
by A6, A9, A12, A29, FINSEQ_1:17;
now ( ( [h,g] in PolyRedRel (P,T) & f - g in P -Ideal ) or ( [g,h] in PolyRedRel (P,T) & f - g in P -Ideal ) )per cases
( [h,g] in PolyRedRel (P,T) or [g,h] in PolyRedRel (P,T) )
by A16, RELAT_1:def 7;
case A31:
[h,g] in PolyRedRel (
P,
T)
;
f - g in P -Ideal then consider h9,
g9 being
object such that A32:
[h,g] = [h9,g9]
and A33:
h9 in NonZero (Polynom-Ring (n,L))
and A34:
g9 in the
carrier of
(Polynom-Ring (n,L))
by RELSET_1:2;
A35:
h = h9
by A32, XTUPLE_0:1;
not
h9 in {(0_ (n,L))}
by A3, A33, XBOOLE_0:def 5;
then
h9 <> 0_ (
n,
L)
by TARSKI:def 1;
then reconsider h =
h as
non-zero Polynomial of
n,
L by A35, POLYNOM7:def 1;
A36:
g = g9
by A32, XTUPLE_0:1;
reconsider g9 =
g9 as
Polynomial of
n,
L by A34, POLYNOM1:def 11;
reconsider h9 =
h as
Element of
(Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider h9 =
h9 as
Element of
(Polynom-Ring (n,L)) ;
h reduces_to g9,
P,
T
by A31, A36, Def13;
then
h9,
g are_congruent_mod P -Ideal
by A36, Lm19;
then
f,
g are_congruent_mod P -Ideal
by A30, Th54;
hence
f - g in P -Ideal
;
verum end; case A37:
[g,h] in PolyRedRel (
P,
T)
;
f - g in P -Ideal then consider g9,
h9 being
object such that A38:
[g,h] = [g9,h9]
and A39:
g9 in NonZero (Polynom-Ring (n,L))
and A40:
h9 in the
carrier of
(Polynom-Ring (n,L))
by RELSET_1:2;
A41:
g = g9
by A38, XTUPLE_0:1;
not
g9 in {(0_ (n,L))}
by A3, A39, XBOOLE_0:def 5;
then A42:
g9 <> 0_ (
n,
L)
by TARSKI:def 1;
A43:
h = h9
by A38, XTUPLE_0:1;
then reconsider h =
h as
Element of
(Polynom-Ring (n,L)) by A40;
reconsider h9 =
h9 as
Polynomial of
n,
L by A43;
reconsider g9 =
g as
non-zero Polynomial of
n,
L by A41, A42, POLYNOM1:def 11, POLYNOM7:def 1;
reconsider gg =
g9 as
Element of
(Polynom-Ring (n,L)) ;
reconsider gg =
gg as
Element of
(Polynom-Ring (n,L)) ;
reconsider h =
h as
Element of
(Polynom-Ring (n,L)) ;
g9 reduces_to h9,
P,
T
by A37, A43, Def13;
then
h,
gg are_congruent_mod P -Ideal
by A43, Lm19, Th53;
then
f,
gg are_congruent_mod P -Ideal
by A30, Th54;
hence
f - g in P -Ideal
;
verum end; end; end; hence
f,
g are_congruent_mod P -Ideal
;
verum end;
hence
S1[
k + 1]
;
verum
end; end;
A44:
S1[1]
proof
let f,
g be
Element of
(Polynom-Ring (n,L));
( (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
;
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)) ~);
( 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 )
;
f,g are_congruent_mod P -Ideal
then A45:
f - g = 0. (Polynom-Ring (n,L))
by RLVECT_1:15;
0. (Polynom-Ring (n,L)) in P -Ideal
by IDEAL_1:3;
hence
f,
g are_congruent_mod P -Ideal
by A45;
verum
end;
A46:
for k being Nat st 1 <= k holds
S1[k]
from NAT_1:sch 8(A44, A4);
consider k being Nat such that
A47:
len p = k
;
1 <= k
by A47, NAT_1:14;
hence
f,g are_congruent_mod P -Ideal
by A46, A1, A2, A47; verum