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 ;
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;

A4: 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 A5: u in Support (- p) ; :: thesis: u in Support p
then reconsider u = u as Element of Bags n ;
reconsider u = u as bag of ;
(- p) . u <> 0. L by A5, 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 A6: SgmX (BagOrder n),(Support p) = SgmX (BagOrder n),(Support (- p)) by A1, TARSKI:2;
consider yp being FinSequence of the carrier of L such that
A7: ( len yp = len (SgmX (BagOrder n),(Support p)) & Sum yp = eval p,x & ( 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;
consider ymp being FinSequence of the carrier of L such that
A8: ( len ymp = len (SgmX (BagOrder n),(Support (- p))) & Sum ymp = eval (- p),x & ( 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;
A9: len ymp = len yp by A1, A4, A7, A8, TARSKI:2;
A10: dom ((- (1. L)) * yp) = dom yp by POLYNOM1:def 2;
consider k being Element of NAT such that
A11: k = len ((- (1. L)) * yp) ;
consider l being Element of NAT such that
A12: l = len yp ;
A13: ( dom ((- (1. L)) * yp) = Seg k & dom yp = Seg l ) by A11, A12, FINSEQ_1:def 3;
then A14: len ymp = len ((- (1. L)) * yp) by A9, A10, A11, A12, FINSEQ_1:8;
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 A15: ( 1 <= k & k <= len ymp ) ; :: thesis: ymp . k = ((- (1. L)) * yp) . k
then A16: k in Seg l by A9, A12, FINSEQ_1:3;
then A17: k in dom yp by A12, FINSEQ_1:def 3;
A18: ( 1 <= k & k <= len ((- (1. L)) * yp) ) by A9, A10, A11, A12, A13, A15, FINSEQ_1:8;
A19: ((- 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 by POLYNOM1:def 14;
k in Seg (len (SgmX (BagOrder n),(Support p))) by A7, A9, A15, FINSEQ_1:3;
then A20: k in dom (SgmX (BagOrder n),(Support p)) by FINSEQ_1:def 3;
A21: ( dom p = Bags n & dom (- p) = Bags n ) by FUNCT_2:def 1;
then A22: ( b in dom p & b in dom (- p) ) ;
then A23: k in dom ((- p) * (SgmX (BagOrder n),(Support p))) by A20, PARTFUN2:6;
A24: k in dom (p * (SgmX (BagOrder n),(Support p))) by A20, A22, PARTFUN2:6;
thus ((- p) * (SgmX (BagOrder n),(Support p))) /. k = (- p) /. b by A23, PARTFUN2:6
.= (- p) . b by A21, PARTFUN1:def 8
.= - (p . b) by POLYNOM1:def 22
.= - (p /. b) by A21, 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 A24, PARTFUN2:6 ; :: thesis: verum

end;

thus ymp . k = ymp /. k by A15, FINSEQ_4:24
.= ((- (1. L)) * ((p * (SgmX (BagOrder n),(Support p))) /. k)) * (eval (((SgmX (BagOrder n),(Support p)) /. k) @ ),x) by A6, A8, A15, A16, A19
.= (- ((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 A7, A9, A15, A16
.= - ((1. L) * (yp /. k)) by VECTSP_1:def 16
.= (- (1. L)) * (yp /. k) by VECTSP_1:41
.= ((- (1. L)) * yp) /. k by A17, POLYNOM1:def 2
.= ((- (1. L)) * yp) . k by A18, FINSEQ_4:24 ; :: thesis: verum

end;

hence eval (- p),x = Sum ((- (1. L)) * yp) by A8, A14, FINSEQ_1:18
.= (- (1. L)) * (eval p,x) by A7, POLYNOM1:28
.= - ((1. L) * (eval p,x)) by VECTSP_1:41
.= - (eval p,x) by VECTSP_1:def 16 ;
:: thesis: verum