:: by Christoph Schwarzweller

::

:: Received October 25, 2020

:: Copyright (c) 2020-2021 Association of Mizar Users

registration

let R be non degenerated non almost_left_invertible comRing;

coherence

not {(0. R)} -Ideal is maximal

end;
coherence

not {(0. R)} -Ideal is maximal

proof end;

:: deftheorem deffc defines field-containing FIELD_6:def 1 :

for R being Ring holds

( R is field-containing iff ex F being Field st F is Subring of R );

for R being Ring holds

( R is field-containing iff ex F being Field st F is Subring of R );

registration

ex b_{1} being Ring st b_{1} is field-containing
end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Abelian add-associative right_zeroed V123() right-distributive left-distributive right_unital well-unital distributive left_unital unital associative V254() V255() V256() V257() K745() -homomorphic field-containing for doubleLoopStr ;

existence ex b

proof end;

definition
end;

:: deftheorem defsubfr defines Subfield FIELD_6:def 2 :

for R being field-containing Ring

for b_{2} being Field holds

( b_{2} is Subfield of R iff b_{2} is Subring of R );

for R being field-containing Ring

for b

( b

registration

let R be non degenerated Ring;

let p be non zero Polynomial of R;

coherence

not LM p is zero

end;
let p be non zero Polynomial of R;

coherence

not LM p is zero

proof end;

theorem thdLM: :: FIELD_6:5

for R being non degenerated Ring

for p being non zero Polynomial of R holds deg (p - (LM p)) < deg p

for p being non zero Polynomial of R holds deg (p - (LM p)) < deg p

proof end;

theorem thE1: :: FIELD_6:6

for R being Ring

for p being Polynomial of R

for i being Nat holds (<%(0. R),(1. R)%> *' p) . (i + 1) = p . i

for p being Polynomial of R

for i being Nat holds (<%(0. R),(1. R)%> *' p) . (i + 1) = p . i

proof end;

theorem :: FIELD_6:8

for R being domRing

for p being non zero Polynomial of R holds deg (<%(0. R),(1. R)%> *' p) = (deg p) + 1

for p being non zero Polynomial of R holds deg (<%(0. R),(1. R)%> *' p) = (deg p) + 1

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;

help3a: for R being domRing

for n being Element of NAT st n <> 0 holds

for a being Element of R holds eval ((<%(0. R),(1. R)%> `^ n),a) = a |^ n

proof end;

theorem :: FIELD_6:9

for R being comRing

for p being Polynomial of R

for a being Element of R holds eval ((<%(0. R),(1. R)%> *' p),a) = a * (eval (p,a))

for p being Polynomial of R

for a being Element of R holds eval ((<%(0. R),(1. R)%> *' p),a) = a * (eval (p,a))

proof end;

ThR1: for R being Ring holds R is Subring of R

by LIOUVIL2:18;

theorem FIELD427: :: FIELD_6:10

for R being Ring

for S being RingExtension of R

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

for a being Element of R

for b being Element of S st b = a holds

Ext_eval (p,b) = eval (p,a)

for S being RingExtension of R

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

for a being Element of R

for b being Element of S st b = a holds

Ext_eval (p,b) = eval (p,a)

proof end;

theorem lemma7: :: FIELD_6:11

for F being Field

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

for E being FieldExtension of F

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

for a being Element of E

for b being Element of K 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 K being b

for a being Element of E

for b being Element of K st a = b holds

Ext_eval (p,a) = Ext_eval (p,b)

proof end;

registration

let L be non empty ZeroStr ;

let a, b be Element of L;

let f be the carrier of L -valued Function;

let x, y be object ;

coherence

f +* ((x,y) --> (a,b)) is the carrier of L -valued

end;
let a, b be Element of L;

let f be the carrier of L -valued Function;

let x, y be object ;

coherence

f +* ((x,y) --> (a,b)) is the carrier of L -valued

proof end;

registration

let L be non empty ZeroStr ;

let a, b be Element of L;

let f be finite-Support sequence of L;

let x, y be object ;

coherence

for b_{1} being sequence of L st b_{1} = f +* ((x,y) --> (a,b)) holds

b_{1} is finite-Support

end;
let a, b be Element of L;

let f be finite-Support sequence of L;

let x, y be object ;

coherence

for b

b

proof end;

theorem Th6: :: FIELD_6:13

for S being Ring

for R1, R2 being Subring of S holds

( R1 is Subring of R2 iff the carrier of R1 c= the carrier of R2 )

for R1, R2 being Subring of S holds

( R1 is Subring of R2 iff the carrier of R1 c= the carrier of R2 )

proof end;

theorem RE1: :: FIELD_6:14

for S being Ring

for R1, R2 being strict Subring of S holds

( R1 = R2 iff the carrier of R1 = the carrier of R2 )

for R1, R2 being strict Subring of S holds

( R1 = R2 iff the carrier of R1 = the carrier of R2 )

proof end;

theorem Th17: :: FIELD_6:15

for S being Ring

for R being Subring of S

for x, y being Element of S

for x1, y1 being Element of R st x = x1 & y = y1 holds

x + y = x1 + y1

for R being Subring of S

for x, y being Element of S

for x1, y1 being Element of R st x = x1 & y = y1 holds

x + y = x1 + y1

proof end;

theorem Th18: :: FIELD_6:16

for S being Ring

for R being Subring of S

for x, y being Element of S

for x1, y1 being Element of R st x = x1 & y = y1 holds

x * y = x1 * y1

for R being Subring of S

for x, y being Element of S

for x1, y1 being Element of R st x = x1 & y = y1 holds

x * y = x1 * y1

proof end;

theorem Th19: :: FIELD_6:17

for S being Ring

for R being Subring of S

for x being Element of S

for x1 being Element of R st x = x1 holds

- x = - x1

for R being Subring of S

for x being Element of S

for x1 being Element of R st x = x1 holds

- x = - x1

proof end;

theorem Th19f: :: FIELD_6:18

for E being Field

for F being Subfield of E

for x being non zero Element of E

for x1 being Element of F st x = x1 holds

x " = x1 "

for F being Subfield of E

for x being non zero Element of E

for x1 being Element of F st x = x1 holds

x " = x1 "

proof end;

theorem pr5: :: FIELD_6:19

for S being Ring

for R being Subring of S

for x being Element of S

for x1 being Element of R

for n being Element of NAT st x = x1 holds

x |^ n = x1 |^ n

for R being Subring of S

for x being Element of S

for x1 being Element of R

for n being Element of NAT st x = x1 holds

x |^ n = x1 |^ n

proof end;

theorem pr20: :: FIELD_6:20

for S being Ring

for R being Subring of S

for x1, x2 being Element of S

for y1, y2 being Element of R st x1 = y1 & x2 = y2 holds

<%x1,x2%> = <%y1,y2%>

for R being Subring of S

for x1, x2 being Element of S

for y1, y2 being Element of R st x1 = y1 & x2 = y2 holds

<%x1,x2%> = <%y1,y2%>

proof end;

theorem helpp: :: FIELD_6:21

for R being comRing

for S being comRingExtension of R

for x1, x2 being Element of S

for y1, y2 being Element of R

for n being Element of NAT st x1 = y1 & x2 = y2 holds

<%x1,x2%> `^ n = <%y1,y2%> `^ n

for S being comRingExtension of R

for x1, x2 being Element of S

for y1, y2 being Element of R

for n being Element of NAT st x1 = y1 & x2 = y2 holds

<%x1,x2%> `^ n = <%y1,y2%> `^ n

proof end;

theorem help3: :: FIELD_6:22

for R being domRing

for S being domRingExtension of R

for n being non zero Element of NAT

for a being Element of S holds Ext_eval ((<%(0. R),(1. R)%> `^ n),a) = a |^ n

for S being domRingExtension of R

for n being non zero Element of NAT

for a being Element of S holds Ext_eval ((<%(0. R),(1. R)%> `^ n),a) = a |^ n

proof end;

Th28: for L being non empty ZeroStr

for a being Element of L holds

( (a | L) . 0 = a & ( for n being Nat st n <> 0 holds

(a | L) . n = 0. L ) )

proof end;

theorem constpol: :: FIELD_6:23

for R being Ring

for S being RingExtension of R

for a being Element of R

for b being Element of S st a = b holds

a | R = b | S

for S being RingExtension of R

for a being Element of R

for b being Element of S st a = b holds

a | R = b | S

proof end;

theorem pr0: :: FIELD_6:24

for F being Field

for E being FieldExtension of F

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

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

NormPolynomial p = NormPolynomial q

for E being FieldExtension of F

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

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

NormPolynomial p = NormPolynomial q

proof end;

theorem pr1: :: FIELD_6:25

for F being Field

for E being FieldExtension of F

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

for a being Element of E holds

( Ext_eval (p,a) = 0. E iff Ext_eval ((NormPolynomial p),a) = 0. E )

for E being FieldExtension of F

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

for a being Element of E holds

( Ext_eval (p,a) = 0. E iff Ext_eval ((NormPolynomial p),a) = 0. E )

proof end;

theorem exevalminus: :: FIELD_6:26

for R being Ring

for S being RingExtension of R

for a being Element of S

for p being Polynomial of R holds Ext_eval ((- p),a) = - (Ext_eval (p,a))

for S being RingExtension of R

for a being Element of S

for p being Polynomial of R holds Ext_eval ((- p),a) = - (Ext_eval (p,a))

proof end;

theorem exevalminus2: :: FIELD_6:27

for R being Ring

for S being RingExtension of R

for a being Element of S

for p, q being Polynomial of R holds Ext_eval ((p - q),a) = (Ext_eval (p,a)) - (Ext_eval (q,a))

for S being RingExtension of R

for a being Element of S

for p, q being Polynomial of R holds Ext_eval ((p - q),a) = (Ext_eval (p,a)) - (Ext_eval (q,a))

proof end;

theorem exevalconst: :: FIELD_6:28

for R being Ring

for S being RingExtension of R

for a being Element of S

for p being constant Polynomial of R holds Ext_eval (p,a) = LC p

for S being RingExtension of R

for a being Element of S

for p being constant Polynomial of R holds Ext_eval (p,a) = LC p

proof end;

theorem exevalLM: :: FIELD_6:29

for R being non degenerated Ring

for S being RingExtension of R

for a, b being Element of S

for p being non zero Polynomial of R st b = LC p holds

Ext_eval ((Leading-Monomial p),a) = b * (a |^ (deg p))

for S being RingExtension of R

for a, b being Element of S

for p being non zero Polynomial of R st b = LC p holds

Ext_eval ((Leading-Monomial p),a) = b * (a |^ (deg p))

proof end;

definition

let R be Ring;

let S be RingExtension of R;

let T be Subset of S;

{ x where x is Element of S : for U being Subring of S st R is Subring of U & T is Subset of U holds

x in U } is non empty Subset of S

end;
let S be RingExtension of R;

let T be Subset of S;

func carrierRA T -> non empty Subset of S equals :: FIELD_6:def 3

{ x where x is Element of S : for U being Subring of S st R is Subring of U & T is Subset of U holds

x in U } ;

coherence { x where x is Element of S : for U being Subring of S st R is Subring of U & T is Subset of U holds

x in U } ;

{ x where x is Element of S : for U being Subring of S st R is Subring of U & T is Subset of U holds

x in U } is non empty Subset of S

proof end;

:: deftheorem defines carrierRA FIELD_6:def 3 :

for R being Ring

for S being RingExtension of R

for T being Subset of S holds carrierRA T = { x where x is Element of S : for U being Subring of S st R is Subring of U & T is Subset of U holds

x in U } ;

for R being Ring

for S being RingExtension of R

for T being Subset of S holds carrierRA T = { x where x is Element of S : for U being Subring of S st R is Subring of U & T is Subset of U holds

x in U } ;

definition

let R be Ring;

let S be RingExtension of R;

let T be Subset of S;

ex b_{1} being strict doubleLoopStr st

( the carrier of b_{1} = carrierRA T & the addF of b_{1} = the addF of S || (carrierRA T) & the multF of b_{1} = the multF of S || (carrierRA T) & the OneF of b_{1} = 1. S & the ZeroF of b_{1} = 0. S )

for b_{1}, b_{2} being strict doubleLoopStr st the carrier of b_{1} = carrierRA T & the addF of b_{1} = the addF of S || (carrierRA T) & the multF of b_{1} = the multF of S || (carrierRA T) & the OneF of b_{1} = 1. S & the ZeroF of b_{1} = 0. S & the carrier of b_{2} = carrierRA T & the addF of b_{2} = the addF of S || (carrierRA T) & the multF of b_{2} = the multF of S || (carrierRA T) & the OneF of b_{2} = 1. S & the ZeroF of b_{2} = 0. S holds

b_{1} = b_{2}
;

end;
let S be RingExtension of R;

let T be Subset of S;

func RingAdjunction (R,T) -> strict doubleLoopStr means :dRA: :: FIELD_6:def 4

( the carrier of it = carrierRA T & the addF of it = the addF of S || (carrierRA T) & the multF of it = the multF of S || (carrierRA T) & the OneF of it = 1. S & the ZeroF of it = 0. S );

existence ( the carrier of it = carrierRA T & the addF of it = the addF of S || (carrierRA T) & the multF of it = the multF of S || (carrierRA T) & the OneF of it = 1. S & the ZeroF of it = 0. S );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem dRA defines RingAdjunction FIELD_6:def 4 :

for R being Ring

for S being RingExtension of R

for T being Subset of S

for b_{4} being strict doubleLoopStr holds

( b_{4} = RingAdjunction (R,T) iff ( the carrier of b_{4} = carrierRA T & the addF of b_{4} = the addF of S || (carrierRA T) & the multF of b_{4} = the multF of S || (carrierRA T) & the OneF of b_{4} = 1. S & the ZeroF of b_{4} = 0. S ) );

for R being Ring

for S being RingExtension of R

for T being Subset of S

for b

( b

notation

let R be Ring;

let S be RingExtension of R;

let T be Subset of S;

synonym RAdj (R,T) for RingAdjunction (R,T);

end;
let S be RingExtension of R;

let T be Subset of S;

synonym RAdj (R,T) for RingAdjunction (R,T);

registration

let R be Ring;

let S be RingExtension of R;

let T be Subset of S;

coherence

not RAdj (R,T) is empty

end;
let S be RingExtension of R;

let T be Subset of S;

coherence

not RAdj (R,T) is empty

proof end;

registration

let R be non degenerated Ring;

let S be RingExtension of R;

let T be Subset of S;

coherence

not RAdj (R,T) is degenerated

end;
let S be RingExtension of R;

let T be Subset of S;

coherence

not RAdj (R,T) is degenerated

proof end;

Lm10: for R being Ring

for S being RingExtension of R

for T being Subset of S

for x being Element of (RAdj (R,T)) holds x is Element of S

proof end;

Lm11: for R being Ring

for S being RingExtension of R

for T being Subset of S

for a, b being Element of S

for x, y being Element of (RAdj (R,T)) st a = x & b = y holds

a + b = x + y

proof end;

Lm12: for R being Ring

for S being RingExtension of R

for T being Subset of S

for a, b being Element of S

for x, y being Element of (RAdj (R,T)) st a = x & b = y holds

a * b = x * y

proof end;

registration

let R be Ring;

let S be RingExtension of R;

let T be Subset of S;

coherence

( RAdj (R,T) is Abelian & RAdj (R,T) is add-associative & RAdj (R,T) is right_zeroed & RAdj (R,T) is right_complementable )

end;
let S be RingExtension of R;

let T be Subset of S;

coherence

( RAdj (R,T) is Abelian & RAdj (R,T) is add-associative & RAdj (R,T) is right_zeroed & RAdj (R,T) is right_complementable )

proof end;

registration

let R be comRing;

let S be comRingExtension of R;

let T be Subset of S;

coherence

RAdj (R,T) is commutative

end;
let S be comRingExtension of R;

let T be Subset of S;

coherence

RAdj (R,T) is commutative

proof end;

registration

let R be Ring;

let S be RingExtension of R;

let T be Subset of S;

coherence

( RAdj (R,T) is associative & RAdj (R,T) is well-unital & RAdj (R,T) is distributive )

end;
let S be RingExtension of R;

let T be Subset of S;

coherence

( RAdj (R,T) is associative & RAdj (R,T) is well-unital & RAdj (R,T) is distributive )

proof end;

theorem RAt: :: FIELD_6:30

for R being Ring

for S being RingExtension of R

for T being Subset of S holds T is Subset of (RAdj (R,T))

for S being RingExtension of R

for T being Subset of S holds T is Subset of (RAdj (R,T))

proof end;

theorem RAsub: :: FIELD_6:31

for R being Ring

for S being RingExtension of R

for T being Subset of S holds R is Subring of RAdj (R,T)

for S being RingExtension of R

for T being Subset of S holds R is Subring of RAdj (R,T)

proof end;

theorem RAsub2: :: FIELD_6:32

for R being Ring

for S being RingExtension of R

for T being Subset of S

for U being Subring of S st R is Subring of U & T is Subset of U holds

RAdj (R,T) is Subring of U

for S being RingExtension of R

for T being Subset of S

for U being Subring of S st R is Subring of U & T is Subset of U holds

RAdj (R,T) is Subring of U

proof end;

theorem :: FIELD_6:33

for R being strict Ring

for S being RingExtension of R

for T being Subset of S holds

( RAdj (R,T) = R iff T is Subset of R )

for S being RingExtension of R

for T being Subset of S holds

( RAdj (R,T) = R iff T is Subset of R )

proof end;

definition

let R be Ring;

let S be RingExtension of R;

let T be Subset of S;

:: original: RingAdjunction

redefine func RAdj (R,T) -> strict Subring of S;

coherence

RingAdjunction (R,T) is strict Subring of S

end;
let S be RingExtension of R;

let T be Subset of S;

:: original: RingAdjunction

redefine func RAdj (R,T) -> strict Subring of S;

coherence

RingAdjunction (R,T) is strict Subring of S

proof end;

registration

let R be Ring;

let S be RingExtension of R;

let T be Subset of S;

coherence

RAdj (R,T) is R -extending

end;
let S be RingExtension of R;

let T be Subset of S;

coherence

RAdj (R,T) is R -extending

proof end;

registration

let F be Field;

let R be RingExtension of F;

let T be Subset of R;

coherence

RAdj (F,T) is field-containing

end;
let R be RingExtension of F;

let T be Subset of R;

coherence

RAdj (F,T) is field-containing

proof end;

theorem :: FIELD_6:34

for F being Field

for R being RingExtension of F

for T being Subset of R holds F is Subfield of RAdj (F,T)

for R being RingExtension of F

for T being Subset of R holds F is Subfield of RAdj (F,T)

proof end;

definition

let F be Field;

let E be FieldExtension of F;

let T be Subset of E;

{ 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 } is non empty Subset of E

end;
let E be FieldExtension of F;

let T be Subset of E;

func carrierFA T -> non empty Subset of E equals :: FIELD_6:def 5

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

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

{ 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 } is non empty Subset of E

proof end;

:: deftheorem defines carrierFA FIELD_6:def 5 :

for F being Field

for E being FieldExtension of F

for T being Subset of E holds 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 } ;

for F being Field

for E being FieldExtension of F

for T being Subset of E holds 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 } ;

definition

let F be Field;

let E be FieldExtension of F;

let T be Subset of E;

ex b_{1} being strict doubleLoopStr st

( the carrier of b_{1} = carrierFA T & the addF of b_{1} = the addF of E || (carrierFA T) & the multF of b_{1} = the multF of E || (carrierFA T) & 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} = carrierFA T & the addF of b_{1} = the addF of E || (carrierFA T) & the multF of b_{1} = the multF of E || (carrierFA T) & the OneF of b_{1} = 1. E & the ZeroF of b_{1} = 0. E & the carrier of b_{2} = carrierFA T & the addF of b_{2} = the addF of E || (carrierFA T) & the multF of b_{2} = the multF of E || (carrierFA T) & 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;

let T be Subset of E;

func FieldAdjunction (F,T) -> strict doubleLoopStr means :dFA: :: FIELD_6:def 6

( the carrier of it = carrierFA T & the addF of it = the addF of E || (carrierFA T) & the multF of it = the multF of E || (carrierFA T) & the OneF of it = 1. E & the ZeroF of it = 0. E );

existence ( the carrier of it = carrierFA T & the addF of it = the addF of E || (carrierFA T) & the multF of it = the multF of E || (carrierFA T) & 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 dFA defines FieldAdjunction FIELD_6:def 6 :

for F being Field

for E being FieldExtension of F

for T being Subset of E

for b_{4} being strict doubleLoopStr holds

( b_{4} = FieldAdjunction (F,T) iff ( the carrier of b_{4} = carrierFA T & the addF of b_{4} = the addF of E || (carrierFA T) & the multF of b_{4} = the multF of E || (carrierFA T) & the OneF of b_{4} = 1. E & the ZeroF of b_{4} = 0. E ) );

for F being Field

for E being FieldExtension of F

for T being Subset of E

for b

( b

notation

let F be Field;

let E be FieldExtension of F;

let T be Subset of E;

synonym FAdj (F,T) for FieldAdjunction (F,T);

end;
let E be FieldExtension of F;

let T be Subset of E;

synonym FAdj (F,T) for FieldAdjunction (F,T);

registration

let F be Field;

let E be FieldExtension of F;

let T be Subset of E;

coherence

not FAdj (F,T) is degenerated

end;
let E be FieldExtension of F;

let T be Subset of E;

coherence

not FAdj (F,T) is degenerated

proof end;

Lm10f: for R being Field

for S being FieldExtension of R

for T being Subset of S

for x being Element of (FAdj (R,T)) holds x is Element of S

proof end;

Lm11f: for R being Field

for S being FieldExtension of R

for T being Subset of S

for a, b being Element of S

for x, y being Element of (FAdj (R,T)) st a = x & b = y holds

a + b = x + y

proof end;

Lm12f: for R being Field

for S being FieldExtension of R

for T being Subset of S

for a, b being Element of S

for x, y being Element of (FAdj (R,T)) st a = x & b = y holds

a * b = x * y

proof end;

registration

let F be Field;

let E be FieldExtension of F;

let T be Subset of E;

coherence

( FAdj (F,T) is Abelian & FAdj (F,T) is add-associative & FAdj (F,T) is right_zeroed & FAdj (F,T) is right_complementable )

end;
let E be FieldExtension of F;

let T be Subset of E;

coherence

( FAdj (F,T) is Abelian & FAdj (F,T) is add-associative & FAdj (F,T) is right_zeroed & FAdj (F,T) is right_complementable )

proof end;

registration

let F be Field;

let E be FieldExtension of F;

let T be Subset of E;

( FieldAdjunction (F,T) is commutative & FieldAdjunction (F,T) is associative & FieldAdjunction (F,T) is well-unital & FieldAdjunction (F,T) is distributive & FieldAdjunction (F,T) is almost_left_invertible )

end;
let E be FieldExtension of F;

let T be Subset of E;

cluster FieldAdjunction (F,T) -> almost_left_invertible strict well-unital distributive associative commutative ;

coherence ( FieldAdjunction (F,T) is commutative & FieldAdjunction (F,T) is associative & FieldAdjunction (F,T) is well-unital & FieldAdjunction (F,T) is distributive & FieldAdjunction (F,T) is almost_left_invertible )

proof end;

theorem FAt: :: FIELD_6:35

for F being Field

for E being FieldExtension of F

for T being Subset of E holds T is Subset of (FAdj (F,T))

for E being FieldExtension of F

for T being Subset of E holds T is Subset of (FAdj (F,T))

proof end;

theorem FAsub: :: FIELD_6:36

for F being Field

for E being FieldExtension of F

for T being Subset of E holds F is Subfield of FAdj (F,T)

for E being FieldExtension of F

for T being Subset of E holds F is Subfield of FAdj (F,T)

proof end;

theorem FAsub2: :: FIELD_6:37

for F being Field

for E being FieldExtension of F

for T being Subset of E

for U being Subfield of E st F is Subfield of U & T is Subset of U holds

FAdj (F,T) is Subfield of U

for E being FieldExtension of F

for T being Subset of E

for U being Subfield of E st F is Subfield of U & T is Subset of U holds

FAdj (F,T) is Subfield of U

proof end;

theorem :: FIELD_6:38

for F being strict 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;

definition

let F be Field;

let E be FieldExtension of F;

let T be Subset of E;

:: original: FieldAdjunction

redefine func FAdj (F,T) -> strict Subfield of E;

coherence

FieldAdjunction (F,T) is strict Subfield of E

end;
let E be FieldExtension of F;

let T be Subset of E;

:: original: FieldAdjunction

redefine func FAdj (F,T) -> strict Subfield of E;

coherence

FieldAdjunction (F,T) is strict Subfield of E

proof end;

registration

let F be Field;

let E be FieldExtension of F;

let T be Subset of E;

coherence

FAdj (F,T) is F -extending

end;
let E be FieldExtension of F;

let T be Subset of E;

coherence

FAdj (F,T) is F -extending

proof end;

theorem RF: :: FIELD_6:39

for F being Field

for E being FieldExtension of F

for T being Subset of E holds RAdj (F,T) is Subring of FAdj (F,T)

for E being FieldExtension of F

for T being Subset of E holds RAdj (F,T) is Subring of FAdj (F,T)

proof end;

theorem RF2: :: FIELD_6:40

for F being Field

for E being FieldExtension of F

for T being Subset of E holds

( RAdj (F,T) = FAdj (F,T) iff RAdj (F,T) is Field )

for E being FieldExtension of F

for T being Subset of E holds

( RAdj (F,T) = FAdj (F,T) iff RAdj (F,T) is Field )

proof end;

lcsub1: for F being Field

for E being FieldExtension of F

for a being Element of E

for n being Element of NAT holds a |^ n in the carrier of (FAdj (F,{a}))

proof end;

registration

let R be non degenerated comRing;

let S be comRingExtension of R;

let a be Element of S;

coherence

( hom_Ext_eval (a,R) is additive & hom_Ext_eval (a,R) is multiplicative & hom_Ext_eval (a,R) is unity-preserving )

end;
let S be comRingExtension of R;

let a be Element of S;

coherence

( hom_Ext_eval (a,R) is additive & hom_Ext_eval (a,R) is multiplicative & hom_Ext_eval (a,R) is unity-preserving )

proof end;

registration

let R be non degenerated comRing;

for b_{1} being comRingExtension of R holds b_{1} is Polynom-Ring R -homomorphic

end;
cluster non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative R -extending -> Polynom-Ring R -homomorphic for doubleLoopStr ;

coherence for b

proof end;

registration

let F be Field;

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

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 Abelian add-associative right_zeroed V123() right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like V254() V255() V256() V257() PID Polynom-Ring F -homomorphic K745() -homomorphic factorial F -extending for doubleLoopStr ;

existence ex b

proof end;

:: deftheorem defines -algebraic FIELD_6:def 7 :

for F being Field

for E being FieldExtension of F

for a being Element of E holds

( a is F -algebraic iff ker (hom_Ext_eval (a,F)) <> {(0. (Polynom-Ring F))} );

for F being Field

for E being FieldExtension of F

for a being Element of E holds

( a is F -algebraic iff ker (hom_Ext_eval (a,F)) <> {(0. (Polynom-Ring F))} );

notation

let F be Field;

let E be FieldExtension of F;

let a be Element of E;

antonym F -transcendental a for F -algebraic ;

end;
let E be FieldExtension of F;

let a be Element of E;

antonym F -transcendental a for F -algebraic ;

theorem alg0: :: FIELD_6:41

for R being Ring

for S being RingExtension of R

for a being Element of S holds Ann_Poly (a,R) = ker (hom_Ext_eval (a,R))

for S being RingExtension of R

for a being Element of S holds Ann_Poly (a,R) = ker (hom_Ext_eval (a,R))

proof end;

theorem alg1: :: FIELD_6:42

for F being Field

for E being FieldExtension of F

for a being Element of E holds

( a is F -algebraic iff a is_integral_over F )

for E being FieldExtension of F

for a being Element of E holds

( a is F -algebraic iff a is_integral_over F )

proof end;

theorem alg00: :: FIELD_6:43

for F being Field

for E being FieldExtension of F

for a being Element of E holds

( a is F -algebraic iff ex p being non zero Polynomial of F st Ext_eval (p,a) = 0. E )

for E being FieldExtension of F

for a being Element of E holds

( a is F -algebraic iff ex p being non zero Polynomial of F st Ext_eval (p,a) = 0. E )

proof end;

registration

let F be Field;

let E be FieldExtension of F;

ex b_{1} being Element of E st b_{1} is F -algebraic

end;
let E be FieldExtension of F;

cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable non irreducible F -algebraic for Element of the carrier of E;

existence ex b

proof end;

lemphi1: for F being Field

for E being FieldExtension of F

for a being Element of E holds rng (hom_Ext_eval (a,F)) = { (Ext_eval (p,a)) where p is Polynomial of F : verum }

proof end;

lemphi2: for F being Field

for E being FieldExtension of F

for a being Element of E holds rng (hom_Ext_eval (a,F)) c= the carrier of (RAdj (F,{a}))

proof end;

lemphi3: for F being Field

for E being Polynom-Ring b

for a being Element of E holds F is Subring of Image (hom_Ext_eval (a,F))

proof end;

theorem lemphi4: :: FIELD_6:44

for F being Field

for E being Polynom-Ring b_{1} -homomorphic FieldExtension of F

for a being Element of E holds RAdj (F,{a}) = Image (hom_Ext_eval (a,F))

for E being Polynom-Ring b

for a being Element of E holds RAdj (F,{a}) = Image (hom_Ext_eval (a,F))

proof end;

theorem lemphi5: :: FIELD_6:45

for F being Field

for E being Polynom-Ring b_{1} -homomorphic FieldExtension of F

for a being Element of E holds the carrier of (RAdj (F,{a})) = { (Ext_eval (p,a)) where p is Polynomial of F : verum }

for E being Polynom-Ring b

for a being Element of E holds the carrier of (RAdj (F,{a})) = { (Ext_eval (p,a)) where p is Polynomial of F : verum }

proof end;

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;

Lm12a: for F being Ring

for E being RingExtension of F

for a, b being Element of E

for s being Element of F

for v being Element of (VecSp (E,F)) st a = s & b = v holds

a * b = s * v

proof end;

Lm12b: for F being Ring

for E being RingExtension of F

for a, b being Element of E

for x, y being Element of F st a = x & b = y holds

a * b = x * y

proof end;

theorem lcsub: :: FIELD_6:46

for F being Field

for V being VectSp of F

for W being Subspace of V

for l1 being Linear_Combination of W ex l2 being Linear_Combination of V st

( Carrier l2 = Carrier l1 & ( for v being Element of V st v in Carrier l2 holds

l2 . v = l1 . v ) )

for V being VectSp of F

for W being Subspace of V

for l1 being Linear_Combination of W ex l2 being Linear_Combination of V st

( Carrier l2 = Carrier l1 & ( for v being Element of V st v in Carrier l2 holds

l2 . v = l1 . v ) )

proof end;

theorem lembasx2: :: FIELD_6:47

for F being Field

for E being FieldExtension of F

for a being Element of E

for n being Element of NAT

for l being Linear_Combination of VecSp (E,F) ex p being Polynomial of F st

( deg p <= n & ( for i being Element of NAT st i <= n holds

p . i = l . (a |^ i) ) )

for E being FieldExtension of F

for a being Element of E

for n being Element of NAT

for l being Linear_Combination of VecSp (E,F) ex p being Polynomial of F st

( deg p <= n & ( for i being Element of NAT st i <= n holds

p . i = l . (a |^ i) ) )

proof end;

theorem lembasx1a: :: FIELD_6:48

for F being Field

for E being FieldExtension of F

for a being Element of E

for n being Element of NAT

for l being Linear_Combination of VecSp (E,F)

for p being non zero Polynomial of F st l . (a |^ (deg p)) = LC p & Carrier l = {(a |^ (deg p))} holds

Sum l = Ext_eval ((LM p),a)

for E being FieldExtension of F

for a being Element of E

for n being Element of NAT

for l being Linear_Combination of VecSp (E,F)

for p being non zero Polynomial of F st l . (a |^ (deg p)) = LC p & Carrier l = {(a |^ (deg p))} holds

Sum l = Ext_eval ((LM p),a)

proof end;

theorem lembasx1: :: FIELD_6:49

for F being Field

for E being FieldExtension of F

for a being Element of E

for n being Element of NAT

for M being Subset of (VecSp (E,F)) st M = { (a |^ i) where i is Element of NAT : i <= n } & ( for i, j being Element of NAT st i < j & j <= n holds

a |^ i <> a |^ j ) holds

for l being Linear_Combination of M

for p being Polynomial of F st deg p <= n & ( for i being Element of NAT st i <= n holds

p . i = l . (a |^ i) ) holds

Ext_eval (p,a) = Sum l

for E being FieldExtension of F

for a being Element of E

for n being Element of NAT

for M being Subset of (VecSp (E,F)) st M = { (a |^ i) where i is Element of NAT : i <= n } & ( for i, j being Element of NAT st i < j & j <= n holds

a |^ i <> a |^ j ) holds

for l being Linear_Combination of M

for p being Polynomial of F st deg p <= n & ( for i being Element of NAT st i <= n holds

p . i = l . (a |^ i) ) holds

Ext_eval (p,a) = Sum l

proof end;

notation

let F be Field;

let E be FieldExtension of F;

let a be F -algebraic Element of E;

synonym MinPoly (a,F) for minimal_polynom (a,F);

end;
let E be FieldExtension of F;

let a be F -algebraic Element of E;

synonym MinPoly (a,F) for minimal_polynom (a,F);

lemminirred: for F being Field

for E being FieldExtension of F

for a being b

proof end;

registration

let F be Field;

let E be FieldExtension of F;

let a be F -algebraic Element of E;

coherence

( MinPoly (a,F) is monic & MinPoly (a,F) is irreducible )

end;
let E be FieldExtension of F;

let a be F -algebraic Element of E;

coherence

( MinPoly (a,F) is monic & MinPoly (a,F) is irreducible )

proof end;

theorem mpol1: :: FIELD_6:50

for F being Field

for E being FieldExtension of F

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

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

( p = MinPoly (a,F) iff ( p is monic & p is irreducible & ker (hom_Ext_eval (a,F)) = {p} -Ideal ) )

for E being FieldExtension of F

for a being b

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

( p = MinPoly (a,F) iff ( p is monic & p is irreducible & ker (hom_Ext_eval (a,F)) = {p} -Ideal ) )

proof end;

theorem mpol2: :: FIELD_6:51

for F being Field

for E being FieldExtension of F

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

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

( p = MinPoly (a,F) iff ( p is monic & Ext_eval (p,a) = 0. E & ( for q being non zero Polynomial of F st Ext_eval (q,a) = 0. E holds

deg p <= deg q ) ) )

for E being FieldExtension of F

for a being b

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

( p = MinPoly (a,F) iff ( p is monic & Ext_eval (p,a) = 0. E & ( for q being non zero Polynomial of F st Ext_eval (q,a) = 0. E holds

deg p <= deg q ) ) )

proof end;

theorem mpol3: :: FIELD_6:52

for F being Field

for E being FieldExtension of F

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

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

( p = MinPoly (a,F) iff ( p is monic & p is irreducible & Ext_eval (p,a) = 0. E ) )

for E being FieldExtension of F

for a being b

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

( p = MinPoly (a,F) iff ( p is monic & p is irreducible & Ext_eval (p,a) = 0. E ) )

proof end;

theorem mpol4: :: FIELD_6:53

for F being Field

for E being FieldExtension of F

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

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

( Ext_eval (p,a) = 0. E iff MinPoly (a,F) divides p )

for E being FieldExtension of F

for a being b

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

( Ext_eval (p,a) = 0. E iff MinPoly (a,F) divides p )

proof end;

theorem :: FIELD_6:54

for F being Field

for E being FieldExtension of F

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

( MinPoly (a,F) = rpoly (1,a) iff a in the carrier of F )

for E being FieldExtension of F

for a being b

( MinPoly (a,F) = rpoly (1,a) iff a in the carrier of F )

proof end;

theorem mpol5: :: FIELD_6:55

for F being Field

for E being FieldExtension of F

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

for i, j being Element of NAT st i < j & j < deg (MinPoly (a,F)) holds

a |^ i <> a |^ j

for E being FieldExtension of F

for a being b

for i, j being Element of NAT st i < j & j < deg (MinPoly (a,F)) holds

a |^ i <> a |^ j

proof end;

theorem ch1: :: FIELD_6:56

for F being Field

for E being Polynom-Ring b_{1} -homomorphic FieldExtension of F

for a being Element of E holds

( a is F -algebraic iff FAdj (F,{a}) = RAdj (F,{a}) )

for E being Polynom-Ring b

for a being Element of E holds

( a is F -algebraic iff FAdj (F,{a}) = RAdj (F,{a}) )

proof end;

theorem :: FIELD_6:57

for F being Field

for E being Polynom-Ring b_{1} -homomorphic FieldExtension of F

for a being non zero Element of E holds

( a is F -algebraic iff a " in RAdj (F,{a}) )

for E being Polynom-Ring b

for a being non zero Element of E holds

( a is F -algebraic iff a " in RAdj (F,{a}) )

proof end;

theorem :: FIELD_6:58

for F being Field

for E being FieldExtension of F

for a being Element of E holds

( a is F -transcendental iff RAdj (F,{a}), Polynom-Ring F are_isomorphic )

for E being FieldExtension of F

for a being Element of E holds

( a is F -transcendental iff RAdj (F,{a}), Polynom-Ring F are_isomorphic )

proof end;

theorem :: FIELD_6:59

for F being Field

for E being Polynom-Ring b_{1} -homomorphic FieldExtension of F

for a being b_{1} -algebraic Element of E holds (Polynom-Ring F) / ({(MinPoly (a,F))} -Ideal), FAdj (F,{a}) are_isomorphic

for E being Polynom-Ring b

for a being b

proof end;

definition

let F be Field;

let E be FieldExtension of F;

let a be F -algebraic Element of E;

{ (a |^ n) where n is Element of NAT : n < deg (MinPoly (a,F)) } is non empty Subset of (VecSp ((FAdj (F,{a})),F))

end;
let E be FieldExtension of F;

let a be F -algebraic Element of E;

func Base a -> non empty Subset of (VecSp ((FAdj (F,{a})),F)) equals :: FIELD_6:def 8

{ (a |^ n) where n is Element of NAT : n < deg (MinPoly (a,F)) } ;

coherence { (a |^ n) where n is Element of NAT : n < deg (MinPoly (a,F)) } ;

{ (a |^ n) where n is Element of NAT : n < deg (MinPoly (a,F)) } is non empty Subset of (VecSp ((FAdj (F,{a})),F))

proof end;

:: deftheorem defines Base FIELD_6:def 8 :

for F being Field

for E being FieldExtension of F

for a being b_{1} -algebraic Element of E holds Base a = { (a |^ n) where n is Element of NAT : n < deg (MinPoly (a,F)) } ;

for F being Field

for E being FieldExtension of F

for a being b

registration

let F be Field;

let E be FieldExtension of F;

let a be F -algebraic Element of E;

coherence

Base a is finite

end;
let E be FieldExtension of F;

let a be F -algebraic Element of E;

coherence

Base a is finite

proof end;

lembas1b: for F being Field

for E being FieldExtension of F

for a being b

for p being Polynomial of F st deg p < deg (MinPoly (a,F)) holds

Ext_eval ((Leading-Monomial p),a) in Lin (Base a)

proof end;

lembas1a: for F being Field

for E being Polynom-Ring b

for a being b

for p being Polynomial of F st deg p < deg (MinPoly (a,F)) holds

Ext_eval (p,a) in Lin (Base a)

proof end;

theorem lembas1: :: FIELD_6:60

for F being Field

for E being FieldExtension of F

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

for p being Polynomial of F holds Ext_eval (p,a) in Lin (Base a)

for E being FieldExtension of F

for a being b

for p being Polynomial of F holds Ext_eval (p,a) in Lin (Base a)

proof end;

theorem lembas2a: :: FIELD_6:61

for F being Field

for E being FieldExtension of F

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

for l being Linear_Combination of Base a ex p being Polynomial of F st

( deg p < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds

p . i = l . (a |^ i) ) )

for E being FieldExtension of F

for a being b

for l being Linear_Combination of Base a ex p being Polynomial of F st

( deg p < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds

p . i = l . (a |^ i) ) )

proof end;

theorem lembas2bb: :: FIELD_6:62

for F being Field

for E being FieldExtension of F

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

for l being Linear_Combination of Base a

for p being non zero Polynomial of F st l . (a |^ (deg p)) = LC p & Carrier l = {(a |^ (deg p))} holds

Sum l = Ext_eval ((LM p),a)

for E being FieldExtension of F

for a being b

for l being Linear_Combination of Base a

for p being non zero Polynomial of F st l . (a |^ (deg p)) = LC p & Carrier l = {(a |^ (deg p))} holds

Sum l = Ext_eval ((LM p),a)

proof end;

theorem lembas2b: :: FIELD_6:63

for F being Field

for E being FieldExtension of F

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

for l being Linear_Combination of Base a

for p being Polynomial of F st deg p < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds

p . i = l . (a |^ i) ) holds

Sum l = Ext_eval (p,a)

for E being FieldExtension of F

for a being b

for l being Linear_Combination of Base a

for p being Polynomial of F st deg p < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds

p . i = l . (a |^ i) ) holds

Sum l = Ext_eval (p,a)

proof end;

theorem lembas2: :: FIELD_6:64

for F being Field

for E being FieldExtension of F

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

for l being Linear_Combination of Base a st Sum l = 0. F holds

l = ZeroLC (VecSp ((FAdj (F,{a})),F))

for E being FieldExtension of F

for a being b

for l being Linear_Combination of Base a st Sum l = 0. F holds

l = ZeroLC (VecSp ((FAdj (F,{a})),F))

proof end;

theorem lembas: :: FIELD_6:65

for F being Field

for E being Polynom-Ring b_{1} -homomorphic FieldExtension of F

for a being b_{1} -algebraic Element of E holds Base a is Basis of (VecSp ((FAdj (F,{a})),F))

for E being Polynom-Ring b

for a being b

proof end;

theorem lembascard: :: FIELD_6:66

for F being Field

for E being FieldExtension of F

for a being b_{1} -algebraic Element of E holds card (Base a) = deg (MinPoly (a,F))

for E being FieldExtension of F

for a being b

proof end;

theorem :: FIELD_6:67

for F being Field

for E being FieldExtension of F

for a being b_{1} -algebraic Element of E holds deg ((FAdj (F,{a})),F) = deg (MinPoly (a,F))

for E being FieldExtension of F

for a being b

proof end;

registration

let F be Field;

let E be FieldExtension of F;

let a be F -algebraic Element of E;

coherence

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

end;
let E be FieldExtension of F;

let a be F -algebraic Element of E;

coherence

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

proof end;

theorem :: FIELD_6:68

for F being Field

for E being FieldExtension of F

for a being Element of E holds

( a is F -algebraic iff FAdj (F,{a}) is F -finite )

for E being FieldExtension of F

for a being Element of E holds

( a is F -algebraic iff FAdj (F,{a}) is F -finite )

proof end;