:: Algebraic Extensions
:: by Christoph Schwarzweller and Agnieszka Rowin\'nska-Schwarzweller
::
:: Copyright (c) 2021 Association of Mizar Users

definition
let L1, L2 be doubleLoopStr ;
pred L1 == L2 means :: FIELD_7:def 1
doubleLoopStr(# the carrier of L1, the addF of L1, the multF of L1, the OneF of L1, the ZeroF of L1 #) = doubleLoopStr(# the carrier of L2, the addF of L2, the multF of L2, the OneF of L2, the ZeroF of L2 #);
reflexivity
for L1 being doubleLoopStr holds doubleLoopStr(# the carrier of L1, the addF of L1, the multF of L1, the OneF of L1, the ZeroF of L1 #) = doubleLoopStr(# the carrier of L1, the addF of L1, the multF of L1, the OneF of L1, the ZeroF of L1 #)
;
symmetry
for L1, L2 being doubleLoopStr st doubleLoopStr(# the carrier of L1, the addF of L1, the multF of L1, the OneF of L1, the ZeroF of L1 #) = doubleLoopStr(# the carrier of L2, the addF of L2, the multF of L2, the OneF of L2, the ZeroF of L2 #) holds
doubleLoopStr(# the carrier of L2, the addF of L2, the multF of L2, the OneF of L2, the ZeroF of L2 #) = doubleLoopStr(# the carrier of L1, the addF of L1, the multF of L1, the OneF of L1, the ZeroF of L1 #)
;
end;

:: deftheorem defines == FIELD_7:def 1 :
for L1, L2 being doubleLoopStr holds
( L1 == L2 iff doubleLoopStr(# the carrier of L1, the addF of L1, the multF of L1, the OneF of L1, the ZeroF of L1 #) = doubleLoopStr(# the carrier of L2, the addF of L2, the multF of L2, the OneF of L2, the ZeroF of L2 #) );

theorem :: FIELD_7:1
for R, S being Ring holds
( R == S iff ex f being Function of R,S st
( f = id R & f is isomorphism ) )
proof end;

theorem :: FIELD_7:2
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 end;

definition
let F1, F2 be Field;
redefine pred F1 == F2 means :: FIELD_7:def 2
( F1 is Subfield of F2 & F2 is Subfield of F1 );
correctness
compatibility
( F1 == F2 iff ( F1 is Subfield of F2 & F2 is Subfield of F1 ) )
;
proof end;
end;

:: deftheorem defines == FIELD_7:def 2 :
for F1, F2 being Field holds
( F1 == F2 iff ( F1 is Subfield of F2 & F2 is Subfield of F1 ) );

theorem Th1: :: FIELD_7:3
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 end;

theorem str12: :: FIELD_7:4
for F being Field
for E1, E2 being FieldExtension of F st E1 == E2 holds
VecSp (E1,F) = VecSp (E2,F)
proof end;

theorem str11: :: FIELD_7:5
for F being Field
for E1, E2 being FieldExtension of F st E1 == E2 holds
deg (E1,F) = deg (E2,F)
proof end;

registration
let F be Field;
let E be FieldExtension of F;
existence
ex b1 being FieldExtension of F st b1 is E -homomorphic
proof end;
existence
ex b1 being FieldExtension of F st b1 is E -monomorphic
proof end;
existence
ex b1 being FieldExtension of F st b1 is E -isomorphic
proof end;
end;

definition
let R be Ring;
let a, b be Element of R;
:: original: {
redefine func {a,b} -> Subset of R;
coherence
{a,b} is Subset of R
proof end;
end;

definition
let F be Field;
let V be VectSp of F;
let a be Element of V;
:: original: {
redefine func {a} -> Subset of V;
coherence
{a} is Subset of V
proof end;
end;

definition
let F be Field;
let V be VectSp of F;
let a, b be Element of V;
:: original: {
redefine func {a,b} -> Subset of V;
coherence
{a,b} is Subset of V
proof end;
end;

registration
let F be Field;
let V be VectSp of F;
cluster V263(F,V) -> linearly-independent for Element of bool the carrier of V;
coherence
for b1 being Basis of V holds b1 is linearly-independent
by VECTSP_7:def 3;
end;

theorem ZMODUL033: :: FIELD_7:6
for F being Field
for 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 end;

registration
let F be Field;
let E be FieldExtension of F;
cluster V263(F, VecSp (E,F)) -> non empty for Element of bool the carrier of (VecSp (E,F));
coherence
for b1 being Basis of (VecSp (E,F)) holds not b1 is empty
proof end;
end;

registration
let F be Field;
let E be FieldExtension of F;
cluster deg (E,F) -> non zero ;
coherence
not deg (E,F) is zero
proof end;
end;

registration
let F be Field;
let E be F -finite FieldExtension of F;
cluster V263(F, VecSp (E,F)) -> finite for Element of bool the carrier of (VecSp (E,F));
coherence
for b1 being Basis of (VecSp (E,F)) holds b1 is finite
proof end;
end;

theorem quah1: :: FIELD_7:7
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 end;

theorem str1a: :: FIELD_7:8
for F being Field
for E being FieldExtension of F holds
( deg (E,F) = 1 iff E == F )
proof end;

theorem quah2: :: FIELD_7:9
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 end;

registration
let F be Field;
let E be FieldExtension of F;
cluster non empty finite linearly-independent for Element of bool the carrier of (VecSp (E,F));
existence
ex b1 being Subset of (VecSp (E,F)) st
( not b1 is empty & b1 is finite & b1 is linearly-independent )
proof end;
end;

theorem ext0: :: FIELD_7:10
for F being Field
for E being FieldExtension of F
for T1, T2 being Subset of E st T1 c= T2 holds
proof end;

definition
let F be Field;
let p be Polynomial of F;
func Coeff p -> Subset of F equals :: FIELD_7:def 3
{ (p . i) where i is Element of NAT : p . i <> 0. F } ;
coherence
{ (p . i) where i is Element of NAT : p . i <> 0. F } is Subset of F
proof end;
end;

:: deftheorem defines Coeff FIELD_7:def 3 :
for F being Field
for p being Polynomial of F holds Coeff p = { (p . i) where i is Element of NAT : p . i <> 0. F } ;

registration
let F be Field;
let p be Polynomial of F;
coherence
Coeff p is finite
proof end;
end;

theorem cof1: :: FIELD_7:11
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 end;

theorem cof2: :: FIELD_7:12
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 end;

theorem m4: :: FIELD_7:13
for R being Ring
for S being RingExtension of R
for p being Element of the carrier of ()
for q being Element of the carrier of () st p = q holds
Roots (S,p) = Roots q
proof end;

registration
let R be domRing;
let p be non zero Element of the carrier of ();
coherence
Roots p is finite
;
end;

registration
let R be domRing;
let S be domRingExtension of R;
let p be non zero Element of the carrier of ();
cluster Roots (S,p) -> finite ;
coherence
Roots (S,p) is finite
proof end;
end;

registration
let F be Field;
let E be FieldExtension of F;
existence
ex b1 being FieldExtension of E st b1 is F -extending
proof end;
end;

registration
let F be Field;
let E be F -finite FieldExtension of F;
existence
ex b1 being F -extending FieldExtension of F st b1 is F -finite
proof end;
end;

registration
let F be Field;
let E be F -finite FieldExtension of F;
existence
ex b1 being F -extending FieldExtension of F st b1 is E -finite
proof end;
end;

theorem lemma7a: :: FIELD_7:14
for F being Field
for p being Element of the carrier of ()
for E being FieldExtension of F
for U being b3 -extending FieldExtension of F
for a being Element of E
for b being Element of U st a = b holds
Ext_eval (p,a) = Ext_eval (p,b)
proof end;

theorem lemma7b: :: FIELD_7:15
for F being Field
for p being Element of the carrier of ()
for E being FieldExtension of F
for q being Element of the carrier of () st q = p holds
for U being b3 -extending FieldExtension of F
for a being Element of U holds Ext_eval (q,a) = Ext_eval (p,a)
proof end;

definition
let R be Ring;
let S be RingExtension of R;
let a be Element of R;
func @ (a,S) -> Element of S equals :: FIELD_7:def 4
a;
coherence
a is Element of S
proof end;
end;

:: deftheorem defines @ FIELD_7:def 4 :
for R being Ring
for S being RingExtension of R
for a being Element of R holds @ (a,S) = a;

definition
let R be Ring;
let S be RingExtension of R;
let a be Element of S;
attr a is R -membered means :defmem: :: FIELD_7:def 5
a in the carrier of R;
end;

:: deftheorem defmem defines -membered FIELD_7:def 5 :
for R being Ring
for S being RingExtension of R
for a being Element of S holds
( a is R -membered iff a in the carrier of R );

registration
let R be Ring;
let S be RingExtension of R;
existence
ex b1 being Element of S st b1 is R -membered
proof end;
end;

definition
let R be Ring;
let 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: :: FIELD_7:def 6
a;
coherence
a is Element of R
by AS;
end;

:: deftheorem defred defines @ FIELD_7:def 6 :
for R being Ring
for S being RingExtension of R
for a being Element of S st a is R -membered holds
@ (R,a) = a;

registration
let R be Ring;
let S be RingExtension of R;
let a be R -membered Element of S;
reduce @ (R,a) to a;
reducibility
@ (R,a) = a
by defred;
end;

registration
let F be Field;
let E be FieldExtension of F;
existence
ex b1 being Element of E st
( not b1 is zero & b1 is F -algebraic )
proof end;
end;

registration
let F be Field;
let E be FieldExtension of F;
let a be Element of F;
cluster @ (a,E) -> F -algebraic ;
coherence
@ (a,E) is F -algebraic
proof end;
end;

registration
let F be Field;
let 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
@ (a,K) is F -algebraic
proof end;
end;

help1: for R being domRing
for n being Element of NAT holds (<%(0. R),(1. R)%> ^ n) . n = 1. R

proof end;

help2: for R being domRing
for n, i being Element of NAT st i <> n holds
(<%(0. R),(1. R)%> ^ n) . i = 0. R

proof end;

theorem sp0: :: FIELD_7:16
for F being Field
for E being FieldExtension of F
for K being b2 -extending FieldExtension of F
for l being Linear_Combination of VecSp (K,F) holds l is Linear_Combination of VecSp (K,E)
proof end;

theorem sp1: :: FIELD_7:17
for F being Field
for E being FieldExtension of F
for K being b2 -extending FieldExtension of F
for BE being Subset of (VecSp (K,E))
for BF being Subset of (VecSp (K,F)) st BF c= BE holds
for l being Linear_Combination of BF holds l is Linear_Combination of BE
proof end;

theorem sp2: :: FIELD_7:18
for F being Field
for E being FieldExtension of F
for K being b2 -extending FieldExtension of F
for BE being finite Subset of (VecSp (K,E))
for BF being finite Subset of (VecSp (K,F))
for l1 being Linear_Combination of BF
for l2 being Linear_Combination of BE st l1 = l2 & BF c= BE holds
Sum l1 = Sum l2
proof end;

definition
let F be Field;
let E be FieldExtension of F;
let K be F -extending FieldExtension of F;
let BE be Subset of (VecSp (E,F));
let BK be Subset of (VecSp (K,E));
func Base (BE,BK) -> Subset of (VecSp (K,F)) equals :: FIELD_7:def 7
{ (a * b) where a, b is Element of K : ( a in BE & b in BK ) } ;
coherence
{ (a * b) where a, b is Element of K : ( a in BE & b in BK ) } is Subset of (VecSp (K,F))
proof end;
end;

:: deftheorem defines Base FIELD_7:def 7 :
for F being Field
for E being FieldExtension of F
for K being b1 -extending FieldExtension of F
for BE being Subset of (VecSp (E,F))
for BK being Subset of (VecSp (K,E)) holds Base (BE,BK) = { (a * b) where a, b is Element of K : ( a in BE & b in BK ) } ;

registration
let F be Field;
let E be FieldExtension of F;
let K be F -extending FieldExtension of F;
let BE be non empty Subset of (VecSp (E,F));
let BK be non empty Subset of (VecSp (K,E));
cluster Base (BE,BK) -> non empty ;
coherence
not Base (BE,BK) is empty
proof end;
end;

BE0: for F being Field
for E being FieldExtension of F
for K being b1 -extending FieldExtension of F
for BE being linearly-independent Subset of (VecSp (E,F))
for 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 end;

theorem :: FIELD_7:19
for F being Field
for E being FieldExtension of F
for K being b1 -extending FieldExtension of F
for BE being linearly-independent Subset of (VecSp (E,F))
for 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 & a1 * b1 = a2 * b2 holds
( a1 = a2 & b1 = b2 )
proof end;

theorem BE1: :: FIELD_7:20
for F being Field
for E being FieldExtension of F
for K being b1 -extending FieldExtension of F
for BE being non empty linearly-independent Subset of (VecSp (E,F))
for BK being non empty linearly-independent Subset of (VecSp (K,E)) holds card (Base (BE,BK)) = card [:BE,BK:]
proof end;

theorem BE2: :: FIELD_7:21
for F being Field
for E being FieldExtension of F
for K being b1 -extending FieldExtension of F
for BE being non empty finite linearly-independent Subset of (VecSp (E,F))
for BK being non empty finite linearly-independent Subset of (VecSp (K,E)) holds card (Base (BE,BK)) = (card BE) * (card BK)
proof end;

registration
let F be Field;
let E be FieldExtension of F;
let K be F -extending FieldExtension of F;
let BE be non empty finite linearly-independent Subset of (VecSp (E,F));
let BK be non empty finite linearly-independent Subset of (VecSp (K,E));
cluster Base (BE,BK) -> finite ;
coherence
Base (BE,BK) is finite
proof end;
end;

definition
let F be Field;
let E be FieldExtension of F;
let K be F -extending FieldExtension of F;
let BE be non empty finite linearly-independent Subset of (VecSp (E,F));
let 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: :: FIELD_7:def 8
( ( 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
ex b1 being Linear_Combination of BE st
( ( for a being Element of K st a in BE & b in BK holds
b1 . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds
b1 . a = 0. F ) )
proof end;
uniqueness
for b1, b2 being Linear_Combination of BE st ( for a being Element of K st a in BE & b in BK holds
b1 . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds
b1 . a = 0. F ) & ( for a being Element of K st a in BE & b in BK holds
b2 . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds
b2 . a = 0. F ) holds
b1 = b2
proof end;
end;

:: deftheorem down1 defines down FIELD_7:def 8 :
for F being Field
for E being FieldExtension of F
for K being b1 -extending FieldExtension of F
for BE being non empty finite linearly-independent Subset of (VecSp (E,F))
for BK being non empty linearly-independent Subset of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK)
for b being Element of K
for b8 being Linear_Combination of BE holds
( b8 = down (l,b) iff ( ( for a being Element of K st a in BE & b in BK holds
b8 . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds
b8 . a = 0. F ) ) );

definition
let F be Field;
let E be FieldExtension of F;
let K be F -extending FieldExtension of F;
let BE be non empty finite linearly-independent Subset of (VecSp (E,F));
let 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: :: FIELD_7:def 9
for b being Element of K st b in BK holds
it . b = Sum (down (l,b));
existence
ex b1 being Linear_Combination of BK st
for b being Element of K st b in BK holds
b1 . b = Sum (down (l,b))
proof end;
uniqueness
for b1, b2 being Linear_Combination of BK st ( for b being Element of K st b in BK holds
b1 . b = Sum (down (l,b)) ) & ( for b being Element of K st b in BK holds
b2 . b = Sum (down (l,b)) ) holds
b1 = b2
proof end;
end;

:: deftheorem down2 defines down FIELD_7:def 9 :
for F being Field
for E being FieldExtension of F
for K being b1 -extending FieldExtension of F
for BE being non empty finite linearly-independent Subset of (VecSp (E,F))
for BK being non empty finite linearly-independent Subset of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK)
for b7 being Linear_Combination of BK holds
( b7 = down l iff for b being Element of K st b in BK holds
b7 . b = Sum (down (l,b)) );

T0: for F being Field
for E being FieldExtension of F
for K being b1 -extending FieldExtension of F
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 end;

definition
let F be Field;
let E be F -finite FieldExtension of F;
let K be F -extending FieldExtension of F;
let BE be Basis of (VecSp (E,F));
let 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: :: FIELD_7:def 10
for b being Element of K st b in BK holds
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
ex b1 being Linear_Combination of Base (BE,BK) st
for b being Element of K st b in BK holds
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
b1 . (a * b) = l2 . a ) )
proof end;
uniqueness
for b1, b2 being Linear_Combination of Base (BE,BK) st ( for b being Element of K st b in BK holds
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
b1 . (a * b) = l2 . a ) ) ) & ( for b being Element of K st b in BK holds
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
b2 . (a * b) = l2 . a ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem lif defines lift FIELD_7:def 10 :
for F being Field
for E being b1 -finite FieldExtension of F
for K being b1 -extending FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being non empty finite linearly-independent Subset of (VecSp (K,E))
for l1 being Linear_Combination of BK
for b7 being Linear_Combination of Base (BE,BK) holds
( b7 = lift (l1,BE) iff for b being Element of K st b in BK holds
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
b7 . (a * b) = l2 . a ) ) );

theorem :: FIELD_7:22
for F being Field
for E being b1 -finite FieldExtension of F
for K being b1 -extending b2 -finite FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK) holds lift ((down l),BE) = l
proof end;

theorem Tlift2: :: FIELD_7:23
for F being Field
for E being b1 -finite FieldExtension of F
for K being b1 -extending b2 -finite FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E))
for l being Linear_Combination of BK holds down (lift (l,BE)) = l
proof end;

theorem LSum1a: :: FIELD_7:24
for F being Field
for E being FieldExtension of F
for K being b1 -extending FieldExtension of F
for BE being non empty finite linearly-independent Subset of (VecSp (E,F))
for 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
for b being Element of K holds down (l,b) = (down (l1,b)) + (down (l2,b))
proof end;

theorem LSum1: :: FIELD_7:25
for F being Field
for E being FieldExtension of F
for K being b1 -extending FieldExtension of F
for BE being non empty finite linearly-independent Subset of (VecSp (E,F))
for 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 end;

LSum2: for F being Field
for E being FieldExtension of F
for K being b1 -extending FieldExtension of F
for BE being non empty finite linearly-independent Subset of (VecSp (E,F))
for BK being non empty finite linearly-independent Subset of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK) st card () = 1 holds
Sum l = Sum (down l)

