let n be Ordinal; for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f being Polynomial of n,L
for p being non-zero Polynomial of n,L holds
( f is_reducible_wrt p,T iff ex b being bag of n st
( b in Support f & HT (p,T) divides b ) )
let T be connected TermOrder of n; for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f being Polynomial of n,L
for p being non-zero Polynomial of n,L holds
( f is_reducible_wrt p,T iff ex b being bag of n st
( b in Support f & HT (p,T) divides b ) )
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; for f being Polynomial of n,L
for p being non-zero Polynomial of n,L holds
( f is_reducible_wrt p,T iff ex b being bag of n st
( b in Support f & HT (p,T) divides b ) )
let f be Polynomial of n,L; for p being non-zero Polynomial of n,L holds
( f is_reducible_wrt p,T iff ex b being bag of n st
( b in Support f & HT (p,T) divides b ) )
let p be non-zero Polynomial of n,L; ( f is_reducible_wrt p,T iff ex b being bag of n st
( b in Support f & HT (p,T) divides b ) )
A1:
now ( ex b being bag of n st
( b in Support f & HT (p,T) divides b ) implies f is_reducible_wrt p,T )A2:
p <> 0_ (
n,
L)
by POLYNOM7:def 1;
assume
ex
b being
bag of
n st
(
b in Support f &
HT (
p,
T)
divides b )
;
f is_reducible_wrt p,Tthen consider b being
bag of
n such that A3:
b in Support f
and A4:
HT (
p,
T)
divides b
;
consider s being
bag of
n such that A5:
b = (HT (p,T)) + s
by A4, TERMORD:1;
set g =
f - (((f . b) / (HC (p,T))) * (s *' p));
f <> 0_ (
n,
L)
by A3, POLYNOM7:1;
then
f reduces_to f - (((f . b) / (HC (p,T))) * (s *' p)),
p,
b,
T
by A3, A5, A2;
then
f reduces_to f - (((f . b) / (HC (p,T))) * (s *' p)),
p,
T
;
hence
f is_reducible_wrt p,
T
;
verum end;
now ( f is_reducible_wrt p,T implies ex b being bag of n st
( b in Support f & HT (p,T) divides b ) )assume
f is_reducible_wrt p,
T
;
ex b being bag of n st
( b in Support f & HT (p,T) divides b )then consider g being
Polynomial of
n,
L such that A6:
f reduces_to g,
p,
T
;
consider b being
bag of
n such that A7:
f reduces_to g,
p,
b,
T
by A6;
ex
s being
bag of
n st
(
s + (HT (p,T)) = b &
g = f - (((f . b) / (HC (p,T))) * (s *' p)) )
by A7;
then A8:
HT (
p,
T)
divides b
by TERMORD:1;
b in Support f
by A7;
hence
ex
b being
bag of
n st
(
b in Support f &
HT (
p,
T)
divides b )
by A8;
verum end;
hence
( f is_reducible_wrt p,T iff ex b being bag of n st
( b in Support f & HT (p,T) divides b ) )
by A1; verum