:: by Christoph Schwarzweller and Agnieszka Rowin\'nska-Schwarzweller

::

:: Received March 30, 2021

:: Copyright (c) 2021 Association of Mizar Users

definition

let L1, L2 be doubleLoopStr ;

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;
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 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 #);

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 #) ;

:: 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 #) );

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 ) )

( R == S iff ex f being Function of R,S st

( f = id R & f is isomorphism ) )

proof end;

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;

correctness

compatibility

( F1 == F2 iff ( F1 is Subfield of F2 & F2 is Subfield of F1 ) );

end;
correctness

compatibility

( F1 == F2 iff ( F1 is Subfield of F2 & F2 is Subfield of F1 ) );

proof 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 ) );

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 )

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)

for E1, E2 being FieldExtension of F st E1 == E2 holds

VecSp (E1,F) = VecSp (E2,F)

proof end;

registration

let F be Field;

let E be FieldExtension of F;

ex b_{1} being FieldExtension of F st b_{1} is E -homomorphic

ex b_{1} being FieldExtension of F st b_{1} is E -monomorphic

ex b_{1} being FieldExtension of F st b_{1} is E -isomorphic

end;
let E be FieldExtension of F;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative domRing-like V240() V241() V242() V243() V254() E -homomorphic Polynom-Ring F -homomorphic factorial F -extending for doubleLoopStr ;

existence ex b

proof end;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative domRing-like V240() V241() V242() V243() V254() Polynom-Ring F -homomorphic factorial F -extending E -monomorphic for doubleLoopStr ;

existence ex b

proof end;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative domRing-like V240() V241() V242() V243() V254() Polynom-Ring F -homomorphic factorial F -extending E -isomorphic for doubleLoopStr ;

existence ex b

proof 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

end;
let a, b be Element of R;

:: original: {

redefine func {a,b} -> Subset of R;

coherence

{a,b} is Subset of R

proof 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

end;
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;

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

end;
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;

registration

let F be Field;

let V be VectSp of F;

coherence

for b_{1} being Basis of V holds b_{1} is linearly-independent
by VECTSP_7:def 3;

end;
let V be VectSp of F;

coherence

for b

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 )

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;

coherence

for b_{1} being Basis of (VecSp (E,F)) holds not b_{1} is empty

end;
let E be FieldExtension of F;

coherence

for b

proof end;

registration
end;

registration

let F be Field;

let E be F -finite FieldExtension of F;

coherence

for b_{1} being Basis of (VecSp (E,F)) holds b_{1} is finite

end;
let E be F -finite FieldExtension of F;

coherence

for b

proof 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 )

for E being FieldExtension of F holds

( deg (E,F) = 1 iff the carrier of E = the carrier of 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)) )

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;

existence

ex b_{1} being Subset of (VecSp (E,F)) st

( not b_{1} is empty & b_{1} is finite & b_{1} is linearly-independent )

end;
let E be FieldExtension of F;

existence

ex b

( not b

proof 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

FAdj (F,T1) is Subfield of FAdj (F,T2)

for 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 end;

definition

let F be Field;

let p be Polynomial of F;

{ (p . i) where i is Element of NAT : p . i <> 0. F } is Subset of F

end;
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 } ;

{ (p . i) where i is Element of NAT : p . i <> 0. F } is Subset of F

proof 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 } ;

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 } ;

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

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

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 (Polynom-Ring R)

for q being Element of the carrier of (Polynom-Ring S) st p = q holds

Roots (S,p) = Roots q

for 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 end;

registration

let R be domRing;

let p be non zero Element of the carrier of (Polynom-Ring R);

coherence

Roots p is finite ;

end;
let p be non zero Element of the carrier of (Polynom-Ring R);

coherence

Roots p is finite ;

registration

let R be domRing;

let S be domRingExtension of R;

let p be non zero Element of the carrier of (Polynom-Ring R);

coherence

Roots (S,p) is finite

end;
let S be domRingExtension of R;

let p be non zero Element of the carrier of (Polynom-Ring R);

coherence

Roots (S,p) is finite

proof end;

registration

let F be Field;

let E be FieldExtension of F;

ex b_{1} being FieldExtension of E st b_{1} is F -extending

end;
let E be FieldExtension of F;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative domRing-like V240() V241() V242() V243() V254() Polynom-Ring E -homomorphic factorial F -extending E -extending for doubleLoopStr ;

