let E be FieldExtension of F; ( E is F -finite implies E is F -algebraic )
assume AS:
E is F -finite
; E is F -algebraic
then reconsider n = deg (E,F) as Element of NAT by ORDINAL1:def 12;
H:
n = dim (VecSp (E,F))
by FIELD_4:def 7;
now for a being Element of E holds a is F -algebraic let a be
Element of
E;
b1 is F -algebraic per cases
( ex i, j being Element of NAT st
( i < j & j <= n & a |^ i = a |^ j ) or for i, j being Element of NAT holds
( not i < j or not j <= n or not a |^ i = a |^ j ) )
;
suppose
ex
i,
j being
Element of
NAT st
(
i < j &
j <= n &
a |^ i = a |^ j )
;
b1 is F -algebraic then consider i,
j being
Element of
NAT such that U:
(
i < j &
j <= n &
a |^ i = a |^ j )
;
set p1 =
<%(0. F),(1. F)%> `^ j;
set p2 =
<%(0. F),(1. F)%> `^ i;
set p =
(<%(0. F),(1. F)%> `^ j) - (<%(0. F),(1. F)%> `^ i);
then reconsider p =
(<%(0. F),(1. F)%> `^ j) - (<%(0. F),(1. F)%> `^ i) as non
zero Polynomial of
F by UPROOTS:def 5;
per cases
( i = 0 or not i is zero )
;
suppose T:
i = 0
;
b1 is F -algebraic then W:
a |^ i = 1_ E
by BINOM:8;
Ext_eval (
p,
a) =
(Ext_eval ((<%(0. F),(1. F)%> `^ j),a)) - (Ext_eval ((<%(0. F),(1. F)%> `^ i),a))
by FIELD_6:27
.=
(Ext_eval ((<%(0. F),(1. F)%> `^ j),a)) - (Ext_eval ((1_. F),a))
by T, POLYNOM5:15
.=
(Ext_eval ((<%(0. F),(1. F)%> `^ j),a)) - (1. E)
by FIELD_4:23
.=
(a |^ j) - (1. E)
by U, FIELD_6:22
.=
0. E
by W, U, RLVECT_1:15
;
hence
a is
F -algebraic
by FIELD_6:43;
verum end; suppose T:
not
i is
zero
;
b1 is F -algebraic Ext_eval (
p,
a) =
(Ext_eval ((<%(0. F),(1. F)%> `^ j),a)) - (Ext_eval ((<%(0. F),(1. F)%> `^ i),a))
by FIELD_6:27
.=
(a |^ j) - (Ext_eval ((<%(0. F),(1. F)%> `^ i),a))
by U, FIELD_6:22
.=
(a |^ j) - (a |^ i)
by T, FIELD_6:22
.=
0. E
by U, RLVECT_1:15
;
hence
a is
F -algebraic
by FIELD_6:43;
verum end; end; end; suppose U:
for
i,
j being
Element of
NAT holds
( not
i < j or not
j <= n or not
a |^ i = a |^ j )
;
b1 is F -algebraic set M =
{ (a |^ i) where i is Element of NAT : i <= n } ;
set V =
VecSp (
E,
F);
I:
{ (a |^ i) where i is Element of NAT : i <= n } c= the
carrier of
(VecSp (E,F))
{ (a |^ i) where i is Element of NAT : i <= n } is
finite
then reconsider M =
{ (a |^ i) where i is Element of NAT : i <= n } as
finite Subset of
(VecSp (E,F)) by I;
card M = n + 1
proof
set m =
n + 1;
defpred S1[
object ,
object ]
means ex
x being
Element of
Seg (n + 1) ex
y being
Element of
NAT st
(
F = x &
y = x - 1 &
c2 = a |^ y );
B1:
for
x,
y1,
y2 being
object st
x in Seg (n + 1) &
S1[
x,
y1] &
S1[
x,
y2] holds
y1 = y2
;
consider f being
Function such that C:
(
dom f = Seg (n + 1) & ( for
x being
object st
x in Seg (n + 1) holds
S1[
x,
f . x] ) )
from FUNCT_1:sch 2(B1, B2);
then A:
rng f = M
by A1, TARSKI:2;
now f is one-to-one assume
not
f is
one-to-one
;
contradictionthen consider x1,
x2 being
object such that A1:
(
x1 in dom f &
x2 in dom f &
f . x1 = f . x2 &
x1 <> x2 )
;
consider n1 being
Element of
Seg (n + 1),
y1 being
Element of
NAT such that A2:
(
x1 = n1 &
y1 = n1 - 1 &
f . x1 = a |^ y1 )
by A1, C;
consider n2 being
Element of
Seg (n + 1),
y2 being
Element of
NAT such that A3:
(
x2 = n2 &
y2 = n2 - 1 &
f . x2 = a |^ y2 )
by A1, C;
(
n1 <= n + 1 &
n2 <= n + 1 )
by FINSEQ_1:1;
then A4:
(
y1 < ((n + 1) - 1) + 1 &
y2 < ((n + 1) - 1) + 1 )
by A3, A2, XREAL_1:9, NAT_1:13;
A5:
y1 <> y2
by A1, A2, A3;
A6:
(
y1 <= n &
y2 <= n )
by A4, NAT_1:13;
end;
then card M =
card (Seg (n + 1))
by A, C, CARD_1:70
.=
n + 1
by FINSEQ_1:57
;
hence
card M = n + 1
;
verum
end; then
card M > n
by NAT_1:13;
then
M is
linearly-dependent
by H, AS, lemlin;
then consider l being
Linear_Combination of
M such that D1:
(
Sum l = 0. (VecSp (E,F)) &
Carrier l <> {} )
by VECTSP_7:def 1;
set z = the
Element of
Carrier l;
consider v being
Element of
(VecSp (E,F)) such that D2:
( the
Element of
Carrier l = v &
l . v <> 0. F )
by D1, VECTSP_6:1;
Carrier l c= M
by VECTSP_6:def 4;
then
the
Element of
Carrier l in M
by D1;
then consider i being
Element of
NAT such that D3:
( the
Element of
Carrier l = a |^ i &
i <= n )
;
consider pM being
Polynomial of
F such that D4a:
(
deg pM <= n & ( for
i being
Element of
NAT st
i <= n holds
pM . i = l . (a |^ i) ) )
by FIELD_6:47;
pM . i <> 0. F
by D3, D2, D4a;
then
pM <> 0_. F
;
then reconsider pM =
pM as non
zero Polynomial of
F by UPROOTS:def 5;
Ext_eval (
pM,
a) =
0. (VecSp (E,F))
by U, D1, D4a, FIELD_6:49
.=
0. E
by FIELD_4:def 6
;
hence
a is
F -algebraic
by FIELD_6:43;
verum end; end; end;
hence
E is F -algebraic
; verum