proof end;

theorem TSum: :: FIELD_7:26
for F being Field
for E being b1 -finite FieldExtension of F
for K being b1 -extending b2 -finite FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK) holds Sum l = Sum (down l)
proof end;

theorem T1: :: FIELD_7:27
for F being Field
for E being b1 -finite FieldExtension of F
for K being b1 -extending b2 -finite FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK) st Sum l = 0. (VecSp (K,F)) holds
Carrier l = {}
proof end;

theorem T2: :: FIELD_7:28
for F being Field
for E being b1 -finite FieldExtension of F
for K being b1 -extending b2 -finite FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E)) holds Lin (Base (BE,BK)) = ModuleStr(# the carrier of (VecSp (K,F)), the addF of (VecSp (K,F)), the ZeroF of (VecSp (K,F)), the lmult of (VecSp (K,F)) #)
proof end;

for F being Field
for E being b1 -finite FieldExtension of F
for K being b1 -extending b2 -finite FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E)) holds Base (BE,BK) is Basis of (VecSp (K,F))
proof end;

theorem degmult: :: FIELD_7:30
for F being Field
for E being b1 -finite FieldExtension of F
for K being b1 -extending b2 -finite FieldExtension of F holds deg (K,F) = (deg (K,E)) * (deg (E,F))
proof end;