existence ex b

proof end;

registration

let F be Field;

let E be F -finite FieldExtension of F;

ex b_{1} being F -extending FieldExtension of F st b_{1} is F -finite

end;
let E be F -finite FieldExtension of F;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative domRing-like V240() V241() V242() V243() V254() Polynom-Ring E -homomorphic factorial F -extending E -extending F -finite for doubleLoopStr ;

existence ex b

proof end;

registration

let F be Field;

let E be F -finite FieldExtension of F;

ex b_{1} being F -extending FieldExtension of F st b_{1} is E -finite

end;
let E be F -finite FieldExtension of F;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative domRing-like V240() V241() V242() V243() V254() Polynom-Ring E -homomorphic factorial F -extending E -extending E -finite for doubleLoopStr ;

existence ex b

proof end;

theorem lemma7a: :: FIELD_7:14

for F being Field

for p being Element of the carrier of (Polynom-Ring F)

for E being FieldExtension of F

for U being b_{3} -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)

for p being Element of the carrier of (Polynom-Ring F)

for E being FieldExtension of F

for U being b

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 (Polynom-Ring F)

for E being FieldExtension of F

for q being Element of the carrier of (Polynom-Ring E) st q = p holds

for U being b_{3} -extending FieldExtension of F

for a being Element of U holds Ext_eval (q,a) = Ext_eval (p,a)

for p being Element of the carrier of (Polynom-Ring F)

for E being FieldExtension of F

for q being Element of the carrier of (Polynom-Ring E) st q = p holds

for U being b

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;

coherence

a is Element of S

end;
let S be RingExtension of R;

let a be Element of R;

coherence

a is Element of S

proof 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;

for R being Ring

for S being RingExtension of R

for a being Element of R holds @ (a,S) = a;

:: 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 );

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;

ex b_{1} being Element of S st b_{1} is R -membered

end;
let S be RingExtension of R;

cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable R -membered for Element of the carrier of S;

existence ex b

proof end;

definition

let R be Ring;

let S be RingExtension of R;

let a be Element of S;

assume AS: a is R -membered ;

coherence

a is Element of R by AS;

end;
let S be RingExtension of R;

let a be Element of S;

assume AS: a is R -membered ;

coherence

a is Element of R by AS;

:: 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;

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;

reducibility

@ (R,a) = a by defred;

end;
let S be RingExtension of R;

let a be R -membered Element of S;

reducibility

@ (R,a) = a by defred;

registration

let F be Field;

let E be FieldExtension of F;

ex b_{1} being Element of E st

( not b_{1} is zero & b_{1} is F -algebraic )

end;
let E be FieldExtension of F;

cluster non zero left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable V278(E) F -algebraic for Element of the carrier of E;

existence ex b

( not b

proof end;

registration

let F be Field;

let E be FieldExtension of F;

let a be Element of F;

coherence

@ (a,E) is F -algebraic

end;
let E be FieldExtension of F;

let a be Element of F;

coherence

@ (a,E) is F -algebraic

proof 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;

coherence

@ (a,K) is F -algebraic

end;
let E be FieldExtension of F;

let K be E -extending FieldExtension of F;

let a be F -algebraic Element of E;

coherence

@ (a,K) is F -algebraic

proof 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 b_{2} -extending FieldExtension of F

for l being Linear_Combination of VecSp (K,F) holds l is Linear_Combination of VecSp (K,E)

for E being FieldExtension of F

for K being b

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 b_{2} -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

for E being FieldExtension of F

for K being b

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 b_{2} -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

for E being FieldExtension of F

for K being b

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));

{ (a * b) where a, b is Element of K : ( a in BE & b in BK ) } is Subset of (VecSp (K,F))

end;
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 ) } ;

{ (a * b) where a, b is Element of K : ( a in BE & b in BK ) } is Subset of (VecSp (K,F))

proof end;

:: deftheorem defines Base FIELD_7:def 7 :

for F being Field

for E being FieldExtension of F

for K being b_{1} -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 ) } ;

for F being Field

for E being FieldExtension of F

for K being b

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));

coherence

not Base (BE,BK) is empty

end;
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));

coherence

not Base (BE,BK) is empty

proof end;

BE0: for F being Field

