let n be Ordinal; :: thesis: for L being non empty 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 empty non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: 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; :: thesis: for x being Function of n,L holds eval (- p),x = - (eval p,x)
let x be Function of n,L; :: thesis: eval (- p),x = - (eval p,x)
set mp = - p;
A1: for u being set st u in Support p holds
u in Support (- p)

proof

let u be set ; :: thesis: ( u in Support p implies u in Support (- p) )
assume A2: u in Support p ; :: thesis: u in Support (- p)
then reconsider u = u as Element of Bags n ;
reconsider u = u as bag of n ;
A3: p . u <> 0. L by A2, POLYNOM1:def 9;
(- p) . u <> 0. L

proof

assume (- p) . u = 0. L ; :: thesis: contradiction
then - (- (p . u)) = - (0. L) by POLYNOM1:def 22;
then p . u = - (0. L) by RLVECT_1:30;
hence contradiction by A3, RLVECT_1:25; :: thesis: verum

end;

hence u in Support (- p) by POLYNOM1:def 9; :: thesis: verum

end;

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 Def4;
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 Def4;
A10: for u being set st u in Support (- p) holds
u in Support p

proof

let u be set ; :: thesis: ( u in Support (- p) implies u in Support p )
assume A11: u in Support (- p) ; :: thesis: u in Support p
then reconsider u = u as Element of Bags n ;
reconsider u = u as bag of n ;
(- p) . u <> 0. L by A11, POLYNOM1:def 9;
then - (p . u) <> 0. L by POLYNOM1:def 22;
then p . u <> 0. L by RLVECT_1:25;
hence u in Support p by POLYNOM1:def 9; :: thesis: verum

end;

then A12: len ymp = len yp by A1, A7, A4, TARSKI:2;
A13: dom ((- (1. L)) * yp) = dom yp by POLYNOM1:def 2;
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; :: thesis: ( 1 <= k & k <= len ymp implies ymp . k = ((- (1. L)) * yp) . k )
assume that
A19: 1 <= k and
A20: k <= len ymp ; :: thesis: 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 by PRE_POLY:def 12;
k in Seg (len (SgmX (BagOrder n),(Support p))) by A7, A12, A19, A20, FINSEQ_1:3;
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:6;
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:6;
hence ((- p) * (SgmX (BagOrder n),(Support p))) /. k = (- p) /. b by PARTFUN2:6
.= (- p) . b by A26, PARTFUN1:def 8
.= - (p . b) by POLYNOM1:def 22
.= - (p /. b) by A24, PARTFUN1:def 8
.= - ((1. L) * (p /. b)) by VECTSP_1:def 16
.= (- (1. L)) * (p /. b) by VECTSP_1:41
.= (- (1. L)) * ((p * (SgmX (BagOrder n),(Support p))) /. k) by A25, PARTFUN2:6 ;
:: thesis: verum

end;

A27: k in Seg l by A12, A15, A19, A20, FINSEQ_1:3;
then A28: k in dom yp by A15, FINSEQ_1:def 3;
thus ymp . k = ymp /. k by A19, A20, FINSEQ_4:24
.= ((- (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:41
.= (- ((p * (SgmX (BagOrder n),(Support p))) /. k)) * (eval (((SgmX (BagOrder n),(Support p)) /. k) @ ),x) by VECTSP_1:def 16
.= - (((p * (SgmX (BagOrder n),(Support p))) /. k) * (eval (((SgmX (BagOrder n),(Support p)) /. k) @ ),x)) by VECTSP_1:41
.= - (yp /. k) by A9, A12, A19, A20, A27
.= - ((1. L) * (yp /. k)) by VECTSP_1:def 16
.= (- (1. L)) * (yp /. k) by VECTSP_1:41
.= ((- (1. L)) * yp) /. k by A28, POLYNOM1:def 2
.= ((- (1. L)) * yp) . k by A19, A21, FINSEQ_4:24 ; :: thesis: 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:8, FINSEQ_1:18
.= (- (1. L)) * (Sum yp) by POLYNOM1:28
.= (- (1. L)) * (eval p,x) by A8, POLYNOM1:28
.= - ((1. L) * (eval p,x)) by VECTSP_1:41
.= - (eval p,x) by VECTSP_1:def 16 ;
:: thesis: verum