let F be Field; :: thesis: for E1 being F -finite FieldExtension of F
for E2 being FieldExtension of F st E1,E2 are_isomorphic_over F holds
( E2 is F -finite & deg (E1,F) = deg (E2,F) )
let E1 be F -finite FieldExtension of F; :: thesis: for E2 being FieldExtension of F st E1,E2 are_isomorphic_over F holds
( E2 is F -finite & deg (E1,F) = deg (E2,F) )
let E2 be FieldExtension of F; :: thesis: ( E1,E2 are_isomorphic_over F implies ( E2 is F -finite & deg (E1,F) = deg (E2,F) ) )
assume E1,E2 are_isomorphic_over F ; :: thesis: ( E2 is F -finite & deg (E1,F) = deg (E2,F) )
then consider h being Function of E1,E2 such that
A: h is F -isomorphism ;
H: ( the carrier of (VecSp (E1,F)) = the carrier of E1 & the carrier of (VecSp (E2,F)) = the carrier of E2 ) by FIELD_4:def 6;
reconsider E = E2 as E1 -homomorphic FieldExtension of F by A, RING_2:def 4;
reconsider h = h as Homomorphism of E1,E by A;
reconsider i = h as linear-transformation of (VecSp (E1,F)),(VecSp (E,F)) by A, lintrans;
C: VecSp (E1,F) is finite-dimensional by FIELD_4:def 8;
i is bijective by H, A;
then D: ( VecSp (E2,F) is finite-dimensional & dim (VecSp (E1,F)) = dim (VecSp (E2,F)) ) by C, VECTSP12:4;
hence E2 is F -finite by FIELD_4:def 8; :: thesis: deg (E1,F) = deg (E2,F)
thus deg (E1,F) = dim (VecSp (E2,F)) by D, FIELD_4:def 7
.= deg (E2,F) by D, FIELD_4:def 7 ; :: thesis: verum