for E being FieldExtension of F

for K being b

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 b_{1} -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 )

for E being FieldExtension of F

for K being b

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 b_{1} -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:]

for E being FieldExtension of F

for K being b

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 b_{1} -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)

for E being FieldExtension of F

for K being b

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));

coherence

Base (BE,BK) is finite

end;
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));

coherence

Base (BE,BK) is finite

proof 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;

ex b_{1} being Linear_Combination of BE st

( ( for a being Element of K st a in BE & b in BK holds

b_{1} . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds

b_{1} . a = 0. F ) )

for b_{1}, b_{2} being Linear_Combination of BE st ( for a being Element of K st a in BE & b in BK holds

b_{1} . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds

b_{1} . a = 0. F ) & ( for a being Element of K st a in BE & b in BK holds

b_{2} . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds

b_{2} . a = 0. F ) holds

b_{1} = b_{2}

end;
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 ( ( 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 ) );

ex b

( ( for a being Element of K st a in BE & b in BK holds

b

b

proof end;

uniqueness for b

b

b

b

b

b

proof end;

:: deftheorem down1 defines down FIELD_7:def 8 :

for F being Field

for E being FieldExtension of F

for K being b_{1} -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 b_{8} being Linear_Combination of BE holds

( b_{8} = down (l,b) iff ( ( for a being Element of K st a in BE & b in BK holds

b_{8} . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds

b_{8} . a = 0. F ) ) );

for F being Field

for E being FieldExtension of F

for K being b

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 b

( b

b

b

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);

ex b_{1} being Linear_Combination of BK st

for b being Element of K st b in BK holds

b_{1} . b = Sum (down (l,b))

for b_{1}, b_{2} being Linear_Combination of BK st ( for b being Element of K st b in BK holds

b_{1} . b = Sum (down (l,b)) ) & ( for b being Element of K st b in BK holds

b_{2} . b = Sum (down (l,b)) ) holds

b_{1} = b_{2}

end;
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 for b being Element of K st b in BK holds

it . b = Sum (down (l,b));

ex b

for b being Element of K st b in BK holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem down2 defines down FIELD_7:def 9 :

for F being Field

for E being FieldExtension of F

for K being b_{1} -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 b_{7} being Linear_Combination of BK holds

( b_{7} = down l iff for b being Element of K st b in BK holds

b_{7} . b = Sum (down (l,b)) );

for F being Field

for E being FieldExtension of F

for K being b

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 b

( b

b

T0: for F being Field

for E being FieldExtension of F

for K being b

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;

ex b_{1} 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

b_{1} . (a * b) = l2 . a ) )

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (a * b) = l2 . a ) ) ) holds

b_{1} = b_{2}

end;
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 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 ) );

ex b

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

b

proof end;

uniqueness for b

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

b

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

b

b

proof end;

:: deftheorem lif defines lift FIELD_7:def 10 :

for F being Field

for E being b_{1} -finite FieldExtension of F

for K being b_{1} -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 b_{7} being Linear_Combination of Base (BE,BK) holds

( b_{7} = 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

b_{7} . (a * b) = l2 . a ) ) );

for F being Field

for E being b

for K being b

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 b

( b

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

b

theorem :: FIELD_7:22

for F being Field

for E being b_{1} -finite FieldExtension of F

for K being b_{1} -extending b_{2} -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

for E being b

for K being b

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 b_{1} -finite FieldExtension of F

for K being b_{1} -extending b_{2} -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

for E being b

for K being b

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 b_{1} -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))

for E being FieldExtension of F

for K being b

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 b_{1} -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)

for E being FieldExtension of F

for K being b

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 b

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 (Carrier l) = 1 holds

Sum l = Sum (down l)

proof end;

theorem TSum: :: FIELD_7:26

for F being Field

for E being b_{1} -finite FieldExtension of F

for K being b_{1} -extending b_{2} -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)

for E being b

for K being b

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 b_{1} -finite FieldExtension of F

for K being b_{1} -extending b_{2} -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 = {}

for E being b

for K being b

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 b_{1} -finite FieldExtension of F

for K being b_{1} -extending b_{2} -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)) #)

for E being b

for K being b

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;

theorem BasKEF: :: FIELD_7:29

for F being Field

for E being b_{1} -finite FieldExtension of F

