let n be Ordinal; 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; 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 ; for p being Polynomial of n,L holds HT ((- p),T) = HT (p,T)
let p be Polynomial of n,L; HT ((- p),T) = HT (p,T)
per cases
( p = 0_ (n,L) or p <> 0_ (n,L) )
;
suppose A1:
p = 0_ (
n,
L)
;
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)
;
verum end; suppose
p <> 0_ (
n,
L)
;
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;
verum end;