let A, B be Ring; for x being Element of B
for z0, z1 being Element of A st A is Subring of B holds
Ext_eval (<%z0,z1%>,x) = (In (z0,B)) + ((In (z1,B)) * x)
let x be Element of B; for z0, z1 being Element of A st A is Subring of B holds
Ext_eval (<%z0,z1%>,x) = (In (z0,B)) + ((In (z1,B)) * x)
let z0, z1 be Element of A; ( A is Subring of B implies Ext_eval (<%z0,z1%>,x) = (In (z0,B)) + ((In (z1,B)) * x) )
assume A0:
A is Subring of B
; Ext_eval (<%z0,z1%>,x) = (In (z0,B)) + ((In (z1,B)) * x)
consider F being FinSequence of B such that
A1:
Ext_eval (<%z0,z1%>,x) = Sum F
and
A2:
len F = len <%z0,z1%>
and
A3:
for n being Element of NAT st n in dom F holds
F . n = (In ((<%z0,z1%> . (n -' 1)),B)) * ((power B) . (x,(n -' 1)))
by Def1;
not not len F = 0 & ... & not len F = 2
by A2, POLYNOM5:39;
per cases then
( len F = 0 or len F = 1 or len F = 2 )
;
suppose
len F = 0
;
Ext_eval (<%z0,z1%>,x) = (In (z0,B)) + ((In (z1,B)) * x)then A4:
<%z0,z1%> = 0_. A
by A2, POLYNOM4:5;
hence Ext_eval (
<%z0,z1%>,
x) =
0. B
by Th17
.=
In (
(0. A),
B)
by A0, Lm5
.=
In (
((0_. A) . 0),
B)
by FUNCOP_1:7
.=
(In (z0,B)) + ((0. B) * x)
by A4, POLYNOM5:38
.=
(In (z0,B)) + ((In ((0. A),B)) * x)
by A0, Lm5
.=
(In (z0,B)) + ((In (((0_. A) . 1),B)) * x)
by FUNCOP_1:7
.=
(In (z0,B)) + ((In (z1,B)) * x)
by A4, POLYNOM5:38
;
verum end; suppose A5:
len F = 1
;
Ext_eval (<%z0,z1%>,x) = (In (z0,B)) + ((In (z1,B)) * x)then F . 1 =
(In ((<%z0,z1%> . (1 -' 1)),B)) * ((power B) . (x,(1 -' 1)))
by A3, FINSEQ_3:25
.=
(In ((<%z0,z1%> . 0),B)) * ((power B) . (x,(1 -' 1)))
by XREAL_1:232
.=
(In ((<%z0,z1%> . 0),B)) * ((power B) . (x,0))
by XREAL_1:232
.=
(In (z0,B)) * ((power B) . (x,0))
by POLYNOM5:38
.=
(In (z0,B)) * (1_ B)
by GROUP_1:def 7
.=
In (
z0,
B)
;
then
F = <*(In (z0,B))*>
by A5, FINSEQ_1:40;
hence Ext_eval (
<%z0,z1%>,
x) =
(In (z0,B)) + ((0. B) * x)
by A1, RLVECT_1:44
.=
(In (z0,B)) + ((In ((0. A),B)) * x)
by A0, Lm5
.=
(In (z0,B)) + ((In ((<%z0,z1%> . 1),B)) * x)
by A2, A5, ALGSEQ_1:8
.=
(In (z0,B)) + ((In (z1,B)) * x)
by POLYNOM5:38
;
verum end; suppose A6:
len F = 2
;
Ext_eval (<%z0,z1%>,x) = (In (z0,B)) + ((In (z1,B)) * x)then A7:
F . 1 =
(In ((<%z0,z1%> . (1 -' 1)),B)) * ((power B) . (x,(1 -' 1)))
by A3, FINSEQ_3:25
.=
(In ((<%z0,z1%> . 0),B)) * ((power B) . (x,(1 -' 1)))
by XREAL_1:232
.=
(In ((<%z0,z1%> . 0),B)) * ((power B) . (x,0))
by XREAL_1:232
.=
(In (z0,B)) * ((power B) . (x,0))
by POLYNOM5:38
.=
(In (z0,B)) * (1_ B)
by GROUP_1:def 7
.=
In (
z0,
B)
;
A8:
2
-' 1
= 2
- 1
by XREAL_0:def 2;
F . 2 =
(In ((<%z0,z1%> . (2 -' 1)),B)) * ((power B) . (x,(2 -' 1)))
by A3, A6, FINSEQ_3:25
.=
(In (z1,B)) * ((power B) . (x,1))
by A8, POLYNOM5:38
.=
(In (z1,B)) * x
by GROUP_1:50
;
then
F = <*(In (z0,B)),((In (z1,B)) * x)*>
by A6, A7, FINSEQ_1:44;
hence
Ext_eval (
<%z0,z1%>,
x)
= (In (z0,B)) + ((In (z1,B)) * x)
by A1, RLVECT_1:45;
verum end;