for K being b_{1} -extending b_{2} -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))

for E being b

for K being b

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 b_{1} -finite FieldExtension of F

for K being b_{1} -extending b_{2} -finite FieldExtension of F holds deg (K,F) = (deg (K,E)) * (deg (E,F))

for E being b

for K being b

proof end;

theorem alg0: :: FIELD_7:31

for F being Field

for E being FieldExtension of F

for K being b_{2} -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) )

for E being FieldExtension of F

for K being b

( 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;

for b_{1} being F -extending E -finite FieldExtension of F holds b_{1} is F -finite

end;
let E be F -finite FieldExtension of F;

cluster non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative F -extending E -extending E -finite -> F -extending F -finite E -finite for doubleLoopStr ;

coherence for b

proof end;

lintrans: for F being Field

for E1 being FieldExtension of F

for E2 being b

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;

end;
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 ;

for a being Element of E holds a is F -algebraic ;

:: 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 );

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 b

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;

for b_{1} being FieldExtension of F st b_{1} is F -finite holds

b_{1} is F -algebraic

end;
cluster non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative F -extending F -finite -> F -algebraic for doubleLoopStr ;

coherence for b

b

proof end;

registration

let F be Field;

let E be F -algebraic FieldExtension of F;

coherence

for b_{1} being Element of E holds b_{1} is F -algebraic
by defa;

end;
let E be F -algebraic FieldExtension of F;

coherence

for b

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 )

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 b_{1} -finite FieldExtension of F st

( E is B -extending & a in B ) )

for E being FieldExtension of F

for a being Element of E holds

( a is F -algebraic iff ex B being b

( 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;

end;
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 ;

for a being Element of E st a in T holds

a is F -algebraic ;

:: 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 );

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;

existence

ex b_{1} being Subset of E st

( b_{1} is finite & b_{1} is F -algebraic )

end;
let E be FieldExtension of F;

existence

ex b

( b

proof 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

FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1})

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

FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1})

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

FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,{b})),T1)

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

FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,{b})),T1)

proof end;

registration

let F be Field;

let E be FieldExtension of F;

let T be finite F -algebraic Subset of E;

coherence

FAdj (F,T) is F -finite

end;
let E be FieldExtension of F;

let T be finite F -algebraic Subset of E;

coherence

FAdj (F,T) is F -finite

proof end;

theorem ft1: :: FIELD_7:36

for F being Field

for E being FieldExtension of F

for a being b_{1} -algebraic Element of E holds

( E == FAdj (F,{a}) iff deg (MinPoly (a,F)) = deg (E,F) )

for E being FieldExtension of F

for a being b

( 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 b_{1} -algebraic Subset of E st E == FAdj (F,T) )

for E being FieldExtension of F holds

( E is F -finite iff ex T being finite b

proof 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);

coherence

Roots (E,p) is F -algebraic

end;
let E be FieldExtension of F;

let p be non zero Element of the carrier of (Polynom-Ring F);

coherence

Roots (E,p) is F -algebraic

proof 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 (Polynom-Ring F) holds FAdj (F,(Roots (E,p))) is F -algebraic ;

for 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 :: FIELD_7:39

for F being Field

for E being FieldExtension of F

for K being b_{2} -extending FieldExtension of F st K is E -algebraic & E is F -algebraic holds

K is F -algebraic

for E being FieldExtension of F

for K being b

K is F -algebraic

proof end;

theorem :: FIELD_7:40

for F being Field

for E being FieldExtension of F

for K being b_{2} -extending FieldExtension of F st K is F -algebraic holds

( K is E -algebraic & E is F -algebraic )

for E being FieldExtension of F

for K being b

