:: by Yasushige Watase

::

:: Received December 15, 2016

:: Copyright (c) 2016-2018 Association of Mizar Users

Lm5: for A, B being Ring st A is Subring of B holds

( In ((0. A),B) = 0. B & In ((1. A),B) = 1. B )

proof end;

Lm6: for A, B being Ring

for a being Element of A st A is Subring of B holds

a is Element of B

proof end;

Lm7: ( In ((0. F_Rat),F_Complex) = 0. F_Complex & In ((1. F_Rat),F_Complex) = 1. F_Complex & In ((0. INT.Ring),F_Complex) = 0. F_Complex & In ((1. INT.Ring),F_Complex) = 1. F_Complex )

by Lm5, Th3, Th4;

theorem Th8: :: ALGNUM_1:5

for A, B being Ring

for x, y being Element of B

for x1, y1 being Element of A st A is Subring of B & x = x1 & y = y1 holds

x + y = x1 + y1

for x, y being Element of B

for x1, y1 being Element of A st A is Subring of B & x = x1 & y = y1 holds

x + y = x1 + y1

proof end;

theorem Th9: :: ALGNUM_1:6

for A, B being Ring

for x, y being Element of B

for x1, y1 being Element of A st A is Subring of B & x = x1 & y = y1 holds

x * y = x1 * y1

for x, y being Element of B

for x1, y1 being Element of A st A is Subring of B & x = x1 & y = y1 holds

x * y = x1 * y1

proof end;

registration
end;

definition

let A, B be Ring;

let p be Polynomial of A;

let x be Element of B;

ex b_{1} being Element of B ex F being FinSequence of B st

( b_{1} = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds

F . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) ) )

for b_{1}, b_{2} being Element of B st ex F being FinSequence of B st

( b_{1} = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds

F . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) ) ) & ex F being FinSequence of B st

( b_{2} = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds

F . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) ) ) holds

b_{1} = b_{2}

end;
let p be Polynomial of A;

let x be Element of B;

func Ext_eval (p,x) -> Element of B means :Def1: :: ALGNUM_1:def 1

ex F being FinSequence of B st

( it = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds

F . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) ) );

existence ex F being FinSequence of B st

( it = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds

F . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) ) );

ex b

( b

F . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) ) )

proof end;

uniqueness for b

( b

F . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) ) ) & ex F being FinSequence of B st

( b

F . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) ) ) holds

b

proof end;

:: deftheorem Def1 defines Ext_eval ALGNUM_1:def 1 :

for A, B being Ring

for p being Polynomial of A

for x, b_{5} being Element of B holds

( b_{5} = Ext_eval (p,x) iff ex F being FinSequence of B st

( b_{5} = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds

F . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) ) ) );

for A, B being Ring

for p being Polynomial of A

for x, b

( b

( b

F . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) ) ) );

theorem Th11: :: ALGNUM_1:7

for n being Element of NAT

for A, B being Ring

for z being Element of A st A is Subring of B holds

(power B) . ((In (z,B)),n) = In (((power A) . (z,n)),B)

for A, B being Ring

for z being Element of A st A is Subring of B holds

(power B) . ((In (z,B)),n) = In (((power A) . (z,n)),B)

proof end;

theorem Th12: :: ALGNUM_1:8

for A, B being Ring

for x1, x2 being Element of A st A is Subring of B holds

(In (x1,B)) + (In (x2,B)) = In ((x1 + x2),B)

for x1, x2 being Element of A st A is Subring of B holds

(In (x1,B)) + (In (x2,B)) = In ((x1 + x2),B)

proof end;

theorem Th13: :: ALGNUM_1:9

for A, B being Ring

for x1, x2 being Element of A st A is Subring of B holds

(In (x1,B)) * (In (x2,B)) = In ((x1 * x2),B)

for x1, x2 being Element of A st A is Subring of B holds

(In (x1,B)) * (In (x2,B)) = In ((x1 * x2),B)

proof end;

theorem Th14: :: ALGNUM_1:10

for A, B being Ring

for F being FinSequence of A

