let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p being non-zero Polynomial of n,L
for q being Polynomial of n,L
for m being non-zero Monomial of n,L st HT (p,T) in Support q holds
HT ((m *' p),T) in Support (m *' q)
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p being non-zero Polynomial of n,L
for q being Polynomial of n,L
for m being non-zero Monomial of n,L st HT (p,T) in Support q holds
HT ((m *' p),T) in Support (m *' q)
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for p being non-zero Polynomial of n,L
for q being Polynomial of n,L
for m being non-zero Monomial of n,L st HT (p,T) in Support q holds
HT ((m *' p),T) in Support (m *' q)
let p be non-zero Polynomial of n,L; :: thesis: for q being Polynomial of n,L
for m being non-zero Monomial of n,L st HT (p,T) in Support q holds
HT ((m *' p),T) in Support (m *' q)
let q be Polynomial of n,L; :: thesis: for m being non-zero Monomial of n,L st HT (p,T) in Support q holds
HT ((m *' p),T) in Support (m *' q)
let m be non-zero Monomial of n,L; :: thesis: ( HT (p,T) in Support q implies HT ((m *' p),T) in Support (m *' q) )
set a = coefficient m;
set b = term m;
assume HT (p,T) in Support q ; :: thesis: HT ((m *' p),T) in Support (m *' q)
then A1: q . (HT (p,T)) <> 0. L by POLYNOM1:def 4;
A2: HC (m,T) <> 0. L ;
then reconsider a = coefficient m as non zero Element of L by TERMORD:23;
m = Monom (a,(term m)) by POLYNOM7:11;
then m *' p = a * ((term m) *' p) by Th22;
then HT ((m *' p),T) = HT (((term m) *' p),T) by Th21
.= (term m) + (HT (p,T)) by Th15 ;
then A3: (m *' q) . (HT ((m *' p),T)) = (m . (term m)) * (q . (HT (p,T))) by Th7;
m . (HT (m,T)) <> 0. L by A2, TERMORD:def 7;
then m . (term m) <> 0. L by POLYNOM7:def 5;
then (m *' q) . (HT ((m *' p),T)) <> 0. L by A1, A3, VECTSP_2:def 1;
hence HT ((m *' p),T) in Support (m *' q) by POLYNOM1:def 4; :: thesis: verum