theorem alg0: :: FIELD_7:31
for F being Field
for E being FieldExtension of F
for K being b2 -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 end;

registration
let F be Field;
let E be F -finite FieldExtension of F;
coherence
for b1 being F -extending E -finite FieldExtension of F holds b1 is F -finite
proof end;
end;

lintrans: for F being Field
for E1 being FieldExtension of F
for E2 being b2 -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 end;

definition
let F be Field;
let E be FieldExtension of F;
attr E is F -algebraic means :defa: :: FIELD_7:def 11
for a being Element of E holds a is F -algebraic ;
end;

:: deftheorem defa defines -algebraic FIELD_7:def 11 :
for F being Field
for E being FieldExtension of F holds
( E is F -algebraic iff for a being Element of E holds a is F -algebraic );

lemlin: for F being Field
for E being b1 -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 end;

registration
let F be Field;
coherence
for b1 being FieldExtension of F st b1 is F -finite holds
b1 is F -algebraic
proof end;
end;

registration
let F be Field;
let E be F -algebraic FieldExtension of F;
cluster -> F -algebraic for Element of the carrier of E;
coherence
for b1 being Element of E holds b1 is F -algebraic
by defa;
end;

theorem :: FIELD_7:32
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 end;

theorem alg1: :: FIELD_7:33
for F being Field
for E being FieldExtension of F
for a being Element of E holds
( a is F -algebraic iff ex B being b1 -finite FieldExtension of F st
( E is B -extending & a in B ) )
proof 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: :: FIELD_7:def 12
for a being Element of E st a in T holds
a is F -algebraic ;
end;

