let n be Ordinal; for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L
for x being Function of n,L holds eval ((- p),x) = - (eval (p,x))
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; for p being Polynomial of n,L
for x being Function of n,L holds eval ((- p),x) = - (eval (p,x))
let p be Polynomial of n,L; for x being Function of n,L holds eval ((- p),x) = - (eval (p,x))
let x be Function of n,L; eval ((- p),x) = - (eval (p,x))
set mp = - p;
A1:
for u being object st u in Support p holds
u in Support (- p)
consider ymp being FinSequence of the carrier of L such that
A4:
len ymp = len (SgmX ((BagOrder n),(Support (- p))))
and
A5:
Sum ymp = eval ((- p),x)
and
A6:
for i being Element of NAT st 1 <= i & i <= len ymp holds
ymp /. i = (((- p) * (SgmX ((BagOrder n),(Support (- p))))) /. i) * (eval (((SgmX ((BagOrder n),(Support (- p)))) /. i),x))
by Def2;
consider yp being FinSequence of the carrier of L such that
A7:
len yp = len (SgmX ((BagOrder n),(Support p)))
and
A8:
Sum yp = eval (p,x)
and
A9:
for i being Element of NAT st 1 <= i & i <= len yp holds
yp /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x))
by Def2;
A10:
for u being object st u in Support (- p) holds
u in Support p
then A12:
len ymp = len yp
by A1, A7, A4, TARSKI:2;
A13:
dom ((- (1. L)) * yp) = dom yp
by POLYNOM1:def 1;
consider k being Element of NAT such that
A14:
k = len ((- (1. L)) * yp)
;
consider l being Element of NAT such that
A15:
l = len yp
;
A16:
dom ((- (1. L)) * yp) = Seg k
by A14, FINSEQ_1:def 3;
A17:
SgmX ((BagOrder n),(Support p)) = SgmX ((BagOrder n),(Support (- p)))
by A1, A10, TARSKI:2;
A18:
for k being Nat st 1 <= k & k <= len ymp holds
ymp . k = ((- (1. L)) * yp) . k
proof
let k be
Nat;
( 1 <= k & k <= len ymp implies ymp . k = ((- (1. L)) * yp) . k )
assume that A19:
1
<= k
and A20:
k <= len ymp
;
ymp . k = ((- (1. L)) * yp) . k
A21:
k <= len ((- (1. L)) * yp)
by A12, A13, A14, A16, A20, FINSEQ_1:def 3;
A22:
((- p) * (SgmX ((BagOrder n),(Support p)))) /. k = (- (1. L)) * ((p * (SgmX ((BagOrder n),(Support p)))) /. k)
proof
reconsider b =
(SgmX ((BagOrder n),(Support p))) /. k as
bag of
n ;
k in Seg (len (SgmX ((BagOrder n),(Support p))))
by A7, A12, A19, A20, FINSEQ_1:1;
then A23:
k in dom (SgmX ((BagOrder n),(Support p)))
by FINSEQ_1:def 3;
A24:
dom p = Bags n
by FUNCT_2:def 1;
then
b in dom p
;
then A25:
k in dom (p * (SgmX ((BagOrder n),(Support p))))
by A23, PARTFUN2:3;
A26:
dom (- p) = Bags n
by FUNCT_2:def 1;
then
b in dom (- p)
;
then
k in dom ((- p) * (SgmX ((BagOrder n),(Support p))))
by A23, PARTFUN2:3;
hence ((- p) * (SgmX ((BagOrder n),(Support p)))) /. k =
(- p) /. b
by PARTFUN2:3
.=
(- p) . b
by A26, PARTFUN1:def 6
.=
- (p . b)
by POLYNOM1:17
.=
- ((1. L) * (p /. b))
by A24, PARTFUN1:def 6
.=
(- (1. L)) * (p /. b)
by VECTSP_1:9
.=
(- (1. L)) * ((p * (SgmX ((BagOrder n),(Support p)))) /. k)
by A25, PARTFUN2:3
;
verum
end;
A27:
k in Seg l
by A12, A15, A19, A20, FINSEQ_1:1;
then A28:
k in dom yp
by A15, FINSEQ_1:def 3;
thus ymp . k =
ymp /. k
by A19, A20, FINSEQ_4:15
.=
((- (1. L)) * ((p * (SgmX ((BagOrder n),(Support p)))) /. k)) * (eval (((SgmX ((BagOrder n),(Support p))) /. k),x))
by A17, A6, A19, A20, A27, A22
.=
(- ((1. L) * ((p * (SgmX ((BagOrder n),(Support p)))) /. k))) * (eval (((SgmX ((BagOrder n),(Support p))) /. k),x))
by VECTSP_1:9
.=
- (((p * (SgmX ((BagOrder n),(Support p)))) /. k) * (eval (((SgmX ((BagOrder n),(Support p))) /. k),x)))
by VECTSP_1:9
.=
- (yp /. k)
by A9, A12, A19, A20, A27
.=
- ((1. L) * (yp /. k))
.=
(- (1. L)) * (yp /. k)
by VECTSP_1:9
.=
((- (1. L)) * yp) /. k
by A28, POLYNOM1:def 1
.=
((- (1. L)) * yp) . k
by A19, A21, FINSEQ_4:15
;
verum
end;
dom yp = Seg l
by A15, FINSEQ_1:def 3;
hence eval ((- p),x) =
Sum ((- (1. L)) * yp)
by A5, A12, A13, A14, A15, A16, A18, FINSEQ_1:6, FINSEQ_1:14
.=
(- (1. L)) * (Sum yp)
by POLYNOM1:12
.=
- ((1. L) * (eval (p,x)))
by VECTSP_1:9, A8
.=
- (eval (p,x))
;
verum