let F be Field; for E being FieldExtension of F holds
( deg (E,F) = 1 iff the carrier of E = the carrier of F )
let E be FieldExtension of F; ( deg (E,F) = 1 iff the carrier of E = the carrier of F )
H0:
( F is Subring of E & F is Subfield of E )
by FIELD_4:def 1, FIELD_4:7;
then A:
( the carrier of F c= the carrier of E & 1. E = 1. F )
by C0SP1:def 3;
set V = VecSp (E,F);
reconsider e = 1. E as Element of (VecSp (E,F)) by FIELD_4:def 6;
Z:
now ( deg (E,F) = 1 implies the carrier of E = the carrier of F )assume AS:
deg (
E,
F)
= 1
;
the carrier of E = the carrier of Fthen H1:
VecSp (
E,
F) is
finite-dimensional
by FIELD_4:def 7;
dim (VecSp (E,F)) = 1
by AS, FIELD_4:def 7;
then consider v being
Element of
(VecSp (E,F)) such that B:
(
v <> 0. (VecSp (E,F)) &
(Omega). (VecSp (E,F)) = Lin {v} )
by H1, VECTSP_9:30;
C:
the
carrier of
(Lin {v}) = the
carrier of
(VecSp (E,F))
by B, VECTSP_4:def 4;
reconsider a =
v as
Element of
E by FIELD_4:def 6;
e in Lin {v}
by C;
then consider l being
Linear_Combination of
{v} such that D2:
e = Sum l
by VECTSP_7:7;
reconsider xF =
l . v as
Element of
F ;
reconsider xE =
xF as
Element of
E by A;
D3:
[xE,a] in [: the carrier of F, the carrier of E:]
by ZFMISC_1:def 2;
D4:
1. E =
(l . v) * v
by D2, VECTSP_6:17
.=
( the multF of E | [: the carrier of F, the carrier of E:]) . (
xF,
a)
by FIELD_4:def 6
.=
xE * a
by D3, FUNCT_1:49
;
then D5:
xE <> 0. E
;
not
xE is
zero
by D4;
then (xF ") * (1. F) =
(xE ") * (1. E)
by H0, FIELD_6:18
.=
((xE ") * xE) * a
by D4, GROUP_1:def 3
.=
(1. E) * a
by D5, VECTSP_1:def 10
;
then reconsider vF =
v as
Element of
F ;
now for o being object st o in the carrier of E holds
o in the carrier of Flet o be
object ;
( o in the carrier of E implies o in the carrier of F )assume
o in the
carrier of
E
;
o in the carrier of Fthen
o in Lin {v}
by C, FIELD_4:def 6;
then consider l being
Linear_Combination of
{v} such that E:
o = Sum l
by VECTSP_7:7;
reconsider x =
l . v as
Element of
F ;
F:
[x,a] in [: the carrier of F, the carrier of E:]
by ZFMISC_1:def 2;
G:
[x,vF] in [: the carrier of F, the carrier of F:]
by ZFMISC_1:def 2;
o =
(l . v) * v
by E, VECTSP_6:17
.=
( the multF of E | [: the carrier of F, the carrier of E:]) . (
x,
vF)
by FIELD_4:def 6
.=
the
multF of
E . (
x,
vF)
by F, FUNCT_1:49
.=
( the multF of E || the carrier of F) . (
x,
vF)
by G, FUNCT_1:49
.=
x * vF
by H0, C0SP1:def 3
;
hence
o in the
carrier of
F
;
verum end; hence
the
carrier of
E = the
carrier of
F
by A, TARSKI:2;
verum end;
now ( the carrier of E = the carrier of F implies deg (E,F) = 1 )assume AS1:
the
carrier of
E = the
carrier of
F
;
deg (E,F) = 1reconsider A =
{e} as
Subset of
(VecSp (E,F)) ;
0. (VecSp (E,F)) = 0. E
by FIELD_4:def 6;
then L:
A is
linearly-independent
by VECTSP_7:3;
H1:
the
carrier of
(Lin A) = { (Sum l) where l is Linear_Combination of A : verum }
by VECTSP_7:def 2;
H2:
now for o being object st o in the carrier of (VecSp (E,F)) holds
o in { (Sum l) where l is Linear_Combination of A : verum } let o be
object ;
( o in the carrier of (VecSp (E,F)) implies o in { (Sum l) where l is Linear_Combination of A : verum } )assume
o in the
carrier of
(VecSp (E,F))
;
o in { (Sum l) where l is Linear_Combination of A : verum } then reconsider v =
o as
Element of the
carrier of
(VecSp (E,F)) ;
reconsider a =
v as
Element of
E by FIELD_4:def 6;
defpred S1[
object ,
object ]
means ( ( $1
= e & $2
= a ) or ( $1
<> e & $2
= 0. E ) );
G0:
for
x being
object st
x in the
carrier of
(VecSp (E,F)) holds
ex
y being
object st
(
y in the
carrier of
E &
S1[
x,
y] )
consider f being
Function of the
carrier of
(VecSp (E,F)), the
carrier of
E such that G1:
for
x being
object st
x in the
carrier of
(VecSp (E,F)) holds
S1[
x,
f . x]
from FUNCT_2:sch 1(G0);
(
dom f = the
carrier of
(VecSp (E,F)) &
rng f c= the
carrier of
E )
by FUNCT_2:def 1;
then reconsider f =
f as
Element of
Funcs ( the
carrier of
(VecSp (E,F)), the
carrier of
F)
by AS1, FUNCT_2:def 2;
ex
T being
finite Subset of
(VecSp (E,F)) st
for
v being
Element of
(VecSp (E,F)) st not
v in T holds
f . v = 0. F
then reconsider l =
f as
Linear_Combination of
VecSp (
E,
F)
by VECTSP_6:def 1;
then
Carrier l c= A
;
then reconsider l =
l as
Linear_Combination of
A by VECTSP_6:def 4;
Sum l =
(l . e) * e
by VECTSP_6:17
.=
( the multF of E | [: the carrier of F, the carrier of E:]) . (
(l . e),
e)
by FIELD_4:def 6
.=
a * (1. E)
by AS1, G1
.=
v
;
hence
o in { (Sum l) where l is Linear_Combination of A : verum }
;
verum end; then
the
carrier of
(VecSp (E,F)) = { (Sum l) where l is Linear_Combination of A : verum }
by H2, TARSKI:2;
then M:
{(1. E)} is
Basis of
(VecSp (E,F))
by H1, L, VECTSP_4:31, VECTSP_7:def 3;
H4:
card {(1. E)} = 1
by CARD_1:30;
H5:
VecSp (
E,
F) is
finite-dimensional
by M, MATRLIN:def 1;
then
dim (VecSp (E,F)) = 1
by M, H4, VECTSP_9:def 1;
hence
deg (
E,
F)
= 1
by H5, FIELD_4:def 7;
verum end;
hence
( deg (E,F) = 1 iff the carrier of E = the carrier of F )
by Z; verum