:: deftheorem defTalg defines -algebraic FIELD_7:def 12 :
for F being Field
for E being FieldExtension of F
for T being Subset of E holds
( T is F -algebraic iff for a being Element of E st a in T holds
a is F -algebraic );

registration
let F be Field;
let E be FieldExtension of F;
cluster finite F -algebraic for Element of bool the carrier of E;
existence
ex b1 being Subset of E st
( b1 is finite & b1 is F -algebraic )
proof end;
end;

theorem ug: :: FIELD_7:34
for F being Field
for E being FieldExtension of F
for b being Element of E
for T being Subset of E
for E1 being FieldExtension of FAdj (F,T)
for b1 being Element of E1 st E1 = E & b1 = b holds
proof end;

theorem ug1: :: FIELD_7:35
for F being Field
for E being FieldExtension of F
for b being Element of E
for T being Subset of E
for E1 being FieldExtension of FAdj (F,{b})
for T1 being Subset of E1 st E1 = E & T1 = T holds
proof end;

registration
let F be Field;
let E be FieldExtension of F;
let T be finite F -algebraic Subset of E;
cluster FieldAdjunction (F,T) -> F -finite ;
coherence
proof end;
end;

theorem ft1: :: FIELD_7:36
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E holds
( E == FAdj (F,{a}) iff deg (MinPoly (a,F)) = deg (E,F) )
proof end;