for G being FinSequence of B st A is Subring of B & F = G holds

In ((Sum F),B) = Sum G

for F being FinSequence of A

for G being FinSequence of B st A is Subring of B & F = G holds

In ((Sum F),B) = Sum G

proof end;

theorem Th15: :: ALGNUM_1:11

for A, B being Ring

for n being Nat

for x being Element of A

for p being Polynomial of A st A is Subring of B holds

(In ((p . (n -' 1)),B)) * ((power B) . ((In (x,B)),(n -' 1))) = In (((p . (n -' 1)) * ((power A) . (x,(n -' 1)))),B)

for n being Nat

for x being Element of A

for p being Polynomial of A st A is Subring of B holds

(In ((p . (n -' 1)),B)) * ((power B) . ((In (x,B)),(n -' 1))) = In (((p . (n -' 1)) * ((power A) . (x,(n -' 1)))),B)

proof end;

theorem Th16: :: ALGNUM_1:12

for A, B being Ring

for x being Element of A

for p being Polynomial of A st A is Subring of B holds

Ext_eval (p,(In (x,B))) = In ((eval (p,x)),B)

for x being Element of A

for p being Polynomial of A st A is Subring of B holds

Ext_eval (p,(In (x,B))) = In ((eval (p,x)),B)

proof end;

:: Modify POLYNOM4:17

:: Modify POLYNOM4:18

theorem Th18: :: ALGNUM_1:14

for A, B being non degenerated Ring

for x being Element of B st A is Subring of B holds

Ext_eval ((1_. A),x) = 1. B

for x being Element of B st A is Subring of B holds

Ext_eval ((1_. A),x) = 1. B

proof end;

:: Modify POLYNOM4:19

theorem Th19: :: ALGNUM_1:15

for A, B being Ring

for x being Element of B

for p, q being Polynomial of A st A is Subring of B holds

Ext_eval ((p + q),x) = (Ext_eval (p,x)) + (Ext_eval (q,x))

for x being Element of B

for p, q being Polynomial of A st A is Subring of B holds

Ext_eval ((p + q),x) = (Ext_eval (p,x)) + (Ext_eval (q,x))

proof end;

theorem Th20: :: ALGNUM_1:16

for A, B being Ring

for p, q being Polynomial of A st A is Subring of B & len p > 0 & len q > 0 holds

