defpred S1[ Nat] means for T being finite F -algebraic Subset of E st card T = F holds
FAdj (F,T) is F -finite ;
X:
F is Subring of E
by FIELD_4:def 1;
IA:
S1[ 0 ]
proof
let T be
finite F -algebraic Subset of
E;
( card T = 0 implies FAdj (F,T) is F -finite )
assume
card T = 0
;
FAdj (F,T) is F -finite
then AS:
T = {}
;
Y:
carrierFA T = { x where x is Element of E : for U being Subfield of E st F is Subfield of U & T is Subset of U holds
x in U }
by FIELD_6:def 5;
set P =
FAdj (
F,
T);
reconsider E1 =
F as
FieldExtension of
F by FIELD_4:6;
A1:
the
carrier of
(FAdj (F,T)) = the
carrier of
E1
B2:
1. (FAdj (F,T)) =
1. E
by FIELD_6:def 6
.=
1. F
by X, C0SP1:def 3
;
B4: the
addF of
(FAdj (F,T)) =
the
addF of
E || (carrierFA T)
by FIELD_6:def 6
.=
the
addF of
E || the
carrier of
F
by A1, FIELD_6:def 6
.=
the
addF of
F
by X, C0SP1:def 3
;
B5: the
multF of
(FAdj (F,T)) =
the
multF of
E || (carrierFA T)
by FIELD_6:def 6
.=
the
multF of
E || the
carrier of
F
by A1, FIELD_6:def 6
.=
the
multF of
F
by X, C0SP1:def 3
;
reconsider h =
id E1 as
Function of
E1,
(FAdj (F,T)) by A1;
reconsider P =
FAdj (
F,
T) as
E1 -homomorphic FieldExtension of
F ;
(
h is
additive &
h is
multiplicative &
h is
unity-preserving )
by B4, B5, B2;
then reconsider h =
h as
Homomorphism of
E1,
P ;
for
a being
Element of
E1 st
a in F holds
h . a = a
;
then reconsider g =
h as
linear-transformation of
(VecSp (E1,F)),
(VecSp (P,F)) by lintrans;
the
carrier of
E1 = the
carrier of
F
;
then
deg (
E1,
F)
= 1
by quah1;
then
{(1. E1)} is
Basis of
(VecSp (E1,F))
by quah2;
then A2:
VecSp (
E1,
F) is
finite-dimensional
by MATRLIN:def 1;
A3:
( the
carrier of
(VecSp (E1,F)) = the
carrier of
E1 & the
carrier of
(VecSp (P,F)) = the
carrier of
P )
by FIELD_4:def 6;
g is
bijective
by A1, A3;
then
VecSp (
P,
F) is
finite-dimensional
by A2, VECTSP12:4;
hence
FAdj (
F,
T) is
F -finite
by FIELD_4:def 8;
verum
end;
IS:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume IV:
S1[
k]
;
S1[k + 1]now for T being finite F -algebraic Subset of E st card T = k + 1 holds
FAdj (F,T) is F -finite let T be
finite F -algebraic Subset of
E;
( card T = k + 1 implies FAdj (F,T) is F -finite )assume AS:
card T = k + 1
;
FAdj (F,T) is F -finite set a = the
Element of
T;
I:
T <> {}
by AS;
then H:
the
Element of
T in T
;
then reconsider a = the
Element of
T as
Element of
E ;
set T1 =
T \ {a};
then
T \ {a} is
F -algebraic
;
then reconsider T1 =
T \ {a} as
finite F -algebraic Subset of
E ;
A0:
{a} \/ T1 = {a} \/ T
by XBOOLE_1:39;
{a} c= T
by H, TARSKI:def 1;
then A1:
T = {a} \/ T1
by A0, XBOOLE_1:12;
then
card T = (card T1) + 1
by A1, CARD_2:41;
then A3:
FAdj (
F,
T1) is
F -finite
by AS, IV;
reconsider E1 =
E as
FieldExtension of
FAdj (
F,
T1)
by FIELD_4:7;
reconsider a1 =
a as
Element of
E1 ;
consider p being non
zero Polynomial of
F such that H1:
Ext_eval (
p,
a)
= 0. E
by I, defTalg, FIELD_6:43;
H3:
p <> 0_. F
;
reconsider p =
p as non
zero Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
the
carrier of
(Polynom-Ring F) c= the
carrier of
(Polynom-Ring (FAdj (F,T1)))
by FIELD_4:10;
then reconsider p1 =
p as
Element of the
carrier of
(Polynom-Ring (FAdj (F,T1))) ;
H4:
p <> 0_. (FAdj (F,T1))
by H3, FIELD_4:12;
reconsider p1 =
p1 as non
zero Element of the
carrier of
(Polynom-Ring (FAdj (F,T1))) by H4, UPROOTS:def 5;
Ext_eval (
p1,
a1)
= 0. E
by H1, lemma7b;
then A4:
a1 is
FAdj (
F,
T1)
-algebraic
by FIELD_6:43;
FAdj (
(FAdj (F,T1)),
{a1})
= FAdj (
F,
T)
by A1, ug;
hence
FAdj (
F,
T) is
F -finite
by A3, A4;
verum end; hence
S1[
k + 1]
;
verum end;
I:
for k being Nat holds S1[k]
from NAT_1:sch 2(IA, IS);
consider n being Nat such that
H:
card T = n
;
thus
FAdj (F,T) is F -finite
by I, H; verum