theorem :: FIELD_7:37
for F being Field
for E being FieldExtension of F holds
( E is F -finite iff ex T being finite b1 -algebraic Subset of E st E == FAdj (F,T) )
proof end;

registration
let F be Field;
let E be FieldExtension of F;
let p be non zero Element of the carrier of ();
cluster Roots (E,p) -> F -algebraic ;
coherence
Roots (E,p) is F -algebraic
proof end;
end;

theorem :: FIELD_7:38
for F being Field
for E being FieldExtension of F
for p being non zero Element of the carrier of () holds FAdj (F,(Roots (E,p))) is F -algebraic ;

theorem :: FIELD_7:39
for F being Field
for E being FieldExtension of F
for K being b2 -extending FieldExtension of F st K is E -algebraic & E is F -algebraic holds
K is F -algebraic
proof end;

theorem :: FIELD_7:40
for F being Field
for E being FieldExtension of F
for K being b2 -extending FieldExtension of F st K is F -algebraic holds
( K is E -algebraic & E is F -algebraic )
proof end;

registration
let F be Field;
let E be FieldExtension of F;
let a, b be F -algebraic Element of E;
cluster FieldAdjunction (F,{a,b}) -> F -finite ;
coherence
proof end;
end;

registration
let F be Field;
let E be FieldExtension of F;
cluster 0. E -> F -algebraic ;
coherence
0. E is F -algebraic
proof end;
cluster 1. E -> F -algebraic ;
coherence
1. E is F -algebraic
proof end;
end;

