let n be Ordinal; :: thesis: for L being non empty non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L st ex b being bag of st Support p = {b} holds
for q being Polynomial of n,L
for x being Function of n,L holds eval (p + q),x = (eval p,x) + (eval q,x)
let L be non empty non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of n,L st ex b being bag of st Support p = {b} holds
for q being Polynomial of n,L
for x being Function of n,L holds eval (p + q),x = (eval p,x) + (eval q,x)
let p be Polynomial of n,L; :: thesis: ( ex b being bag of st Support p = {b} implies for q being Polynomial of n,L
for x being Function of n,L holds eval (p + q),x = (eval p,x) + (eval q,x) )
assume A1: ex b being bag of st Support p = {b} ; :: thesis: for q being Polynomial of n,L
for x being Function of n,L holds eval (p + q),x = (eval p,x) + (eval q,x)
let q be Polynomial of n,L; :: thesis: for x being Function of n,L holds eval (p + q),x = (eval p,x) + (eval q,x)
let x be Function of n,L; :: thesis: eval (p + q),x = (eval p,x) + (eval q,x)
consider b being bag of such that
A2: Support p = {b} by A1;
A3: b is Element of Bags n by POLYNOM1:def 14;
b in Support p by A2, TARSKI:def 1;
then A4: p . b <> 0. L by POLYNOM1:def 9;
A5: for b' being bag of st b' <> b holds
(p + q) . b' = q . b'

proof

