let n be Ordinal; :: thesis: 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 ; :: 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 object st u in Support p holds
u in Support (- p)

proof

let u be object ; :: 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 4;
(- p) . u <> 0. L

proof

assume (- p) . u = 0. L ; :: thesis: contradiction
then - (- (p . u)) = - (0. L) by POLYNOM1:17;
then p . u = - (0. L) by RLVECT_1:17;
hence contradiction by A3, RLVECT_1:12; :: thesis: verum

end;

hence u in Support (- p) by POLYNOM1:def 4; :: 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 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

proof

let u be object ; :: 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 4;
then - (p . u) <> 0. L by POLYNOM1:17;
then p . u <> 0. L by RLVECT_1:12;
hence u in Support p by POLYNOM1:def 4; :: 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 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; :: 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 ;
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 ;
:: thesis: 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 ; :: 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:6, FINSEQ_1:14
.= (- (1. L)) * (Sum yp) by POLYNOM1:12
.= - ((1. L) * (eval (p,x))) by VECTSP_1:9, A8
.= - (eval (p,x)) ;
:: thesis: verum