let L be non empty right_complementable Abelian add-associative right_zeroed unital left-distributive doubleLoopStr ; :: thesis: for p, q being Polynomial of L
for x being Element of L holds eval (p + q),x = (eval p,x) + (eval q,x)
let p, q be Polynomial of L; :: thesis: for x being Element of L holds eval (p + q),x = (eval p,x) + (eval q,x)
let x be Element of L; :: thesis: eval (p + q),x = (eval p,x) + (eval q,x)
consider F1 being FinSequence of the carrier of L such that
A1:
eval p,x = Sum F1
and
A2:
len F1 = len p
and
A3:
for n being Element of NAT st n in dom F1 holds
F1 . n = (p . (n -' 1)) * ((power L) . x,(n -' 1))
by Def2;
consider F2 being FinSequence of the carrier of L such that
A4:
eval q,x = Sum F2
and
A5:
len F2 = len q
and
A6:
for n being Element of NAT st n in dom F2 holds
F2 . n = (q . (n -' 1)) * ((power L) . x,(n -' 1))
by Def2;
consider F3 being FinSequence of the carrier of L such that
A7:
eval (p + q),x = Sum F3
and
A8:
len F3 = len (p + q)
and
A9:
for n being Element of NAT st n in dom F3 holds
F3 . n = ((p + q) . (n -' 1)) * ((power L) . x,(n -' 1))
by Def2;
reconsider k = max (len p),(len q) as Element of NAT by FINSEQ_2:1;
( k >= len p & k >= len q )
by XXREAL_0:25;
then A10:
( k - (len p) >= 0 & k - (len q) >= 0 & k - (len (p + q)) >= 0 )
by Th9, XREAL_1:50;
A11: len (F1 ^ ((k -' (len F1)) |-> (0. L))) =
(len p) + (len ((k -' (len p)) |-> (0. L)))
by A2, FINSEQ_1:35
.=
(len p) + (k -' (len p))
by FINSEQ_1:def 18
.=
(len p) + (k - (len p))
by A10, XREAL_0:def 2
.=
k
;
A12: len (F2 ^ ((k -' (len F2)) |-> (0. L))) =
(len q) + (len ((k -' (len q)) |-> (0. L)))
by A5, FINSEQ_1:35
.=
(len q) + (k -' (len q))
by FINSEQ_1:def 18
.=
(len q) + (k - (len q))
by A10, XREAL_0:def 2
.=
k
;
len (F3 ^ ((k -' (len F3)) |-> (0. L))) =
(len (p + q)) + (len ((k -' (len (p + q))) |-> (0. L)))
by A8, FINSEQ_1:35
.=
(len (p + q)) + (k -' (len (p + q)))
by FINSEQ_1:def 18
.=
(len (p + q)) + (k - (len (p + q)))
by A10, XREAL_0:def 2
.=
k
;
then reconsider G1 = F1 ^ ((k -' (len F1)) |-> (0. L)), G2 = F2 ^ ((k -' (len F2)) |-> (0. L)), G3 = F3 ^ ((k -' (len F3)) |-> (0. L)) as Element of k -tuples_on the carrier of L by A11, A12, FINSEQ_2:110;
A13: Sum G1 =
(Sum F1) + (Sum ((k -' (len F1)) |-> (0. L)))
by RLVECT_1:58
.=
(Sum F1) + (0. L)
by MATRIX_3:13
.=
Sum F1
by RLVECT_1:def 7
;
A14: Sum G2 =
(Sum F2) + (Sum ((k -' (len F2)) |-> (0. L)))
by RLVECT_1:58
.=
(Sum F2) + (0. L)
by MATRIX_3:13
.=
Sum F2
by RLVECT_1:def 7
;
A15: Sum G3 =
(Sum F3) + (Sum ((k -' (len F3)) |-> (0. L)))
by RLVECT_1:58
.=
(Sum F3) + (0. L)
by MATRIX_3:13
.=
Sum F3
by RLVECT_1:def 7
;
now let n be
Nat;
:: thesis: ( n in Seg k implies G3 . b1 = (G1 + G2) . b1 )assume A16:
n in Seg k
;
:: thesis: G3 . b1 = (G1 + G2) . b1then A17:
(
0 + 1
<= n &
n <= k )
by FINSEQ_1:3;
per cases
( len p > len q or len p < len q or len p = len q )
by XXREAL_0:1;
suppose A18:
len p > len q
;
:: thesis: G3 . b1 = (G1 + G2) . b1then A19:
k = len p
by XXREAL_0:def 10;
then A20:
len (p + q) = len p
by A18, Th10;
A21:
n in dom F1
by A2, A16, A19, FINSEQ_1:def 3;
A22:
n in dom F3
by A8, A16, A19, A20, FINSEQ_1:def 3;
A23:
F1 . n = (p . (n -' 1)) * ((power L) . x,(n -' 1))
by A3, A21;
A24:
(
len G1 = k &
len G2 = k )
by FINSEQ_1:def 18;
then A25:
(
n in dom G1 &
n in dom G2 )
by A16, FINSEQ_1:def 3;
then A26:
(
G1 /. n = G1 . n &
G2 /. n = G2 . n )
by PARTFUN1:def 8;
A27:
G1 /. n =
G1 . n
by A25, PARTFUN1:def 8
.=
F1 . n
by A21, FINSEQ_1:def 7
.=
F1 /. n
by A21, PARTFUN1:def 8
;
now per cases
( n <= len q or n > len q )
;
suppose
n <= len q
;
:: thesis: G3 . n = (G1 + G2) . nthen
n in Seg (len q)
by A17, FINSEQ_1:3;
then A28:
n in dom F2
by A5, FINSEQ_1:def 3;
then A29:
F2 . n = (q . (n -' 1)) * ((power L) . x,(n -' 1))
by A6;
A30:
G2 /. n =
G2 . n
by A25, PARTFUN1:def 8
.=
F2 . n
by A28, FINSEQ_1:def 7
.=
F2 /. n
by A28, PARTFUN1:def 8
;
thus G3 . n =
F3 . n
by A22, FINSEQ_1:def 7
.=
((p + q) . (n -' 1)) * ((power L) . x,(n -' 1))
by A9, A22
.=
((p . (n -' 1)) + (q . (n -' 1))) * ((power L) . x,(n -' 1))
by NORMSP_1:def 5
.=
((p . (n -' 1)) * ((power L) . x,(n -' 1))) + ((q . (n -' 1)) * ((power L) . x,(n -' 1)))
by VECTSP_1:def 12
.=
((p . (n -' 1)) * ((power L) . x,(n -' 1))) + (F2 /. n)
by A28, A29, PARTFUN1:def 8
.=
(F1 /. n) + (F2 /. n)
by A21, A23, PARTFUN1:def 8
.=
(G1 + G2) . n
by A16, A26, A27, A30, FVSUM_1:22
;
:: thesis: verum end; suppose A31:
n > len q
;
:: thesis: G3 . n = (G1 + G2) . nthen A32:
n >= (len q) + 1
by NAT_1:13;
then
n - 1
>= len q
by XREAL_1:21;
then A33:
n -' 1
>= len q
by XREAL_0:def 2;
A34:
n - (len F2) >= 1
by A5, A32, XREAL_1:21;
then A35:
n - (len F2) = n -' (len F2)
by XREAL_0:def 2;
n - (len F2) <= k - (len F2)
by A17, XREAL_1:11;
then
n - (len F2) <= k -' (len F2)
by XREAL_0:def 2;
then A36:
n - (len F2) in Seg (k -' (len F2))
by A34, A35, FINSEQ_1:3;
n <= len G2
by A16, A24, FINSEQ_1:3;
then A37:
G2 /. n =
((k -' (len F2)) |-> (0. L)) . (n - (len F2))
by A5, A26, A31, FINSEQ_1:37
.=
0. L
by A36, FUNCOP_1:13
;
thus G3 . n =
F3 . n
by A22, FINSEQ_1:def 7
.=
((p + q) . (n -' 1)) * ((power L) . x,(n -' 1))
by A9, A22
.=
((p . (n -' 1)) + (q . (n -' 1))) * ((power L) . x,(n -' 1))
by NORMSP_1:def 5
.=
((p . (n -' 1)) + (0. L)) * ((power L) . x,(n -' 1))
by A33, ALGSEQ_1:22
.=
(p . (n -' 1)) * ((power L) . x,(n -' 1))
by RLVECT_1:10
.=
F1 . n
by A3, A21
.=
G1 /. n
by A21, A27, PARTFUN1:def 8
.=
(G1 /. n) + (0. L)
by RLVECT_1:10
.=
(G1 + G2) . n
by A16, A26, A37, FVSUM_1:22
;
:: thesis: verum end; hence
G3 . n = (G1 + G2) . n
;
:: thesis: verum end; suppose A38:
len p < len q
;
:: thesis: G3 . b1 = (G1 + G2) . b1then A39:
k = len q
by XXREAL_0:def 10;
then A40:
len (p + q) = len q
by A38, Th10;
A41:
n in dom F2
by A5, A16, A39, FINSEQ_1:def 3;
A42:
n in dom F3
by A8, A16, A39, A40, FINSEQ_1:def 3;
A43:
F2 . n = (q . (n -' 1)) * ((power L) . x,(n -' 1))
by A6, A41;
A44:
(
len G1 = k &
len G2 = k )
by FINSEQ_1:def 18;
then A45:
(
n in dom G1 &
n in dom G2 )
by A16, FINSEQ_1:def 3;
then A46:
(
G1 /. n = G1 . n &
G2 /. n = G2 . n )
by PARTFUN1:def 8;
A47:
G2 /. n =
G2 . n
by A45, PARTFUN1:def 8
.=
F2 . n
by A41, FINSEQ_1:def 7
.=
F2 /. n
by A41, PARTFUN1:def 8
;
now per cases
( n <= len p or n > len p )
;
suppose
n <= len p
;
:: thesis: G3 . n = (G1 + G2) . nthen
n in Seg (len p)
by A17, FINSEQ_1:3;
then A48:
n in dom F1
by A2, FINSEQ_1:def 3;
then A49:
F1 . n = (p . (n -' 1)) * ((power L) . x,(n -' 1))
by A3;
A50:
G1 /. n =
G1 . n
by A45, PARTFUN1:def 8
.=
F1 . n
by A48, FINSEQ_1:def 7
.=
F1 /. n
by A48, PARTFUN1:def 8
;
thus G3 . n =
F3 . n
by A42, FINSEQ_1:def 7
.=
((p + q) . (n -' 1)) * ((power L) . x,(n -' 1))
by A9, A42
.=
((p . (n -' 1)) + (q . (n -' 1))) * ((power L) . x,(n -' 1))
by NORMSP_1:def 5
.=
((p . (n -' 1)) * ((power L) . x,(n -' 1))) + ((q . (n -' 1)) * ((power L) . x,(n -' 1)))
by VECTSP_1:def 12
.=
(F1 /. n) + ((q . (n -' 1)) * ((power L) . x,(n -' 1)))
by A48, A49, PARTFUN1:def 8
.=
(F1 /. n) + (F2 /. n)
by A41, A43, PARTFUN1:def 8
.=
(G1 + G2) . n
by A16, A46, A47, A50, FVSUM_1:22
;
:: thesis: verum end; suppose A51:
n > len p
;
:: thesis: G3 . n = (G1 + G2) . nthen A52:
n >= (len p) + 1
by NAT_1:13;
then
n - 1
>= len p
by XREAL_1:21;
then A53:
n -' 1
>= len p
by XREAL_0:def 2;
A54:
n - (len F1) >= 1
by A2, A52, XREAL_1:21;
then A55:
n - (len F1) = n -' (len F1)
by XREAL_0:def 2;
n - (len F1) <= k - (len F1)
by A17, XREAL_1:11;
then
n - (len F1) <= k -' (len F1)
by XREAL_0:def 2;
then A56:
n - (len F1) in Seg (k -' (len F1))
by A54, A55, FINSEQ_1:3;
n <= len G1
by A16, A44, FINSEQ_1:3;
then A57:
G1 /. n =
((k -' (len F1)) |-> (0. L)) . (n - (len F1))
by A2, A46, A51, FINSEQ_1:37
.=
0. L
by A56, FUNCOP_1:13
;
thus G3 . n =
F3 . n
by A42, FINSEQ_1:def 7
.=
((p + q) . (n -' 1)) * ((power L) . x,(n -' 1))
by A9, A42
.=
((p . (n -' 1)) + (q . (n -' 1))) * ((power L) . x,(n -' 1))
by NORMSP_1:def 5
.=
((0. L) + (q . (n -' 1))) * ((power L) . x,(n -' 1))
by A53, ALGSEQ_1:22
.=
(q . (n -' 1)) * ((power L) . x,(n -' 1))
by RLVECT_1:10
.=
F2 . n
by A6, A41
.=
G2 /. n
by A41, A47, PARTFUN1:def 8
.=
(0. L) + (G2 /. n)
by RLVECT_1:10
.=
(G1 + G2) . n
by A16, A46, A57, FVSUM_1:22
;
:: thesis: verum end; hence
G3 . n = (G1 + G2) . n
;
:: thesis: verum end; suppose A58:
len p = len q
;
:: thesis: G3 . b1 = (G1 + G2) . b1then A59:
(
n in dom F1 &
n in dom F2 )
by A2, A5, A16, FINSEQ_1:def 3;
then A60:
F1 . n = (p . (n -' 1)) * ((power L) . x,(n -' 1))
by A3;
A61:
(
len G1 = k &
len G2 = k &
len G3 = k )
by FINSEQ_1:def 18;
then A62:
(
n in dom G1 &
n in dom G2 &
n in dom G3 )
by A16, FINSEQ_1:def 3;
then A63:
(
G1 /. n = G1 . n &
G2 /. n = G2 . n &
G3 /. n = G3 . n )
by PARTFUN1:def 8;
A64:
G1 /. n =
G1 . n
by A62, PARTFUN1:def 8
.=
F1 . n
by A59, FINSEQ_1:def 7
.=
F1 /. n
by A59, PARTFUN1:def 8
;
now per cases
( n <= len (p + q) or n > len (p + q) )
;
suppose A65:
n <= len (p + q)
;
:: thesis: G3 . n = (G1 + G2) . nA66:
n in dom F2
by A5, A16, A58, FINSEQ_1:def 3;
then A67:
F2 . n = (q . (n -' 1)) * ((power L) . x,(n -' 1))
by A6;
n in Seg (len (p + q))
by A17, A65, FINSEQ_1:3;
then A68:
n in dom F3
by A8, FINSEQ_1:def 3;
A69:
G2 /. n =
G2 . n
by A62, PARTFUN1:def 8
.=
F2 . n
by A66, FINSEQ_1:def 7
.=
F2 /. n
by A66, PARTFUN1:def 8
;
thus G3 . n =
F3 . n
by A68, FINSEQ_1:def 7
.=
((p + q) . (n -' 1)) * ((power L) . x,(n -' 1))
by A9, A68
.=
((p . (n -' 1)) + (q . (n -' 1))) * ((power L) . x,(n -' 1))
by NORMSP_1:def 5
.=
((p . (n -' 1)) * ((power L) . x,(n -' 1))) + ((q . (n -' 1)) * ((power L) . x,(n -' 1)))
by VECTSP_1:def 12
.=
((p . (n -' 1)) * ((power L) . x,(n -' 1))) + (F2 /. n)
by A66, A67, PARTFUN1:def 8
.=
(F1 /. n) + (F2 /. n)
by A59, A60, PARTFUN1:def 8
.=
(G1 + G2) . n
by A16, A63, A64, A69, FVSUM_1:22
;
:: thesis: verum end; suppose A70:
n > len (p + q)
;
:: thesis: G3 . n = (G1 + G2) . nthen A71:
n >= (len (p + q)) + 1
by NAT_1:13;
then A72:
n - (len F3) >= 1
by A8, XREAL_1:21;
then A73:
n - (len F3) = n -' (len F3)
by XREAL_0:def 2;
n - 1
>= ((len (p + q)) + 1) - 1
by A71, XREAL_1:11;
then A74:
n -' 1
>= len (p + q)
by XREAL_0:def 2;
n - (len F3) <= k - (len F3)
by A17, XREAL_1:11;
then
n - (len F3) <= k -' (len F3)
by XREAL_0:def 2;
then A75:
n - (len F3) in Seg (k -' (len F3))
by A72, A73, FINSEQ_1:3;
A76:
G1 . n =
F1 . n
by A59, FINSEQ_1:def 7
.=
(p . (n -' 1)) * ((power L) . x,(n -' 1))
by A3, A59
;
A77:
G2 . n =
F2 . n
by A59, FINSEQ_1:def 7
.=
(q . (n -' 1)) * ((power L) . x,(n -' 1))
by A6, A59
;
n <= len G3
by A16, A61, FINSEQ_1:3;
hence G3 . n =
((k -' (len F3)) |-> (0. L)) . (n - (len F3))
by A8, A70, FINSEQ_1:37
.=
0. L
by A75, FUNCOP_1:13
.=
(0. L) * ((power L) . x,(n -' 1))
by Lm2
.=
((p + q) . (n -' 1)) * ((power L) . x,(n -' 1))
by A74, ALGSEQ_1:22
.=
((p . (n -' 1)) + (q . (n -' 1))) * ((power L) . x,(n -' 1))
by NORMSP_1:def 5
.=
((p . (n -' 1)) * ((power L) . x,(n -' 1))) + ((q . (n -' 1)) * ((power L) . x,(n -' 1)))
by VECTSP_1:def 12
.=
(G1 + G2) . n
by A16, A76, A77, FVSUM_1:22
;
:: thesis: verum end; hence
G3 . n = (G1 + G2) . n
;
:: thesis: verum end; end;
then
G3 = G1 + G2
by FINSEQ_2:139;
hence
eval (p + q),x = (eval p,x) + (eval q,x)
by A1, A4, A7, A13, A14, A15, FVSUM_1:95; :: thesis: verum