let b' be bag of ; :: thesis: ( b' <> b implies (p + q) . b' = q . b' )
assume b' <> b ; :: thesis: (p + q) . b' = q . b'
then A6: not b' in Support p by A2, TARSKI:def 1;
A7: b' is Element of Bags n by POLYNOM1:def 14;
thus (p + q) . b' = (p . b') + (q . b') by POLYNOM1:def 21
.= (0. L) + (q . b') by A6, A7, POLYNOM1:def 9
.= q . b' by RLVECT_1:def 7 ; :: thesis: verum

end;

set sq = SgmX (BagOrder n),(Support q);
set spq = SgmX (BagOrder n),(Support (p + q));
consider ypq being FinSequence of the carrier of L such that
A8: ( len ypq = len (SgmX (BagOrder n),(Support (p + q))) & eval (p + q),x = Sum ypq & ( for i being Element of NAT st 1 <= i & i <= len ypq holds
ypq /. i = (((p + q) * (SgmX (BagOrder n),(Support (p + q)))) /. i) * (eval (((SgmX (BagOrder n),(Support (p + q))) /. i) @ ),x) ) ) by Def4;
consider yq being FinSequence of the carrier of L such that
A9: ( len yq = len (SgmX (BagOrder n),(Support q)) & eval q,x = Sum yq & ( for i being Element of NAT st 1 <= i & i <= len yq holds
yq /. i = ((q * (SgmX (BagOrder n),(Support q))) /. i) * (eval (((SgmX (BagOrder n),(Support q)) /. i) @ ),x) ) ) by Def4;
A10: ( BagOrder n linearly_orders Support q & BagOrder n linearly_orders Support (p + q) ) by Th20;
A11: Support (p + q) c= (Support p) \/ (Support q) by POLYNOM1:79;

now

per cases ( b in Support q or not b in Support q ) ;

case A12: b in Support q ; :: thesis: eval (p + q),x = (eval p,x) + (eval q,x)

now

per cases ( p . b = - (q . b) or p . b <> - (q . b) ) ;

case A13: p . b = - (q . b) ; :: thesis: eval (p + q),x = (eval q,x) + (eval p,x)

(p + q) . b = (p . b) + (q . b) by POLYNOM1:def 21
.= 0. L by A13, RLVECT_1:16 ;
then A14: not b in Support (p + q) by POLYNOM1:def 9;
A15: for u being set st u in (Support (p + q)) \/ {b} holds
u in Support q

proof

let u be set ; :: thesis: ( u in (Support (p + q)) \/ {b} implies u in Support q )
assume A16: u in (Support (p + q)) \/ {b} ; :: thesis: u in Support q

per cases ( u in Support (p + q) or u in {b} ) by A16, XBOOLE_0:def 3;

suppose A17: u in Support (p + q) ; :: thesis: u in Support q

then not u in {b} by A14, TARSKI:def 1;
hence u in Support q by A2, A11, A17, XBOOLE_0:def 3; :: thesis: verum

end;

suppose u in {b} ; :: thesis: u in Support q

hence u in Support q by A12, TARSKI:def 1; :: thesis: verum

end;

end;

end;

for u being set st u in Support q holds
u in (Support (p + q)) \/ {b}

proof

let u be set ; :: thesis: ( u in Support q implies u in (Support (p + q)) \/ {b} )
assume A18: u in Support q ; :: thesis: u in (Support (p + q)) \/ {b}
then reconsider u = u as bag of by POLYNOM1:def 14;

per cases ( u = b or u <> b ) ;

suppose u = b ; :: thesis: u in (Support (p + q)) \/ {b}

then u in {b} by TARSKI:def 1;
hence u in (Support (p + q)) \/ {b} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose u <> b ; :: thesis: u in (Support (p + q)) \/ {b}

then (p + q) . u = q . u by A5;
then A19: (p + q) . u <> 0. L by A18, POLYNOM1:def 9;
u is Element of Bags n by POLYNOM1:def 14;
then u in Support (p + q) by A19, POLYNOM1:def 9;
hence u in (Support (p + q)) \/ {b} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then A20: (Support (p + q)) \/ {b} = Support q by A15, TARSKI:2;
thus eval (p + q),x = (eval (p + q),x) + (0. L) by RLVECT_1:def 7
.= (eval (p + q),x) + (((q . b) * (eval b,x)) + (- ((q . b) * (eval b,x)))) by RLVECT_1:16
.= ((eval (p + q),x) + ((q . b) * (eval b,x))) + (- ((q . b) * (eval b,x))) by RLVECT_1:def 6
.= (eval q,x) + (- ((q . b) * (eval b,x))) by A5, A14, A20, Lm10
.= (eval q,x) + ((p . b) * (eval b,x)) by A13, VECTSP_1:41
.= (eval q,x) + (eval p,x) by A2, Th21 ; :: thesis: verum

end;

case A21: p . b <> - (q . b) ; :: thesis: eval (p + q),x = (eval p,x) + (eval q,x)

(p . b) + (q . b) <> (- (q . b)) + (q . b)

proof

assume A22: (p . b) + (q . b) = (- (q . b)) + (q . b) ; :: thesis: contradiction
p . b = (p . b) + (0. L) by RLVECT_1:def 7
.= (p . b) + ((q . b) + (- (q . b))) by RLVECT_1:16
.= ((- (q . b)) + (q . b)) + (- (q . b)) by A22, RLVECT_1:def 6
.= (0. L) + (- (q . b)) by RLVECT_1:16
.= - (q . b) by RLVECT_1:def 7 ;
hence contradiction by A21; :: thesis: verum

end;

then (p . b) + (q . b) <> 0. L by RLVECT_1:16;
then A23: (p + q) . b <> 0. L by POLYNOM1:def 21;
A24: for u being set st u in Support (p + q) holds
u in Support q

proof

let u be set ; :: thesis: ( u in Support (p + q) implies u in Support q )
assume A25: u in Support (p + q) ; :: thesis: u in Support q
then reconsider u = u as bag of by POLYNOM1:def 14;

per cases ( u in Support p or u in Support q ) by A11, A25, XBOOLE_0:def 3;

suppose u in Support p ; :: thesis: u in Support q

hence u in Support q by A2, A12, TARSKI:def 1; :: thesis: verum

end;

suppose u in Support q ; :: thesis: u in Support q

hence u in Support q ; :: thesis: verum

end;

end;

end;

A26: for u being set st u in Support q holds
u in Support (p + q)

proof

let u be set ; :: thesis: ( u in Support q implies u in Support (p + q) )
assume A27: u in Support q ; :: thesis: u in Support (p + q)
then reconsider u = u as bag of by POLYNOM1:def 14;

per cases ( u = b or u <> b ) ;

suppose u = b ; :: thesis: u in Support (p + q)

hence u in Support (p + q) by A3, A23, POLYNOM1:def 9; :: thesis: verum

end;

suppose u <> b ; :: thesis: u in Support (p + q)

then (p + q) . u = q . u by A5;
then A28: (p + q) . u <> 0. L by A27, POLYNOM1:def 9;
u is Element of Bags n by POLYNOM1:def 14;
hence u in Support (p + q) by A28, POLYNOM1:def 9; :: thesis: verum

end;

end;

end;

then A29: Support (p + q) = Support q by A24, TARSKI:2;
A30: len ypq = len yq by A8, A9, A24, A26, TARSKI:2;
b in rng (SgmX (BagOrder n),(Support q)) by A10, A12, TRIANG_1:def 2;
then consider k being Nat such that
A31: ( k in dom (SgmX (BagOrder n),(Support q)) & (SgmX (BagOrder n),(Support q)) . k = b ) by FINSEQ_2:11;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
consider sqk being Nat such that
A32: dom (SgmX (BagOrder n),(Support q)) = Seg sqk by FINSEQ_1:def 2;
consider spqk being Nat such that
A33: dom (SgmX (BagOrder n),(Support (p + q))) = Seg spqk by FINSEQ_1:def 2;
reconsider k = k, sqk = sqk, spqk = spqk as Element of NAT by ORDINAL1:def 13;
A34: sqk = len (SgmX (BagOrder n),(Support q)) by A32, FINSEQ_1:def 3
.= len (SgmX (BagOrder n),(Support (p + q))) by A24, A26, TARSKI:2
.= spqk by A33, FINSEQ_1:def 3 ;
A35: (SgmX (BagOrder n),(Support q)) /. k = b by A31, PARTFUN1:def 8;
A36: ( 1 <= k & k <= sqk ) by A31, A32, FINSEQ_1:3;
consider i being Nat such that
A37: dom yq = Seg i by FINSEQ_1:def 2;
A38: i in NAT by ORDINAL1:def 13;
then A39: len yq = i by A37, FINSEQ_1:def 3;
A40: sqk = len yq by A9, A32, FINSEQ_1:def 3;
then k <= i by A36, A37, A38, FINSEQ_1:def 3;
then A41: k in dom yq by A36, A37, FINSEQ_1:3;
A42: len ypq = sqk by A8, A33, A34, FINSEQ_1:def 3;
A43: dom q = Bags n by FUNCT_2:def 1;
then (SgmX (BagOrder n),(Support q)) . k in dom q by A31, POLYNOM1:def 14;
then A44: k in dom (q * (SgmX (BagOrder n),(Support q))) by A31, FUNCT_1:21;
A45: dom (p + q) = Bags n by FUNCT_2:def 1;
then (SgmX (BagOrder n),(Support q)) . k in dom (p + q) by A31, POLYNOM1:def 14;
then A46: k in dom ((p + q) * (SgmX (BagOrder n),(Support q))) by A31, FUNCT_1:21;
then A47: ((p + q) * (SgmX (BagOrder n),(Support q))) /. k = ((p + q) * (SgmX (BagOrder n),(Support q))) . k by PARTFUN1:def 8
.= (p + q) . b by A31, A46, FUNCT_1:22 ;
A48: (q * (SgmX (BagOrder n),(Support q))) /. k = (q * (SgmX (BagOrder n),(Support q))) . k by A44, PARTFUN1:def 8
.= q . b by A31, A44, FUNCT_1:22 ;
A49: ypq /. k = (((p + q) * (SgmX (BagOrder n),(Support (p + q)))) /. k) * (eval (((SgmX (BagOrder n),(Support (p + q))) /. k) @ ),x) by A8, A36, A42
.= ((p . b) + (q . b)) * (eval b,x) by A29, A35, A47, POLYNOM1:def 21
.= ((p . b) * (eval b,x)) + (((q * (SgmX (BagOrder n),(Support q))) /. k) * (eval (((SgmX (BagOrder n),(Support q)) /. k) @ ),x)) by A35, A48, VECTSP_1:def 18
.= ((p . b) * (eval b,x)) + (yq /. k) by A9, A36, A40 ;
for i' being Element of NAT st i' in dom yq & i' <> k holds
ypq /. i' = yq /. i'

proof

let i' be Element of NAT ; :: thesis: ( i' in dom yq & i' <> k implies ypq /. i' = yq /. i' )
assume A50: ( i' in dom yq & i' <> k ) ; :: thesis: ypq /. i' = yq /. i'
then A51: ( 1 <= i' & i' <= len yq ) by A37, A39, FINSEQ_1:3;
i' in Seg (len (SgmX (BagOrder n),(Support (p + q)))) by A8, A30, A50, FINSEQ_1:def 3;
then A52: i' in dom (SgmX (BagOrder n),(Support (p + q))) by FINSEQ_1:def 3;
A53: (SgmX (BagOrder n),(Support (p + q))) /. i' <> b

proof

assume (SgmX (BagOrder n),(Support (p + q))) /. i' = b ; :: thesis: contradiction
then A54: (SgmX (BagOrder n),(Support (p + q))) . i' = b by A52, PARTFUN1:def 8;
A55: (SgmX (BagOrder n),(Support (p + q))) . k = b by A24, A26, A31, TARSKI:2;
SgmX (BagOrder n),(Support (p + q)) is one-to-one by Th20, TRIANG_1:8;
hence contradiction by A31, A32, A33, A34, A50, A52, A54, A55, FUNCT_1:def 8; :: thesis: verum

end;

(SgmX (BagOrder n),(Support (p + q))) /. i' = (SgmX (BagOrder n),(Support (p + q))) . i' by A52, PARTFUN1:def 8;
then A56: i' in dom ((p + q) * (SgmX (BagOrder n),(Support (p + q)))) by A45, A52, FUNCT_1:21;
then A57: ((p + q) * (SgmX (BagOrder n),(Support (p + q)))) /. i' = ((p + q) * (SgmX (BagOrder n),(Support (p + q)))) . i' by PARTFUN1:def 8
.= (p + q) . ((SgmX (BagOrder n),(Support (p + q))) . i') by A56, FUNCT_1:22
.= (p + q) . ((SgmX (BagOrder n),(Support (p + q))) /. i') by A52, PARTFUN1:def 8 ;
A58: i' in dom (SgmX (BagOrder n),(Support q)) by A9, A37, A39, A50, FINSEQ_1:def 3;
(SgmX (BagOrder n),(Support q)) /. i' = (SgmX (BagOrder n),(Support q)) . i' by A32, A33, A34, A52, PARTFUN1:def 8;
then A59: i' in dom (q * (SgmX (BagOrder n),(Support q))) by A43, A58, FUNCT_1:21;
then A60: (q * (SgmX (BagOrder n),(Support q))) /. i' = (q * (SgmX (BagOrder n),(Support q))) . i' by PARTFUN1:def 8
.= q . ((SgmX (BagOrder n),(Support q)) . i') by A59, FUNCT_1:22
.= q . ((SgmX (BagOrder n),(Support q)) /. i') by A58, PARTFUN1:def 8 ;
thus ypq /. i' = (((p + q) * (SgmX (BagOrder n),(Support (p + q)))) /. i') * (eval (((SgmX (BagOrder n),(Support (p + q))) /. i') @ ),x) by A8, A30, A51
.= (q . ((SgmX (BagOrder n),(Support q)) /. i')) * (eval (((SgmX (BagOrder n),(Support q)) /. i') @ ),x) by A5, A29, A53, A57
.= yq /. i' by A9, A51, A60 ; :: thesis: verum

end;

hence eval (p + q),x = ((p . b) * (eval b,x)) + (Sum yq) by A8, A30, A41, A49, Th7
.= (eval p,x) + (eval q,x) by A2, A9, Th21 ;
:: thesis: verum

end;

end;

end;

hence eval (p + q),x = (eval p,x) + (eval q,x) ; :: thesis: verum

end;

case A61: not b in Support q ; :: thesis: eval (p + q),x = (eval q,x) + (eval p,x)

A62: (p + q) . b = (p . b) + (q . b) by POLYNOM1:def 21
.= (p . b) + (0. L) by A3, A61, POLYNOM1:def 9
.= p . b by RLVECT_1:def 7 ;
A63: for u being set st u in Support (p + q) holds
u in (Support p) \/ (Support q) by A11;
for u being set st u in (Support p) \/ (Support q) holds
u in Support (p + q)

proof

let u be set ; :: thesis: ( u in (Support p) \/ (Support q) implies u in Support (p + q) )
assume A64: u in (Support p) \/ (Support q) ; :: thesis: u in Support (p + q)

per cases ( u in Support p or u in Support q ) by A64, XBOOLE_0:def 3;

suppose u in Support p ; :: thesis: u in Support (p + q)

then u = b by A2, TARSKI:def 1;
hence u in Support (p + q) by A3, A4, A62, POLYNOM1:def 9; :: thesis: verum

end;

suppose A65: u in Support q ; :: thesis: u in Support (p + q)

then reconsider u = u as bag of by POLYNOM1:def 14;
A66: q . u <> 0. L by A65, POLYNOM1:def 9;
(p + q) . u = q . u by A5, A61, A65;
hence u in Support (p + q) by A65, A66, POLYNOM1:def 9; :: thesis: verum

end;

end;

end;

then Support (p + q) = {b} \/ (Support q) by A2, A63, TARSKI:2;
hence eval (p + q),x = (eval q,x) + (((p + q) . b) * (eval b,x)) by A5, A61, Lm10
.= (eval q,x) + (eval p,x) by A2, A62, Th21 ;
:: thesis: verum

end;

end;

end;

hence eval (p + q),x = (eval p,x) + (eval q,x) ; :: thesis: verum