let F be Field; for E being FieldExtension of F
for K being b1 -extending FieldExtension of F st K is F -finite holds
( E is F -finite & deg (E,F) <= deg (K,F) & K is E -finite & deg (K,E) <= deg (K,F) )
let E be FieldExtension of F; for K being E -extending FieldExtension of F st K is F -finite holds
( E is F -finite & deg (E,F) <= deg (K,F) & K is E -finite & deg (K,E) <= deg (K,F) )
let K be E -extending FieldExtension of F; ( K is F -finite implies ( E is F -finite & deg (E,F) <= deg (K,F) & K is E -finite & deg (K,E) <= deg (K,F) ) )
assume AS:
K is F -finite
; ( E is F -finite & deg (E,F) <= deg (K,F) & K is E -finite & deg (K,E) <= deg (K,F) )
hence
( E is F -finite & deg (E,F) <= deg (K,F) )
by FIELD_5:15; ( K is E -finite & deg (K,E) <= deg (K,F) )
set BF = the Basis of (VecSp (K,F));
reconsider BF = the Basis of (VecSp (K,F)) as finite Subset of (VecSp (K,F)) by AS;
H0: the carrier of (VecSp (K,E)) =
the carrier of K
by FIELD_4:def 6
.=
the carrier of (VecSp (K,F))
by FIELD_4:def 6
;
then reconsider BE = BF as finite Subset of (VecSp (K,E)) ;
Lin BE = VecSp (K,E)
then consider I being Subset of (VecSp (K,E)) such that
A:
( I c= BE & I is linearly-independent & Lin I = VecSp (K,E) )
by VECTSP_7:18;
reconsider I = I as finite Subset of (VecSp (K,E)) by A;
B:
I is Basis of (VecSp (K,E))
by A, VECTSP_7:def 3;
D:
VecSp (K,E) is finite-dimensional
by A, VECTSP_7:def 3, MATRLIN:def 1;
hence
K is E -finite
by FIELD_4:def 8; deg (K,E) <= deg (K,F)
VecSp (K,F) is finite-dimensional
by AS, FIELD_4:def 8;
then F:
( dim (VecSp (K,E)) = card I & dim (VecSp (K,F)) = card BE )
by B, D, VECTSP_9:def 1;
( deg (K,E) = dim (VecSp (K,E)) & deg (K,F) = dim (VecSp (K,F)) )
by AS, D, FIELD_4:def 7;
hence
deg (K,E) <= deg (K,F)
by F, A, NAT_1:43; verum