registration
let F be Field;
let E be FieldExtension of F;
let a, b be F -algebraic Element of E;
cluster a + b -> F -algebraic ;
coherence
a + b is F -algebraic
proof end;
cluster a - b -> F -algebraic ;
coherence
a - b is F -algebraic
proof end;
cluster a * b -> F -algebraic ;
coherence
a * b is F -algebraic
proof end;
end;

registration
let F be Field;
let E be FieldExtension of F;
let a be F -algebraic Element of E;
cluster - a -> F -algebraic ;
coherence
- a is F -algebraic
proof end;
end;

registration
let F be Field;
let E be FieldExtension of F;
let a be non zero F -algebraic Element of E;
cluster / a -> F -algebraic ;
coherence
a " is F -algebraic
proof end;
end;

definition
let F be Field;
let E be FieldExtension of F;
func Alg_El E -> Subset of E equals :: FIELD_7:def 13
{ a where a is F -algebraic Element of E : verum } ;
coherence
{ a where a is F -algebraic Element of E : verum } is Subset of E
proof end;
end;

:: deftheorem defines Alg_El FIELD_7:def 13 :
for F being Field
for E being FieldExtension of F holds Alg_El E = { a where a is b1 -algebraic Element of E : verum } ;

definition
let F be Field;
let E be FieldExtension of F;
func Field_of_Algebraic_Elements E -> strict doubleLoopStr means :d: :: FIELD_7:def 14
( 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
ex b1 being strict doubleLoopStr st
( the carrier of b1 = Alg_El E & the addF of b1 = the addF of E || the carrier of b1 & the multF of b1 = the multF of E || the carrier of b1 & the OneF of b1 = 1. E & the ZeroF of b1 = 0. E )
proof end;
uniqueness
for b1, b2 being strict doubleLoopStr st the carrier of b1 = Alg_El E & the addF of b1 = the addF of E || the carrier of b1 & the multF of b1 = the multF of E || the carrier of b1 & the OneF of b1 = 1. E & the ZeroF of b1 = 0. E & the carrier of b2 = Alg_El E & the addF of b2 = the addF of E || the carrier of b2 & the multF of b2 = the multF of E || the carrier of b2 & the OneF of b2 = 1. E & the ZeroF of b2 = 0. E holds
b1 = b2
;
end;

:: deftheorem d defines Field_of_Algebraic_Elements FIELD_7:def 14 :
for F being Field
for E being FieldExtension of F
for b3 being strict doubleLoopStr holds
( b3 = Field_of_Algebraic_Elements E iff ( the carrier of b3 = Alg_El E & the addF of b3 = the addF of E || the carrier of b3 & the multF of b3 = the multF of E || the carrier of b3 & the OneF of b3 = 1. E & the ZeroF of b3 = 0. E ) );

notation
let F be Field;
let E be FieldExtension of F;
synonym F_Alg E for Field_of_Algebraic_Elements E;
end;

registration
let F be Field;
let E be FieldExtension of F;
coherence
not F_Alg E is degenerated
proof end;
end;

Lm10: for R being Field
for E being FieldExtension of R
for x being Element of () holds x is Element of E

proof end;

Lm11: for R being Field
for E being FieldExtension of R
for a, b being Element of E
for x, y being Element of () st a = x & b = y holds
a + b = x + y

proof end;

Lm12: for R being Field
for S being FieldExtension of R
for a, b being Element of S
for x, y being Element of () st a = x & b = y holds
a * b = x * y

proof end;

registration
let F be Field;
let E be FieldExtension of F;
coherence
proof end;
end;

registration
let F be Field;
let E be FieldExtension of F;
coherence
proof end;
end;

ee: for F being Field
for E being FieldExtension of F holds E is FieldExtension of F_Alg E

proof end;

registration
let F be Field;
let E be FieldExtension of F;
coherence
F_Alg E is F -extending
proof end;
end;

registration
let F be Field;
let E be FieldExtension of F;
coherence
F_Alg E is F -algebraic
proof end;
end;

theorem :: FIELD_7:41
for F being Field
for E being FieldExtension of F holds F_Alg E is FieldExtension of F ;

theorem :: FIELD_7:42
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 b1 -algebraic FieldExtension of F holds F_Alg E is FieldExtension of E

proof end;

theorem :: FIELD_7:43
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 end;

theorem :: FIELD_7:44
for F being Field
for E being b1 -algebraic FieldExtension of F holds F_Alg E == E
proof end;