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 9;
m <> 0_ n,L by POLYNOM7:def 2;
then A2: HC m,T <> 0. L by TERMORD:17;
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 6;
then (m *' q) . (HT (m *' p),T) <> 0. L by A1, A3, VECTSP_2:def 5;
hence HT (m *' p),T in Support (m *' q) by POLYNOM1:def 9; :: thesis: verum