( 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;

coherence

FAdj (F,{a,b}) is F -finite

end;
let E be FieldExtension of F;

let a, b be F -algebraic Element of E;

coherence

FAdj (F,{a,b}) is F -finite

proof end;

registration

let F be Field;

let E be FieldExtension of F;

coherence

0. E is F -algebraic

1. E is F -algebraic

end;
let E be FieldExtension of F;

coherence

0. E is F -algebraic

proof end;

coherence 1. 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;

coherence

a + b is F -algebraic

a - b is F -algebraic

a * b is F -algebraic

end;
let E be FieldExtension of F;

let a, b be F -algebraic Element of E;

coherence

a + b is F -algebraic

proof end;

coherence a - b is F -algebraic

proof end;

coherence a * b is F -algebraic

proof end;

registration

let F be Field;

let E be FieldExtension of F;

let a be F -algebraic Element of E;

coherence

- a is F -algebraic

end;
let E be FieldExtension of F;

let a be F -algebraic Element of E;

coherence

- a is F -algebraic

proof end;

registration

let F be Field;

let E be FieldExtension of F;

let a be non zero F -algebraic Element of E;

coherence

a " is F -algebraic

end;
let E be FieldExtension of F;

let a be non zero F -algebraic Element of E;

coherence

a " is F -algebraic

proof end;

definition

let F be Field;

let E be FieldExtension of F;

{ a where a is F -algebraic Element of E : verum } is Subset of E

end;
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 } ;

{ a where a is F -algebraic Element of E : verum } is Subset of E

proof 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 b_{1} -algebraic Element of E : verum } ;

for F being Field

for E being FieldExtension of F holds Alg_El E = { a where a is b

definition

let F be Field;

let E be FieldExtension of F;

ex b_{1} being strict doubleLoopStr st

( the carrier of b_{1} = Alg_El E & the addF of b_{1} = the addF of E || the carrier of b_{1} & the multF of b_{1} = the multF of E || the carrier of b_{1} & the OneF of b_{1} = 1. E & the ZeroF of b_{1} = 0. E )

for b_{1}, b_{2} being strict doubleLoopStr st the carrier of b_{1} = Alg_El E & the addF of b_{1} = the addF of E || the carrier of b_{1} & the multF of b_{1} = the multF of E || the carrier of b_{1} & the OneF of b_{1} = 1. E & the ZeroF of b_{1} = 0. E & the carrier of b_{2} = Alg_El E & the addF of b_{2} = the addF of E || the carrier of b_{2} & the multF of b_{2} = the multF of E || the carrier of b_{2} & the OneF of b_{2} = 1. E & the ZeroF of b_{2} = 0. E holds

b_{1} = b_{2}
;

end;
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 ( 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 );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem d defines Field_of_Algebraic_Elements FIELD_7:def 14 :

for F being Field

for E being FieldExtension of F

for b_{3} being strict doubleLoopStr holds

( b_{3} = Field_of_Algebraic_Elements E iff ( the carrier of b_{3} = Alg_El E & the addF of b_{3} = the addF of E || the carrier of b_{3} & the multF of b_{3} = the multF of E || the carrier of b_{3} & the OneF of b_{3} = 1. E & the ZeroF of b_{3} = 0. E ) );

for F being Field

for E being FieldExtension of F

for b

( b

notation
end;

registration
end;

Lm10: for R being Field

for E being FieldExtension of R

for x being Element of (F_Alg E) 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 (F_Alg E) 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 (F_Alg S) st a = x & b = y holds

a * b = x * y

proof end;

registration

let F be Field;

let E be FieldExtension of F;

( F_Alg E is Abelian & F_Alg E is add-associative & F_Alg E is right_zeroed & F_Alg E is right_complementable )

end;
let E be FieldExtension of F;

cluster Field_of_Algebraic_Elements E -> right_complementable strict Abelian add-associative right_zeroed ;

coherence ( F_Alg E is Abelian & F_Alg E is add-associative & F_Alg E is right_zeroed & F_Alg E is right_complementable )

proof end;

registration

let F be Field;

let E be FieldExtension of F;

( F_Alg E is commutative & F_Alg E is associative & F_Alg E is well-unital & F_Alg E is distributive & F_Alg E is almost_left_invertible )

end;
let E be FieldExtension of F;

cluster Field_of_Algebraic_Elements E -> almost_left_invertible strict well-unital distributive associative commutative ;

coherence ( F_Alg E is commutative & F_Alg E is associative & F_Alg E is well-unital & F_Alg E is distributive & F_Alg E is almost_left_invertible )

proof end;

ee: for F being Field

for E being FieldExtension of F holds E is FieldExtension of F_Alg E

proof end;

registration
end;

registration
end;

theorem :: FIELD_7:41

theorem :: FIELD_7:42

t2: for F being Field

for E being b

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

for E being FieldExtension of F

for K being FieldExtension of E holds F_Alg K is FieldExtension of F_Alg E

proof end;