let n be Ordinal; :: thesis: for T being connected TermOrder of n

for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr

for p being Polynomial of n,L holds HT ((- p),T) = HT (p,T)

let T be connected TermOrder of n; :: thesis: for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr

for p being Polynomial of n,L holds HT ((- p),T) = HT (p,T)

let L be non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of n,L holds HT ((- p),T) = HT (p,T)

let p be Polynomial of n,L; :: thesis: HT ((- p),T) = HT (p,T)

for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr

for p being Polynomial of n,L holds HT ((- p),T) = HT (p,T)

let T be connected TermOrder of n; :: thesis: for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr

for p being Polynomial of n,L holds HT ((- p),T) = HT (p,T)

let L be non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of n,L holds HT ((- p),T) = HT (p,T)

let p be Polynomial of n,L; :: thesis: HT ((- p),T) = HT (p,T)

per cases
( p = 0_ (n,L) or p <> 0_ (n,L) )
;

end;

suppose A1:
p = 0_ (n,L)
; :: thesis: HT ((- p),T) = HT (p,T)

reconsider x = - p as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;

reconsider x = x as Element of (Polynom-Ring (n,L)) ;

A2: - (0_ (n,L)) = (- (0_ (n,L))) + (0_ (n,L)) by POLYNOM1:23

.= 0_ (n,L) by POLYRED:3 ;

0. (Polynom-Ring (n,L)) = 0_ (n,L) by POLYNOM1:def 11;

then x + (0. (Polynom-Ring (n,L))) = (- p) + (0_ (n,L)) by POLYNOM1:def 11

.= 0_ (n,L) by A1, A2, POLYNOM1:23

.= 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11 ;

then - p = - (0. (Polynom-Ring (n,L))) by RLVECT_1:6

.= 0. (Polynom-Ring (n,L)) by RLVECT_1:12

.= p by A1, POLYNOM1:def 11 ;

hence HT ((- p),T) = HT (p,T) ; :: thesis: verum

end;reconsider x = x as Element of (Polynom-Ring (n,L)) ;

A2: - (0_ (n,L)) = (- (0_ (n,L))) + (0_ (n,L)) by POLYNOM1:23

.= 0_ (n,L) by POLYRED:3 ;

0. (Polynom-Ring (n,L)) = 0_ (n,L) by POLYNOM1:def 11;

then x + (0. (Polynom-Ring (n,L))) = (- p) + (0_ (n,L)) by POLYNOM1:def 11

.= 0_ (n,L) by A1, A2, POLYNOM1:23

.= 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11 ;

then - p = - (0. (Polynom-Ring (n,L))) by RLVECT_1:6

.= 0. (Polynom-Ring (n,L)) by RLVECT_1:12

.= p by A1, POLYNOM1:def 11 ;

hence HT ((- p),T) = HT (p,T) ; :: thesis: verum

suppose
p <> 0_ (n,L)
; :: thesis: HT ((- p),T) = HT (p,T)

then A3:
Support p <> {}
by POLYNOM7:1;

then Support (- p) <> {} by Th5;

then HT ((- p),T) in Support (- p) by TERMORD:def 6;

then HT ((- p),T) in Support p by Th5;

then A4: HT ((- p),T) <= HT (p,T),T by TERMORD:def 6;

HT (p,T) in Support p by A3, TERMORD:def 6;

then HT (p,T) in Support (- p) by Th5;

then HT (p,T) <= HT ((- p),T),T by TERMORD:def 6;

hence HT ((- p),T) = HT (p,T) by A4, TERMORD:7; :: thesis: verum

end;then Support (- p) <> {} by Th5;

then HT ((- p),T) in Support (- p) by TERMORD:def 6;

then HT ((- p),T) in Support p by Th5;

then A4: HT ((- p),T) <= HT (p,T),T by TERMORD:def 6;

HT (p,T) in Support p by A3, TERMORD:def 6;

then HT (p,T) in Support (- p) by Th5;

then HT (p,T) <= HT ((- p),T),T by TERMORD:def 6;

hence HT ((- p),T) = HT (p,T) by A4, TERMORD:7; :: thesis: verum