let A, B be Ring; for x being Element of B
for p, q being Polynomial of A st A is Subring of B holds
Ext_eval ((p + q),x) = (Ext_eval (p,x)) + (Ext_eval (q,x))
let x be Element of B; for p, q being Polynomial of A st A is Subring of B holds
Ext_eval ((p + q),x) = (Ext_eval (p,x)) + (Ext_eval (q,x))
let p, q be Polynomial of A; ( A is Subring of B implies Ext_eval ((p + q),x) = (Ext_eval (p,x)) + (Ext_eval (q,x)) )
assume A0:
A is Subring of B
; Ext_eval ((p + q),x) = (Ext_eval (p,x)) + (Ext_eval (q,x))
reconsider k = max ((len p),(len q)) as Element of NAT ;
A1:
k - (len p) >= 0
by XREAL_1:48, XXREAL_0:25;
consider F1 being FinSequence of B such that
A2:
Ext_eval (p,x) = Sum F1
and
A3:
len F1 = len p
and
A4:
for n being Element of NAT st n in dom F1 holds
F1 . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by Def1;
A5: len (F1 ^ ((k -' (len F1)) |-> (0. B))) =
(len p) + (len ((k -' (len p)) |-> (0. B)))
by A3, FINSEQ_1:22
.=
(len p) + (k -' (len p))
by CARD_1:def 7
.=
(len p) + (k - (len p))
by A1, XREAL_0:def 2
.=
k
;
A6:
k - (len q) >= 0
by XREAL_1:48, XXREAL_0:25;
( k >= len p & k >= len q )
by XXREAL_0:25;
then A7:
k - (len (p + q)) >= 0
by POLYNOM4:6, XREAL_1:48;
consider F3 being FinSequence of B such that
A8:
Ext_eval ((p + q),x) = Sum F3
and
A9:
len F3 = len (p + q)
and
A10:
for n being Element of NAT st n in dom F3 holds
F3 . n = (In (((p + q) . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by Def1;
A11: len (F3 ^ ((k -' (len F3)) |-> (0. B))) =
(len F3) + (len ((k -' (len F3)) |-> (0. B)))
by FINSEQ_1:22
.=
(len (p + q)) + (k -' (len (p + q)))
by CARD_1:def 7, A9
.=
(len (p + q)) + (k - (len (p + q)))
by A7, XREAL_0:def 2
.=
k
;
consider F2 being FinSequence of B such that
A12:
Ext_eval (q,x) = Sum F2
and
A13:
len F2 = len q
and
A14:
for n being Element of NAT st n in dom F2 holds
F2 . n = (In ((q . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by Def1;
len (F2 ^ ((k -' (len F2)) |-> (0. B))) =
(len q) + (len ((k -' (len q)) |-> (0. B)))
by A13, FINSEQ_1:22
.=
(len q) + (k -' (len q))
by CARD_1:def 7
.=
(len q) + (k - (len q))
by A6, XREAL_0:def 2
.=
k
;
then reconsider G1 = F1 ^ ((k -' (len F1)) |-> (0. B)), G2 = F2 ^ ((k -' (len F2)) |-> (0. B)), G3 = F3 ^ ((k -' (len F3)) |-> (0. B)) as Element of k -tuples_on the carrier of B by A5, A11, FINSEQ_2:92;
now for n being Nat st n in Seg k holds
G3 . n = (G1 + G2) . nlet n be
Nat;
( n in Seg k implies G3 . b1 = (G1 + G2) . b1 )assume A15:
n in Seg k
;
G3 . b1 = (G1 + G2) . b1then A16:
0 + 1
<= n
by FINSEQ_1:1;
A17:
n <= k
by A15, FINSEQ_1:1;
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
;
G3 . b1 = (G1 + G2) . b1then
k = len p
by XXREAL_0:def 10;
then
len (p + q) = len p
by A18, POLYNOM4:7;
then A20:
n in dom F3
by A9, A15, A18, XXREAL_0:def 10, FINSEQ_1:def 3;
A21:
len G2 = k
by CARD_1:def 7;
then A22:
n in dom G2
by A15, FINSEQ_1:def 3;
then A23:
G2 /. n = G2 . n
by PARTFUN1:def 6;
len G1 = k
by CARD_1:def 7;
then A24:
n in dom G1
by A15, FINSEQ_1:def 3;
then A25:
G1 /. n = G1 . n
by PARTFUN1:def 6;
A26:
n in dom F1
by A3, A15, A18, XXREAL_0:def 10, FINSEQ_1:def 3;
A27:
G1 /. n =
G1 . n
by A24, PARTFUN1:def 6
.=
F1 . n
by A26, FINSEQ_1:def 7
.=
F1 /. n
by A26, PARTFUN1:def 6
;
A28:
F1 . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by A4, A26;
now G3 . n = (G1 + G2) . nper cases
( n <= len q or n > len q )
;
suppose
n <= len q
;
G3 . n = (G1 + G2) . nthen A29:
n in dom F2
by A16, A13, FINSEQ_3:25;
then A30:
F2 . n = (In ((q . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by A14;
A31:
G2 /. n =
G2 . n
by A22, PARTFUN1:def 6
.=
F2 . n
by A29, FINSEQ_1:def 7
.=
F2 /. n
by A29, PARTFUN1:def 6
;
thus G3 . n =
F3 . n
by A20, FINSEQ_1:def 7
.=
(In (((p + q) . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by A10, A20
.=
(In (((p . (n -' 1)) + (q . (n -' 1))),B)) * ((power B) . (x,(n -' 1)))
by NORMSP_1:def 2
.=
((In ((p . (n -' 1)),B)) + (In ((q . (n -' 1)),B))) * ((power B) . (x,(n -' 1)))
by A0, Th12
.=
((In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))) + ((In ((q . (n -' 1)),B)) * ((power B) . (x,(n -' 1))))
by VECTSP_1:def 3
.=
((In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))) + (F2 /. n)
by A29, A30, PARTFUN1:def 6
.=
(F1 /. n) + (F2 /. n)
by A26, A28, PARTFUN1:def 6
.=
(G1 + G2) . n
by A15, A25, A23, A27, A31, FVSUM_1:18
;
verum end; suppose A32:
n > len q
;
G3 . n = (G1 + G2) . nthen A33:
n >= (len q) + 1
by NAT_1:13;
then
n - 1
>= len q
by XREAL_1:19;
then A34:
n -' 1
>= len q
by XREAL_0:def 2;
n - (len F2) <= k - (len F2)
by A17, XREAL_1:9;
then A35:
n - (len F2) <= k -' (len F2)
by XREAL_0:def 2;
A36:
n - (len F2) >= 1
by A13, A33, XREAL_1:19;
then
n - (len F2) = n -' (len F2)
by XREAL_0:def 2;
then A37:
n - (len F2) in Seg (k -' (len F2))
by A36, A35;
n <= len G2
by A15, A21, FINSEQ_1:1;
then A38:
G2 /. n =
((k -' (len F2)) |-> (0. B)) . (n - (len F2))
by A13, A23, A32, FINSEQ_1:24
.=
0. B
by A37, FUNCOP_1:7
;
thus G3 . n =
F3 . n
by A20, FINSEQ_1:def 7
.=
(In (((p + q) . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by A10, A20
.=
(In (((p . (n -' 1)) + (q . (n -' 1))),B)) * ((power B) . (x,(n -' 1)))
by NORMSP_1:def 2
.=
(In (((p . (n -' 1)) + (0. A)),B)) * ((power B) . (x,(n -' 1)))
by A34, ALGSEQ_1:8
.=
F1 . n
by A4, A26
.=
(G1 /. n) + (0. B)
by A26, A27, PARTFUN1:def 6
.=
(G1 + G2) . n
by A15, A25, A23, A38, FVSUM_1:18
;
verum end; hence
G3 . n = (G1 + G2) . n
;
verum end; suppose A39:
len p < len q
;
G3 . b1 = (G1 + G2) . b1then
k = len q
by XXREAL_0:def 10;
then
len (p + q) = len q
by A39, POLYNOM4:7;
then A41:
n in dom F3
by A9, A15, A39, XXREAL_0:def 10, FINSEQ_1:def 3;
A42:
len G1 = k
by CARD_1:def 7;
then A43:
n in dom G1
by A15, FINSEQ_1:def 3;
then A44:
G1 /. n = G1 . n
by PARTFUN1:def 6;
len G2 = k
by CARD_1:def 7;
then A45:
n in dom G2
by A15, FINSEQ_1:def 3;
then A46:
G2 /. n = G2 . n
by PARTFUN1:def 6;
A47:
n in dom F2
by A13, A15, A39, XXREAL_0:def 10, FINSEQ_1:def 3;
A48:
G2 /. n =
G2 . n
by A45, PARTFUN1:def 6
.=
F2 . n
by A47, FINSEQ_1:def 7
.=
F2 /. n
by A47, PARTFUN1:def 6
;
A49:
F2 . n = (In ((q . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by A14, A47;
now G3 . n = (G1 + G2) . nper cases
( n <= len p or n > len p )
;
suppose
n <= len p
;
G3 . n = (G1 + G2) . nthen A50:
n in dom F1
by A16, A3, FINSEQ_3:25;
then A51:
F1 . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by A4;
A52:
G1 /. n =
G1 . n
by A43, PARTFUN1:def 6
.=
F1 . n
by A50, FINSEQ_1:def 7
.=
F1 /. n
by A50, PARTFUN1:def 6
;
thus G3 . n =
F3 . n
by A41, FINSEQ_1:def 7
.=
(In (((p + q) . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by A10, A41
.=
(In (((p . (n -' 1)) + (q . (n -' 1))),B)) * ((power B) . (x,(n -' 1)))
by NORMSP_1:def 2
.=
((In ((p . (n -' 1)),B)) + (In ((q . (n -' 1)),B))) * ((power B) . (x,(n -' 1)))
by A0, Th12
.=
((In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))) + ((In ((q . (n -' 1)),B)) * ((power B) . (x,(n -' 1))))
by VECTSP_1:def 3
.=
(F1 /. n) + ((In ((q . (n -' 1)),B)) * ((power B) . (x,(n -' 1))))
by A50, A51, PARTFUN1:def 6
.=
(F1 /. n) + (F2 /. n)
by A47, A49, PARTFUN1:def 6
.=
(G1 + G2) . n
by A15, A44, A46, A48, A52, FVSUM_1:18
;
verum end; suppose A53:
n > len p
;
G3 . n = (G1 + G2) . nthen A54:
n >= (len p) + 1
by NAT_1:13;
then
n - 1
>= len p
by XREAL_1:19;
then A55:
n -' 1
>= len p
by XREAL_0:def 2;
n - (len F1) <= k - (len F1)
by A17, XREAL_1:9;
then A56:
n - (len F1) <= k -' (len F1)
by XREAL_0:def 2;
A57:
n - (len F1) >= 1
by A3, A54, XREAL_1:19;
then
n - (len F1) = n -' (len F1)
by XREAL_0:def 2;
then A58:
n - (len F1) in Seg (k -' (len F1))
by A57, A56;
n <= len G1
by A15, A42, FINSEQ_1:1;
then A59:
G1 /. n =
((k -' (len F1)) |-> (0. B)) . (n - (len F1))
by A3, A44, A53, FINSEQ_1:24
.=
0. B
by A58, FUNCOP_1:7
;
thus G3 . n =
F3 . n
by A41, FINSEQ_1:def 7
.=
(In (((p + q) . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by A10, A41
.=
(In (((p . (n -' 1)) + (q . (n -' 1))),B)) * ((power B) . (x,(n -' 1)))
by NORMSP_1:def 2
.=
(In (((0. A) + (q . (n -' 1))),B)) * ((power B) . (x,(n -' 1)))
by A55, ALGSEQ_1:8
.=
F2 . n
by A14, A47
.=
(0. B) + (G2 /. n)
by A47, A48, PARTFUN1:def 6
.=
(G1 + G2) . n
by A15, A44, A46, A59, FVSUM_1:18
;
verum end; hence
G3 . n = (G1 + G2) . n
;
verum end; suppose A60:
len p = len q
;
G3 . b1 = (G1 + G2) . b1
len G2 = k
by CARD_1:def 7;
then A61:
n in dom G2
by A15, FINSEQ_1:def 3;
then A62:
G2 /. n = G2 . n
by PARTFUN1:def 6;
len G1 = k
by CARD_1:def 7;
then A63:
n in dom G1
by A15, FINSEQ_1:def 3;
then A64:
G1 /. n = G1 . n
by PARTFUN1:def 6;
A65:
len G3 = k
by CARD_1:def 7;
A66:
n in dom F2
by A13, A15, A60, FINSEQ_1:def 3;
A67:
n in dom F1
by A3, A15, A60, FINSEQ_1:def 3;
then A68:
F1 . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by A4;
A69:
G1 /. n =
G1 . n
by A63, PARTFUN1:def 6
.=
F1 . n
by A67, FINSEQ_1:def 7
.=
F1 /. n
by A67, PARTFUN1:def 6
;
now G3 . n = (G1 + G2) . nper cases
( n <= len (p + q) or n > len (p + q) )
;
suppose A70:
n <= len (p + q)
;
G3 . n = (G1 + G2) . nA71:
n in dom F2
by A13, A15, A60, FINSEQ_1:def 3;
then A72:
F2 . n = (In ((q . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by A14;
A73:
G2 /. n =
G2 . n
by A61, PARTFUN1:def 6
.=
F2 . n
by A71, FINSEQ_1:def 7
.=
F2 /. n
by A71, PARTFUN1:def 6
;
n in Seg (len (p + q))
by A16, A70;
then A74:
n in dom F3
by A9, FINSEQ_1:def 3;
hence G3 . n =
F3 . n
by FINSEQ_1:def 7
.=
(In (((p + q) . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by A10, A74
.=
(In (((p . (n -' 1)) + (q . (n -' 1))),B)) * ((power B) . (x,(n -' 1)))
by NORMSP_1:def 2
.=
((In ((p . (n -' 1)),B)) + (In ((q . (n -' 1)),B))) * ((power B) . (x,(n -' 1)))
by A0, Th12
.=
((In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))) + ((In ((q . (n -' 1)),B)) * ((power B) . (x,(n -' 1))))
by VECTSP_1:def 3
.=
((In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))) + (F2 /. n)
by A71, A72, PARTFUN1:def 6
.=
(F1 /. n) + (F2 /. n)
by A67, A68, PARTFUN1:def 6
.=
(G1 + G2) . n
by A15, A64, A62, A69, A73, FVSUM_1:18
;
verum end; suppose A75:
n > len (p + q)
;
G3 . n = (G1 + G2) . nthen A76:
n >= (len (p + q)) + 1
by NAT_1:13;
then
n - 1
>= ((len (p + q)) + 1) - 1
by XREAL_1:9;
then A77:
n -' 1
>= len (p + q)
by XREAL_0:def 2;
n - (len F3) <= k - (len F3)
by A17, XREAL_1:9;
then A78:
n - (len F3) <= k -' (len F3)
by XREAL_0:def 2;
A79:
G2 . n =
F2 . n
by A66, FINSEQ_1:def 7
.=
(In ((q . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by A14, A66
;
A80:
G1 . n =
F1 . n
by A67, FINSEQ_1:def 7
.=
(In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by A4, A67
;
A81:
n - (len F3) >= 1
by A9, A76, XREAL_1:19;
then
n - (len F3) = n -' (len F3)
by XREAL_0:def 2;
then A82:
n - (len F3) in Seg (k -' (len F3))
by A81, A78;
n <= len G3
by A15, A65, FINSEQ_1:1;
hence G3 . n =
((k -' (len F3)) |-> (0. B)) . (n - (len F3))
by A9, A75, FINSEQ_1:24
.=
(0. B) * ((power B) . (x,(n -' 1)))
by A82, FUNCOP_1:7
.=
(In ((0. A),B)) * ((power B) . (x,(n -' 1)))
by A0, Lm5
.=
(In (((p + q) . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by A77, ALGSEQ_1:8
.=
(In (((p . (n -' 1)) + (q . (n -' 1))),B)) * ((power B) . (x,(n -' 1)))
by NORMSP_1:def 2
.=
((In ((p . (n -' 1)),B)) + (In ((q . (n -' 1)),B))) * ((power B) . (x,(n -' 1)))
by A0, Th12
.=
((In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))) + ((In ((q . (n -' 1)),B)) * ((power B) . (x,(n -' 1))))
by VECTSP_1:def 3
.=
(G1 + G2) . n
by A15, A80, A79, FVSUM_1:18
;
verum end; hence
G3 . n = (G1 + G2) . n
;
verum end; end;
then A83:
G3 = G1 + G2
by FINSEQ_2:119;
A84: Sum G3 =
(Sum F3) + (Sum ((k -' (len F3)) |-> (0. B)))
by RLVECT_1:41
.=
(Sum F3) + (0. B)
by MATRIX_3:11
.=
Sum F3
;
A85: Sum G2 =
(Sum F2) + (Sum ((k -' (len F2)) |-> (0. B)))
by RLVECT_1:41
.=
(Sum F2) + (0. B)
by MATRIX_3:11
.=
Sum F2
;
Sum G1 =
(Sum F1) + (Sum ((k -' (len F1)) |-> (0. B)))
by RLVECT_1:41
.=
(Sum F1) + (0. B)
by MATRIX_3:11
.=
Sum F1
;
hence
Ext_eval ((p + q),x) = (Ext_eval (p,x)) + (Ext_eval (q,x))
by A2, A12, A8, A85, A84, A83, FVSUM_1:76; verum