for x being Element of B holds Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (In (((p . ((len p) -' 1)) * (q . ((len q) -' 1))),B)) * ((power B) . (x,(((len p) + (len q)) -' 2)))

for p, q being Polynomial of A st A is Subring of B & len p > 0 & len q > 0 holds

for x being Element of B holds Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (In (((p . ((len p) -' 1)) * (q . ((len q) -' 1))),B)) * ((power B) . (x,(((len p) + (len q)) -' 2)))

proof end;

theorem Th21: :: ALGNUM_1:17

for A, B being Ring

for p being Polynomial of A

for x being Element of B st A is Subring of B holds

Ext_eval ((Leading-Monomial p),x) = (In ((p . ((len p) -' 1)),B)) * ((power B) . (x,((len p) -' 1)))

for p being Polynomial of A

for x being Element of B st A is Subring of B holds

Ext_eval ((Leading-Monomial p),x) = (In ((p . ((len p) -' 1)),B)) * ((power B) . (x,((len p) -' 1)))

proof end;

::Modify POLYNOM_4:Lm3:

theorem Th22: :: ALGNUM_1:18

for A being Ring

for B being comRing

for p, q being Polynomial of A

for x being Element of B st A is Subring of B holds

Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (Ext_eval ((Leading-Monomial p),x)) * (Ext_eval ((Leading-Monomial q),x))

for B being comRing

for p, q being Polynomial of A

for x being Element of B st A is Subring of B holds

Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (Ext_eval ((Leading-Monomial p),x)) * (Ext_eval ((Leading-Monomial q),x))

proof end;

:: Modify POLYNOM4:23

theorem Th15: :: ALGNUM_1:19

for A being Ring

for B being comRing

for p, q being Polynomial of A

for x being Element of B st A is Subring of B holds

Ext_eval (((Leading-Monomial p) *' q),x) = (Ext_eval ((Leading-Monomial p),x)) * (Ext_eval (q,x))

for B being comRing

for p, q being Polynomial of A

for x being Element of B st A is Subring of B holds

Ext_eval (((Leading-Monomial p) *' q),x) = (Ext_eval ((Leading-Monomial p),x)) * (Ext_eval (q,x))

proof end;

:: Modify POLYNOM4:24

theorem Th24: :: ALGNUM_1:20

for A being Ring

for B being comRing

for p, q being Polynomial of A

for x being Element of B st A is Subring of B holds

Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x))

for B being comRing

for p, q being Polynomial of A

for x being Element of B st A is Subring of B holds

Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x))

proof end;

:: modified POLYNOM5:37

theorem Th25: :: ALGNUM_1:21

for A, B being Ring

for x being Element of B

for z0 being Element of A st A is Subring of B holds

Ext_eval (<%z0%>,x) = In (z0,B)

for x being Element of B

for z0 being Element of A st A is Subring of B holds

Ext_eval (<%z0%>,x) = In (z0,B)

proof end;

:: modified POLYNOM5:44

theorem :: ALGNUM_1:22

for A, B being Ring

for x being Element of B

for z0, z1 being Element of A st A is Subring of B holds

Ext_eval (<%z0,z1%>,x) = (In (z0,B)) + ((In (z1,B)) * x)

for x being Element of B

for z0, z1 being Element of A st A is Subring of B holds

Ext_eval (<%z0,z1%>,x) = (In (z0,B)) + ((In (z1,B)) * x)

proof end;

:: Definition of Integral Element over A in B

definition

let A, B be Ring;

let x be Element of B;

end;
let x be Element of B;

pred x is_integral_over A means :: ALGNUM_1:def 2

ex f being Polynomial of A st

( LC f = 1. A & Ext_eval (f,x) = 0. B );

ex f being Polynomial of A st

( LC f = 1. A & Ext_eval (f,x) = 0. B );

:: deftheorem defines is_integral_over ALGNUM_1:def 2 :

for A, B being Ring

for x being Element of B holds

( x is_integral_over A iff ex f being Polynomial of A st

( LC f = 1. A & Ext_eval (f,x) = 0. B ) );

for A, B being Ring

for x being Element of B holds

( x is_integral_over A iff ex f being Polynomial of A st

( LC f = 1. A & Ext_eval (f,x) = 0. B ) );

theorem Th27: :: ALGNUM_1:23

for B being Ring

for A being non degenerated Ring

for a being Element of A st A is Subring of B holds

In (a,B) is_integral_over A

for A being non degenerated Ring

for a being Element of A st A is Subring of B holds

In (a,B) is_integral_over A

proof end;

definition

let A be non degenerated Ring;

let B be Ring;

assume A0: A is Subring of B ;

{ z where z is Element of B : z is_integral_over A } is non empty Subset of B

end;
let B be Ring;

assume A0: A is Subring of B ;

func integral_closure (A,B) -> non empty Subset of B equals :: ALGNUM_1:def 3

{ z where z is Element of B : z is_integral_over A } ;

coherence { z where z is Element of B : z is_integral_over A } ;

{ z where z is Element of B : z is_integral_over A } is non empty Subset of B

proof end;

:: deftheorem defines integral_closure ALGNUM_1:def 3 :

for A being non degenerated Ring

for B being Ring st A is Subring of B holds

integral_closure (A,B) = { z where z is Element of B : z is_integral_over A } ;

for A being non degenerated Ring

for B being Ring st A is Subring of B holds

integral_closure (A,B) = { z where z is Element of B : z is_integral_over A } ;

definition

let c be Complex;

end;
attr c is algebraic means :: ALGNUM_1:def 4

ex x being Element of F_Complex st

( x = c & x is_integral_over F_Rat );

ex x being Element of F_Complex st

( x = c & x is_integral_over F_Rat );

:: deftheorem defines algebraic ALGNUM_1:def 4 :

for c being Complex holds

( c is algebraic iff ex x being Element of F_Complex st

( x = c & x is_integral_over F_Rat ) );

for c being Complex holds

( c is algebraic iff ex x being Element of F_Complex st

( x = c & x is_integral_over F_Rat ) );

definition
end;

:: deftheorem defines algebraic ALGNUM_1:def 5 :

for x being Element of F_Complex holds

( x is algebraic iff x is_integral_over F_Rat );

for x being Element of F_Complex holds

( x is algebraic iff x is_integral_over F_Rat );

definition

let c be Complex;

end;
attr c is algebraic_integer means :: ALGNUM_1:def 6

ex x being Element of F_Complex st

( x = c & x is_integral_over INT.Ring );

ex x being Element of F_Complex st

( x = c & x is_integral_over INT.Ring );

:: deftheorem defines algebraic_integer ALGNUM_1:def 6 :

for c being Complex holds

( c is algebraic_integer iff ex x being Element of F_Complex st

( x = c & x is_integral_over INT.Ring ) );

for c being Complex holds

( c is algebraic_integer iff ex x being Element of F_Complex st

( x = c & x is_integral_over INT.Ring ) );

definition

let x be Element of F_Complex;

compatibility

( x is algebraic_integer iff x is_integral_over INT.Ring ) ;

end;
compatibility

( x is algebraic_integer iff x is_integral_over INT.Ring ) ;

:: deftheorem defines algebraic_integer ALGNUM_1:def 7 :

for x being Element of F_Complex holds

( x is algebraic_integer iff x is_integral_over INT.Ring );

for x being Element of F_Complex holds

( x is algebraic_integer iff x is_integral_over INT.Ring );

registration
end;

registration

existence

ex b_{1} being Complex st b_{1} is algebraic
by GAUSSINT:14;

ex b_{1} being Element of F_Complex st b_{1} is algebraic
by Lm7;

end;
ex b

cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable complex reducible algebraic for Element of F_Complex;

existence ex b

registration
end;

registration

existence

ex b_{1} being Complex st b_{1} is algebraic_integer
by GAUSSINT:14;

ex b_{1} being Element of F_Complex st b_{1} is algebraic_integer
by Lm7;

end;
ex b

cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable complex reducible algebraic_integer for Element of F_Complex;

existence ex b

definition

let A, B be Ring;

let x be Element of B;

{ p where p is Polynomial of A : Ext_eval (p,x) = 0. B } is non empty Subset of (Polynom-Ring A)

end;
let x be Element of B;

func Ann_Poly (x,A) -> non empty Subset of (Polynom-Ring A) equals :: ALGNUM_1:def 8

{ p where p is Polynomial of A : Ext_eval (p,x) = 0. B } ;

coherence { p where p is Polynomial of A : Ext_eval (p,x) = 0. B } ;

{ p where p is Polynomial of A : Ext_eval (p,x) = 0. B } is non empty Subset of (Polynom-Ring A)

proof end;

:: deftheorem defines Ann_Poly ALGNUM_1:def 8 :

for A, B being Ring

for x being Element of B holds Ann_Poly (x,A) = { p where p is Polynomial of A : Ext_eval (p,x) = 0. B } ;

for A, B being Ring

for x being Element of B holds Ann_Poly (x,A) = { p where p is Polynomial of A : Ext_eval (p,x) = 0. B } ;

theorem Lm30: :: ALGNUM_1:24

for A, B being Ring

for w being Element of B

for x, y being Element of (Polynom-Ring A) st A is Subring of B & x in Ann_Poly (w,A) & y in Ann_Poly (w,A) holds

x + y in Ann_Poly (w,A)

for w being Element of B

for x, y being Element of (Polynom-Ring A) st A is Subring of B & x in Ann_Poly (w,A) & y in Ann_Poly (w,A) holds

x + y in Ann_Poly (w,A)

proof end;

theorem Th31: :: ALGNUM_1:25

for A being Ring

for B being comRing

for z being Element of B

for p, x being Element of (Polynom-Ring A) st A is Subring of B & x in Ann_Poly (z,A) holds

p * x in Ann_Poly (z,A)

for B being comRing

for z being Element of B

for p, x being Element of (Polynom-Ring A) st A is Subring of B & x in Ann_Poly (z,A) holds

p * x in Ann_Poly (z,A)

proof end;

theorem Lm32: :: ALGNUM_1:26

for A being Ring

for B being comRing

for w being Element of B

for p, x being Element of (Polynom-Ring A) st A is Subring of B & x in Ann_Poly (w,A) holds

x * p in Ann_Poly (w,A)

for B being comRing

for w being Element of B

for p, x being Element of (Polynom-Ring A) st A is Subring of B & x in Ann_Poly (w,A) holds

x * p in Ann_Poly (w,A)

proof end;

theorem Th33: :: ALGNUM_1:27

for A being non degenerated Ring

for B being non degenerated comRing

for w being Element of B st A is Subring of B holds

Ann_Poly (w,A) is proper Ideal of (Polynom-Ring A)

for B being non degenerated comRing

for w being Element of B st A is Subring of B holds

Ann_Poly (w,A) is proper Ideal of (Polynom-Ring A)

proof end;

theorem Th34: :: ALGNUM_1:28

for K, L being Field

for w being Element of L st K is Subring of L holds

ex g being Element of (Polynom-Ring K) st {g} -Ideal = Ann_Poly (w,K)

for w being Element of L st K is Subring of L holds

ex g being Element of (Polynom-Ring K) st {g} -Ideal = Ann_Poly (w,K)

proof end;

theorem Th35: :: ALGNUM_1:29

for K, L being Field

for z being Element of L st z is_integral_over K holds

Ann_Poly (z,K) <> {(0. (Polynom-Ring K))}

for z being Element of L st z is_integral_over K holds

Ann_Poly (z,K) <> {(0. (Polynom-Ring K))}

proof end;

theorem Lm37: :: ALGNUM_1:30

for K being Field

for p being Element of (Polynom-Ring K) st p <> 0_. K holds

p is non zero Element of the carrier of (Polynom-Ring K)

for p being Element of (Polynom-Ring K) st p <> 0_. K holds

p is non zero Element of the carrier of (Polynom-Ring K)

proof end;

theorem Th38: :: ALGNUM_1:31

for K, L being Field

for w being Element of L st K is Subring of L holds

Ann_Poly (w,K) is quasi-prime

for w being Element of L st K is Subring of L holds

Ann_Poly (w,K) is quasi-prime

proof end;

theorem Th39: :: ALGNUM_1:32

for K, L being Field

for w being Element of L st K is Subring of L & w is_integral_over K holds

Ann_Poly (w,K) is prime

for w being Element of L st K is Subring of L & w is_integral_over K holds

Ann_Poly (w,K) is prime

proof end;

theorem Th40: :: ALGNUM_1:33

for K, L being Field

for z being Element of L st K is Subring of L & z is_integral_over K holds

ex f being Element of (Polynom-Ring K) st

( f <> 0_. K & {f} -Ideal = Ann_Poly (z,K) & f = NormPolynomial f )

for z being Element of L st K is Subring of L & z is_integral_over K holds

ex f being Element of (Polynom-Ring K) st

( f <> 0_. K & {f} -Ideal = Ann_Poly (z,K) & f = NormPolynomial f )

proof end;

theorem Th41: :: ALGNUM_1:34

for K, L being Field

for z being Element of L

for f, g being Element of (Polynom-Ring K) st z is_integral_over K & {f} -Ideal = Ann_Poly (z,K) & f = NormPolynomial f & {g} -Ideal = Ann_Poly (z,K) & g = NormPolynomial g holds

f = g

for z being Element of L

for f, g being Element of (Polynom-Ring K) st z is_integral_over K & {f} -Ideal = Ann_Poly (z,K) & f = NormPolynomial f & {g} -Ideal = Ann_Poly (z,K) & g = NormPolynomial g holds

f = g

proof end;

definition

let K, L be Field;

let z be Element of L;

assume that

A1: K is Subring of L and

A2: z is_integral_over K ;

ex b_{1} being Element of the carrier of (Polynom-Ring K) st

( b_{1} <> 0_. K & {b_{1}} -Ideal = Ann_Poly (z,K) & b_{1} = NormPolynomial b_{1} )
by A1, A2, Th40;

uniqueness

for b_{1}, b_{2} being Element of the carrier of (Polynom-Ring K) st b_{1} <> 0_. K & {b_{1}} -Ideal = Ann_Poly (z,K) & b_{1} = NormPolynomial b_{1} & b_{2} <> 0_. K & {b_{2}} -Ideal = Ann_Poly (z,K) & b_{2} = NormPolynomial b_{2} holds

b_{1} = b_{2}
by Th41, A2;

end;
let z be Element of L;

assume that

A1: K is Subring of L and

A2: z is_integral_over K ;

func minimal_polynom (z,K) -> Element of the carrier of (Polynom-Ring K) means :Def7: :: ALGNUM_1:def 9

( it <> 0_. K & {it} -Ideal = Ann_Poly (z,K) & it = NormPolynomial it );

existence ( it <> 0_. K & {it} -Ideal = Ann_Poly (z,K) & it = NormPolynomial it );

ex b

( b

uniqueness

for b

b

:: deftheorem Def7 defines minimal_polynom ALGNUM_1:def 9 :

for K, L being Field

for z being Element of L st K is Subring of L & z is_integral_over K holds

for b_{4} being Element of the carrier of (Polynom-Ring K) holds

( b_{4} = minimal_polynom (z,K) iff ( b_{4} <> 0_. K & {b_{4}} -Ideal = Ann_Poly (z,K) & b_{4} = NormPolynomial b_{4} ) );

for K, L being Field

for z being Element of L st K is Subring of L & z is_integral_over K holds

for b

( b

definition

let K, L be Field;

let z be Element of L;

assume that

A1: K is Subring of L and

A2: z is_integral_over K ;

deg (minimal_polynom (z,K)) is Element of NAT

end;
let z be Element of L;

assume that

A1: K is Subring of L and

A2: z is_integral_over K ;

func deg_of_integral_element (z,K) -> Element of NAT equals :: ALGNUM_1:def 10

deg (minimal_polynom (z,K));

coherence deg (minimal_polynom (z,K));

deg (minimal_polynom (z,K)) is Element of NAT

proof end;

:: deftheorem defines deg_of_integral_element ALGNUM_1:def 10 :

for K, L being Field

for z being Element of L st K is Subring of L & z is_integral_over K holds

deg_of_integral_element (z,K) = deg (minimal_polynom (z,K));

for K, L being Field

for z being Element of L st K is Subring of L & z is_integral_over K holds

deg_of_integral_element (z,K) = deg (minimal_polynom (z,K));

definition

let A, B be Ring;

let x be Element of B;

ex b_{1} being Function of (Polynom-Ring A),B st

for p being Polynomial of A holds b_{1} . p = Ext_eval (p,x)

for b_{1}, b_{2} being Function of (Polynom-Ring A),B st ( for p being Polynomial of A holds b_{1} . p = Ext_eval (p,x) ) & ( for p being Polynomial of A holds b_{2} . p = Ext_eval (p,x) ) holds

b_{1} = b_{2}

end;
let x be Element of B;

func hom_Ext_eval (x,A) -> Function of (Polynom-Ring A),B means :Def9: :: ALGNUM_1:def 11

for p being Polynomial of A holds it . p = Ext_eval (p,x);

existence for p being Polynomial of A holds it . p = Ext_eval (p,x);

ex b

for p being Polynomial of A holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def9 defines hom_Ext_eval ALGNUM_1:def 11 :

for A, B being Ring

for x being Element of B

for b_{4} being Function of (Polynom-Ring A),B holds

( b_{4} = hom_Ext_eval (x,A) iff for p being Polynomial of A holds b_{4} . p = Ext_eval (p,x) );

for A, B being Ring

for x being Element of B

for b

( b

registration

let x be Element of F_Complex;

coherence

( hom_Ext_eval (x,F_Rat) is unity-preserving & hom_Ext_eval (x,F_Rat) is additive & hom_Ext_eval (x,F_Rat) is multiplicative )

end;
coherence

( hom_Ext_eval (x,F_Rat) is unity-preserving & hom_Ext_eval (x,F_Rat) is additive & hom_Ext_eval (x,F_Rat) is multiplicative )

proof end;

definition
end;

:: deftheorem defines FQ ALGNUM_1:def 12 :

for x being Element of F_Complex holds FQ x = rng (hom_Ext_eval (x,F_Rat));

for x being Element of F_Complex holds FQ x = rng (hom_Ext_eval (x,F_Rat));

registration
end;

definition

let x be Element of F_Complex;

correctness

coherence

addcomplex || (FQ x) is BinOp of (FQ x);

end;
correctness

coherence

addcomplex || (FQ x) is BinOp of (FQ x);

proof end;

:: deftheorem defines FQ_add ALGNUM_1:def 13 :

for x being Element of F_Complex holds FQ_add x = addcomplex || (FQ x);

for x being Element of F_Complex holds FQ_add x = addcomplex || (FQ x);

definition

let x be Element of F_Complex;

correctness

coherence

multcomplex || (FQ x) is BinOp of (FQ x);

end;
correctness

coherence

multcomplex || (FQ x) is BinOp of (FQ x);

proof end;

:: deftheorem defines FQ_mult ALGNUM_1:def 14 :

for x being Element of F_Complex holds FQ_mult x = multcomplex || (FQ x);

for x being Element of F_Complex holds FQ_mult x = multcomplex || (FQ x);

definition

let x be Element of F_Complex;

doubleLoopStr(# (FQ x),(FQ_add x),(FQ_mult x),(In ((1. F_Complex),(FQ x))),(In ((0. F_Complex),(FQ x))) #) is non empty strict doubleLoopStr ;

end;
func FQ_Ring x -> non empty strict doubleLoopStr equals :: ALGNUM_1:def 15

doubleLoopStr(# (FQ x),(FQ_add x),(FQ_mult x),(In ((1. F_Complex),(FQ x))),(In ((0. F_Complex),(FQ x))) #);

coherence doubleLoopStr(# (FQ x),(FQ_add x),(FQ_mult x),(In ((1. F_Complex),(FQ x))),(In ((0. F_Complex),(FQ x))) #);

doubleLoopStr(# (FQ x),(FQ_add x),(FQ_mult x),(In ((1. F_Complex),(FQ x))),(In ((0. F_Complex),(FQ x))) #) is non empty strict doubleLoopStr ;

:: deftheorem defines FQ_Ring ALGNUM_1:def 15 :

for x being Element of F_Complex holds FQ_Ring x = doubleLoopStr(# (FQ x),(FQ_add x),(FQ_mult x),(In ((1. F_Complex),(FQ x))),(In ((0. F_Complex),(FQ x))) #);

for x being Element of F_Complex holds FQ_Ring x = doubleLoopStr(# (FQ x),(FQ_add x),(FQ_mult x),(In ((1. F_Complex),(FQ x))),(In ((0. F_Complex),(FQ x))) #);

registration

let x be Element of F_Complex;

( FQ_Ring x is Abelian & FQ_Ring x is add-associative & FQ_Ring x is right_zeroed & FQ_Ring x is right_complementable & FQ_Ring x is associative & FQ_Ring x is well-unital & FQ_Ring x is distributive ) by Th54;

end;
cluster FQ_Ring x -> non empty right_complementable strict Abelian add-associative right_zeroed well-unital distributive associative ;

coherence ( FQ_Ring x is Abelian & FQ_Ring x is add-associative & FQ_Ring x is right_zeroed & FQ_Ring x is right_complementable & FQ_Ring x is associative & FQ_Ring x is well-unital & FQ_Ring x is distributive ) by Th54;

registration

let z be Element of F_Complex;

coherence

( FQ_Ring z is domRing-like & FQ_Ring z is commutative & not FQ_Ring z is degenerated )

end;
coherence

( FQ_Ring z is domRing-like & FQ_Ring z is commutative & not FQ_Ring z is degenerated )

proof end;

Lm55: for x being Element of F_Complex holds the carrier of F_Rat c= the carrier of (FQ_Ring x)

by Lm48;

theorem Lm56: :: ALGNUM_1:45

for x being Element of F_Complex holds

( [:RAT,RAT:] c= [:(FQ x),(FQ x):] & [:(FQ x),(FQ x):] c= [:COMPLEX,COMPLEX:] )

( [:RAT,RAT:] c= [:(FQ x),(FQ x):] & [:(FQ x),(FQ x):] c= [:COMPLEX,COMPLEX:] )

proof end;

theorem Th80: :: ALGNUM_1:49

for K being Field

for f, g being Element of (Polynom-Ring K) st f <> 0. (Polynom-Ring K) & {f} -Ideal is prime & not g in {f} -Ideal holds

{f,g} -Ideal = the carrier of (Polynom-Ring K)

for f, g being Element of (Polynom-Ring K) st f <> 0. (Polynom-Ring K) & {f} -Ideal is prime & not g in {f} -Ideal holds

{f,g} -Ideal = the carrier of (Polynom-Ring K)

proof end;

theorem Th81: :: ALGNUM_1:50

for K being Field

for f, g being Element of (Polynom-Ring K) st f <> 0. (Polynom-Ring K) & {f} -Ideal is prime & not g in {f} -Ideal holds

{f} -Ideal ,{g} -Ideal are_co-prime

for f, g being Element of (Polynom-Ring K) st f <> 0. (Polynom-Ring K) & {f} -Ideal is prime & not g in {f} -Ideal holds

{f} -Ideal ,{g} -Ideal are_co-prime

proof end;

theorem Lm62: :: ALGNUM_1:51

for x being Element of F_Complex

for a being Element of (FQ_Ring x) ex g being Element of (Polynom-Ring F_Rat) st a = (hom_Ext_eval (x,F_Rat)) . g

for a being Element of (FQ_Ring x) ex g being Element of (Polynom-Ring F_Rat) st a = (hom_Ext_eval (x,F_Rat)) . g

proof end;

theorem Th83: :: ALGNUM_1:52

for x, a being Element of F_Complex st a <> 0. F_Complex & a in the carrier of (FQ_Ring x) holds

ex g being Element of (Polynom-Ring F_Rat) st

( not g in Ann_Poly (x,F_Rat) & a = (hom_Ext_eval (x,F_Rat)) . g )

ex g being Element of (Polynom-Ring F_Rat) st

( not g in Ann_Poly (x,F_Rat) & a = (hom_Ext_eval (x,F_Rat)) . g )

proof end;

theorem Th84: :: ALGNUM_1:53

for x, a being Element of F_Complex st x is algebraic & a <> 0. F_Complex & a in the carrier of (FQ_Ring x) holds

ex f, g being Element of (Polynom-Ring F_Rat) st

( {f} -Ideal = Ann_Poly (x,F_Rat) & not g in Ann_Poly (x,F_Rat) & a = (hom_Ext_eval (x,F_Rat)) . g & {f} -Ideal ,{g} -Ideal are_co-prime )

ex f, g being Element of (Polynom-Ring F_Rat) st

( {f} -Ideal = Ann_Poly (x,F_Rat) & not g in Ann_Poly (x,F_Rat) & a = (hom_Ext_eval (x,F_Rat)) . g & {f} -Ideal ,{g} -Ideal are_co-prime )

proof end;

theorem Th85: :: ALGNUM_1:54

for x, a being Element of F_Complex st x is algebraic & a <> 0. F_Complex & a in the carrier of (FQ_Ring x) holds

ex b being Element of F_Complex st

( b in the carrier of (FQ_Ring x) & a * b = 1. F_Complex )

ex b being Element of F_Complex st

( b in the carrier of (FQ_Ring x) & a * b = 1. F_Complex )

proof end;

:: based upon POLYNOM4