:: Algebraic Extensions
:: by Christoph Schwarzweller and Agnieszka Rowin\'nska-Schwarzweller
::
:: Received March 30, 2021
:: Copyright (c) 2021-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_3, VECTSP_1, ALGSTR_0, TARSKI, VECTSP_2, STRUCT_0,
SUBSET_1, SUPINF_2, BINOP_1, NAT_1, MESFUNC1, REALSET1, C0SP1, FUNCT_2,
POLYNOM1, POLYNOM2, POLYNOM3, FUNCSDOM, RLVECT_5, CARD_1, HURWITZ,
RLVECT_1, RLVECT_2, FINSEQ_1, FUNCT_1, RELAT_1, LATTICES, EC_PF_1,
RANKNULL, XBOOLE_0, FINSET_1, NUMBERS, POLYNOM5, GROUP_1, ZFMISC_1,
FUNCT_7, AFINSQ_1, MSSUBFAM, GROUP_6, PBOOLE, ALGNUM_1, ARYTM_1,
RLVECT_3, MOD_4, RING_2, RING_3, FIELD_4, NEWTON, XXREAL_0, CARD_3,
XCMPLX_0, QC_LANG1, FOMODEL1, FIELD_1, RLSUB_1, FIELD_6, GLIB_000,
FIELD_7;
notations TARSKI, XBOOLE_0, SUBSET_1, BINOP_1, RELAT_1, REALSET1, FUNCT_1,
RELSET_1, FUNCT_2, PARTFUN1, FINSEQ_1, MEMBERED, ZFMISC_1, ORDINAL1,
NUMBERS, FINSET_1, CARD_1, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, INT_1,
STRUCT_0, VFUNCT_1, POLYNOM1, POLYNOM3, POLYNOM4, POLYNOM5, GROUP_1,
GROUP_4, GROUP_6, MOD_4, VECTSP_4, VECTSP_6, VECTSP_7, BINOM, ALGSTR_0,
ALGSTR_1, RLVECT_1, VECTSP_2, VECTSP_9, RANKNULL, MATRLIN, HURWITZ,
VECTSP_1, ALGSEQ_1, C0SP1, EC_PF_1, RATFUNC1, RING_2, RING_3, RING_4,
ALGNUM_1, FIELD_1, FIELD_4, FIELD_6;
constructors XREAL_0, HURWITZ, VECTSP_1, STRUCT_0, C0SP1, ARYTM_1, ARYTM_0,
XCMPLX_0, XXREAL_0, SUBSET_1, ORDINAL1, NAT_1, ALGSTR_0, NORMSP_1, INT_1,
POLYNOM4, XBOOLE_0, RELSET_1, ARYTM_3, QUOFIELD, PARTFUN1, RLVECT_1,
NAT_D, FUNCT_7, VFUNCT_1, CARD_1, FINSET_1, POLYNOM1, RATFUNC1, GCD_1,
POLYNOM5, REALSET1, MEMBERED, BINOM, POLYDIFF, EC_PF_1, ALGSEQ_1,
VECTSP_9, RLVECT_5, RING_2, RINGCAT1, FUNCOP_1, GROUP_4, ALGNUM_1,
VECTSP_6, VECTSP_7, GROUP_6, RANKNULL, FIELD_1, FIELD_4, FIELD_5,
FIELD_6;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, XXREAL_0, XREAL_0,
INT_1, MEMBERED, STRUCT_0, VECTSP_1, ALGSTR_1, NUMBERS, EC_PF_1,
POLYNOM4, FUNCT_2, ALGSTR_0, POLYNOM3, SUBSET_1, GROUP_1, MOD_4,
RLVECT_1, FINSET_1, FUNCT_1, CARD_1, C0SP1, RATFUNC1, RELAT_1, RINGCAT1,
RING_2, RING_4, NAT_1, UPROOTS, REALSET1, PRE_POLY, POLYNOM1, POLYNOM5,
FIELD_4, FIELD_6;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions STRUCT_0, ALGSTR_0, VECTSP_1, GROUP_1, RLVECT_1, FUNCT_1, TARSKI,
XBOOLE_0, POLYNOM3, GROUP_6, ALGNUM_1;
equalities BINOP_1, REALSET1, XCMPLX_0, STRUCT_0, ALGSTR_0, POLYNOM3,
VECTSP_1, ALGNUM_1;
expansions STRUCT_0, GROUP_1, ALGSTR_0, RLVECT_1, VECTSP_1, TARSKI, GROUP_6,
REALSET1, FUNCT_1, FUNCT_2, ALGNUM_1;
theorems GROUP_1, VECTSP_1, VECTSP_2, RLVECT_1, FUNCT_2, XBOOLE_1, XBOOLE_0,
SUBSET_1, TARSKI, CARD_1, FUNCT_1, RING_3, REALSET1, ORDINAL1, UPROOTS,
VECTSP_6, POLYNOM5, CARD_2, EC_PF_1, RING_2, XREAL_1, INT_1, BINOM,
C0SP1, HURWITZ, POLYNOM3, ALGNUM_1, NAT_1, FINSEQ_1, GROUP_6, VECTSP12,
ZFMISC_1, FIELD_4, MATRLIN, VECTSP_4, POLYDIFF, VECTSP_7, VECTSP_9,
XXREAL_0, MOD_2, ALGSEQ_1, POLYNOM1, FIELD_1, XCMPLX_1, FIELD_5, FIELD_6;
schemes NAT_1, FUNCT_1, FUNCT_2, FINSEQ_1;
begin :: Preliminaries
definition
let L1,L2 be doubleLoopStr;
pred L1 == L2 means
the doubleLoopStr of L1 = the doubleLoopStr of L2;
reflexivity;
symmetry;
end;
theorem
for R,S being Ring
holds R == S iff ex f being Function of R,S st f = id R & f is isomorphism
proof
let R,S being Ring;
A: now assume B0: R == S;
thus ex f being Function of R,S st f = id R & f is isomorphism
proof
reconsider f = id R as Function of R,S by B0;
take f;
f is additive multiplicative unity-preserving by B0;
hence thesis by B0;
end;
end;
now assume ex f being Function of R,S st f = id R & f is isomorphism;
then consider f being Function of R,S such that
B0: f = id R & f is isomorphism;
B1: now let o be object;
assume o in the carrier of R;
then reconsider a = o as Element of R;
f.a in the carrier of S;
hence o in the carrier of S by B0;
end;
BB: now let o be object;
assume B2: o in the carrier of S;
rng f = the carrier of S by B0,FUNCT_2:def 3;
hence o in the carrier of R by B2,B0;
end; then
B2: the carrier of S = the carrier of R by B1,TARSKI:2;
H: f is additive multiplicative unity-preserving by B0;
B4: 0.S = f.(0.R) by B0,RING_2:6 .= 0.R by B0;
now let x be object;
assume x in [:the carrier of R,the carrier of R:]; then
consider a,b being object such that
B5: a in the carrier of R & b in the carrier of R & x = [a,b]
by ZFMISC_1:def 2;
reconsider a,b as Element of R by B5;
thus (the addF of R).x = f.(a + b) by B5,B0
.= f.a + f.b by H
.= (the addF of S).x by B0,B5;
end; then
B5: the addF of R = the addF of S by B2;
now let x be object;
assume x in [:the carrier of R,the carrier of R:]; then
consider a,b being object such that
B5: a in the carrier of R & b in the carrier of R & x = [a,b]
by ZFMISC_1:def 2;
reconsider a,b as Element of R by B5;
thus (the multF of R).x = f.(a * b) by B5,B0
.= f.a * f.b by H
.= (the multF of S).x by B0,B5;
end; then
the multF of R = the multF of S by B2;
hence R == S by B1,BB,TARSKI:2,H,B0,B4,B5;
end;
hence thesis by A;
end;
theorem
for R,S being strict Ring holds R == S iff R = S;
Th0:
for F1,F2 being Field
st F1 is Subfield of F2 & F2 is Subfield of F1 holds F1 == F2
proof
let F1,F2 be Field;
assume AS1: F1 is Subfield of F2 & F2 is Subfield of F1;
then B: 1.F1 = 1.F2 & 0.F1 = 0.F2 by EC_PF_1:def 1;
A: the carrier of F1 c= the carrier of F2 &
the carrier of F2 c= the carrier of F1 by AS1,EC_PF_1:def 1; then
E: the carrier of F2 = the carrier of F1 by TARSKI:2;
C: the addF of F1
= (the addF of F2) || the carrier of F1 by AS1,EC_PF_1:def 1
.= the addF of F2 by E;
the multF of F1
= (the multF of F2) || the carrier of F1 by AS1,EC_PF_1:def 1
.= the multF of F2 by E;
hence thesis by A,B,C,TARSKI:2;
end;
definition
let F1,F2 be Field;
redefine pred F1 == F2 means :: redefines == (FIELD_7, definition)
F1 is Subfield of F2 & F2 is Subfield of F1;
correctness
proof
now assume F1 == F2; then
A: the carrier of F1 = the carrier of F2 &
the addF of F1 = (the addF of F2) || (the carrier of F1) &
the multF of F1 = (the multF of F2) || (the carrier of F1) &
1.F1 = 1.F2 & 0.F1 = 0.F2;
hence F1 is Subfield of F2 by EC_PF_1:def 1;
thus F2 is Subfield of F1 by A,EC_PF_1:def 1;
end;
hence thesis by Th0;
end;
end;
theorem Th1:
for F being Field
for E being FieldExtension of F
for T being Subset of E holds FAdj(F,T) == F iff T is Subset of F
proof
let R be Field, S be FieldExtension of R; let T be Subset of S;
set P = FAdj(R,T);
X: R is Subring of S by FIELD_4:def 1;
X1: R is Subfield of R & R is Subfield of S by FIELD_4:7,FIELD_4:1;
X2: carrierFA(T) = {x where x is Element of S :
for U being Subfield of S
st R is Subfield of U & T is Subset of U holds x in U}
by FIELD_6:def 5;
Z: now let o be object;
assume C1: o in the carrier of R;
the carrier of R c= the carrier of S by X,C0SP1:def 3;
then reconsider a = o as Element of S by C1;
now let U be Subfield of S;
assume R is Subfield of U & T is Subset of U;
then the carrier of R c= the carrier of U by EC_PF_1:def 1;
hence o in U by C1;
end;
then a in carrierFA(T) by X2;
hence o in the carrier of P by FIELD_6:def 6;
end;
now assume B0: T is Subset of R;
B5: now let o be object;
assume o in the carrier of P;
then o in carrierFA(T) by FIELD_6:def 6;
then consider x being Element of S such that
B1: x = o & for U being Subfield of S
st R is Subfield of U & T is Subset of U holds x in U
by X2;
x in R by X1,B0,B1;
hence o in the carrier of R by B1;
end; then
B1: the carrier of R = the carrier of P by Z,TARSKI:2;
B2: 1.P = 1.S by FIELD_6:def 6 .= 1.R by X,C0SP1:def 3;
B3: 0.P = 0.S by FIELD_6:def 6 .= 0.R by X,C0SP1:def 3;
B4: the addF of P = (the addF of S)||carrierFA(T) by FIELD_6:def 6
.= (the addF of S)||the carrier of R by B1,FIELD_6:def 6
.= (the addF of R)||the carrier of R by X,C0SP1:def 3;
the multF of P = (the multF of S)||carrierFA(T) by FIELD_6:def 6
.= (the multF of S)||the carrier of R by B1,FIELD_6:def 6
.= (the multF of R)||the carrier of R by X,C0SP1:def 3;
hence FAdj(R,T) == R by B5,B2,B3,B4,Z,TARSKI:2;
end;
hence thesis by FIELD_6:35;
end;
theorem str12:
for F being Field
for E1,E2 being FieldExtension of F
st E1 == E2 holds VecSp(E1,F) = VecSp(E2,F)
proof
let F be Field, E1,E2 be FieldExtension of F;
set V1 = VecSp(E1,F), V2 = VecSp(E2,F);
assume AS: E1 == E2;
A: the carrier of V1 = the carrier of E2 by AS,FIELD_4:def 6
.= the carrier of V2 by FIELD_4:def 6;
B: the addF of V1 = the addF of E2 by AS,FIELD_4:def 6
.= the addF of V2 by FIELD_4:def 6;
C: the ZeroF of V1 = 0.E1 by FIELD_4:def 6
.= 0.E2 by AS
.= the ZeroF of V2 by FIELD_4:def 6;
the lmult of V1 = (the multF of E2)|[:the carrier of F,the carrier of E2:]
by AS,FIELD_4:def 6
.= the lmult of V2 by FIELD_4:def 6;
hence VecSp(E1,F) = VecSp(E2,F) by A,B,C;
end;
theorem str11:
for F being Field
for E1,E2 being FieldExtension of F st E1 == E2 holds deg(E1,F) = deg(E2,F)
proof
let F be Field, E1,E2 be FieldExtension of F;
set V1 = VecSp(E1,F), V2 = VecSp(E2,F);
assume E1 == E2; then AS: V1 = V2 by str12;
per cases;
suppose F: V1 is finite-dimensional;
hence deg(E1,F) = dim V2 by AS,FIELD_4:def 7
.= deg(E2,F) by AS,F,FIELD_4:def 7;
end;
suppose F: not V1 is finite-dimensional;
hence deg(E1,F) = -1 by FIELD_4:def 7
.= deg(E2,F) by AS,F,FIELD_4:def 7;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
cluster E-homomorphic for FieldExtension of F;
existence
proof
take E;
id E is additive multiplicative unity-preserving;
hence thesis by RING_2:def 4;
end;
cluster E-monomorphic for FieldExtension of F;
existence
proof
take E;
id E is additive multiplicative unity-preserving monomorphism;
hence thesis by RING_3:def 3;
end;
cluster E-isomorphic for FieldExtension of F;
existence
proof
take E;
id E is additive multiplicative unity-preserving isomorphism;
hence thesis by RING_3:def 4;
end;
end;
definition
let R be Ring;
let a,b be Element of R;
redefine func {a,b} -> Subset of R; :: redefines { (TARSKI, definition)
coherence
proof
now let o be object;
assume o in {a,b};
then per cases by TARSKI:def 2;
suppose o = a;
hence o in the carrier of R;
end;
suppose o = b;
hence o in the carrier of R;
end;
end;
hence thesis by TARSKI:def 3;
end;
end;
definition
let F be Field;
let V be VectSp of F;
let a be Element of V;
redefine func {a} -> Subset of V; :: redefines { (TARSKI, definition)
coherence
proof
now let o be object;
assume o in {a};
then o = a by TARSKI:def 1;
hence o in the carrier of V;
end;
hence thesis by TARSKI:def 3;
end;
end;
definition
let F be Field;
let V be VectSp of F;
let a,b be Element of V;
redefine func {a,b} -> Subset of V; :: redefines { (TARSKI, definition)
coherence
proof
now let o be object;
assume o in {a,b};
then per cases by TARSKI:def 2;
suppose o = a;
hence o in the carrier of V;
end;
suppose o = b;
hence o in the carrier of V;
end;
end;
hence thesis by TARSKI:def 3;
end;
end;
registration
let F be Field;
let V be VectSp of F;
cluster -> linearly-independent for Basis of V;
coherence by VECTSP_7:def 3;
end;
theorem ZMODUL033:
for F being Field,
V being VectSp of F
for X being Subset of V
holds X is linearly-independent iff
for l1,l2 being Linear_Combination of X st Sum l1 = Sum l2 holds l1 = l2
proof
let F be Field, V be VectSp of F; let X be Subset of V;
A: now assume A1: X is linearly-independent;
now let KL1,KL2 be Linear_Combination of X;
A2: Carrier(KL1) c= X by VECTSP_6:def 4;
Carrier(KL2) c= X by VECTSP_6:def 4; then
A3: Carrier(KL1) \/ Carrier(KL2) c= X by A2,XBOOLE_1:8;
assume Sum(KL1) = Sum(KL2);
then Sum(KL1) - Sum(KL2) = 0.V by RLVECT_1:5; then
A4: KL1 - KL2 is Linear_Combination of Carrier(KL1 - KL2) &
Sum(KL1 - KL2) = 0.V by VECTSP_6:47,VECTSP_6:def 4;
Carrier(KL1 - KL2) c= Carrier(KL1) \/ Carrier(KL2) by VECTSP_6:41; then
A5: Carrier(KL1 - KL2) is linearly-independent
by A1,A3,XBOOLE_1:1,VECTSP_7:1;
now
let v be Vector of V;
not v in Carrier(KL1 - KL2) by VECTSP_7:def 1,A5,A4;
then (KL1 - KL2).v = 0.F by VECTSP_6:2;
then KL1.v - KL2.v = 0.F by VECTSP_6:40;
hence KL1.v = KL2.v by RLVECT_1:21;
end;
hence KL1 = KL2;
end;
hence for l1,l2 being Linear_Combination of X
st Sum l1 = Sum l2 holds l1 = l2;
end;
now assume A1:
for l1,l2 being Linear_Combination of X st Sum l1 = Sum l2 holds l1 = l2;
now let l be Linear_Combination of X;
assume A2: Sum(l) = 0.V;
A3: Sum(ZeroLC(V)) = 0.V by VECTSP_6:15;
Carrier(ZeroLC(V)) c= X by VECTSP_6:def 3; then
ZeroLC(V) is Linear_Combination of X by VECTSP_6:def 4;
hence Carrier(l) = {} by A1,A2,A3,VECTSP_6:def 3;
end;
hence X is linearly-independent by VECTSP_7:def 1;
end;
hence thesis by A;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster -> non empty for Basis of VecSp(E,F);
coherence
proof
let B be Basis of VecSp(E,F);
A: Lin B = the ModuleStr of VecSp(E,F) by VECTSP_7:def 3;
now assume B = {}; then
B = {}(the carrier of VecSp(E,F)); then
Lin(B) = (0).VecSp(E,F) by VECTSP_7:9; then
the carrier of VecSp(E,F) = {0.VecSp(E,F)} by A,VECTSP_4:def 3; then
the carrier of E = {0.E} by FIELD_4:def 6;
hence contradiction;
end;
hence thesis;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster deg(E,F) -> non zero;
coherence
proof
set V = VecSp(E,F);
per cases;
suppose E is F-finite; then
H1: V is finite-dimensional by FIELD_4:def 8;
now assume deg(E,F) = 0; then
A: dim V = 0 by FIELD_4:def 7;
the ModuleStr of V = (Omega).V by VECTSP_4:def 4
.= (0).V by A,H1,VECTSP_9:29;
then the carrier of (the ModuleStr of V) = {0.V} by VECTSP_4:def 3;
then 1.E = 0.E by FIELD_4:def 6;
hence contradiction;
end;
hence thesis;
end;
suppose not E is F-finite;
then not VecSp(E,F) is finite-dimensional by FIELD_4:def 8;
hence thesis by FIELD_4:def 7;
end;
end;
end;
registration
let F be Field;
let E be F-finite FieldExtension of F;
cluster -> finite for Basis of VecSp(E,F);
coherence
proof
let B be Basis of VecSp(E,F);
VecSp(E,F) is finite-dimensional by FIELD_4:def 8;
hence thesis by VECTSP_9:20;
end;
end;
theorem quah1:
for F being Field
for E being FieldExtension of F
holds deg(E,F) = 1 iff the carrier of E = the carrier of F
proof
let F be Field; let E be FieldExtension 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 V by FIELD_4:def 6;
Z: now assume AS: deg(E,F) = 1; then
H1: V is finite-dimensional by FIELD_4:def 7;
dim V = 1 by AS,FIELD_4:def 7; then
consider v being Element of V such that
B: v <> 0.V & (Omega).V = Lin {v} by H1,VECTSP_9:30;
C: the carrier of Lin {v} = the carrier of V 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;
xE is non 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 let o be object;
assume o in the carrier of E; then
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;
end;
hence the carrier of E = the carrier of F by A,TARSKI:2;
end;
now assume AS1: the carrier of E = the carrier of F;
reconsider A = {e} as Subset of V;
0.V = 0.E by FIELD_4:def 6;
then L: A is linearly-independent by VECTSP_7:3;
H1: the carrier of Lin(A) =
the set of all Sum(l) where l is Linear_Combination of A by VECTSP_7:def 2;
H2: now let o be object;
assume o in the carrier of V;
then reconsider v = o as Element of the carrier of V;
reconsider a = v as Element of E by FIELD_4:def 6;
defpred P[object,object] means ($1 = e & $2 = a) or ($1 <> e & $2 = 0.E);
G0: for x being object st x in the carrier of V
ex y being object st y in the carrier of E & P[x,y]
proof
let o be object;
assume o in the carrier of V;
per cases;
suppose A: o = e; take a; thus thesis by A; end;
suppose A: o <> e; take 0.E; thus thesis by A; end;
end;
consider f being Function of the carrier of V, the carrier of E such that
G1: for x being object st x in the carrier of V holds P[x,f.x]
from FUNCT_2:sch 1(G0);
dom f = the carrier of V & rng f c= the carrier of E by FUNCT_2:def 1; then
reconsider f as Element of Funcs(the carrier of V, the carrier of F)
by AS1,FUNCT_2:def 2;
ex T being finite Subset of V st
for v being Element of V st not v in T holds f.v = 0.F
proof
reconsider T = {e} as finite Subset of V;
take T;
now let u be Element of V;
assume not u in T;
then u <> e by TARSKI:def 1;
hence f.u = 0.E by G1 .= 0.F by H0,C0SP1:def 3;
end;
hence thesis;
end;
then reconsider l = f as Linear_Combination of V by VECTSP_6:def 1;
now let o be object;
assume o in Carrier l; then
o in {v where v is Element of V: l.v <> 0.F} by VECTSP_6:def 2;
then consider u being Element of V such that
I: o = u & l.u <> 0.F;
l.u <> 0.E by I,H0,C0SP1:def 3; then
u = e by G1;
hence o in A by I,TARSKI:def 1;
end;
then Carrier l c= A;
then reconsider 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 the set of all Sum(l) where l is Linear_Combination of A;
end;
now let o be object;
assume o in the set of all Sum(l) where l is Linear_Combination of A;
then consider l being Linear_Combination of A such that G: o = Sum l;
thus o in the carrier of V by G;
end;
then the carrier of V = the set of all Sum(l) where
l is Linear_Combination of A 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: V is finite-dimensional by M,MATRLIN:def 1; then
dim V = 1 by M,H4,VECTSP_9:def 1;
hence deg(E,F) = 1 by H5,FIELD_4:def 7;
end;
hence thesis by Z;
end;
theorem str1a:
for F being Field
for E being FieldExtension of F holds deg(E,F) = 1 iff E == F
proof
let F be Field; let E be FieldExtension of F;
now assume deg(E,F) = 1;
then A: the carrier of E = the carrier of F by quah1;
F is Subfield of E by FIELD_4:7; then
the carrier of F c= the carrier of E &
the addF of F = (the addF of E) || the carrier of F &
the multF of F = (the multF of E) || the carrier of F &
1.F = 1.E & 0.F = 0.E by EC_PF_1:def 1;
hence E == F by A;
end;
hence thesis by quah1;
end;
theorem quah2:
for F being Field
for E being FieldExtension of F
holds deg(E,F) = 1 iff {1.E} is Basis of VecSp(E,F)
proof
let F be Field; let E be FieldExtension of F;
set V = VecSp(E,F);
H0: F is Subring of E & F is Subfield of E by FIELD_4:def 1,FIELD_4:7;
reconsider e = 1.E as Element of V by FIELD_4:def 6;
Z: now assume deg(E,F) = 1; then
AS1: the carrier of E = the carrier of F by quah1;
reconsider A = {e} as Subset of V;
0.V = 0.E by FIELD_4:def 6;
then L: A is linearly-independent by VECTSP_7:3;
H1: the carrier of Lin(A) =
the set of all Sum(l) where l is Linear_Combination of A by VECTSP_7:def 2;
H2: now let o be object;
assume o in the carrier of V;
then reconsider v = o as Element of the carrier of V;
reconsider a = v as Element of E by FIELD_4:def 6;
defpred P[object,object] means ($1 = e & $2 = a) or ($1 <> e & $2 = 0.E);
G0: for x being object st x in the carrier of V
ex y being object st y in the carrier of E & P[x,y]
proof
let o be object;
assume o in the carrier of V;
per cases;
suppose A: o = e; take a; thus thesis by A; end;
suppose A: o <> e; take 0.E; thus thesis by A; end;
end;
consider f being Function of the carrier of V, the carrier of E such that
G1: for x being object st x in the carrier of V holds P[x,f.x]
from FUNCT_2:sch 1(G0);
dom f = the carrier of V & rng f c= the carrier of E by FUNCT_2:def 1; then
reconsider f as Element of Funcs(the carrier of V, the carrier of F)
by AS1,FUNCT_2:def 2;
ex T being finite Subset of V st
for v being Element of V st not v in T holds f.v = 0.F
proof
reconsider T = {e} as finite Subset of V;
take T;
now let u be Element of V;
assume not u in T;
then u <> e by TARSKI:def 1;
hence f.u = 0.E by G1 .= 0.F by H0,C0SP1:def 3;
end;
hence thesis;
end;
then reconsider l = f as Linear_Combination of V by VECTSP_6:def 1;
now let o be object;
assume o in Carrier l; then
o in {v where v is Element of V: l.v <> 0.F} by VECTSP_6:def 2;
then consider u being Element of V such that
I: o = u & l.u <> 0.F;
l.u <> 0.E by I,H0,C0SP1:def 3; then
u = e by G1;
hence o in A by I,TARSKI:def 1;
end;
then Carrier l c= A;
then reconsider 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 the set of all Sum(l) where l is Linear_Combination of A;
end;
now let o be object;
assume o in the set of all Sum(l) where l is Linear_Combination of A;
then consider l being Linear_Combination of A such that G: o = Sum l;
thus o in the carrier of V by G;
end;
then the carrier of V = the set of all Sum(l) where
l is Linear_Combination of A by H2,TARSKI:2;
hence {1.E} is Basis of VecSp(E,F) by H1,L,VECTSP_4:31,VECTSP_7:def 3;
end;
now assume M: {1.E} is Basis of VecSp(E,F);
H4: card {1.E} = 1 by CARD_1:30;
H5: V is finite-dimensional by M,MATRLIN:def 1; then
dim V = 1 by M,H4,VECTSP_9:def 1;
hence deg(E,F) = 1 by H5,FIELD_4:def 7;
end;
hence thesis by Z;
end;
registration
let F be Field,
E be FieldExtension of F;
cluster non empty finite linearly-independent for Subset of VecSp(E,F);
existence
proof
set B = the Basis of VecSp(E,F);
set v = the Element of B;
v in B; then
{v} c= B by TARSKI:def 1;
hence thesis by VECTSP_7:1;
end;
end;
theorem ext0:
for F being Field,
E being FieldExtension of F
for T1,T2 being Subset of E
st T1 c= T2 holds FAdj(F,T1) is Subfield of FAdj(F,T2)
proof
let F be Field, E be FieldExtension of F; let T1,T2 be Subset of E;
assume AS: T1 c= T2;
X: T2 is Subset of FAdj(F,T2) by FIELD_6:35;
now let o be object;
assume o in T1;
then o in T2 by AS;
hence o in the carrier of FAdj(F,T2) by X;
end; then
A: T1 c= the carrier of FAdj(F,T2);
F is Subfield of FAdj(F,T2) by FIELD_4:7;
hence FAdj(F,T1) is Subfield of FAdj(F,T2) by A,FIELD_6:37;
end;
definition
let F be Field;
let p be Polynomial of F;
func Coeff p -> Subset of F equals
{ p.i where i is Element of NAT : p.i <> 0.F };
coherence
proof
now let o be object;
assume o in { p.i where i is Element of NAT : p.i <> 0.F }; then
consider i being Element of NAT such that H: o = p.i & p.i <> 0.F;
thus o in the carrier of F by H;
end;
then { p.i where i is Element of NAT : p.i <> 0.F } c= the carrier of F;
hence thesis;
end;
end;
registration
let F be Field;
let p be Polynomial of F;
cluster Coeff p -> finite;
coherence
proof
set M = Coeff p, X = Support p;
now let o be object;
assume o in M; then
consider i being Element of NAT such that
H1: o = p.i & p.i <> 0.F;
H2: dom p = NAT by FUNCT_2:def 1; then
i in Support p by H1,POLYNOM1:def 3;
hence o in p.:X by H1,H2,FUNCT_1:def 6;
end; then
A: M c= p.:X;
Support p is finite by POLYNOM1:def 5;
hence thesis by A;
end;
end;
theorem cof1:
for F being Field
for E being FieldExtension of F
for p being Polynomial of E
st Coeff p c= the carrier of F holds p is Polynomial of F
proof
let F be Field, E be FieldExtension of F, p be Polynomial of E;
assume AS: Coeff p c= the carrier of F;
F is Subring of E by FIELD_4:def 1; then
A: 0.E = 0.F by C0SP1:def 3;
now let y be object;
assume y in rng p;
then consider x being object such that
A1: x in dom p & y = p.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A1;
per cases;
suppose p.x = 0.F;
hence y in the carrier of F by A1;
end;
suppose p.x <> 0.F;
then y in Coeff p by A,A1;
hence y in the carrier of F by AS;
end;
end; then
rng p c= the carrier of F; then
reconsider q = p as sequence of the carrier of F by FUNCT_2:6;
consider n being Nat such that
C: for i being Nat st i >= n holds p.i = 0.E by ALGSEQ_1:def 1;
for i being Nat st i >= n holds q.i = 0.F by C,A;
hence thesis by ALGSEQ_1:def 1;
end;
theorem cof2:
for F being Field
for E being FieldExtension of F
for p being non zero Polynomial of E
st Coeff p c= the carrier of F holds p is non zero Polynomial of F
proof
let F be Field, E be FieldExtension of F, p be non zero Polynomial of E;
assume Coeff p c= the carrier of F; then
reconsider q = p as Polynomial of F by cof1;
p <> 0_.(E);
then q <> 0_.(F) by FIELD_4:12;
hence thesis by UPROOTS:def 5;
end;
theorem m4:
for R being Ring,
S being RingExtension of R
for p being Element of the carrier of Polynom-Ring R
for q being Element of the carrier of Polynom-Ring S
st p = q holds Roots(S,p) = Roots(q)
proof
let R be Ring, S be RingExtension of R;
let p be Element of the carrier of Polynom-Ring R;
let q be Element of the carrier of Polynom-Ring S;
I: Roots(S,p) = {a where a is Element of S : a is_a_root_of p,S}
by FIELD_4:def 4;
assume AS: p = q;
A: now let o be object;
assume A0: o in Roots q; then
reconsider a = o as Element of S;
a is_a_root_of q by A0,POLYNOM5:def 10; then
0.S = eval(q,a) by POLYNOM5:def 7
.= Ext_eval(p,a) by AS,FIELD_4:26; then
a is_a_root_of p,S by FIELD_4:def 2;
hence o in Roots(S,p) by I;
end;
now let o be object;
assume o in Roots(S,p);
then consider a being Element of S such that
A1: o = a & a is_a_root_of p,S by I;
0.S = Ext_eval(p,a) by A1,FIELD_4:def 2
.= eval(q,a) by AS,FIELD_4:26; then
a is_a_root_of q by POLYNOM5:def 7;
hence o in Roots q by A1,POLYNOM5:def 10;
end;
hence thesis by A,TARSKI:2;
end;
registration
let R be domRing;
let p be non zero Element of the carrier of Polynom-Ring R;
cluster Roots p -> finite;
coherence;
end;
registration
let R be domRing,
S be domRingExtension of R;
let p be non zero Element of the carrier of Polynom-Ring R;
cluster Roots(S,p) -> finite;
coherence
proof
p <> 0_.(R); then
A: p <> 0_.(S) by FIELD_4:12;
the carrier of Polynom-Ring R c= the carrier of Polynom-Ring S
by FIELD_4:10; then
reconsider p1 = p as non zero Element of the carrier of Polynom-Ring S
by A,UPROOTS:def 5;
Roots(S,p) = Roots p1 by m4;
hence thesis;
end;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster F-extending for FieldExtension of E;
existence
proof
set K = the FieldExtension of E;
take K;
thus thesis;
end;
end;
registration
let F be Field,
E be F-finite FieldExtension of F;
cluster F-finite for F-extending FieldExtension of E;
existence
proof
reconsider K = E as F-extending FieldExtension of E by FIELD_4:6;
take K;
thus thesis;
end;
end;
registration
let F be Field;
let E be F-finite FieldExtension of F;
cluster E-finite for F-extending FieldExtension of E;
existence
proof
reconsider K = E as F-extending FieldExtension of E by FIELD_4:6;
take K;
the carrier of K = the carrier of E;
then deg(K,E) = 1 by quah1;
then {1.K} is Basis of VecSp(K,E) by quah2;
then VecSp(K,E) is finite-dimensional by MATRLIN:def 1;
hence thesis by FIELD_4:def 8;
end;
end;
theorem lemma7a:
for F being Field,
p being Element of the carrier of Polynom-Ring F
for E being FieldExtension of F,
U being E-extending FieldExtension of F
for a being Element of E, b being Element of U st a = b
holds Ext_eval(p,a) = Ext_eval(p,b)
proof
let F be Field,
p be Element of the carrier of Polynom-Ring F;
let E be FieldExtension of F,
U be E-extending FieldExtension of F;
let a be Element of E, b be Element of U;
assume AS2: a = b;
H1: E is Subring of U by FIELD_4:def 1; then
H2: the carrier of E c= the carrier of U by C0SP1:def 3;
F is Subring of E by FIELD_4:def 1; then
H4: the carrier of F c= the carrier of E by C0SP1:def 3;
consider Fp being FinSequence of E such that
A: Ext_eval(p,a) = Sum Fp & len Fp = len p &
for n being Element of NAT st n in dom Fp holds
Fp.n = In(p.(n-'1),E) * (power E).(a,n-'1) by ALGNUM_1:def 1;
consider Fq being FinSequence of U such that
B: Ext_eval(p,b) = Sum Fq & len Fq = len p &
for n being Element of NAT st n in dom Fq holds
Fq.n = In(p.(n-'1),U) * (power U).(b,n-'1) by ALGNUM_1:def 1;
C: now let n be Element of NAT;
thus (power U).(b,n-'1) = (power U).(In(b,U),n-'1)
.= In((power E).(a,n-'1),U) by AS2,H1,ALGNUM_1:7
.= (power E).(a,n-'1) by H2,SUBSET_1:def 8;
end;
D: dom Fp = Seg(len Fq) by A,B,FINSEQ_1:def 3 .= dom Fq by FINSEQ_1:def 3;
E: now let n be Element of NAT;
p.(n-'1) in U by H2,H4;
hence In(p.(n-'1),U) = p.(n-'1) by SUBSET_1:def 8
.= In(p.(n-'1),E) by H4,SUBSET_1:def 8;
end;
H: for n being Element of NAT holds [In(p.(n-'1),E),(power E).(a,n-'1)]
in [:the carrier of E,the carrier of E:] by ZFMISC_1:def 2;
now let n be Nat;
assume F: n in dom Fq;
G: n is Element of NAT by ORDINAL1:def 12;
thus Fq.n = In(p.(n-'1),U) * (power U).(b,n-'1) by B,F
.= (the multF of U).(In(p.(n-'1),U),(power E).(a,n-'1)) by C,G
.= (the multF of U).(In(p.(n-'1),E),(power E).(a,n-'1)) by E,G
.= ((the multF of U)||(the carrier of E)).
(In(p.(n-'1),E),(power E).(a,n-'1)) by G,H,FUNCT_1:49
.= In(p.(n-'1),E) * (power E).(a,n-'1) by H1,C0SP1:def 3
.= Fp.n by A,D,F;
end;
then Fp = Fq by D;
hence thesis by H1,A,B,FIELD_4:2;
end;
theorem lemma7b:
for F being Field,
p being Element of the carrier of Polynom-Ring F
for E being FieldExtension of F,
q being Element of the carrier of Polynom-Ring E st q = p
for U being E-extending FieldExtension of F
for a being Element of U
holds Ext_eval(q,a) = Ext_eval(p,a)
proof
let F be Field,
p be Element of the carrier of Polynom-Ring F;
let E be FieldExtension of F,
q being Element of the carrier of Polynom-Ring E;
assume AS1: q = p;
let U be E-extending FieldExtension of F;
let a be Element of U;
consider Fp being FinSequence of U such that
A: Ext_eval(p,a) = Sum Fp & len Fp = len p &
for n being Element of NAT st n in dom Fp holds
Fp.n = In(p.(n-'1),U) * (power U).(a,n-'1) by ALGNUM_1:def 1;
consider Fq being FinSequence of U such that
B: Ext_eval(q,a) = Sum Fq & len Fq = len q &
for n being Element of NAT st n in dom Fq holds
Fq.n = In(q.(n-'1),U) * (power U).(a,n-'1) by ALGNUM_1:def 1;
C: len p - 1 = deg p by HURWITZ:def 2
.= deg q by AS1,FIELD_4:20
.= len q - 1 by HURWITZ:def 2;
D: dom Fp = Seg(len Fq) by A,B,C,FINSEQ_1:def 3
.= dom Fq by FINSEQ_1:def 3;
now let n be Nat;
assume F: n in dom Fq;
hence Fq.n = In(p.(n-'1),U) * (power U).(a,n-'1) by B,AS1
.= Fp.n by A,D,F;
end;
then Fp = Fq by D;
hence thesis by A,B;
end;
definition
let R be Ring, S be RingExtension of R;
let a be Element of R;
func @(a,S) -> Element of S equals
a;
coherence
proof
R is Subring of S by FIELD_4:def 1;
then the carrier of R c= the carrier of S by C0SP1:def 3;
hence thesis;
end;
end;
definition
let R be Ring, S be RingExtension of R;
let a be Element of S;
attr a is R-membered means :defmem:
a in the carrier of R;
end;
registration
let R be Ring, S be RingExtension of R;
cluster R-membered for Element of S;
existence
proof
take 1.S;
R is Subring of S by FIELD_4:def 1; then
1.S = 1.R by C0SP1:def 3;
hence thesis;
end;
end;
definition
let R be Ring, S be RingExtension of R;
let a be Element of S;
assume AS:a is R-membered;
func @(R,a) -> Element of R equals :defred:
a;
coherence by AS;
end;
registration
let R be Ring, S be RingExtension of R;
let a be R-membered Element of S;
reduce @(R,a) to a;
reducibility by defred;
end;
registration
let F be Field,
E be FieldExtension of F;
cluster non zero F-algebraic for Element of E;
existence
proof
take a = 1.E;
A: F is Subring of E by FIELD_4:def 1;
then a = 1.F by C0SP1:def 3;
then In(a,E) is_integral_over F by A,ALGNUM_1:23;
hence thesis by FIELD_6:42;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
let a be Element of F;
cluster @(a,E) -> F-algebraic;
coherence
proof
F is Subring of E by FIELD_4:def 1;
then In(a,E) is_integral_over F by ALGNUM_1:23;
hence thesis by FIELD_6:42;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
let K be E-extending FieldExtension of F;
let a be F-algebraic Element of E;
cluster @(a,K) -> F-algebraic;
coherence
proof
consider p being non zero Polynomial of F such that
A: Ext_eval(p,a) = 0.E by FIELD_6:43;
reconsider p as Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
B: E is Subring of K by FIELD_4:def 1;
Ext_eval(p,@(a,K)) = Ext_eval(p,a) by lemma7a .= 0.K by A,B,C0SP1:def 3;
hence thesis by FIELD_6:43;
end;
end;
help1:
for R being domRing, n being Element of NAT holds (<%0.R,1.R%>`^n).n = 1.R
proof
let R be domRing, n be Element of NAT;
<%0.R,1.R%>`^n = anpoly(1.R,n) by FIELD_1:12;
hence thesis by POLYDIFF:24;
end;
help2:
for R being domRing, n,i being Element of NAT
st i <> n holds (<%0.R,1.R%>`^n).i = 0.R
proof
let R be domRing, n,i be Element of NAT;
assume AS: i <> n;
<%0.R,1.R%>`^n = anpoly(1.R,n) by FIELD_1:12;
hence (<%0.R,1.R%>`^n).i = 0.R by AS,POLYDIFF:25;
end;
begin :: More on Finite Extensions
theorem sp0:
for F being Field,
E being FieldExtension of F,
K being E-extending FieldExtension of F
for l being Linear_Combination of VecSp(K,F)
holds l is Linear_Combination of VecSp(K,E)
proof
let F be Field, E be FieldExtension of F, K be E-extending FieldExtension of F;
let l be Linear_Combination of VecSp(K,F);
H0: the carrier of VecSp(K,F) = the carrier of K by FIELD_4:def 6
.= the carrier of VecSp(K,E) by FIELD_4:def 6;
H1: F is Subring of E & E is Subring of K by FIELD_4:def 1; then
H2: the carrier of F c= the carrier of E &
the carrier of E c= the carrier of K by C0SP1:def 3;
rng l c= the carrier of E by H2; then
l is Function of the carrier of VecSp(K,E),the carrier of E by H0,FUNCT_2:6;
then A: l in Funcs(the carrier of VecSp(K,E),the carrier of E) by FUNCT_2:8;
consider T being finite Subset of VecSp(K,F) such that
B: for v being Element of VecSp(K,F) st not v in T holds l.v = 0.F
by VECTSP_6:def 1;
reconsider T1 = T as finite Subset of VecSp(K,E) by H0;
now let v1 be Element of VecSp(K,E);
assume C: not v1 in T1;
reconsider v = v1 as Element of VecSp(K,F) by H0;
l.v = 0.F by B,C;
hence l.v1 = 0.E by H1,C0SP1:def 3;
end;
hence thesis by A,VECTSP_6:def 1;
end;
theorem sp1:
for F being Field,
E being FieldExtension of F,
K being E-extending FieldExtension of F
for BE being Subset of VecSp(K,E), BF being Subset of VecSp(K,F) st BF c= BE
for l being Linear_Combination of BF holds l is Linear_Combination of BE
proof
let F be Field, E be FieldExtension of F, K be E-extending FieldExtension of F;
let BE be Subset of VecSp(K,E), BF be Subset of VecSp(K,F);
assume AS: BF c= BE;
let l be Linear_Combination of BF;
reconsider l1 = l as Linear_Combination of VecSp(K,E) by sp0;
H0: the carrier of VecSp(K,F) = the carrier of K by FIELD_4:def 6
.= the carrier of VecSp(K,E) by FIELD_4:def 6;
H1: F is Subring of E & E is Subring of K by FIELD_4:def 1;
now let o be object;
assume o in Carrier l1; then
consider v1 being Element of VecSp(K,E) such that
A: o = v1 & l1.v1 <> 0.E by VECTSP_6:1;
reconsider v = v1 as Element of VecSp(K,F) by H0;
0.E = 0.F by H1,C0SP1:def 3; then
B: v in Carrier l by A,VECTSP_6:1;
Carrier l c= BF by VECTSP_6:def 4;
hence o in BE by B,A,AS;
end;
then Carrier l1 c= BE;
hence thesis by VECTSP_6:def 4;
end;
theorem sp2:
for F being Field,
E being FieldExtension of F,
K being E-extending FieldExtension of F
for BE being finite Subset of VecSp(K,E), BF being finite Subset of VecSp(K,F)
for l1 being Linear_Combination of BF, l2 being Linear_Combination of BE
st l1 = l2 & BF c= BE holds Sum l1 = Sum l2
proof
let F be Field, E be FieldExtension of F, K be E-extending FieldExtension of F;
let BE be finite Subset of VecSp(K,E), BF be finite Subset of VecSp(K,F);
let l1 be Linear_Combination of BF, l2 be Linear_Combination of BE;
assume AS: l1 = l2 & BF c= BE;
H0: the carrier of VecSp(K,F) = the carrier of K by FIELD_4:def 6
.= the carrier of VecSp(K,E) by FIELD_4:def 6;
H1: F is Subring of E & E is Subring of K by FIELD_4:def 1; then
H2: the carrier of F c= the carrier of E &
the carrier of E c= the carrier of K by C0SP1:def 3;
defpred P[Nat] means
for l1 being Linear_Combination of BF, l2 being Linear_Combination of BE
st l1 = l2 & BF c= BE & card(Carrier l1) = $1 holds Sum l1 = Sum l2;
IA: P[0]
proof
now let l1 be Linear_Combination of BF, l2 be Linear_Combination of BE;
assume A: l1 = l2 & BF c= BE & card(Carrier l1) = 0;
card(Carrier l2) = 0
proof
now assume B1: Carrier l2 <> {};
set o = the Element of Carrier l2;
consider v2 being Element of VecSp(K,E) such that
B2: o = v2 & l2.v2 <> 0.E by B1,VECTSP_6:1;
reconsider v1 = v2 as Element of VecSp(K,F) by H0;
0.E = 0.F by H1,C0SP1:def 3;
then o in Carrier l1 by A,B2,VECTSP_6:1;
hence contradiction by A;
end;
hence thesis;
end; then
A0: Carrier l1 = {} & Carrier l2 = {} by A;
hence Sum l1 = 0.VecSp(K,F) by VECTSP_6:19
.= 0.K by FIELD_4:def 6
.= 0.VecSp(K,E) by FIELD_4:def 6
.= Sum l2 by A0,VECTSP_6:19;
end;
hence thesis;
end;
IS: now let k be Nat;
assume IV: P[k];
now let l1 be Linear_Combination of BF, l2 be Linear_Combination of BE;
assume A0: l1 = l2 & BF c= BE & card(Carrier l1) = k + 1; then
A1: Carrier l1 <> {};
set o = the Element of Carrier l1;
A2: o in Carrier l1 by A1; then
reconsider v1 = o as Element of VecSp(K,F);
A3: the carrier of VecSp(K,F) = the carrier of K &
the carrier of VecSp(K,E) = the carrier of K by FIELD_4:def 6;
A4: Carrier l1 c= BF & Carrier l2 c= BE by VECTSP_6:def 4;
reconsider v2 = v1 as Element of VecSp(K,E) by A3;
defpred P[Element of K,Element of F] means
($1 = v1 & $2 = l1.v1) or ($1 <> v1 & $2 = 0.F);
G0: now let x be Element of K;
per cases;
suppose x = o;
hence ex y being Element of F st P[x,y];
end;
suppose x <> o;
hence ex y being Element of F st P[x,y];
end;
end;
consider f being Function of the carrier of K,the carrier of F
such that
G1: for x being Element of K holds P[x,f.x] from FUNCT_2:sch 3(G0);
dom f = the carrier of VecSp(K,F) &
rng f c= the carrier of F by A3,FUNCT_2:def 1;
then reconsider f as
Element of Funcs(the carrier of VecSp(K,F), the carrier of F)
by FUNCT_2:def 2;
now let v be Element of VecSp(K,F);
assume not v in BF;
then not v in Carrier l1 by A4;
hence f.v = 0.F by G1,A2,A3;
end; then
reconsider h=f as Linear_Combination of VecSp(K,F) by VECTSP_6:def 1;
Z100:now let o be object;
assume C1: o in Carrier h; then
reconsider v = o as Element of VecSp(K,F);
reconsider x = v as Element of K by FIELD_4:def 6;
h.x <> 0.F by C1,VECTSP_6:2;
then v = v1 by G1;
hence o in {v1} by TARSKI:def 1;
end;
then Carrier h c= {v1};
then Y: h is Linear_Combination of {v1} by VECTSP_6:def 4;
{v1} c= Carrier l1 by A2,TARSKI:def 1; then
{v1} c= BF by A4; then
reconsider h1 = h as Linear_Combination of BF by Y,VECTSP_6:4;
reconsider h2 = h1 as Linear_Combination of BE by A0,sp1;
Z: h2 is Linear_Combination of {v2}
proof
now let o be object;
assume Z1: o in Carrier h2; then
reconsider v = o as Element of VecSp(K,E);
reconsider x = v as Element of VecSp(K,E);
h2.v <> 0.E by Z1,VECTSP_6:2;
then h1.x <> 0.F & x in the carrier of K by A3,H1,C0SP1:def 3;
then x = v1 by G1;
hence o in {v2} by TARSKI:def 1;
end;
then Carrier h2 c= {v2};
hence thesis by VECTSP_6:def 4;
end;
Z1: h2.v2 = h1.v1;
Z3: [h1.v1,v2] in [:the carrier of F,the carrier of K:]
by A3,ZFMISC_1:def 2;
Z4: [h2.v1,v2] in [:the carrier of E,the carrier of K:]
by A3,Z1,ZFMISC_1:def 2;
Z5: Sum h1 = h1.v1 * v1 by Y,VECTSP_6:17
.= ((the multF of K)|[:the carrier of F,the carrier of K:]).(h1.v1,v2)
by FIELD_4:def 6
.= (the multF of K).(h1.v1,v2) by Z3,FUNCT_1:49
.= ((the multF of K)|[:the carrier of E,the carrier of K:]).(h2.v2,v2)
by Z4,FUNCT_1:49
.= h2.v2 * v2 by FIELD_4:def 6
.= Sum h2 by Z,VECTSP_6:17;
reconsider li1 = l1 - h1 as Linear_Combination of BF by VECTSP_6:42;
li1 - (l1 - h1) = ZeroLC(VecSp(K,F)) by VECTSP_6:43; then
B: l1 = li1 - (l1 - h1) + l1 by VECTSP_6:27
.= li1 + -(l1 - h1) + l1 by VECTSP_6:def 11
.= li1 + -(l1 + -h1) + l1 by VECTSP_6:def 11
.= li1 + (-(l1 + -h1) + l1) by VECTSP_6:26
.= li1 + ((-1.F)*(l1 + -h1) + l1) by VECTSP_6:def 10
.= li1 + (((-1.F)*l1 + (-1.F)*(-h1)) + l1) by VECTSP_6:33
.= li1 + (((-1.F)*l1 + (-1.F)*((-1.F)*h1)) + l1) by VECTSP_6:def 10
.= li1 + (((-1.F)*l1 + ((-1.F)*(-1.F))*h1) + l1) by VECTSP_6:34
.= li1 + (((-1.F)*l1 + ((1.F)*(1.F))*h1) + l1) by VECTSP_1:10
.= li1 + (((-1.F)*l1 + h1) + l1) by VECTSP_6:35
.= li1 + ((-l1 + h1) + l1) by VECTSP_6:def 10
.= li1 + ((h1 + -l1) + l1) by VECTSP_6:25
.= li1 + (h1 + (-l1 + l1)) by VECTSP_6:26
.= li1 + (h1 + (l1 + -l1)) by VECTSP_6:25
.= li1 + (h1 + (l1 - l1)) by VECTSP_6:def 11
.= li1 + (h1 + ZeroLC(VecSp(K,F))) by VECTSP_6:43
.= li1 + h1 by VECTSP_6:27;
reconsider li2 = l2 - h2 as Linear_Combination of BE by VECTSP_6:42;
li2 - (l2 - h2) = ZeroLC(VecSp(K,E)) by VECTSP_6:43; then
C: l2 = li2 - (l2 - h2) + l2 by VECTSP_6:27
.= li2 + -(l2 - h2) + l2 by VECTSP_6:def 11
.= li2 + -(l2 + -h2) + l2 by VECTSP_6:def 11
.= li2 + (-(l2 + -h2) + l2) by VECTSP_6:26
.= li2 + ((-1.E)*(l2 + -h2) + l2) by VECTSP_6:def 10
.= li2 + (((-1.E)*l2 + (-1.E)*(-h2)) + l2) by VECTSP_6:33
.= li2 + (((-1.E)*l2 + (-1.E)*((-1.E)*h2)) + l2) by VECTSP_6:def 10
.= li2 + (((-1.E)*l2 + ((-1.E)*(-1.E))*h2) + l2) by VECTSP_6:34
.= li2 + (((-1.E)*l2 + ((1.E)*(1.E))*h2) + l2) by VECTSP_1:10
.= li2 + (((-1.E)*l2 + h2) + l2) by VECTSP_6:35
.= li2 + ((-l2 + h2) + l2) by VECTSP_6:def 10
.= li2 + ((h2 + -l2) + l2) by VECTSP_6:25
.= li2 + (h2 + (-l2 + l2)) by VECTSP_6:26
.= li2 + (h2 + (l2 + -l2)) by VECTSP_6:25
.= li2 + (h2 + (l2 - l2)) by VECTSP_6:def 11
.= li2 + (h2 + ZeroLC(VecSp(K,E))) by VECTSP_6:43
.= li2 + h2 by VECTSP_6:27;
Z6: li1 = li2
proof
D1: dom li1 = the carrier of VecSp(K,F) by FUNCT_2:def 1
.= dom li2 by A3,FUNCT_2:def 1;
now let o be object;
assume D2: o in dom li1; then
reconsider vF = o as Element of VecSp(K,F);
reconsider vE = o as Element of VecSp(K,E) by D1,D2;
reconsider lF = li1.vF, aF = h1.vF as Element of K by H2;
reconsider lE = li2.vE, aE = h2.vE as Element of K by H2;
D4: [lF,aF]
in [:the carrier of F,the carrier of F:] by ZFMISC_1:def 2;
D5:[:the carrier of F,the carrier of F:] c=
[:the carrier of E,the carrier of E:] by H2,ZFMISC_1:96;
D6: l1.vF
= li1.vF + h1.vF by B,VECTSP_6:22
.= ((the addF of E)||the carrier of F).(lF,aF) by H1,C0SP1:def 3
.= (the addF of E).(lF,aF) by D4,FUNCT_1:49
.= ((the addF of K)||the carrier of E).(lF,aF) by H1,C0SP1:def 3
.= lF + aF by D4,D5,FUNCT_1:49;
D7: [lE,aE] in [:the carrier of E,the carrier of E:]
by ZFMISC_1:def 2;
D8: l2.vF
= li2.vE + h2.vE by C,VECTSP_6:22
.= ((the addF of K)||the carrier of E).(lE,aE) by H1,C0SP1:def 3
.= lE + aE by D7,FUNCT_1:49;
lF = lF + 0.K
.= lF + (aF + -aF) by RLVECT_1:5
.= (lF + aF) + -aF by RLVECT_1:def 3
.= lE + (aE + -aE) by A0,D6,D8,RLVECT_1:def 3
.= lE + 0.K by RLVECT_1:5;
hence li1.o = li2.o;
end;
hence thesis by D1;
end;
ZZ: v1 is Element of K by FIELD_4:def 6;
Z7: li1.v1 = l1.v1 - h1.v1 by VECTSP_6:40
.= l1.v1 - l1.v1 by ZZ,G1
.= 0.F by RLVECT_1:5;
Carrier l1 = (Carrier li1) \/ {v1}
proof
B9: li1.v1 = l1.v1 - h1.v1 by VECTSP_6:40
.= l1.v1 + -l1.v1 by ZZ,G1
.= 0.F by RLVECT_1:5;
B0: for x being Element of K st x <> v1 holds li1.x = l1.x
proof
let x be Element of K;
reconsider v = x as Element of VecSp(K,F) by FIELD_4:def 6;
assume x <> v1;
then not v in {v1} by TARSKI:def 1;
then h1.v = 0.F by Z100,VECTSP_6:1;
then li1.v = l1.v - 0.F by VECTSP_6:40;
hence thesis;
end;
B7: now let o be object;
assume B8: o in Carrier li1; then
reconsider v = o as Element of VecSp(K,F);
reconsider vK = v as Element of K by FIELD_4:def 6;
B1: li1.v <> 0.F by B8,VECTSP_6:2; then
li1.vK = l1.vK by B0,B9;
hence o in Carrier l1 by B1,VECTSP_6:2;
end;
B1: now let o be object;
assume B2: o in Carrier l1; then
reconsider v = o as Element of VecSp(K,F);
ZZ: v is Element of K by FIELD_4:def 6;
per cases;
suppose o = v1;
then o in {v1} by TARSKI:def 1;
hence o in (Carrier li1) \/ {v1} by XBOOLE_0:def 3;
end;
suppose o <> v1;
then l1.v = li1.v by ZZ,B0;
then li1.v <> 0.F by B2,VECTSP_6:2;
then v in Carrier li1 by VECTSP_6:2;
hence o in (Carrier li1) \/ {v1} by XBOOLE_0:def 3;
end;
end;
now let o be object;
assume o in (Carrier li1) \/ {v1};
then per cases by XBOOLE_0:def 3;
suppose o in Carrier li1;
hence o in Carrier l1 by B7;
end;
suppose o in {v1};
hence o in Carrier l1 by A2,TARSKI:def 1;
end;
end;
hence thesis by B1,TARSKI:2;
end; then
Z8: card(Carrier li1) + 1 = k + 1 by Z7,A0,VECTSP_6:2,CARD_2:41;
thus Sum l1 = Sum li1 + Sum h1 by B,VECTSP_6:44
.= (the addF of VecSp(K,F)).(Sum li2,Sum h2) by Z8,Z6,Z5,A0,IV
.= (the addF of K).(Sum li2,Sum h2) by FIELD_4:def 6
.= Sum li2 + Sum h2 by FIELD_4:def 6
.= Sum l2 by C,VECTSP_6:44;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
consider n being Nat such that H: card(Carrier l1) = n;
thus thesis by AS,I,H;
end;
definition
let F be Field,
E be FieldExtension of F,
K be F-extending FieldExtension of E;
:: without attribute F-extending Mizar gives an error!
let BE be Subset of VecSp(E,F), BK be Subset of VecSp(K,E);
func Base(BE,BK) -> Subset of VecSp(K qua FieldExtension of F,F) equals
{ a * b where a,b is Element of K : a in BE & b in BK };
coherence
proof
now let o be object;
assume o in { a * b where a,b is Element of K : a in BE & b in BK };
then consider a,b being Element of K such that
A: o = a * b & a in BE & b in BK;
the carrier of VecSp((K qua FieldExtension of F),F)
= the carrier of K by FIELD_4:def 6;
hence o in the carrier of VecSp((K qua FieldExtension of F),F) by A;
end;
then {a*b where a,b is Element of K : a in BE & b in BK} c=
the carrier of VecSp((K qua FieldExtension of F),F);
hence thesis;
end;
end;
registration
let F be Field,
E be FieldExtension of F,
K be F-extending FieldExtension of E;
let BE be non empty Subset of VecSp(E,F),
BK be non empty Subset of VecSp(K,E);
cluster Base(BE,BK) -> non empty;
coherence
proof
F is Subring of E & E is Subring of K by FIELD_4:def 1; then
H3: the carrier of E c= the carrier of K by C0SP1:def 3;
H2: the carrier of VecSp(K,E) = the carrier of K &
the carrier of VecSp(E,F) = the carrier of E by FIELD_4:def 6;
set x = the Element of BE, y = the Element of BK;
reconsider a = x, b = y as Element of K by H2,H3;
a * b in {a * b where a,b is Element of K : a in BE & b in BK};
hence thesis;
end;
end;
BE0:
for F being Field,
E being FieldExtension of F,
K being F-extending FieldExtension of E
for BE being linearly-independent Subset of VecSp(E,F),
BK being linearly-independent Subset of VecSp(K,E)
for a1,a2,b1,b2 being Element of K
st a1 in BE & a2 in BE & b1 in BK & b2 in BK & b1 <> b2
holds a1 * b1 <> a2 * b2
proof
let F be Field, E be FieldExtension of F,
K be F-extending FieldExtension of E;
let BE be linearly-independent Subset of VecSp(E,F),
BK be linearly-independent Subset of VecSp(K,E);
let a1, a2, b1, b2 be Element of K;
set VE = VecSp(E,F), VK = VecSp(K,E);
assume A0: a1 in BE & a2 in BE & b1 in BK & b2 in BK & b1 <> b2;
then reconsider a1v = a1, a2v = a2 as Element of VE;
reconsider b1v = b1, b2v = b2 as Element of VK by A0;
A1: a1 <> 0.VE by A0,VECTSP_7:2;
A3: 0.VE = 0.E & 0.VK = 0.K by FIELD_4:def 6;
A5: E is Subring of K & E is Subfield of K by FIELD_4:7,FIELD_4:def 1; then
Z: 0.K = 0.E & 1.E = 1.K by C0SP1:def 3;
reconsider a1e=a1, a2e=a2 as Element of the carrier of E by A0,FIELD_4:def 6;
a1 is non zero by A1,A3,A5,C0SP1:def 3; then
a1e" = a1" by A5,FIELD_6:18; then
a1e" * a2e = a1" * a2 by A5,FIELD_6:16; then
ZZ: -a1e" * a2e = -a1" * a2 by A5,FIELD_6:17;
defpred P[object,object] means
($1 = b1 & $2 = 1.E) or ($1 = b2 & $2 = -a1" * a2) or
($1 <> b1 & $1 <> b2 & $2 = 0.E);
A: for x being object st x in the carrier of VK
ex y being object st y in the carrier of E & P[x,y]
proof
let x be object;
assume x in the carrier of VK;
per cases;
suppose x = b1;
hence ex y being object st y in the carrier of E & P[x,y];
end;
suppose x = b2;
hence ex y being object st y in the carrier of E & P[x,y] by ZZ;
end;
suppose x <> b1 & x <> b2;
hence ex y being object st y in the carrier of E & P[x,y];
end;
end;
consider l being Function of the carrier of VK,the carrier of E such that
L: for x being object st x in the carrier of VK holds P[x,l.x]
from FUNCT_2:sch 1(A);
reconsider l as Element of Funcs(the carrier of VK, the carrier of E)
by FUNCT_2:8;
for v being Element of VK st not v in {b1v,b2v} holds l.v = 0.E
proof
let v being Element of VK;
assume not v in {b1v,b2v};
then v <> b1 & v <> b2 by TARSKI:def 2;
hence l.v = 0.E by L;
end;
then reconsider l as Linear_Combination of VK by VECTSP_6:def 1;
B: l.b1v = 1.E by A0,L .= 1.K by A5,C0SP1:def 3; then
A6: b1 in Carrier(l) <> {} by Z,VECTSP_6:1;
C1: [l.b1v, b1v] in [:the carrier of E,the carrier of K:] by ZFMISC_1:def 2;
D: l.b1v * b1v
= ((the multF of K)|[:the carrier of E,the carrier of K:]).(l.b1v,b1v)
by FIELD_4:def 6
.= 1.K * b1 by B,C1,FUNCT_1:49;
C1: [l.b2v, b2v] in [:the carrier of E,the carrier of K:] by ZFMISC_1:def 2;
E: l.b2v * b2v
= ((the multF of K)|[:the carrier of E,the carrier of K:]).(l.b2v,b2v)
by FIELD_4:def 6
.= (the multF of K).(l.b2v,b2v) by C1,FUNCT_1:49
.= (-a1" * a2) * b2 by A0,L;
now let o be object;
assume o in Carrier l;
then consider v being Element of VK such that
A1: o = v & l.v <> 0.E by VECTSP_6:1;
(v = b1 & l.v = 1.E) or (v = b2 & l.v = -a1" * a2) by L,A1;
hence o in {b1v,b2v} by A1,TARSKI:def 2;
end;
then Carrier(l) c= {b1v,b2v};
then reconsider l as Linear_Combination of {b1v,b2v} by VECTSP_6:def 4;
A7: Sum(l) = l.b1v * b1v + l.b2v * b2v by A0,VECTSP_6:18
.= 1.K * b1 + (-a1" * a2) * b2 by D,E,FIELD_4:def 6;
A8: {b1v,b2v} c= BK by A0,TARSKI:def 2;
A9: a1 <> 0.K by A3,A1,A5,C0SP1:def 3;
now assume a1 * b1 = a2 * b2;
then 0.K = a1 * b1 - 1.K * (a2 * b2) by RLVECT_1:15
.= a1 * b1 - (a1" * a1) * (a2 * b2) by A9,VECTSP_1:def 10
.= a1 * b1 - (a1 * a1") * (a2 * b2) by GROUP_1:def 12
.= a1 * b1 - a1 * (a1" * (a2 * b2)) by GROUP_1:def 3
.= a1 * (b1 - a1" * (a2 * b2)) by VECTSP_1:11;
then 0.K = 1.K * b1 - a1" * (a2 * b2) by Z,A1,A3,VECTSP_2:def 1
.= 1.K * b1 + -((a1" * a2) * b2) by GROUP_1:def 3
.= Sum l by A7,VECTSP_1:9;
hence contradiction by A3,A6,A8,VECTSP_7:1,VECTSP_7:def 1;
end;
hence thesis;
end;
theorem
for F being Field,
E being FieldExtension of F,
K being F-extending FieldExtension of E
for BE being linearly-independent Subset of VecSp(E,F),
BK being linearly-independent Subset of VecSp(K,E)
for a1,a2,b1,b2 being Element of K
st a1 in BE & a2 in BE & b1 in BK & b2 in BK
holds a1 * b1 = a2 * b2 implies (a1 = a2 & b1 = b2)
proof
let F be Field, E be FieldExtension of F,
K be F-extending FieldExtension of E;
let BE be linearly-independent Subset of VecSp(E,F),
BK be linearly-independent Subset of VecSp(K,E);
let a1, a2, b1, b2 be Element of K;
assume A1: a1 in BE & a2 in BE & b1 in BK & b2 in BK;
then reconsider b1v = b1 as Element of VecSp(K,E);
assume A2: a1 * b1 = a2 * b2;
{b1v} c= BK by A1,TARSKI:def 1;
then b1v <> 0.VecSp(K,E) by VECTSP_7:1,VECTSP_7:3;
then A3: b1 <> 0.K by FIELD_4:def 6;
A4: b1 = b2 by A1,A2,BE0;
a1 * b1 = b2 * a2 by A2,GROUP_1:def 12;
then b1 * a1 = b2 * a2 by GROUP_1:def 12;
hence thesis by A3,A4,VECTSP_2:8;
end;
theorem BE1:
for F being Field,
E being FieldExtension of F,
K being F-extending FieldExtension of E
for BE being non empty linearly-independent Subset of VecSp(E,F),
BK being non empty linearly-independent Subset of VecSp(K,E)
holds card Base(BE,BK) = card [:BE,BK:]
proof
let F be Field, E be FieldExtension of F, K be F-extending FieldExtension of E;
let BE be non empty linearly-independent Subset of VecSp(E,F),
BK be non empty linearly-independent Subset of VecSp(K,E);
defpred P[object,object] means
ex a,b being Element of K st a in BE & b in BK & $1 = a * b & $2 = [a,b];
A: now let x be object;
assume x in Base(BE,BK); then
consider a,b being Element of K such that
B1: x = a * b & a in BE & b in BK;
thus ex y being object st y in [:BE,BK:] & P[x,y]
proof
take [a,b];
thus thesis by B1,ZFMISC_1:def 2;
end;
end;
consider f being Function of Base(BE,BK),[:BE,BK:] such that
B: for x being object st x in Base(BE,BK) holds P[x,f.x]
from FUNCT_2:sch 1(A);
C: dom f = Base(BE,BK) by FUNCT_2:def 1;
H1: the carrier of VecSp(K,E) = the carrier of K &
the carrier of VecSp(E,F) = the carrier of E by FIELD_4:def 6;
H2: 0.VecSp(K,E) = 0.K by FIELD_4:def 6;
E is Subring of K by FIELD_4:def 1; then
H5: the carrier of E c= the carrier of K by C0SP1:def 3;
D: rng f = [:BE,BK:]
proof
D1: now let o be object;
assume o in [:BE,BK:]; then
consider a,b being object such that
E1: a in BE & b in BK & o = [a,b] by ZFMISC_1:def 2;
reconsider a,b as Element of K by E1,H1,H5;
E0: a * b in Base(BE,BK) by E1;
a * b in dom f by E1,C;
then E2: f.(a*b) in rng f by FUNCT_1:3;
consider a1,b1 being Element of K such that
E3: a1 in BE & b1 in BK & a * b = a1 * b1 & f.(a*b) = [a1,b1] by E0,B;
E4: b1 = b by BE0,E3,E1;
reconsider bV = b as Element of VecSp(K,E) by FIELD_4:def 6;
{b} c= BK by E1,TARSKI:def 1; then
{bV} is linearly-independent by VECTSP_7:1; then
E5: b <> 0.K by H2,VECTSP_7:3;
b * a = a1 * b by E3,E4,GROUP_1:def 12
.= b * a1 by GROUP_1:def 12;
hence o in rng f by E1,E2,E3,E4,E5,VECTSP_1:5;
end;
rng f c= [:BE,BK:];
hence thesis by D1,TARSKI:2;
end;
f is one-to-one
proof
now let x1,x2 be object;
assume F0: x1 in Base(BE,BK) & x2 in Base(BE,BK) & f.x1 = f.x2;
then consider a1,b1 being Element of K such that
F1: x1 = a1 * b1 & a1 in BE & b1 in BK;
consider a2,b2 being Element of K such that
F2: x2 = a2 * b2 & a2 in BE & b2 in BK by F0;
F3: f.(a1*b1) = [a1,b1]
proof
P[a1*b1,f.(a1*b1)] by F0,F1,B; then
consider a3,b3 being Element of K such that
E3: a3 in BE & b3 in BK & a1 * b1 = a3 * b3 & f.(a3*b3) = [a3,b3];
E4: b3 = b1 by BE0,F1,E3;
reconsider b1V = b1 as Element of VecSp(K,E) by FIELD_4:def 6;
{b1} c= BK by F1,TARSKI:def 1; then
{b1V} is linearly-independent by VECTSP_7:1; then
E5: b1 <> 0.K by H2,VECTSP_7:3;
b1 * a1 = a3 * b1 by E3,E4,GROUP_1:def 12
.= b1 * a3 by GROUP_1:def 12;
hence thesis by E4,E3,E5,VECTSP_1:5;
end;
f.(a2*b2) = [a2,b2]
proof
P[a2*b2,f.(a2*b2)] by F0,F2,B; then
consider a3,b3 being Element of K such that
E3: a3 in BE & b3 in BK & a2 * b2 = a3 * b3 & f.(a3*b3) = [a3,b3];
E4: b3 = b2 by BE0,F2,E3;
reconsider b2V = b2 as Element of VecSp(K,E) by FIELD_4:def 6;
{b2} c= BK by F2,TARSKI:def 1; then
{b2V} is linearly-independent by VECTSP_7:1; then
E5: b2 <> 0.K by H2,VECTSP_7:3;
b2 * a2 = a3 * b2 by E3,E4,GROUP_1:def 12
.= b2 * a3 by GROUP_1:def 12;
hence thesis by E4,E3,E5,VECTSP_1:5;
end;
hence x1 = x2 by F0,F1,F2,F3;
end;
hence thesis by FUNCT_2:19;
end;
hence thesis by C,D,CARD_1:70;
end;
theorem BE2:
for F being Field,
E being FieldExtension of F,
K being F-extending FieldExtension of E
for BE being non empty finite linearly-independent Subset of VecSp(E,F),
BK being non empty finite linearly-independent Subset of VecSp(K,E)
holds card Base(BE,BK) = card BE * card BK
proof
let F be Field, E be FieldExtension of F,
K be F-extending FieldExtension of E;
let BE be non empty finite linearly-independent Subset of VecSp(E,F),
BK be non empty finite linearly-independent Subset of VecSp(K,E);
thus card BE * card BK = card [:BE,BK:] by CARD_2:46
.= card Base(BE,BK) by BE1;
end;
registration
let F be Field,
E be FieldExtension of F,
K be F-extending FieldExtension of E;
let BE be non empty finite linearly-independent Subset of VecSp(E,F),
BK be non empty finite linearly-independent Subset of VecSp(K,E);
cluster Base(BE,BK) -> finite;
coherence
proof
card [:BE,BK:] is finite; then
card Base(BE,BK) is finite by BE1;
hence thesis;
end;
end;
definition
let F be Field,
E be FieldExtension of F,
K be F-extending FieldExtension of E;
let BE be non empty finite linearly-independent Subset of VecSp(E,F),
BK be non empty linearly-independent Subset of VecSp(K,E);
let l be Linear_Combination of Base(BE,BK);
let b be Element of K;
func down(l,b) -> Linear_Combination of BE means :down1:
(for a being Element of K st a in BE & b in BK holds it.a = l.(a*b)) &
(for a being Element of E st not a in BE or not b in BK holds it.a = 0.F);
existence
proof
set V = VecSp(E,F);
H0: the carrier of V = the carrier of E &
the carrier of VecSp(K,F) = the carrier of K by FIELD_4:def 6;
defpred P[Element of E,Element of F] means
($1 in BE & b in BK & $2 = l.(@($1,K)*b)) or
((not $1 in BE or not b in BK) & $2 = 0.F);
G0: now let x be Element of E;
per cases;
suppose G: x in BE & b in BK;
thus ex y being Element of F st P[x,y]
proof
take l.(@(x,K)*b);
thus thesis by G,H0,FUNCT_2:5;
end;
end;
suppose not x in BE;
hence ex y being Element of F st P[x,y];
end;
suppose not b in BK;
hence ex y being Element of F st P[x,y];
end;
end;
consider f being Function of the carrier of E, the carrier of F such that
G1: for x being Element of E holds P[x,f.x] from FUNCT_2:sch 3(G0);
dom f = the carrier of V & rng f c= the carrier of F by H0,FUNCT_2:def 1; then
reconsider f as Element of Funcs(the carrier of V, the carrier of F)
by FUNCT_2:def 2;
for v being Element of V st not v in BE holds f.v = 0.F by H0,G1;
then reconsider l1 = f as Linear_Combination of V by VECTSP_6:def 1;
now let o be object;
assume C1: o in Carrier l1; then
reconsider v = o as Element of V;
l1.v <> 0.F by C1,VECTSP_6:2;
hence o in BE by H0,G1;
end;
then Carrier l1 c= BE;
then reconsider l1 as Linear_Combination of BE by VECTSP_6:def 4;
take l1;
now let a be Element of K;
assume G: a in BE & b in BK;
then reconsider aE = a as Element of E by FIELD_4:def 6;
thus l1.a = l.(@(aE,K)*b) by G,G1 .= l.(a*b);
end;
hence thesis by G1;
end;
uniqueness
proof
let l1,l2 be Linear_Combination of BE such that A1:
(for a being Element of K st a in BE & b in BK holds l1.a = l.(a*b)) &
(for a being Element of E st not a in BE or not b in BK holds l1.a = 0.F)
and A2:
(for a being Element of K st a in BE & b in BK holds l2.a = l.(a*b)) &
(for a being Element of E st not a in BE or not b in BK holds l2.a = 0.F);
A3: the carrier of VecSp(E,F) = the carrier of E by FIELD_4:def 6;
E is Subring of K by FIELD_4:def 1; then
A5: the carrier of E c= the carrier of K by C0SP1:def 3;
now let o be object;
assume A: o in the carrier of VecSp(E,F);
per cases;
suppose A7: o in BE & b in BK;
reconsider a = o as Element of K by A,A3,A5;
l1.a = l.(a*b) by A1,A7 .= l2.a by A7,A2;
hence l1.o = l2.o;
end;
suppose A7: not o in BE or not b in BK;
reconsider a = o as Element of E by A,FIELD_4:def 6;
l1.a = 0.F by A1,A7 .= l2.a by A7,A2;
hence l1.o = l2.o;
end;
end;
hence thesis;
end;
end;
definition
let F be Field,
E be FieldExtension of F,
K be F-extending FieldExtension of E;
let BE be non empty finite linearly-independent Subset of VecSp(E,F),
BK be non empty finite linearly-independent Subset of VecSp(K,E);
let l be Linear_Combination of Base(BE,BK);
func down l -> Linear_Combination of BK means :down2:
for b being Element of K st b in BK holds it.b = Sum down(l,b);
existence
proof
set V = VecSp(K,E);
H0: the carrier of V = the carrier of K &
the carrier of VecSp(E,F) = the carrier of E by FIELD_4:def 6;
defpred P[Element of K,Element of E] means
($1 in BK & $2 = Sum down(l,$1)) or (not $1 in BK & $2 = 0.E);
G0: now let x be Element of K;
per cases;
suppose x in BK;
hence ex y being Element of E st P[x,y] by H0;
end;
suppose not x in BK;
hence ex y being Element of E st P[x,y];
end;
end;
consider f being Function of the carrier of K, the carrier of E such that
G1: for x being Element of K holds P[x,f.x] from FUNCT_2:sch 3(G0);
dom f = the carrier of V & rng f c= the carrier of E by H0,FUNCT_2:def 1; then
reconsider f as Element of Funcs(the carrier of V, the carrier of E)
by FUNCT_2:def 2;
for v being Element of V st not v in BK holds f.v = 0.E by H0,G1;
then reconsider l1 = f as Linear_Combination of V by VECTSP_6:def 1;
now let o be object;
assume C1: o in Carrier l1; then
reconsider v = o as Element of V;
l1.v <> 0.E by C1,VECTSP_6:2;
hence o in BK by H0,G1;
end;
then Carrier l1 c= BK;
then reconsider l1 as Linear_Combination of BK by VECTSP_6:def 4;
take l1;
thus thesis by G1;
end;
uniqueness
proof
let l1,l2 be Linear_Combination of BK such that
A1: for b being Element of K st b in BK holds l1.b = Sum down(l,b) and
A2: for b being Element of K st b in BK holds l2.b = Sum down(l,b);
A6: Carrier l1 c= BK & Carrier l2 c= BK by VECTSP_6:def 4;
now let o be object;
assume A: o in the carrier of VecSp(K,E); then
reconsider b = o as Element of K by FIELD_4:def 6;
reconsider bV = o as Element of VecSp(K,E) by A;
per cases;
suppose A7: b in BK;
then l1.b = Sum down(l,b) by A1 .= l2.b by A7,A2;
hence l1.o = l2.o;
end;
suppose A7: not b in BK;
then l1.bV = 0.E by A6,VECTSP_6:2 .= l2.bV by A6,A7,VECTSP_6:2;
hence l1.o = l2.o;
end;
end;
hence thesis;
end;
end;
T0: for F being Field,
E being FieldExtension of F,
K being F-extending FieldExtension of E
for BE being Basis of VecSp(E,F)
for l1 being Linear_Combination of VecSp(K,E)
for b being Element of K
ex l2 being Linear_Combination of BE st l1.b = Sum l2
proof
let F be Field, E be FieldExtension of F, K be F-extending FieldExtension of E;
let BE be Basis of VecSp(E,F);
let l1 be Linear_Combination of VecSp(K,E), b be Element of K;
A: the carrier of VecSp(K,E) = the carrier of K by FIELD_4:def 6;
B: the carrier of VecSp(E,F) = the carrier of E by FIELD_4:def 6;
VecSp(E,F) = Lin BE by VECTSP_7:def 3; then
l1.b in Lin BE by A,B,FUNCT_2:5;
hence thesis by VECTSP_7:7;
end;
definition
let F be Field,
E be F-finite FieldExtension of F,
K be F-extending FieldExtension of E;
let BE be Basis of VecSp(E,F),
BK be non empty finite linearly-independent Subset of VecSp(K,E);
let l1 be Linear_Combination of BK;
func lift(l1,BE) -> Linear_Combination of Base(BE,BK) means :lif:
for b being Element of K st b in BK
ex l2 being Linear_Combination of BE
st Sum l2 = l1.b &
for a being Element of K st a in BE & a * b in Base(BE,BK)
holds it.(a*b) = l2.a;
existence
proof
set V = VecSp(K,F);
H0: the carrier of V = the carrier of K &
the carrier of VecSp(E,F) = the carrier of E &
the carrier of VecSp(K,E) = the carrier of K by FIELD_4:def 6;
defpred P[Element of K,Element of F] means
($1 in Base(BE,BK) &
ex a,b being Element of K
st $1 = a * b & a in BE & b in BK & a * b in Base(BE,BK) &
ex l2 being Linear_Combination of BE st Sum l2 = l1.b & $2 = l2.a)
or (not $1 in Base(BE,BK) & $2 = 0.F);
G0: now let x be Element of K;
per cases;
suppose G: x in Base(BE,BK); then
consider a,b being Element of K such that
G1: x = a * b & a in BE & b in BK;
consider l2 being Linear_Combination of BE such that
G2: l1.b = Sum l2 by T0;
reconsider y = l2.a as Element of F by G1,FUNCT_2:5;
P[x,y] by G,G2,G1;
hence ex y being Element of F st P[x,y];
end;
suppose not x in Base(BE,BK);
hence ex y being Element of F st P[x,y];
end;
end;
consider f being Function of the carrier of K, the carrier of F such that
G1: for x being Element of K holds P[x,f.x] from FUNCT_2:sch 3(G0);
dom f = the carrier of V & rng f c= the carrier of F by H0,FUNCT_2:def 1; then
reconsider f as Element of Funcs(the carrier of V, the carrier of F)
by FUNCT_2:def 2;
for v being Element of V st not v in Base(BE,BK) holds f.v = 0.F by H0,G1;
then reconsider l = f as Linear_Combination of V by VECTSP_6:def 1;
now let o be object;
assume C1: o in Carrier l; then
reconsider v = o as Element of V;
l.v <> 0.F by C1,VECTSP_6:2;
hence o in Base(BE,BK) by H0,G1;
end;
then Carrier l c= Base(BE,BK);
then reconsider l as Linear_Combination of Base(BE,BK) by VECTSP_6:def 4;
take l;
now let b be Element of K;
assume F1: b in BK;
consider l2 being Linear_Combination of BE such that
F2: l1.b = Sum l2 by T0;
now let a be Element of K;
assume F3: a in BE & a * b in Base(BE,BK);
reconsider y = l.(a*b) as Element of F by FUNCT_2:5;
P[a*b,y] by G1; then
consider a1,b1 being Element of K such that
F4: a * b = a1 * b1 & a1 in BE & b1 in BK & a * b in Base(BE,BK) &
ex l3 being Linear_Combination of BE st Sum l3 = l1.b1 & y = l3.a1
by F3;
consider l3 being Linear_Combination of BE such that
F5: Sum l3 = l1.b1 & y = l3.a1 by F4;
F7: b1 = b by BE0,F4,F3,F1;
then F8: l2 = l3 by F5,F2,ZMODUL033;
H2: 0.VecSp(K,E) = 0.K by FIELD_4:def 6;
reconsider b1V = b1 as Element of VecSp(K,E) by FIELD_4:def 6;
{b1} c= BK by F4,TARSKI:def 1; then
{b1V} is linearly-independent by VECTSP_7:1; then
F9: b1 <> 0.K by H2,VECTSP_7:3;
b1 * a1 = a1 * b1 by GROUP_1:def 12 .= b1 * a by F4,F7,GROUP_1:def 12;
hence l.(a*b) = l2.a by F8,F5,F9,VECTSP_1:5;
end;
hence
ex l2 being Linear_Combination of BE
st Sum l2 = l1.b &
for a being Element of K st a in BE & a * b in Base(BE,BK)
holds l.(a*b) = l2.a by F2;
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Linear_Combination of Base(BE,BK) such that
A1: for b being Element of K st b in BK
ex l2 being Linear_Combination of BE
st Sum l2 = l1.b &
for a being Element of K st a in BE & a * b in Base(BE,BK)
holds f1.(a*b) = l2.a and
A2: for b being Element of K st b in BK
ex l2 being Linear_Combination of BE
st Sum l2 = l1.b &
for a being Element of K st a in BE & a * b in Base(BE,BK)
holds f2.(a*b) = l2.a;
A6: Carrier f1 c= Base(BE,BK) & Carrier f2 c= Base(BE,BK) by VECTSP_6:def 4;
now let o be object;
assume A: o in the carrier of VecSp(K,F); then
reconsider c = o as Element of K by FIELD_4:def 6;
reconsider cV = o as Element of VecSp(K,F) by A;
per cases;
suppose B0: c in Base(BE,BK); then
consider a,b being Element of K such that
B1: c = a * b & a in BE & b in BK;
consider f1l2 being Linear_Combination of BE such that
B2: Sum f1l2 = l1.b &
for a being Element of K st a in BE & a * b in Base(BE,BK)
holds f1.(a*b) = f1l2.a by B1,A1;
consider f2l2 being Linear_Combination of BE such that
B3: Sum f2l2 = l1.b &
for a being Element of K st a in BE & a * b in Base(BE,BK)
holds f2.(a*b) = f2l2.a by B1,A2;
f1l2 = f2l2 by B2,B3,ZMODUL033; then
f1.(a*b) = f2l2.a by B0,B1,B2 .= f2.(a*b) by B0,B1,B3;
hence f1.o = f2.o by B1;
end;
suppose A7: not c in Base(BE,BK);
then f1.cV = 0.F by A6,VECTSP_6:2 .= f2.cV by A6,A7,VECTSP_6:2;
hence f1.o = f2.o;
end;
end;
hence thesis;
end;
end;
theorem
for F being Field,
E being F-finite FieldExtension of F,
K being E-finite F-extending FieldExtension of E
for BE being Basis of VecSp(E,F), BK being Basis of VecSp(K,E)
for l being Linear_Combination of Base(BE,BK) holds lift(down l,BE) = l
proof
let F be Field, E be F-finite FieldExtension of F,
K be E-finite F-extending FieldExtension of E;
let BE be Basis of VecSp(E,F), BK be Basis of VecSp(K,E);
let l be Linear_Combination of Base(BE,BK);
H4: Carrier l c= Base(BE,BK) by VECTSP_6:def 4;
now let o be object;
assume AS: o in the carrier of VecSp(K,F); then
reconsider c = o as Element of K by FIELD_4:def 6;
reconsider cV = o as Element of VecSp(K,F) by AS;
per cases;
suppose AS: c in Base(BE,BK); then
consider a,b being Element of K such that
A: c = a * b & a in BE & b in BK;
B: (down l).b = Sum down(l,b) by A,down2;
consider l2 being Linear_Combination of BE such that
D: Sum l2 = (down l).b &
for a being Element of K st a in BE & a * b in Base(BE,BK)
holds lift(down l,BE).(a*b) = l2.a by A,lif;
l2 = down(l,b) by D,B,ZMODUL033;
then lift(down l,BE).(a*b)
= down(l,b).a by A,D,AS
.= l.(a*b) by A,down1;
hence l.o = lift(down l,BE).o by A;
end;
suppose X: not c in Base(BE,BK); then
A: l.cV = 0.F by H4,VECTSP_6:2;
Carrier lift(down l,BE) c= Base(BE,BK) by VECTSP_6:def 4;
hence l.o = lift(down l,BE).o by A,X,VECTSP_6:2;
end;
end;
hence thesis;
end;
theorem Tlift2:
for F being Field,
E being F-finite FieldExtension of F,
K being E-finite F-extending FieldExtension of E
for BE being Basis of VecSp(E,F), BK being Basis of VecSp(K,E)
for l being Linear_Combination of BK holds down lift(l,BE) = l
proof
let F be Field,
E be F-finite FieldExtension of F,
K be E-finite F-extending FieldExtension of E;
let BE being Basis of VecSp(E,F), BK being Basis of VecSp(K,E);
let l1 being Linear_Combination of BK;
H1: the carrier of VecSp(K,E) = the carrier of K &
the carrier of VecSp(E,F) = the carrier of E by FIELD_4:def 6;
E is Subring of K by FIELD_4:def 1; then
H3: the carrier of E c= the carrier of K by C0SP1:def 3;
H4: Carrier l1 c= BK by VECTSP_6:def 4;
now let o be object;
assume AS: o in the carrier of VecSp(K,E); then
reconsider b = o as Element of K by FIELD_4:def 6;
reconsider bV = o as Element of VecSp(K,E) by AS;
per cases;
suppose X: b in BK; then
consider l2 being Linear_Combination of BE such that
A: Sum l2 = l1.b &
for a being Element of K st a in BE & a * b in Base(BE,BK)
holds lift(l1,BE).(a*b) = l2.a by lif;
C: Carrier l2 c= BE by VECTSP_6:def 4;
down(lift(l1,BE),b) = l2
proof
now let o be object;
assume AS: o in the carrier of VecSp(E,F); then
reconsider a = o as Element of K by H1,H3;
reconsider aV = o as Element of VecSp(E,F) by AS;
per cases;
suppose Y: a in BE; then
Z: a * b in Base(BE,BK) by X;
down(lift(l1,BE),b).a = lift(l1,BE).(a*b) by X,Y,down1
.= l2.a by A,Y,Z;
hence down(lift(l1,BE),b).o = l2.o;
end;
suppose AS1: not a in BE; then
D: l2.aV = 0.F by C,VECTSP_6:2;
Carrier down(lift(l1,BE),b) c= BE by VECTSP_6:def 4;
hence down(lift(l1,BE),b).o = l2.o by D,AS1,VECTSP_6:2;
end;
end;
hence thesis;
end;
hence (down lift(l1,BE)).o = l1.o by A,X,down2;
end;
suppose X: not b in BK; then
A: l1.bV = 0.E by H4,VECTSP_6:2;
Carrier down lift(l1,BE) c= BK by VECTSP_6:def 4;
hence (down lift(l1,BE)).o = l1.o by A,X,VECTSP_6:2;
end;
end;
hence thesis;
end;
theorem LSum1a:
for F being Field,
E being FieldExtension of F,
K being F-extending FieldExtension of E
for BE being non empty finite linearly-independent Subset of VecSp(E,F),
BK being non empty finite linearly-independent Subset of VecSp(K,E)
for l,l1,l2 being Linear_Combination of Base(BE,BK) st l = l1 + l2
for b being Element of K holds down(l,b) = down(l1,b) + down(l2,b)
proof
let F be Field, E be FieldExtension of F,
K be F-extending FieldExtension of E;
let BE be non empty finite linearly-independent Subset of VecSp(E,F),
BK be non empty finite linearly-independent Subset of VecSp(K,E);
let l,l1,l2 be Linear_Combination of Base(BE,BK);
assume AS: l = l1 + l2;
let b be Element of K;
E is Subring of K by FIELD_4:def 1; then
X1: the carrier of E c= the carrier of K by C0SP1:def 3;
now let o be object;
assume A0: o in the carrier of VecSp(E,F); then
A2: o in the carrier of E by FIELD_4:def 6; then
reconsider a = o as Element of K by X1;
reconsider aE = o as Element of E by A0,FIELD_4:def 6;
reconsider aV = o as Element of VecSp(E,F) by A0;
reconsider abV = a * b as Element of VecSp(K,F) by FIELD_4:def 6;
per cases;
suppose A1: a in BE & b in BK;
then down(l,b).a
= l.(a*b) by down1
.= l1.abV + l2.abV by AS,VECTSP_6:22
.= (the addF of F).[down(l1,b).a,l2.abV] by A1,down1
.= down(l1,b).aV + down(l2,b).aV by A1,down1
.= (down(l1,b) + down(l2,b)).aV by VECTSP_6:22;
hence down(l,b).o = (down(l1,b) + down(l2,b)).o;
end;
suppose A1: not a in BE or not b in BK;
then A3: down(l1,b).a = 0.F & down(l2,b).a = 0.F by A2,down1;
down(l,b).a = down(l1,b).aV + down(l2,b).aV by A3,A1,A2,down1;
hence down(l,b).o = (down(l1,b) + down(l2,b)).o by VECTSP_6:22;
end;
end;
hence thesis;
end;
theorem LSum1:
for F being Field,
E being FieldExtension of F,
K being F-extending FieldExtension of E
for BE being non empty finite linearly-independent Subset of VecSp(E,F),
BK being non empty finite linearly-independent Subset of VecSp(K,E)
for l,l1,l2 being Linear_Combination of Base(BE,BK) st l = l1 + l2
holds down l = down l1 + down l2
proof
let F be Field, E be FieldExtension of F,
K be F-extending FieldExtension of E;
let BE be non empty finite linearly-independent Subset of VecSp(E,F),
BK be non empty finite linearly-independent Subset of VecSp(K,E);
let l,l1,l2 be Linear_Combination of Base(BE,BK);
assume AS: l = l1 + l2;
now let o be object;
assume A0: o in the carrier of VecSp(K,E); then
reconsider b = o as Element of K by FIELD_4:def 6;
reconsider bV = o as Element of VecSp(K,E) by A0;
H1: Carrier(down l) c= BK & Carrier(down l1) c= BK &
Carrier(down l2) c= BK by VECTSP_6:def 4;
per cases;
suppose A1: b in BK;
then A2: (down l1).b = Sum down(l1,b) by down2;
(down l).b = Sum down(l,b) by A1,down2
.= Sum(down(l1,b) + down(l2,b)) by AS,LSum1a
.= Sum down(l1,b) + Sum down(l2,b) by VECTSP_6:44
.= (the addF of E).[Sum down(l1,b),Sum down(l2,b)]
by FIELD_4:def 6
.= (down l1).bV + (down l2).bV by A1,A2,down2;
hence (down l).o = (down l1 + down l2).o by VECTSP_6:22;
end;
suppose A1: not b in BK;
then (down l).bV = 0.E by H1,VECTSP_6:2
.= (down l1).bV + 0.E by A1,H1,VECTSP_6:2
.= (down l1).bV + (down l2).bV by A1,H1,VECTSP_6:2;
hence (down l).o = (down l1 + down l2).o by VECTSP_6:22;
end;
end;
hence thesis;
end;
LSum2:
for F being Field,
E being FieldExtension of F,
K being F-extending FieldExtension of E
for BE being non empty finite linearly-independent Subset of VecSp(E,F),
BK being non empty finite linearly-independent Subset of VecSp(K,E)
for l being Linear_Combination of Base(BE,BK)
st card(Carrier l) = 1 holds Sum l = Sum(down l)
proof
let F be Field, E be FieldExtension of F,
K be F-extending FieldExtension of E;
let BE be non empty finite linearly-independent Subset of VecSp(E,F),
BK be non empty finite linearly-independent Subset of VecSp(K,E);
let l be Linear_Combination of Base(BE,BK);
H1: the carrier of VecSp(E,F) = the carrier of E &
the carrier of VecSp(K,E) = the carrier of K &
the carrier of VecSp(K,F) = the carrier of K by FIELD_4:def 6;
H2: E is Subring of K & F is Subring of E by FIELD_4:def 1; then
H3: the carrier of E c= the carrier of K &
the carrier of F c= the carrier of E by C0SP1:def 3;
assume card(Carrier l) = 1;
then consider o being object such that
D1: Carrier l = {o} by CARD_2:42;
D2: o in Carrier l by D1,TARSKI:def 1; then
reconsider v = o as Element of VecSp(K,F);
Carrier l c= Base(BE,BK) by VECTSP_6:def 4; then
o in Base(BE,BK) by D2; then
consider a,b being Element of K such that
D3: o = a * b & a in BE & b in BK;
reconsider vab = a * b as Element of VecSp(K,F) by D2,D3;
reconsider vb = b as Element of VecSp(K,E) by FIELD_4:def 6;
reconsider va = a as Element of VecSp(E,F) by D3;
reconsider aE = va as Element of E by FIELD_4:def 6;
a * b is Element of VecSp(K,F) by FIELD_4:def 6; then
B0: l.(a*b) is Element of F by FUNCT_2:5; then
reconsider labE = l.(a*b) as Element of E by H3;
reconsider lab = l.(a*b) as Element of K by B0,H3;
{va} c= BE by D3,TARSKI:def 1; then
a <> 0.VecSp(E,F) by VECTSP_7:3,VECTSP_7:1; then
D7a: a <> 0.E by FIELD_4:def 6;
{vb} c= BK by D3,TARSKI:def 1; then
b <> 0.VecSp(K,E) by VECTSP_7:3,VECTSP_7:1; then
D6a: b <> 0.K by FIELD_4:def 6;
D6: Carrier down(l,b) = {a}
proof
C1: now let u be object;
assume u in {a}; then
C2: u = a by TARSKI:def 1;
C3: down(l,b).a = l.v by D3,down1;
down(l,b).va <> 0.F by C3,D2,VECTSP_6:2;
hence u in Carrier down(l,b) by C2,VECTSP_6:2;
end;
now let u be object;
assume C2: u in Carrier down(l,b); then
reconsider aE = u as Element of E by FIELD_4:def 6;
reconsider aK = aE as Element of K by H3;
reconsider abV = aK * b as Element of VecSp(K,F) by FIELD_4:def 6;
C3: down(l,b).aE <> 0.F by C2,VECTSP_6:2; then
aE in BE & b in BK by down1; then
down(l,b).aK = l.(aK*b) by down1; then
abV in Carrier l by C3,VECTSP_6:2; then
aK * b = a * b by D1,D3,TARSKI:def 1 .= b * a by GROUP_1:def 12; then
b * aK = b * a by GROUP_1:def 12; then
aK = a by D6a,VECTSP_2:8;
hence u in {a} by TARSKI:def 1;
end;
hence thesis by C1,TARSKI:2;
end; then
D7: Sum down(l,b) = down(l,b).va * va by VECTSP_6:20;
D9: down(l,b).a = l.(a*b) = l.v by D3,down1; then
down(l,b).va <> 0.F by D2,VECTSP_6:2; then
D8: labE <> 0.E by D9,H2,C0SP1:def 3;
D10a: for b1 being Element of K
st b1 in BK & b1 <> b holds Carrier down(l,b1) = {}
proof
let b1 be Element of K;
assume E0: b1 in BK & b1 <> b;
now let o be object;
assume E1: o in Carrier down(l,b1);
E2: Carrier down(l,b1) c= BE by VECTSP_6:def 4;
reconsider v = o as Element of VecSp(E,F) by E1;
reconsider vE = v as Element of E by FIELD_4:def 6;
reconsider vb1 = @(vE,K)*b1 as Element of VecSp(K,F)
by FIELD_4:def 6;
E3: down(l,b1).v = l.(@(vE,K)*b1) by E1,E2,E0,down1;
E4: down(l,b1).v <> 0.F by E1,VECTSP_6:2;
vb1 in Carrier l by E3,E4,VECTSP_6:2; then
@(vE,K)*b1 = a * b by D1,D3,TARSKI:def 1;
hence contradiction by D3,E0,E1,E2,BE0;
end;
hence thesis by XBOOLE_0:def 1;
end;
D10: for b1 being Element of K
st b1 in BK & b1 <> b holds (down l).b1 = 0.E
proof
let b1 be Element of K;
assume E1: b1 in BK & b1 <> b; then
E2: (down l).b1 = Sum down(l,b1) by down2;
Carrier down(l,b1) = {} by E1,D10a; then
Sum down(l,b1) = 0.VecSp(E,F) by VECTSP_6:19;
hence thesis by E2,FIELD_4:def 6;
end;
D5: Carrier(down l) = {b}
proof
C0: [labE,aE] in [:the carrier of F,the carrier of E:]
by B0,ZFMISC_1:def 2;
C1: now let u be object;
assume C2: u in {b};
C3: (down l).b
= (the lmult of VecSp(E,F)).[lab,a] by D9,D3,D7,down2
.= ((the multF of E)|[:the carrier of F,the carrier of E:]).
[labE,aE] by FIELD_4:def 6
.= (the multF of E).[labE,aE] by C0,FUNCT_1:49;
labE * aE <> 0.E by D7a,D8,VECTSP_2:def 1; then
vb in Carrier(down l) by C3,VECTSP_6:2;
hence u in Carrier(down l) by C2,TARSKI:def 1;
end;
now let u be object;
assume C2: u in Carrier(down l);
C3: Carrier(down l) c= BK by VECTSP_6:def 4;
reconsider bK = u as Element of K by C2,FIELD_4:def 6;
reconsider bV = bK as Element of VecSp(K,E) by FIELD_4:def 6;
(down l).bK <> 0.E by C2,VECTSP_6:2; then
bK = b by C3,C2,D10;
hence u in {b} by TARSKI:def 1;
end;
hence thesis by C1,TARSKI:2;
end;
B2: down(l,b).a = l.(a*b) by D3,down1;
B3: [l.(a*b),a] in [:the carrier of F,the carrier of E:]
by H1,D3,B0,ZFMISC_1:def 2;
l.(a*b) is Element of the carrier of E by B0,H3; then
B4: [l.(a*b),a] in [:the carrier of E,the carrier of E:]
by H1,D3,ZFMISC_1:def 2;
B6: (down l).vb
= Sum down(l,b) by D3,down2
.= down(l,b).va * va by D6,VECTSP_6:20
.= ((the multF of E)|[:the carrier of F,the carrier of E:]).(l.(a*b),a)
by B2,FIELD_4:def 6
.= (the multF of E).(l.(a*b),a) by B3,FUNCT_1:49
.= ((the multF of K)||(the carrier of E)).(l.(a*b),a)
by H2,C0SP1:def 3
.= lab * a by B4,FUNCT_1:49; then
B7: [lab * a,b] in [:the carrier of E,the carrier of K:]
by ZFMISC_1:def 2;
B: Sum(down l)
= (down l).vb * vb by D5,VECTSP_6:20
.= ((the multF of K)|[:the carrier of E,the carrier of K:]).(lab * a,b)
by B6,FIELD_4:def 6
.= (the multF of K).(lab * a,b) by B7,FUNCT_1:49;
B1: [l.(a*b),a*b] in [:the carrier of F,the carrier of K:]
by B0,ZFMISC_1:def 2;
Sum l
= l.vab * vab by D1,D3,VECTSP_6:20
.= ((the multF of K)|[:the carrier of F,the carrier of K:]).(l.(a*b),a*b)
by FIELD_4:def 6
.= lab * (a * b) by B1,FUNCT_1:49
.= (lab * a) * b by GROUP_1:def 3;
hence Sum l = Sum(down l) by B;
end;
theorem TSum:
for F being Field,
E being F-finite FieldExtension of F,
K being E-finite F-extending FieldExtension of E
for BE being Basis of VecSp(E,F),
BK being Basis of VecSp(K,E)
for l being Linear_Combination of Base(BE,BK) holds Sum l = Sum(down l)
proof
let F be Field, E be F-finite FieldExtension of F,
K be E-finite F-extending FieldExtension of E;
let BE be Basis of VecSp(E,F), BK be Basis of VecSp(K,E);
let l be Linear_Combination of Base(BE,BK);
defpred P[Nat] means
for l being Linear_Combination of Base(BE,BK)
st card(Carrier l) = $1 holds Sum l = Sum(down l);
IA: P[0]
proof
now let l be Linear_Combination of Base(BE,BK);
assume A: card(Carrier l) = 0; then
Carrier l = {}; then
A0: Sum l = 0.VecSp(K,F) by VECTSP_6:19 .= 0.K by FIELD_4:def 6;
A1: now let b be Element of K;
now let o be object;
assume B2: o in Carrier down(l,b);
reconsider a = o as Element of E by B2,FIELD_4:def 6;
reconsider abV = @(a,K)*b as Element of VecSp(K,F)
by FIELD_4:def 6;
B3: down(l,b).a <> 0.F by B2,VECTSP_6:2; then
a in BE & b in BK by down1; then
down(l,b).a = l.(@(a,K)*b) by down1; then
abV in Carrier l by B3,VECTSP_6:2;
hence contradiction by A;
end;
then Carrier down(l,b) = {} by XBOOLE_0:def 1;
hence Sum down(l,b) = 0.VecSp(E,F) by VECTSP_6:19
.= 0.E by FIELD_4:def 6;
end;
A2: for b being Element of K holds (down l).b = 0.E
proof
let b be Element of K;
per cases;
suppose b in BK;
hence (down l).b = Sum down(l,b) by down2 .= 0.E by A1;
end;
suppose B0: not b in BK;
B1: Carrier down l c= BK by VECTSP_6:def 4;
reconsider bV = b as Element of VecSp(K,E) by FIELD_4:def 6;
thus (down l).b = (down l).bV .= 0.E by B0,B1,VECTSP_6:2;
end;
end;
now let o be object;
assume B0: o in Carrier(down l);
reconsider bV = o as Element of VecSp(K,E) by B0;
reconsider b = o as Element of K by B0,FIELD_4:def 6;
(down l).b <> 0.E by B0,VECTSP_6:2;
hence contradiction by A2;
end; then
Carrier(down l) = {} by XBOOLE_0:def 1; then
Sum(down l) = 0.VecSp(K,E) by VECTSP_6:19 .= 0.K by FIELD_4:def 6;
hence Sum l = Sum(down l) by A0;
end;
hence thesis;
end;
H1: the carrier of VecSp(E,F) = the carrier of E &
the carrier of VecSp(K,E) = the carrier of K &
the carrier of VecSp(K,F) = the carrier of K by FIELD_4:def 6;
E is Subring of K & F is Subring of E by FIELD_4:def 1; then
H3: the carrier of E c= the carrier of K &
the carrier of F c= the carrier of E by C0SP1:def 3;
IS: now let k be Nat;
assume IV: P[k];
now let l be Linear_Combination of Base(BE,BK);
assume A0: card(Carrier l) = k + 1; then
A1: Carrier l <> {};
set o = the Element of Carrier l;
A2: o in Carrier l by A1;
A6: Carrier l c= Base(BE,BK) by VECTSP_6:def 4; then
A3: o in Base(BE,BK) by A1; then
consider a,b being Element of K such that
A4: o = a * b & a in BE & b in BK;
reconsider abv = a * b as Element of VecSp(K,F) by FIELD_4:def 6;
defpred P[Element of K,Element of F] means
($1 = a*b & $2 = l.(a*b)) or ($1 <> a*b & $2 = 0.F);
G0: now let x be Element of K;
per cases;
suppose G: x = a * b;
l.(a*b) in the carrier of F by H1,FUNCT_2:5;
hence ex y being Element of F st P[x,y] by G;
end;
suppose x <> a * b;
hence ex y being Element of F st P[x,y];
end;
end;
consider f being Function of the carrier of K,the carrier of F
such that
G1: for x being Element of K holds P[x,f.x] from FUNCT_2:sch 3(G0);
dom f = the carrier of VecSp(K,F) &
rng f c= the carrier of F by H1,FUNCT_2:def 1; then
reconsider f as
Element of Funcs(the carrier of VecSp(K,F), the carrier of F)
by FUNCT_2:def 2;
now let v be Element of VecSp(K,F);
assume not v in Base(BE,BK);
then v <> a * b by A4;
hence f.v = 0.F by H1,G1;
end; then
reconsider h=f as Linear_Combination of VecSp(K,F) by VECTSP_6:def 1;
Z:now let o be object;
assume C1: o in Carrier h; then
reconsider v = o as Element of VecSp(K,F);
reconsider x = v as Element of K by FIELD_4:def 6;
h.x <> 0.F by C1,VECTSP_6:2;
then v = a * b by G1;
hence o in {abv} by TARSKI:def 1;
end;
then Carrier h c= {abv};
then Y: h is Linear_Combination of {abv} by VECTSP_6:def 4;
{abv} c= Base(BE,BK) by A3,A4,TARSKI:def 1; then
reconsider h as Linear_Combination of Base(BE,BK) by Y,VECTSP_6:4;
Carrier h = {abv}
proof
now let o be object;
assume o in {abv}; then
B2: o = abv by TARSKI:def 1;
h.abv = l.(a*b) by G1; then
h.abv <> 0.F by A1,A4,VECTSP_6:2;
hence o in Carrier h by B2,VECTSP_6:2;
end;
hence thesis by Z,TARSKI:2;
end; then
A12: card(Carrier h) = 1 by CARD_2:42;
l.(a*b) is Element of the carrier of F by H1,FUNCT_2:5; then
reconsider lab = l.(a*b) as Element of K by H3;
reconsider labF = l.(a*b) as Element of F by H1,FUNCT_2:5;
set li = l - h;
li - (l - h) = ZeroLC(VecSp(K,F)) by VECTSP_6:43; then
B: l = li - (l - h) + l by VECTSP_6:27
.= li + -(l - h) + l by VECTSP_6:def 11
.= li + -(l + -h) + l by VECTSP_6:def 11
.= li + (-(l + -h) + l) by VECTSP_6:26
.= li + ((-1.F)*(l + -h) + l) by VECTSP_6:def 10
.= li + (((-1.F)*l + (-1.F)*(-h)) + l) by VECTSP_6:33
.= li + (((-1.F)*l + (-1.F)*((-1.F)*h)) + l) by VECTSP_6:def 10
.= li + (((-1.F)*l + ((-1.F)*(-1.F))*h) + l) by VECTSP_6:34
.= li + (((-1.F)*l + ((1.F)*(1.F))*h) + l) by VECTSP_1:10
.= li + (((-1.F)*l + h) + l) by VECTSP_6:35
.= li + ((-l + h) + l) by VECTSP_6:def 10
.= li + ((h + -l) + l) by VECTSP_6:25
.= li + (h + (-l + l)) by VECTSP_6:26
.= li + (h + (l + -l)) by VECTSP_6:25
.= li + (h + (l - l)) by VECTSP_6:def 11
.= li + (h + ZeroLC(VecSp(K,F))) by VECTSP_6:43
.= li + h by VECTSP_6:27;
A8: li.(a*b) = l.abv - h.abv by VECTSP_6:40
.= labF + -labF by G1
.= 0.F by RLVECT_1:5;
A9: for x being Element of K st x <> a * b holds li.x = l.x
proof
let x be Element of K;
reconsider v = x as Element of VecSp(K,F) by FIELD_4:def 6;
assume x <> a * b;
then not v in {abv} by TARSKI:def 1;
then h.v = 0.F by Z,VECTSP_6:1;
then li.v = l.v - 0.F by VECTSP_6:40;
hence thesis;
end;
A10:now let o be object;
assume B0: o in Carrier li; then
reconsider v = o as Element of VecSp(K,F);
reconsider vK = v as Element of K by FIELD_4:def 6;
B1: li.v <> 0.F by B0,VECTSP_6:2; then
li.vK = l.vK by A9,A8;
hence o in Carrier l by B1,VECTSP_6:2;
end;
then Carrier li c= Base(BE,BK) by A6; then
reconsider li as Linear_Combination of Base(BE,BK) by VECTSP_6:def 4;
A11: not (a * b) in Carrier li by A8,VECTSP_6:2;
Carrier l = (Carrier li) \/ {a * b}
proof
B1: now let o be object;
assume B2: o in Carrier l; then
reconsider ab = o as Element of K by FIELD_4:def 6;
reconsider abV = ab as Element of VecSp(K,F) by FIELD_4:def 6;
per cases;
suppose o = a * b;
then o in {a*b} by TARSKI:def 1;
hence o in (Carrier li) \/ {a * b} by XBOOLE_0:def 3;
end;
suppose o <> a * b;
then l.ab = li.ab by A9;
then li.ab <> 0.F by B2,VECTSP_6:2;
then abV in Carrier li by VECTSP_6:2;
hence o in (Carrier li) \/ {a * b} by XBOOLE_0:def 3;
end;
end;
now let o be object;
assume o in (Carrier li) \/ {a * b};
then per cases by XBOOLE_0:def 3;
suppose o in Carrier li;
hence o in Carrier l by A10;
end;
suppose o in {a * b};
hence o in Carrier l by A2,A4,TARSKI:def 1;
end;
end;
hence thesis by B1,TARSKI:2;
end;
then card(Carrier li) + 1 = k + 1 by A0,A11,CARD_2:41; then
G2: Sum li = Sum(down li) by IV;
G3: Sum h = Sum(down h) by A12,LSum2;
G4a: [h.abv,abv] in [:the carrier of F,the carrier of K:]
by ZFMISC_1:def 2;
G4: Sum h = h.abv * abv by Y,VECTSP_6:17
.= (the multF of K)|[:the carrier of F,the carrier of K:].[h.abv,abv]
by FIELD_4:def 6
.= (the multF of K).[h.abv,abv] by G4a,FUNCT_1:49
.= lab * (a*b) by G1;
G5: down l = down li + down h by B,LSum1;
reconsider Sdli = Sum(down li) as Element of K by FIELD_4:def 6;
G6: Sdli + lab * (a*b)
= Sum(down li) + Sum(down h) by G3,G4,FIELD_4:def 6
.= Sum(down l) by G5,VECTSP_6:44;
thus Sum l = Sum li + Sum h by B,VECTSP_6:44
.= Sum(down l) by G6,G4,G2,FIELD_4:def 6;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
consider n being Nat such that H: card(Carrier l) = n;
thus thesis by I,H;
end;
theorem T1:
for F being Field,
E being F-finite FieldExtension of F,
K being E-finite F-extending FieldExtension of E
for BE being Basis of VecSp(E,F),
BK being Basis of VecSp(K,E)
for l being Linear_Combination of Base(BE,BK)
st Sum(l) = 0.VecSp(K qua FieldExtension of F,F) holds Carrier(l) = {}
proof
let F be Field, E be F-finite FieldExtension of F,
K be E-finite F-extending FieldExtension of E;
let BE be Basis of VecSp(E,F), BK be Basis of VecSp(K,E);
let l1 be Linear_Combination of Base(BE,BK);
set l2 = down l1;
assume AS: Sum l1 = 0.VecSp((K qua FieldExtension of F),F);
B: Sum l2 = Sum l1 by TSum
.= 0.K by AS,FIELD_4:def 6
.= 0.VecSp(K,E) by FIELD_4:def 6;
C: Carrier(l2) = {} by B,VECTSP_7:def 1;
D:now let x be Element of K;
assume x in Base(BE,BK); then
consider a,b being Element of K such that
B1: x = a * b & a in BE & b in BK;
reconsider bv = b as Element of VecSp(K,E) by FIELD_4:def 6;
0.VecSp(E,F) = 0.E by FIELD_4:def 6
.= l2.bv by C,VECTSP_6:2
.= Sum down(l1,b) by B1,down2; then
B3: Carrier down(l1,b) = {} by VECTSP_7:def 1;
reconsider av = a as Element of VecSp(E,F) by B1;
0.F = down(l1,b).av by B3,VECTSP_6:2 .= l1.(a*b) by B1,down1;
hence not x in Carrier l1 by B1,VECTSP_6:2;
end;
now let o be object;
assume C1: o in Carrier l1; then
reconsider x = o as Element of K by FIELD_4:def 6;
Carrier l1 c= Base(BE,BK) by VECTSP_6:def 4; then
x in Base(BE,BK) by C1;
hence contradiction by D,C1;
end;
hence thesis by XBOOLE_0:def 1;
end;
theorem T2:
for F being Field,
E being F-finite FieldExtension of F,
K being E-finite F-extending FieldExtension of E
for BE being Basis of VecSp(E,F),
BK being Basis of VecSp(K,E)
holds Lin Base(BE,BK) = the ModuleStr of VecSp(K qua FieldExtension of F,F)
proof
let F be Field, E be F-finite FieldExtension of F,
K be E-finite F-extending FieldExtension of E;
let BE be Basis of VecSp(E,F), BK be Basis of VecSp(K,E);
set V = VecSp((K qua FieldExtension of F),F);
H1: the carrier of V = the carrier of K by FIELD_4:def 6;
H2: Lin BE = the ModuleStr of VecSp(E,F) &
Lin BK = the ModuleStr of VecSp(K,E) by VECTSP_7:def 3;
A: now let o be object;
assume o in the carrier of V;
then o in Lin BK by H1,H2,FIELD_4:def 6;
then consider l1 being Linear_Combination of BK such that
A0: o = Sum l1 by VECTSP_7:7;
set l = lift(l1,BE);
down l = l1 by Tlift2;
then Sum l = o by A0,TSum; then
o in the set of all Sum(l) where l is Linear_Combination of Base(BE,BK);
hence o in the carrier of Lin Base(BE,BK) by VECTSP_7:def 2;
end;
now let o be object;
assume A: o in the carrier of Lin Base(BE,BK);
the carrier of Lin Base(BE,BK) = the set of all Sum(l) where
l is Linear_Combination of Base(BE,BK) by VECTSP_7:def 2;
then consider l1 being Linear_Combination of Base(BE,BK) such that
B: o = Sum l1 by A;
thus o in the carrier of V by B;
end;
hence thesis by A,TARSKI:2,VECTSP_4:31;
end;
theorem BasKEF:
for F being Field,
E being F-finite FieldExtension of F,
K being E-finite F-extending FieldExtension of E
for BE being Basis of VecSp(E,F),
BK being Basis of VecSp(K,E)
holds Base(BE,BK) is Basis of VecSp(K qua FieldExtension of F,F)
proof
let F be Field, E be F-finite FieldExtension of F,
K be E-finite F-extending FieldExtension of E;
let BE be Basis of VecSp(E,F), BK be Basis of VecSp(K,E);
A: for l being Linear_Combination of Base(BE,BK)
st Sum(l) = 0.VecSp((K qua FieldExtension of F),F) holds Carrier(l) = {} by T1;
Lin Base(BE,BK) = the ModuleStr of VecSp((K qua FieldExtension of F),F) by T2;
hence thesis by A,VECTSP_7:def 1,VECTSP_7:def 3;
end;
theorem degmult:
for F being Field,
E being F-finite FieldExtension of F,
K being E-finite F-extending FieldExtension of E
holds deg(K,F) = deg(K,E) * deg(E,F)
proof
let F be Field, E be F-finite FieldExtension of F,
K be E-finite F-extending FieldExtension of E;
set BE = the Basis of VecSp(E,F), BK = the Basis of VecSp(K,E);
BE is finite; then
B1: VecSp(E,F) is finite-dimensional by MATRLIN:def 1;
BK is finite; then
B2: VecSp(K,E) is finite-dimensional by MATRLIN:def 1;
A: Base(BE,BK) is Basis of VecSp((K qua FieldExtension of F),F) by BasKEF; then
B: VecSp(K,F) is finite-dimensional by MATRLIN:def 1;
hence deg(K,F) = dim VecSp(K,F) by FIELD_4:def 7
.= card Base(BE,BK) by VECTSP_9:def 1,B,A
.= card BE * card BK by BE2
.= dim VecSp(E,F) * card BK by VECTSP_9:def 1,B1
.= deg(E,F) * card BK by FIELD_4:def 7
.= deg(E,F) * dim VecSp(K,E) by VECTSP_9:def 1,B2
.= deg(K,E) * deg(E,F) by FIELD_4:def 7;
end;
theorem alg0:
for F being Field,
E being FieldExtension of F,
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)
proof
let F be Field, E be FieldExtension of F, K be E-extending FieldExtension of F;
assume AS: K is F-finite;
hence E is F-finite & deg(E,F) <= deg(K,F) by FIELD_5:15;
set BF = the Basis of VecSp(K,F);
reconsider BF 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)
proof
H1: the carrier of Lin BE c= the carrier of VecSp(K,E) by VECTSP_4:def 2;
the carrier of VecSp(K,E) c= the carrier of Lin BE
proof
now let o be object;
assume o in the carrier of VecSp(K,E); then
o in Lin BF by H0,VECTSP_7:def 3; then
consider l being Linear_Combination of BF such that
H2: o = Sum l by VECTSP_7:7;
reconsider l1 = l as Linear_Combination of BE by sp1;
o = Sum l1 by H2,sp2; then
o in Lin BE by VECTSP_7:7;
hence o in the carrier of Lin BE;
end;
hence thesis;
end;
hence thesis by H1,TARSKI:2,VECTSP_4:31;
end; 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 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;
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;
end;
registration
let F be Field;
let E be F-finite FieldExtension of F;
cluster -> F-finite for E-finite F-extending FieldExtension of E;
coherence
proof
let K be E-finite F-extending FieldExtension of E;
set BE = the Basis of VecSp(E,F), BK = the Basis of VecSp(K,E);
Base(BE,BK) is Basis of VecSp(K,F) by BasKEF; then
VecSp(K,F) is finite-dimensional by MATRLIN:def 1;
hence thesis by FIELD_4:def 8;
end;
end;
lintrans:
for F being Field,
E1 being FieldExtension of F,
E2 being E1-homomorphic FieldExtension of F
for h being Homomorphism of E1,E2 st
for a being Element of E1 st a in F holds h.a = a
holds h is linear-transformation of VecSp(E1,F),VecSp(E2,F)
proof
let F be Field, E1 be FieldExtension of F,
E2 be E1-homomorphic FieldExtension of F;
let h be Homomorphism of E1,E2;
assume AS: for a being Element of E1 st a in F holds h.a = a;
H: dom h = the carrier of E1 by FUNCT_2:def 1
.= the carrier of VecSp(E1,F) by FIELD_4:def 6;
rng h c= the carrier of E2; then
rng h c= the carrier of VecSp(E2,F) by FIELD_4:def 6; then
reconsider f = h as Function of VecSp(E1,F),VecSp(E2,F) by H,FUNCT_2:2;
now let x,y be Element of VecSp(E1,F);
reconsider a = x, b = y as Element of E1 by FIELD_4:def 6;
x + y = a + b by FIELD_4:def 6;
hence f.(x+y) = h.a + h.b by VECTSP_1:def 20
.= f.x + f.y by FIELD_4:def 6;
end; then
A: f is additive;
now let a be Scalar of F, x be Vector of VecSp(E1,F);
reconsider v = x as Element of E1 by FIELD_4:def 6;
F is Subring of E1 by FIELD_4:def 1; then
the carrier of F c= the carrier of E1 by C0SP1:def 3; then
reconsider u1 = a as Element of E1;
F is Subring of E2 by FIELD_4:def 1; then
the carrier of F c= the carrier of E2 by C0SP1:def 3; then
reconsider u2 = a as Element of E2;
I: [u1,v] in [:the carrier of F,the carrier of E1:] by ZFMISC_1:def 2;
H: a * x = (the multF of E1)|[:the carrier of F,the carrier of E1:].(u1,v)
by FIELD_4:def 6
.= u1 * v by I,FUNCT_1:49;
J: [u2,h.v] in [:the carrier of F,the carrier of E2:] by ZFMISC_1:def 2;
K: a in F;
thus f.(a*x) = h.u1 * h.v by H,GROUP_6:def 6
.= u2 * h.v by AS,K
.= (the multF of E2)|[:the carrier of F,the carrier of E2:].(u2,h.v)
by J,FUNCT_1:49
.= a * f.x by FIELD_4:def 6;
end;
hence thesis by A,MOD_2:def 2;
end;
begin :: Algebraic Extensions
definition
let F be Field,
E be FieldExtension of F;
attr E is F-algebraic means :defa:
for a being Element of E holds a is F-algebraic;
end;
lemlin:
for F being Field, E being F-finite FieldExtension of F
for A being finite Subset of VecSp(E,F) st card A > dim VecSp(E,F)
holds A is linearly-dependent
proof
let F be Field, E be F-finite FieldExtension of F;
let A be finite Subset of VecSp(E,F);
assume H: card A > dim VecSp(E,F);
Y: VecSp(E,F) is finite-dimensional by FIELD_4:def 8;
now assume A is linearly-independent;
then consider I being Basis of VecSp(E,F) such that
X: A c= I by VECTSP_7:19;
card I = dim VecSp(E,F) by Y,VECTSP_9:def 1;
hence contradiction by H,X,CARD_1:11,FIELD_5:3;
end;
hence thesis;
end;
registration
let F be Field;
cluster F-finite -> F-algebraic for FieldExtension of F;
coherence
proof
let E be FieldExtension of F;
assume AS: E is F-finite;
then reconsider n = deg(E,F) as Element of NAT by ORDINAL1:def 12;
H: n = dim VecSp(E,F) by FIELD_4:def 7;
now let a be Element of E;
per cases;
suppose ex i,j being Element of NAT st i < j & j <= n & a|^i = a|^j;
then consider i,j being Element of NAT such that
U: i < j & j <= n & a|^i = a|^j;
set p1 = <%0.F,1.F%>`^j, p2 = <%0.F,1.F%>`^i;
set p = p1 - p2;
now assume p = 0_.(F);
then 0.F = p.j
.= p1.j - p2.j by POLYNOM3:27
.= 1.F - p2.j by help1
.= 1.F - 0.F by U,help2;
hence contradiction;
end;
then reconsider p as non zero Polynomial of F by UPROOTS:def 5;
per cases;
suppose T: i = 0; then
W: a|^i = 1_E by BINOM:8;
Ext_eval(p,a) = Ext_eval(p1,a) - Ext_eval(p2,a) by FIELD_6:27
.= Ext_eval(p1,a) - Ext_eval(1_.(F),a) by T,POLYNOM5:15
.= Ext_eval(p1,a) - 1.E by FIELD_4:23
.= a|^j - 1.E by U,FIELD_6:22
.= 0.E by W,U,RLVECT_1:15;
hence a is F-algebraic by FIELD_6:43;
end;
suppose T: i is non zero;
Ext_eval(p,a) = Ext_eval(p1,a) - Ext_eval(p2,a) by FIELD_6:27
.= a|^j - Ext_eval(p2,a) by U,FIELD_6:22
.= a|^j - a|^i by T,FIELD_6:22
.= 0.E by U,RLVECT_1:15;
hence a is F-algebraic by FIELD_6:43;
end;
end;
suppose U: not ex i,j being Element of NAT st i < j & j <= n & a|^i = a|^j;
set M = {a|^i where i is Element of NAT : i <= n}, V = VecSp(E,F);
I: M c= the carrier of VecSp(E,F)
proof
now let o be object;
assume o in M;
then consider i being Element of NAT such that
H: o = a|^i & i <= n;
the carrier of VecSp(E,F) = the carrier of E by FIELD_4:def 6;
hence o in the carrier of VecSp(E,F) by H;
end;
hence thesis;
end;
M is finite
proof
deffunc F(Nat) = a|^($1);
defpred P[Nat] means $1 <= n;
D: {F(i) where i is Nat: i<=n & P[i]} is finite from FINSEQ_1:sch 6;
E: now let o be object;
assume o in {F(i) where i is Nat: i<=n & P[i]};
then consider i being Nat such that
E1: o = a|^i & i <= n & i <= n;
i is Element of NAT by ORDINAL1:def 12;
hence o in M by E1;
end;
now let o be object;
assume o in M; then
consider i being Element of NAT such that E1: o = a|^i & i <= n;
thus o in {F(i) where i is Nat: i<=n & P[i]} by E1;
end;
hence thesis by D,E,TARSKI:2;
end; then
reconsider M as finite Subset of VecSp(E,F) by I;
card M = n + 1
proof
set m = n + 1;
defpred P[object,object] means
ex x being Element of Seg m,
y being Element of NAT st $1 = x & y = x-1 & $2 = a|^y;
B1: for x,y1,y2 being object st x in Seg m & P[x,y1] & P[x,y2]
holds y1 = y2;
B2: now let x be object;
assume x in Seg m;
then reconsider i = x as Element of Seg m;
1 <= i by FINSEQ_1:1; then
reconsider z = i - 1 as Element of NAT by INT_1:3;
thus ex y being object st P[x,y]
proof
take a|^z;
thus thesis;
end;
end;
consider f being Function such that
C: dom f = Seg m &
for x being object st x in Seg m holds P[x,f.x]
from FUNCT_1:sch 2(B1,B2);
A1: now let o be object;
assume o in M;
then consider i being Element of NAT such that
A2: o = a|^i & i <= n;
0 + 1 <= i + 1 & i + 1 <= n+1 by A2,XREAL_1:6; then
reconsider x = i + 1 as Element of Seg m by FINSEQ_1:1;
P[x,f.x] by C;
hence o in rng f by C,A2,FUNCT_1:def 3;
end;
now let o be object;
assume o in rng f;
then consider u being object such that
A2: u in dom f & o = f.u by FUNCT_1:def 3;
P[u,f.u] by C,A2; then
consider x being Element of Seg m, y being Element of NAT such that
A3: u = x & y = x-1 & f.x = a|^y;
1 <= x & x <= m by FINSEQ_1:1; then
y < m - 1 + 1 by A3,XREAL_1:9,NAT_1:13; then
y <= n by NAT_1:13;
hence o in M by A2,A3;
end;
then A: rng f = M by A1,TARSKI:2;
now assume not f is one-to-one;
then consider x1,x2 being object such that
A1: x1 in dom f & x2 in dom f & f.x1 = f.x2 & x1 <> x2;
consider n1 being Element of Seg m,
y1 being Element of NAT such that
A2: x1 = n1 & y1 = n1-1 & f.x1 = a|^y1 by A1,C;
consider n2 being Element of Seg m,
y2 being Element of NAT such that
A3: x2 = n2 & y2 = n2-1 & f.x2 = a|^y2 by A1,C;
n1 <= m & n2 <= m by FINSEQ_1:1; then
A4: y1 < m - 1 + 1 & y2 < m - 1 + 1 by A3,A2,XREAL_1:9,NAT_1:13;
A5: y1 <> y2 by A1,A2,A3;
A6: y1 <= n & y2 <= n by A4,NAT_1:13;
per cases by A5,XXREAL_0:1;
suppose y1 < y2;
hence contradiction by U,A1,A2,A3,A6;
end;
suppose y1 > y2;
hence contradiction by U,A1,A2,A3,A6;
end;
end;
then card M = card(Seg m) by A,C,CARD_1:70 .= m by FINSEQ_1:57;
hence thesis;
end;
then card M > n by NAT_1:13;
then M is linearly-dependent by H,AS,lemlin;
then consider l being Linear_Combination of M such that
D1: Sum(l) = 0.V & Carrier(l) <> {} by VECTSP_7:def 1;
set z = the Element of Carrier(l);
consider v being Element of V such that
D2: z = v & l.v <> 0.F by D1,VECTSP_6:1;
Carrier(l) c= M by VECTSP_6:def 4; then
z in M by D1; then
consider i being Element of NAT such that
D3: z = a|^i & i <= n;
consider pM being Polynomial of F such that
D4a: deg pM <= n &
for i being Element of NAT st i <= n holds pM.i = l.(a|^i)
by FIELD_6:47;
pM.i <> 0.F by D3,D2,D4a;
then pM <> 0_.(F); then
reconsider pM as non zero Polynomial of F by UPROOTS:def 5;
Ext_eval(pM,a) = 0.V by U,D1,D4a,FIELD_6:49 .= 0.E by FIELD_4:def 6;
hence a is F-algebraic by FIELD_6:43;
end;
end;
hence thesis;
end;
end;
registration
let F be Field;
let E be F-algebraic FieldExtension of F;
cluster -> F-algebraic for Element of E;
coherence by defa;
end;
theorem
for F being Field
for E being FieldExtension of F
holds E is F-algebraic iff
for a being Element of E holds FAdj(F,{a}) is F-finite
proof
let F be Field, E be FieldExtension of F;
now assume A: for a being Element of E holds FAdj(F,{a}) is F-finite;
now let a be Element of E;
FAdj(F,{a}) is F-finite by A;
hence a is F-algebraic by FIELD_6:68;
end;
hence E is F-algebraic;
end;
hence thesis;
end;
theorem alg1:
for F being Field,
E being FieldExtension of F
for a being Element of E
holds a is F-algebraic iff
ex B being F-finite FieldExtension of F st E is B-extending & a in B
proof
let F be Field, E be FieldExtension of F; let a be Element of E;
A: now assume A0: a is F-algebraic;
A1: {a} is Subset of FAdj(F,{a}) by FIELD_6:35;
FAdj(F,{a}) is Subring of E by FIELD_5:12; then
A2: E is FAdj(F,{a})-extending by FIELD_4:def 1;
a in {a} by TARSKI:def 1;
then a in FAdj(F,{a}) by A1;
hence ex B being F-finite FieldExtension of F
st E is B-extending & a in B by A0,A2;
end;
now assume ex B being F-finite FieldExtension of F
st E is B-extending & a in B; then
consider B being F-finite FieldExtension of F such that
A0: E is B-extending & a in B;
reconsider E1 = E as B-extending FieldExtension of F by A0;
reconsider a1 = a as B-membered Element of E1 by A0,defmem;
@(@(B,a1),E1) is F-algebraic;
hence a is F-algebraic;
end;
hence thesis by A;
end;
definition
let F be Field;
let E be FieldExtension of F;
let T be Subset of E;
attr T is F-algebraic means :defTalg:
for a being Element of E st a in T holds a is F-algebraic;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster finite F-algebraic for Subset of E;
existence
proof
{} c= the carrier of E; then
reconsider T = {} as Subset of the carrier of E;
take T;
thus thesis;
end;
end;
theorem ug:
for F being Field,
E being FieldExtension of F
for b being Element of E, T being Subset of E
for E1 being FieldExtension of FAdj(F,T), b1 being Element of E1
st E1 = E & b1 = b holds FAdj(F,{b}\/T) = FAdj(FAdj(F,T),{b1})
proof
let F be Field, E be FieldExtension of F;
let b be Element of E, T be Subset of E;
let E1 be FieldExtension of FAdj(F,T), b1 be Element of E1;
assume AS: E1 = E & b1 = b;
A1: F is Subfield of FAdj(FAdj(F,T),{b1}) by FIELD_4:7;
{b} \/ T c= the carrier of FAdj(FAdj(F,T),{b1})
proof
now let o be object;
assume o in {b} \/ T; then
per cases by XBOOLE_0:def 3;
suppose o in {b}; then
B1: o = b by TARSKI:def 1;
B2: {b1} is Subset of FAdj(FAdj(F,T),{b1}) by FIELD_6:35;
b in {b1} by AS,TARSKI:def 1;
hence o in the carrier of FAdj(FAdj(F,T),{b1}) by B1,B2;
end;
suppose B1: o in T;
B2: T is Subset of FAdj(F,T) by FIELD_6:35;
FAdj(F,T) is Subfield of FAdj(FAdj(F,T),{b1}) by FIELD_6:36; then
the carrier of FAdj(F,T) c= the carrier of FAdj(FAdj(F,T),{b1})
by EC_PF_1:def 1;
hence o in the carrier of FAdj(FAdj(F,T),{b1}) by B2,B1;
end;
end;
hence thesis;
end; then
A: FAdj(F,{b}\/T) is Subfield of FAdj(FAdj(F,T),{b1}) by AS,A1,FIELD_6:37;
A1: FAdj(F,T) is Subfield of FAdj(F,{b}\/T) by ext0,XBOOLE_1:7;
{b}\/T is Subset of FAdj(F,{b}\/T) by FIELD_6:35; then
{b1} c= the carrier of FAdj(F,{b}\/T) by AS,XBOOLE_1:11; then
FAdj(FAdj(F,T),{b1}) is Subfield of FAdj(F,{b}\/T) by A1,AS,FIELD_6:37;
hence thesis by A,EC_PF_1:4;
end;
theorem ug1:
for F being Field,
E being FieldExtension of F
for b being Element of E, T being Subset of E
for E1 being FieldExtension of FAdj(F,{b}), T1 being Subset of E1
st E1 = E & T1 = T holds FAdj(F,{b}\/T) = FAdj(FAdj(F,{b}),T1)
proof
let F be Field, E be FieldExtension of F;
let b be Element of E, T be Subset of E;
let E1 be FieldExtension of FAdj(F,{b}), T1 be Subset of E1;
assume AS: E1 = E & T1 = T;
A1: F is Subfield of FAdj(FAdj(F,{b}),T1) by FIELD_4:7;
{b} \/ T c= the carrier of FAdj(FAdj(F,{b}),T1)
proof
now let o be object;
assume o in {b} \/ T; then
per cases by XBOOLE_0:def 3;
suppose B1: o in {b};
{b} is Subset of FAdj(FAdj(F,{b}),T1)
proof
now let o be object;
assume B3: o in {b};
B4: {b} is Subset of FAdj(F,{b}) by FIELD_6:35;
FAdj(F,{b}) is Subfield of FAdj(FAdj(F,{b}),T1) by FIELD_6:36;
then the carrier of FAdj(F,{b}) c=
the carrier of FAdj(FAdj(F,{b}),T1) by EC_PF_1:def 1;
hence o in the carrier of FAdj(FAdj(F,{b}),T1) by B3,B4;
end;
hence thesis by TARSKI:def 3;
end;
hence o in the carrier of FAdj(FAdj(F,{b}),T1) by B1;
end;
suppose B1: o in T;
T is Subset of FAdj(FAdj(F,{b}),T1) by AS,FIELD_6:35;
hence o in the carrier of FAdj(FAdj(F,{b}),T1) by B1;
end;
end;
hence thesis;
end; then
A: FAdj(F,{b}\/T) is Subfield of FAdj(FAdj(F,{b}),T1) by AS,A1,FIELD_6:37;
A1: FAdj(F,{b}) is Subfield of FAdj(F,{b}\/T) by ext0,XBOOLE_1:7;
{b}\/T is Subset of FAdj(F,{b}\/T) by FIELD_6:35; then
T1 c= the carrier of FAdj(F,{b}\/T) by AS,XBOOLE_1:11; then
FAdj(FAdj(F,{b}),T1) is Subfield of FAdj(F,{b}\/T) by A1,AS,FIELD_6:37;
hence thesis by A,EC_PF_1:4;
end;
registration
let F be Field;
let E be FieldExtension of F;
let T be finite F-algebraic Subset of E;
cluster FAdj(F,T) -> F-finite;
coherence
proof
defpred P[Nat] means
for T being finite F-algebraic Subset of E
st card T = $1 holds FAdj(F,T) is F-finite;
X: F is Subring of E by FIELD_4:def 1;
IA: P[0]
proof
let T be finite F-algebraic Subset of E;
assume card T = 0; 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 P = the carrier of E1
proof
C1: now let o be object;
assume o in the carrier of P; then
o in carrierFA(T) by FIELD_6:def 6; then
consider a being Element of E such that
C2: o = a & for U being Subfield of E
st F is Subfield of U & T is Subset of U holds a in U by Y;
F is Subfield of E & F is Subfield of F & T is Subset of F
by FIELD_4:7,FIELD_4:1,AS,XBOOLE_1:2; then
a in F by C2;
hence o in the carrier of E1 by C2;
end;
now let o be object;
assume C3: o in the carrier of F;
F is Subfield of P by FIELD_6:36; then
the carrier of F c= the carrier of P by EC_PF_1:def 1;
hence o in the carrier of P by C3;
end;
hence thesis by C1,TARSKI:2;
end;
B2: 1.P = 1.E by FIELD_6:def 6 .= 1.F by X,C0SP1:def 3;
B4: the addF of P = (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 P = (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,P by A1;
reconsider P as E1-homomorphic FieldExtension of F;
h is additive multiplicative unity-preserving by B4,B5,B2; then
reconsider 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;
end;
IS: now let k be Nat;
assume IV: P[k];
now let T be finite F-algebraic Subset of E;
assume AS: card T = k + 1;
set a = the Element of T;
I: T <> {} by AS; then
H: a in T; then
reconsider a as Element of E;
set T1 = T \ {a};
now let b be Element of E;
assume b in T1;
then b in T & not b in {a} by XBOOLE_0:def 5;
hence b is F-algebraic by defTalg;
end; then
T1 is F-algebraic; then
reconsider T1 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;
now assume a in T1;
then a in T & not a in {a} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end; 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 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 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;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
consider n being Nat such that H: card T = n;
thus thesis by I,H;
end;
end;
theorem ft1:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
holds E == FAdj(F,{a}) iff deg MinPoly(a,F) = deg(E,F)
proof
let F be Field, E be FieldExtension of F;
let a be F-algebraic Element of E;
A: now assume A0: E == FAdj(F,{a});
deg(FAdj(F,{a}),F) = deg MinPoly(a,F) by FIELD_6:67;
hence deg MinPoly(a,F) = deg(E,F) by A0,str11;
end;
now assume B0: deg MinPoly(a,F) = deg(E,F);
reconsider Fa = FAdj(F,{a}) as FieldExtension of F;
reconsider E1 = E as Fa-extending FieldExtension of F by FIELD_4:7;
VecSp(E1,F) is finite-dimensional by B0,FIELD_4:def 7; then
E1 is F-finite by FIELD_4:def 8; then
reconsider E1 = E as
F-extending FAdj(F,{a})-finite FieldExtension of FAdj(F,{a}) by alg0;
reconsider d1 = deg(E,F) as non zero Nat by B0;
deg(E,F) = deg(E1,FAdj(F,{a})) * deg(FAdj(F,{a}),F) by degmult
.= deg(E1,FAdj(F,{a})) * deg(E,F) by B0,FIELD_6:67;
:: then deg(E1,FAdj(F,{a})) = 1 by XCMPLX_1:7;
hence E == FAdj(F,{a}) by str1a,XCMPLX_1:7;
end;
hence thesis by A;
end;
theorem
for F being Field,
E being FieldExtension of F
holds E is F-finite iff
ex T being finite F-algebraic Subset of E st E == FAdj(F,T)
proof
let F be Field, E be FieldExtension of F;
defpred P[Nat] means
for F being Field
for E being FieldExtension of F st deg(E,F) = $1
ex T being finite F-algebraic Subset of E st E == FAdj(F,T);
IA: now let F be Field, E be FieldExtension of F;
assume deg(E,F) = 1;
then A: F == E by str1a;
{} c= the carrier of E; then
reconsider T = {} as finite Subset of E;
T is F-algebraic; then
reconsider T as finite F-algebraic Subset of E;
{} c= the carrier of F;
then FAdj(F,T) == F by Th1;
then E == FAdj(F,T) by A;
hence ex T being finite F-algebraic Subset of E st E == FAdj(F,T);
end;
IS: now let k be Nat;
assume AS: k >= 1 & (for n being Nat st n >= 1 & n < k holds P[n]);
now let F be Field, E be FieldExtension of F;
assume Z: deg(E,F) = k; then
VecSp(E,F) is finite-dimensional by FIELD_4:def 7; then
reconsider K = E as F-finite FieldExtension of F by FIELD_4:def 8;
per cases by AS,XXREAL_0:1;
suppose k = 1; hence
ex T being finite F-algebraic Subset of E st E == FAdj(F,T) by Z,IA;
end;
suppose B0: k > 1;
now assume B1: not ex a being Element of K st not a in the carrier of F;
for o be object holds o in the carrier of E iff o in the carrier of F
proof
let o be object;
now assume B: o in the carrier of F;
F is Subfield of E by FIELD_4:7; then
the carrier of F c= the carrier of E by EC_PF_1:def 1;
hence o in the carrier of E by B;
end;
hence thesis by B1;
end;
hence contradiction by Z,B0,quah1,TARSKI:2;
end; then
consider a being Element of K such that C1: not a in the carrier of F;
set p = MinPoly(a,F);
C2: {a} is F-algebraic;
C3: deg(FAdj(F,{a}),F) <= k & deg(FAdj(F,{a}),F) > 1
proof
K is FAdj(F,{a})-extending by FIELD_4:7;
hence deg(FAdj(F,{a}),F) <= k by Z,FIELD_5:15;
C5: {a} is Subset of the carrier of FAdj(F,{a}) by FIELD_6:35;
a in {a} by TARSKI:def 1; then
C6: a in the carrier of FAdj(F,{a}) by C5;
deg(FAdj(F,{a}),F) + 1 > 0 + 1 by XREAL_1:6;
then deg(FAdj(F,{a}),F) >= 1 by NAT_1:13;
hence deg(FAdj(F,{a}),F) > 1 by C6,C1,quah1,XXREAL_0:1;
end;
deg p = deg(FAdj(F,{a}),F) by FIELD_6:67; then
per cases by C3,XXREAL_0:1;
suppose deg p = k;
then K == FAdj(F,{a}) by Z,ft1;
hence ex T being finite F-algebraic Subset of E st E == FAdj(F,T)
by C2;
end;
suppose deg p < k;
set K = FAdj(F,{a});
reconsider E1 = E as K-finite F-extending FieldExtension of K
by alg0,FIELD_4:7;
reconsider j = deg(E1,K) as Element of NAT by ORDINAL1:def 12;
j >= 1 & j < k
proof
j + 1 > 0 + 1 by XREAL_1:6;
hence j >= 1 by NAT_1:13;
D7: k = deg(E1,K) * deg(K,F) by Z,degmult;
D6: j <= k by D7,NAT_1:24;
now assume j = k;
then k / k = (k * deg(K,F)) / k by Z,degmult
.= (k / k) * deg(K,F);
then k / k = 1 * deg(K,F) by B0,XCMPLX_1:60;
hence contradiction by C3,XCMPLX_1:60;
end;
hence j < k by D6,XXREAL_0:1;
end; then
consider T1 being finite K-algebraic Subset of E1 such that
D3: E1 == FAdj(K,T1) by AS;
reconsider T = T1 as Subset of E;
reconsider a1 = a as Element of E;
for b being Element of E1 st b in T \/ {a} holds b is F-algebraic;
then
reconsider T2 = {a1} \/ T as F-algebraic Subset of E by defTalg;
FAdj(K,T1) = FAdj(F,T2) by ug1;
hence ex T being finite F-algebraic Subset of E st E == FAdj(F,T)
by D3;
end;
end;
end;
hence P[k];
end;
I: for k being Nat st k >= 1 holds P[k] from NAT_1:sch 9(IS);
A: now assume E is F-finite;
then reconsider k = deg(E,F) as Element of NAT by ORDINAL1:def 12;
k >= 0 + 1 by NAT_1:13;
hence ex T being finite F-algebraic Subset of E st E == FAdj(F,T) by I;
end;
now assume ex T being finite F-algebraic Subset of E st E == FAdj(F,T);
then consider T being finite F-algebraic Subset of E such that
B0: E == FAdj(F,T);
VecSp(FAdj(F,T),F) is finite-dimensional by FIELD_4:def 8;
then VecSp(E,F) is finite-dimensional by B0,str12;
hence E is F-finite by FIELD_4:def 8;
end;
hence thesis by A;
end;
registration
let F be Field;
let E be FieldExtension of F;
let p be non zero Element of the carrier of Polynom-Ring F;
cluster Roots(E,p) -> F-algebraic;
coherence
proof
now let a be Element of E;
assume a in Roots(E,p); then
a in {a where a is Element of E : a is_a_root_of p,E} by FIELD_4:def 4; then
consider b being Element of E such that
A: b = a & b is_a_root_of p,E;
Ext_eval(p,a) = 0.E by A,FIELD_4:def 2;
hence a is F-algebraic by FIELD_6:43;
end;
hence thesis;
end;
end;
theorem
for F being Field,
E being FieldExtension of F
for p being non zero Element of the carrier of Polynom-Ring F
holds FAdj(F,Roots(E,p)) is F-algebraic;
theorem
for F being Field
for E being FieldExtension of F
for K being E-extending FieldExtension of F
st K is E-algebraic & E is F-algebraic holds K is F-algebraic
proof
let F be Field, E be FieldExtension of F;
let K be E-extending FieldExtension of F;
assume AS: K is E-algebraic & E is F-algebraic;
now let a be Element of K;
consider p being non zero Polynomial of E such that
A: Ext_eval(p,a) = 0.K by AS,FIELD_6:43;
reconsider T = Coeff p as finite Subset of E;
T is F-algebraic by AS; then
reconsider T as finite F-algebraic Subset of E;
set B = FAdj(F,T);
E is FieldExtension of B by FIELD_4:7; then
reconsider K1 = K as FieldExtension of B;
E: K1 is B-extending & E is B-extending by FIELD_4:7;
reconsider a1 = a as Element of K1;
T is Subset of B by FIELD_6:35; then
reconsider p1 = p as non zero Polynomial of B by E,cof2;
p1 is Element of the carrier of Polynom-Ring B &
p is Element of the carrier of Polynom-Ring E by POLYNOM3:def 10; then
Ext_eval(p1,a) = 0.K by A,E,lemma7b; then
reconsider a1 = a as B-algebraic Element of K1 by FIELD_6:43;
reconsider B1 = FAdj(B,{a1}) as FieldExtension of F;
F: {a} is Subset of FAdj(B,{a1}) by FIELD_6:35;
G: K is B1-extending by FIELD_4:7;
a in {a} by TARSKI:def 1;
then a in FAdj(B,{a1}) by F;
hence a is F-algebraic by G,alg1;
end;
hence thesis;
end;
theorem
for F being Field
for E being FieldExtension of F
for K being E-extending FieldExtension of F
st K is F-algebraic holds K is E-algebraic & E is F-algebraic
proof
let F be Field, E be FieldExtension of F, K be E-extending FieldExtension of F;
H0: E is Subring of K & F is Subring of E by FIELD_4:def 1; then
H1: 0.K = 0.E by C0SP1:def 3;
assume AS: K is F-algebraic;
now let a be Element of K;
consider p being non zero Polynomial of F such that
A: Ext_eval(p,a) = 0.K by AS,FIELD_6:43;
reconsider p1 = p as Polynomial of E by H0,FIELD_4:9;
0_.(E) = 0_.(F) & p <> 0_.(F) by FIELD_4:12; then
reconsider p1 as non zero Polynomial of E by UPROOTS:def 5;
p is Element of the carrier of Polynom-Ring F &
p1 is Element of the carrier of Polynom-Ring E by POLYNOM3:def 10; then
Ext_eval(p1,a) = Ext_eval(p,a) by lemma7b .= 0.E by A,H0,C0SP1:def 3;
hence a is E-algebraic by H1,FIELD_6:43;
end;
hence K is E-algebraic;
now let a be Element of E;
:: @(a,K) is F-algebraic by AS; then
consider p being non zero Polynomial of F such that
A: Ext_eval(p,@(a,K)) = 0.K by AS,FIELD_6:43;
p is Element of the carrier of Polynom-Ring F by POLYNOM3:def 10; then
Ext_eval(p,a) = Ext_eval(p,@(a,K)) by FIELD_6:11 .= 0.E by A,H0,C0SP1:def 3;
hence a is F-algebraic by FIELD_6:43;
end;
hence thesis;
end;
begin :: The Field of Algebraic Elements
registration
let F be Field;
let E be FieldExtension of F;
let a,b be F-algebraic Element of E;
cluster FAdj(F,{a,b}) -> F-finite;
coherence
proof
now let o be Element of E;
assume o in {a,b};
then per cases by TARSKI:def 2;
suppose o = a;
hence o is F-algebraic;
end;
suppose o = b;
hence o is F-algebraic;
end;
end;
then {a,b} is F-algebraic;
hence thesis;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
cluster 0.E -> F-algebraic;
coherence
proof
A: F is Subring of E by FIELD_4:def 1;
then 0.E = 0.F by C0SP1:def 3;
then In(0.E,E) is_integral_over F by A,ALGNUM_1:23;
hence thesis by FIELD_6:42;
end;
cluster 1.E -> F-algebraic;
coherence
proof
A: F is Subring of E by FIELD_4:def 1;
then 1.E = 1.F by C0SP1:def 3;
then In(1.E,E) is_integral_over F by A,ALGNUM_1:23;
hence thesis by FIELD_6:42;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
let a,b be F-algebraic Element of E;
cluster a + b -> F-algebraic;
coherence
proof
A: FAdj(F,{a,b}) is Subring of E by FIELD_5:12; then
reconsider E1 = E as F-extending FieldExtension of FAdj(F,{a,b})
by FIELD_4:def 1;
B: {a,b} is Subset of FAdj(F,{a,b}) by FIELD_6:35;
a in {a,b} by TARSKI:def 2;
then reconsider a1 = a as Element of the carrier of FAdj(F,{a,b}) by B;
b in {a,b} by TARSKI:def 2;
then reconsider b1 = b as Element of the carrier of FAdj(F,{a,b}) by B;
a + b = a1 + b1 by A,FIELD_6:15;
then reconsider c = a + b as FAdj(F,{a,b})-membered Element of E1 by defmem;
@(@(FAdj(F,{a,b}),c),E1) is F-algebraic;
hence thesis;
end;
cluster a - b -> F-algebraic;
coherence
proof
A: FAdj(F,{a,b}) is Subring of E by FIELD_5:12; then
reconsider E1 = E as F-extending FieldExtension of FAdj(F,{a,b})
by FIELD_4:def 1;
B: {a,b} is Subset of FAdj(F,{a,b}) by FIELD_6:35;
a in {a,b} by TARSKI:def 2;
then reconsider a1 = a as Element of the carrier of FAdj(F,{a,b}) by B;
b in {a,b} by TARSKI:def 2;
then reconsider b1 = b as Element of the carrier of FAdj(F,{a,b}) by B;
- b = - b1 by A,FIELD_6:17; then
a + (-b) = a1 + (-b1) by A,FIELD_6:15;
then reconsider c = a - b as FAdj(F,{a,b})-membered Element of E1 by defmem;
@(@(FAdj(F,{a,b}),c),E1) is F-algebraic;
hence thesis;
end;
cluster a * b -> F-algebraic;
coherence
proof
A: FAdj(F,{a,b}) is Subring of E by FIELD_5:12; then
reconsider E1 = E as F-extending FieldExtension of FAdj(F,{a,b})
by FIELD_4:def 1;
B: {a,b} is Subset of FAdj(F,{a,b}) by FIELD_6:35;
a in {a,b} by TARSKI:def 2;
then reconsider a1 = a as Element of the carrier of FAdj(F,{a,b}) by B;
b in {a,b} by TARSKI:def 2;
then reconsider b1 = b as Element of the carrier of FAdj(F,{a,b}) by B;
a * b = a1 * b1 by A,FIELD_6:16;
then reconsider c = a * b as FAdj(F,{a,b})-membered Element of E1 by defmem;
@(@(FAdj(F,{a,b}),c),E1) is F-algebraic;
hence thesis;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
let a be F-algebraic Element of E;
cluster -a -> F-algebraic;
coherence
proof
A: FAdj(F,{a}) is Subring of E by FIELD_5:12; then
reconsider E1 = E as F-extending FieldExtension of FAdj(F,{a})
by FIELD_4:def 1;
B: {a} is Subset of FAdj(F,{a}) by FIELD_6:35;
a in {a} by TARSKI:def 1;
then reconsider a1 = a as Element of the carrier of FAdj(F,{a}) by B;
-a = -a1 by A,FIELD_6:17;
then reconsider c = -a as FAdj(F,{a})-membered Element of E1 by defmem;
@(@(FAdj(F,{a}),c),E1) is F-algebraic;
hence thesis;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
let a be non zero F-algebraic Element of E;
cluster a" -> F-algebraic;
coherence
proof
FAdj(F,{a}) is Subring of E by FIELD_5:12; then
reconsider E1 = E as F-extending FieldExtension of FAdj(F,{a})
by FIELD_4:def 1;
B: {a} is Subset of FAdj(F,{a}) by FIELD_6:35;
a in {a} by TARSKI:def 1;
then reconsider a1 = a as Element of the carrier of FAdj(F,{a}) by B;
a" = a1" by FIELD_6:18;
then reconsider c = a" as FAdj(F,{a})-membered Element of E1 by defmem;
@(@(FAdj(F,{a}),c),E1) is F-algebraic;
hence thesis;
end;
end;
definition
let F be Field,
E be FieldExtension of F;
func Alg_El E -> Subset of E equals
the set of all a where a is F-algebraic Element of E;
coherence
proof
now let o be object;
assume o in the set of all a where a is F-algebraic Element of E;
then consider a being F-algebraic Element of E such that A: a = o;
thus o in the carrier of E by A;
end;
hence thesis by TARSKI:def 3;
end;
end;
definition
let F be Field,
E be FieldExtension of F;
func Field_of_Algebraic_Elements E -> strict doubleLoopStr means :d:
the carrier of it = Alg_El E &
the addF of it = (the addF of E)||the carrier of it &
the multF of it = (the multF of E)||the carrier of it &
the OneF of it = 1.E &
the ZeroF of it = 0.E;
existence
proof
set C = Alg_El E;
set f = the addF of E;
C is Preserv of f
proof
now let x be set;
assume x in [:C,C:];
then consider x1,x2 being object such that
A1: x1 in C and
A2: x2 in C and
A3: x = [x1,x2] by ZFMISC_1:def 2;
consider a1 being F-algebraic Element of E such that
A4: a1 = x1 by A1;
consider a2 being F-algebraic Element of E such that
A5: a2 = x2 by A2;
a1 + a2 = f.(a1,a2);
hence f.x in C by A4,A5,A3;
end;
hence thesis by REALSET1:def 1;
end;
then reconsider C as Preserv of the addF of E;
set f = the multF of E;
now let x be set;
assume x in [:C,C:];
then consider x1,x2 being object such that
A1: x1 in C and
A2: x2 in C and
A3: x = [x1,x2] by ZFMISC_1:def 2;
consider a1 being F-algebraic Element of E such that
A4: a1 = x1 by A1;
consider a2 being F-algebraic Element of E such that
A5: a2 = x2 by A2;
a1 * a2 = f.(a1,a2);
hence f.x in C by A4,A5,A3;
end;
then C is f-binopclosed; then
reconsider m = (the multF of E)||C as BinOp of C by REALSET1:2;
1.E in C & 0.E in C; then
reconsider o = 1.E, z = 0.E as Element of C;
take doubleLoopStr (# C,(the addF of E)||C,m,o,z #);
thus thesis;
end;
uniqueness;
end;
notation
let F be Field,
E be FieldExtension of F;
synonym F_Alg E for Field_of_Algebraic_Elements E;
end;
registration
let F be Field,
E be FieldExtension of F;
cluster F_Alg E -> non degenerated;
coherence
proof
set FE = F_Alg E;
0.FE = 0.E & 1.FE = 1.E by d;
hence 0.FE <> 1.FE;
end;
end;
Lm10:
for R be Field, E be FieldExtension of R
for x being Element of F_Alg E holds x is Element of E
proof
let R be Field, E be FieldExtension of R; let x be Element of F_Alg E;
A1: the carrier of F_Alg E = Alg_El E by d;
x in the carrier of F_Alg E;
hence thesis by A1;
end;
Lm11:
for R be Field, E be FieldExtension of R
for a,b being Element of E
for x,y being Element of F_Alg E st a = x & b = y holds a+b = x+y
proof
let R be Field, E be FieldExtension of R; let a,b being Element of E;
let x,y be Element of F_Alg E such that
A1: a = x & b = y;
A2: the carrier of F_Alg E = Alg_El E by d;
hence a+b = (the addF of E)||(Alg_El E).(x,y) by A1,RING_3:1
.= x+y by d,A2;
end;
Lm12:
for R be Field, S be FieldExtension of R
for a,b being Element of S
for x,y being Element of F_Alg S st a = x & b = y holds a*b = x*y
proof
let R be Field, S be FieldExtension of R;
let a,b be Element of S;
let x,y be Element of F_Alg S;
assume a = x & b = y;
hence a*b
= (the multF of S)||(the carrier of (F_Alg S)).(x,y) by RING_3:1
.= x*y by d;
end;
registration
let F be Field,
E be FieldExtension of F;
cluster F_Alg E -> Abelian add-associative right_zeroed right_complementable;
coherence
proof
set FE = F_Alg E;
A1: 0.FE = 0.E by d;
A2: the carrier of FE = Alg_El E by d;
hereby
let x,y be Element of FE;
reconsider a = x, b = y as Element of E by Lm10;
thus x+y = a+b by Lm11
.= y+x by Lm11;
end;
hereby
let x,y,z be Element of FE;
reconsider a = x, b = y, c = z as Element of E by Lm10;
A3: y+z = b+c by Lm11;
x+y = a+b by Lm11;
hence x+y+z = a+b+c by Lm11
.= a+(b+c) by RLVECT_1:def 3
.= x+(y+z) by A3,Lm11;
end;
hereby
let x be Element of FE;
reconsider a = x as Element of E by Lm10;
thus x+0.FE = a+0.E by A1,Lm11
.= x;
end;
let x be Element of FE;
x in Alg_El E by A2; then
consider a being F-algebraic Element of E such that H: a = x;
x in Alg_El E by A2;
then consider x1 being Element of E such that
A4: x = x1;
-a in Alg_El E;
then reconsider y = -x1 as Element of FE by H,A4,d;
take y;
thus x+y = a+-x1 by H,Lm11 .= 0.FE by A1,A4,H,RLVECT_1:5;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
cluster F_Alg E-> commutative associative well-unital distributive
almost_left_invertible;
coherence
proof
set P = F_Alg E;
A1: 1.P = 1.E by d;
A2: 0.P = 0.E by d;
now let x,y be Element of P;
reconsider a = x, b = y as Element of E by Lm10;
thus x*y = a*b by Lm12 .= b*a by GROUP_1:def 12 .= y*x by Lm12;
end;
hence P is commutative;
now let x,y,z be Element of P;
reconsider a = x, b = y, c = z as Element of E by Lm10;
A3: y*z = b*c by Lm12;
x*y = a*b by Lm12;
hence (x*y)*z = (a*b)*c by Lm12
.= a*(b*c) by GROUP_1:def 3
.= x*(y*z) by A3,Lm12;
end;
hence P is associative;
now let x be Element of P;
reconsider a = x as Element of E by Lm10;
thus x * 1.P = a * 1.E by A1,Lm12
.= x;
thus 1.P * x = 1.E * a by A1,Lm12
.= x;
end;
hence P is well-unital;
now let x,y,z be Element of P;
reconsider a = x, b = y, c = z as Element of E by Lm10;
A4: a*b = x*y & a*c = x*z by Lm12;
A6: b*a = y*x & c*a = z*x by Lm12;
A5: y+z = b+c by Lm11;
hence x*(y+z) = a*(b+c) by Lm12
.= a*b+a*c by VECTSP_1:def 7
.= x*y+x*z by A4,Lm11;
thus (y+z)*x = (b+c)*a by A5,Lm12
.= b*a+c*a by VECTSP_1:def 7
.= y*x+z*x by A6,Lm11;
end;
hence P is distributive;
now let x be Element of P such that
A5: x <> 0.P;
reconsider a = x as Element of E by Lm10;
the carrier of P = Alg_El E by d;
then x in Alg_El E;
then consider x1 being F-algebraic Element of E such that
A6: x = x1;
x1 is non zero by d,A5,A6;
then x1" in Alg_El E;
then reconsider y = x1" as Element of P by d;
take y;
thus y*x = x1"*a by Lm12
.= 1.P by A1,A2,A5,A6,VECTSP_1:def 10;
end;
hence thesis;
end;
end;
ee:
for F being Field,
E being FieldExtension of F holds E is FieldExtension of (F_Alg E)
proof
let F be Field, E be FieldExtension of F;
set FE = F_Alg E;
H: the carrier of FE = Alg_El E by d
.= the set of all a where a is F-algebraic Element of E;
A: the carrier of FE c= the carrier of E
proof
now let o be object;
assume o in the carrier of FE;
then consider a being F-algebraic Element of E such that B: a = o by H;
thus o in the carrier of E by B;
end;
hence thesis;
end;
the addF of FE = (the addF of E)||the carrier of FE
& the multF of FE = (the multF of E)||the carrier of FE
& 1.FE = 1.E & 0.FE = 0.E by d;
then (F_Alg E) is Subring of E by A,C0SP1:def 3;
hence thesis by FIELD_4:def 1;
end;
registration
let F be Field,
E be FieldExtension of F;
cluster F_Alg E -> F-extending;
coherence
proof
set FE = F_Alg E;
H1: the carrier of FE = Alg_El E by d
.= the set of all a where a is F-algebraic Element of E;
H2: F is Subring of E by FIELD_4:def 1;
A: the carrier of F c= the carrier of FE
proof
now let o be object;
assume o in the carrier of F;
then reconsider a = o as Element of F;
@(a,E) is F-algebraic;
hence o in the carrier of FE by H1;
end;
hence thesis;
end;
then Y: [:the carrier of F,the carrier of F:] c=
[:the carrier of FE,the carrier of FE:] by ZFMISC_1:96;
B: (the addF of FE)||the carrier of F
= ((the addF of E)||the carrier of FE)||the carrier of F by d
.= (the addF of E)||the carrier of F by Y,FUNCT_1:51
.= the addF of F by H2,C0SP1:def 3;
C: (the multF of FE)||the carrier of F
= ((the multF of E)||the carrier of FE)||the carrier of F by d
.= (the multF of E)||the carrier of F by Y,FUNCT_1:51
.= the multF of F by H2,C0SP1:def 3;
D: 1.FE = 1.E by d .= 1.F by H2,C0SP1:def 3;
0.FE = 0.E by d .= 0.F by H2,C0SP1:def 3;
then F is Subring of FE by A,B,C,D,C0SP1:def 3;
hence thesis by FIELD_4:def 1;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
cluster F_Alg E -> F-algebraic;
coherence
proof
now let a be Element of F_Alg E;
the carrier of (F_Alg E) = Alg_El E by d
.= the set of all x where x is F-algebraic Element of E; then
a in the set of all x where x is F-algebraic Element of E; then
consider a1 being F-algebraic Element of E such that
A: a1 = a;
consider p being non zero Polynomial of F such that
B: Ext_eval(p,a1) = 0.E by FIELD_6:43;
reconsider p as Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
E is (F_Alg E)-extending by ee; then
Ext_eval(p,a) = 0.E by A,B,lemma7a .= 0.(F_Alg E) by d;
hence a is F-algebraic by FIELD_6:43;
end;
hence thesis;
end;
end;
theorem
for F being Field
for E being FieldExtension of F holds F_Alg E is FieldExtension of F;
theorem
for F being Field
for E being FieldExtension of F holds E is FieldExtension of F_Alg E by ee;
t2:
for F being Field
for E being F-algebraic FieldExtension of F
holds F_Alg E is FieldExtension of E
proof
let F be Field, E be F-algebraic FieldExtension of F;
set FE = F_Alg E;
H1: the carrier of FE = Alg_El E by d
.= the set of all a where a is F-algebraic Element of E;
A: the carrier of E c= the carrier of FE by H1; then
H3: [:the carrier of E,the carrier of E:] c=
[:the carrier of FE,the carrier of FE:] by ZFMISC_1:96;
B: (the addF of FE)||the carrier of E
= ((the addF of E)||the carrier of FE)||the carrier of E by d
.= (the addF of E)||the carrier of E by H3,FUNCT_1:51;
C: (the multF of FE)||the carrier of E
= ((the multF of E)||the carrier of FE)||the carrier of E by d
.= (the multF of E)||the carrier of E by H3,FUNCT_1:51;
D: 1.FE = 1.E by d;
0.FE = 0.E by d;
then E is Subring of FE by A,B,C,D,C0SP1:def 3;
hence thesis by FIELD_4:def 1;
end;
theorem
for F being Field
for E being FieldExtension of F
for K being FieldExtension of E holds F_Alg K is FieldExtension of F_Alg E
proof
let F be Field, E be FieldExtension of F, K be FieldExtension of E;
set FE = F_Alg E, FK = F_Alg K;
H0: F is Subring of E & E is Subring of K by FIELD_4:def 1;
H1: the carrier of FE = Alg_El E by d
.= the set of all a where a is F-algebraic Element of E;
H5: the carrier of FK = Alg_El K by d
.= the set of all a where a is E-algebraic Element of K;
the carrier of FE c= the carrier of E
proof
now let o be object;
assume o in the carrier of FE;
then consider a being F-algebraic Element of E such that B: a = o by H1;
thus o in the carrier of E by B;
end;
hence thesis;
end; then
H4: [:the carrier of FE,the carrier of FE:] c=
[:the carrier of E,the carrier of E:] by ZFMISC_1:96;
now let o be object;
assume o in the carrier of FE; then
consider a being F-algebraic Element of E such that B: a = o by H1;
@(a,K) is E-algebraic;
hence o in the carrier of FK by B,H5;
end; then
A: the carrier of FE c= the carrier of FK; then
H3: [:the carrier of FE,the carrier of FE:] c=
[:the carrier of FK,the carrier of FK:] by ZFMISC_1:96;
B: (the addF of FK)||the carrier of FE
= ((the addF of K)||the carrier of FK)||the carrier of FE by d
.= (the addF of K)||the carrier of FE by H3,FUNCT_1:51
.= ((the addF of K)||the carrier of E)||the carrier of FE by H4,FUNCT_1:51
.= (the addF of E)||the carrier of FE by H0,C0SP1:def 3
.= the addF of FE by d;
C: (the multF of FK)||the carrier of FE
= ((the multF of K)||the carrier of FK)||the carrier of FE by d
.= (the multF of K)||the carrier of FE by H3,FUNCT_1:51
.= ((the multF of K)||the carrier of E)||the carrier of FE by H4,FUNCT_1:51
.= (the multF of E)||the carrier of FE by H0,C0SP1:def 3
.= the multF of FE by d;
D: 1.FK = 1.K by d .= 1.E by H0,C0SP1:def 3 .= 1.FE by d;
0.FK = 0.K by d .= 0.E by H0,C0SP1:def 3 .= 0.FE by d;
then FE is Subring of FK by A,B,C,D,C0SP1:def 3;
hence thesis by FIELD_4:def 1;
end;
theorem
for F being Field
for E being F-algebraic FieldExtension of F holds F_Alg E == E
proof
let F be Field, E be F-algebraic FieldExtension of F;
A: E is FieldExtension of F_Alg E by ee;
F_Alg E is FieldExtension of E by t2;
hence F_Alg E == E by A,FIELD_4:7;
end;