let p be Prime; :: thesis: for n being non zero Nat
for F being Field
for E being FieldExtension of F st card E = p |^ n & F == PrimeField E holds
deg (E,F) = n
let n be non zero Nat; :: thesis: for F being Field
for E being FieldExtension of F st card E = p |^ n & F == PrimeField E holds
deg (E,F) = n
let F be Field; :: thesis: for E being FieldExtension of F st card E = p |^ n & F == PrimeField E holds
deg (E,F) = n
let E be FieldExtension of F; :: thesis: ( card E = p |^ n & F == PrimeField E implies deg (E,F) = n )
assume AS: ( card E = p |^ n & F == PrimeField E ) ; :: thesis: deg (E,F) = n
then A: ( E is finite & F is Subfield of E ) by FIELD_4:7;
then reconsider F1 = F as finite Field ;
reconsider E1 = E as FieldExtension of F1 ;
reconsider P = PrimeField E as finite Field by A;
set V = VecSp (E1,F1);
[#] (VecSp (E1,F1)) = the carrier of E1 by FIELD_4:def 6;
then [#] (VecSp (E1,F1)) is finite by AS;
then C: VecSp (E1,F1) is finite-dimensional by RANKNULL:4;
consider T being linear-transformation of (VecSp (E1,F1)),(F1 ^* (dim (VecSp (E1,F1)))) such that
E: T is bijective by C, VECTSP13:30, VECTSP13:def 10;
F: dom T = the carrier of (VecSp (E1,F1)) by FUNCT_2:def 1;
G: rng T = the carrier of (F1 ^* (dim (VecSp (E1,F1)))) by E, FUNCT_2:def 3;
card (dom T) = card (rng T) by E, CARD_1:70;
then A: card the carrier of (VecSp (E1,F1)) = (card P) |^ (dim (VecSp (E1,F1))) by AS, F, G, VECTSP13:31
.= p |^ (dim (VecSp (E1,F1))) by AS, FA2 ;
card the carrier of (VecSp (E1,F1)) = p |^ n by AS, FIELD_4:def 6;
then dim (VecSp (E1,F1)) = n by A, lemp;
hence deg (E,F) = n by C, FIELD_4:def 7; :: thesis: verum