:: Algebraic Numbers
:: by Yasushige Watase
::
:: Received December 15, 2016
:: Copyright (c) 2016-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSEQ_1, SUBSET_1, FUNCT_1, ARYTM_3, TARSKI, NAT_1,
XBOOLE_0, SUPINF_2, ZFMISC_1, GROUP_1, STRUCT_0, POLYNOM1, POLYNOM2,
C0SP1, REALSET1, ARYTM_1, RELAT_1, CARD_1, XXREAL_0, VECTSP_1, ALGSTR_0,
FUNCT_7, AFINSQ_1, CARD_3, MESFUNC1, POLYNOM3, FUNCSDOM, ORDINAL4, INT_2,
GAUSSINT, BINOP_2, COMPLFLD, EC_PF_1, XCMPLX_0, FINSEQ_2, INT_3,
ALGSEQ_1, POLYNOM4, PARTFUN1, IDEAL_1, CARD_FIL, VECTSP_2, POLYNOM5,
HURWITZ, RATFUNC1, MSSUBFAM, QUOFIELD, BINOP_1, RING_1, RING_2, LATTICES,
GCD_1, RLVECT_1, ALGNUM_1, RAT_1, INT_1, WAYBEL_8;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, DOMAIN_1,
ORDINAL1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NUMBERS, INT_1,
FUNCOP_1, BINOP_1, FUNCT_4, FUNCT_7, SETWISEO, FINSEQ_1, FINSEQ_2,
XCMPLX_0, XXREAL_0, CARD_1, XREAL_0, PBOOLE, VALUED_0, NAT_1, NAT_D,
RAT_1, NEWTON, BINOP_2, MEMBERED, STRUCT_0, ALGSTR_0, C0SP1, NORMSP_1,
VFUNCT_1, VECTSP_2, ALGSEQ_1, ALGSTR_1, RLVECT_1, GROUP_1, VECTSP_1,
RINGCAT1, RING_3, GROUP_6, RING_2, POLYNOM1, UPROOTS, HURWITZ, RATFUNC1,
BINOM, INT_3, GCD_1, RVSUM_1, COMPLFLD, POLYNOM3, POLYNOM4, POLYNOM5,
FVSUM_1, PRE_POLY, REALSET1, COMPLEX1, EC_PF_1, GAUSSINT, IDEAL_1,
RING_1, MSSUBFAM, QUOFIELD, RING_4;
constructors TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELSET_1, NUMBERS,
ORDINAL1, FUNCT_2, FINSEQ_1, FINSEQOP, STRUCT_0, ALGSTR_0, C0SP1,
VECTSP_1, NORMSP_1, VFUNCT_1, POLYNOM3, SETWISEO, BINOP_1, REAL_1,
RFINSEQ, FINSOP_1, BINARITH, VECTSP_2, GRCAT_1, REALSET2, QUOFIELD,
ALGSTR_1, POLYNOM4, POLYNOM5, NAT_D, FVSUM_1, ALGSEQ_1, FUNCT_7, BINOP_2,
INT_1, RLVECT_1, GROUP_1, RINGCAT1, MOD_4, GROUP_6, RING_3, RING_2,
GROUP_4, FINSEQ_4, MATRIX_1, POLYNOM1, UPROOTS, HURWITZ, POLYNOM2,
RING_4, XXREAL_2, XTUPLE_0, PARTFUN1, RVSUM_1, XCMPLX_0, RAT_1, NEWTON,
VALUED_0, MEMBERED, NAT_1, FINSEQ_2, RATFUNC1, BINOM, GCD_1, IDEAL_1,
EC_PF_1, GAUSSINT, AFINSQ_2, FUNCT_4, REALSET1, MSSUBFAM;
registrations ALGSTR_0, GAUSSINT, CARD_1, INT_3, FINSEQ_2, FUNCT_2, INT_1,
MEMBERED, NAT_1, NUMBERS, ORDINAL1, POLYNOM3, POLYNOM5, REALSET1,
RELAT_1, RING_2, STRUCT_0, VECTSP_1, XREAL_0, RATFUNC1, RAT_1, XXREAL_0,
COMPLFLD, XCMPLX_0, VALUED_0, POLYNOM4, ALGSTR_1, RLVECT_1, RING_1,
RING_4, XBOOLE_0, RINGCAT1, RELSET_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions VECTSP_1, GROUP_1, GROUP_6, ALGSTR_0;
equalities BINOP_1, ALGSTR_0, REALSET1, FINSEQ_1, FINSEQ_2, XCMPLX_0,
POLYNOM3, POLYNOM5, RATFUNC1, HURWITZ, STRUCT_0, GAUSSINT, INT_3;
expansions STRUCT_0, SUBSET_1, FINSEQ_1, TARSKI, ALGSEQ_1, FUNCT_2, IDEAL_1,
FUNCT_1, RING_2, ALGSTR_0, UPROOTS;
theorems TARSKI, ZFMISC_1, FUNCT_1, XREAL_0, VECTSP_1, NORMSP_1, FINSEQ_1,
FINSEQ_2, FINSEQ_3, NAT_1, XREAL_1, ORDINAL1, C0SP1, CARD_1, RELAT_1,
XXREAL_0, SUBSET_1, GROUP_1, MATRIX_3, FVSUM_1, FUNCOP_1, POLYNOM3,
POLYNOM5, RLVECT_1, IDEAL_1, BINOP_2, RING_3, GAUSSINT, INT_1, ALGSEQ_1,
POLYNOM4, POLYNOM2, PARTFUN1, RING_2, RING_1, VECTSP_2, RING_4, XCMPLX_0,
FUNCT_2, COMPLFLD, ALGSTR_0, STRUCT_0, GCD_1, EC_PF_1, RAT_1;
schemes NAT_1, FINSEQ_2, FUNCT_2;
begin :: Preliminaries
reserve i,j for Nat;
reserve A,B for Ring;
theorem Th1:
for L1,L2,L3 be Ring st L1 is Subring of L2 & L2 is Subring of L3 holds
L1 is Subring of L3
proof
let L1,L2,L3 be Ring;
assume that
A1: L1 is Subring of L2 and
A2: L2 is Subring of L3;
A3: the carrier of L1 c= the carrier of L2
& the addF of L1 = (the addF of L2) || the carrier of L1
& the multF of L1 = (the multF of L2) || the carrier of L1
& 1.L1 = 1.L2& 0.L1 = 0.L2 by A1,C0SP1:def 3;
A4: the carrier of L2 c= the carrier of L3
& the addF of L2= (the addF of L3) || the carrier of L2
& the multF of L2= (the multF of L3) || the carrier of L2
& 1.L2= 1.L3 & 0.L2= 0.L3 by A2,C0SP1:def 3;
set A1 = [:the carrier of L1, the carrier of L1:];
set A2 = [:the carrier of L2, the carrier of L2:];
set A3 = [:the carrier of L3, the carrier of L3:];
A8: the carrier of L1 c= the carrier of L3 by A3,A4;
A9: the addF of L1 = (the addF of L2) || the carrier of L1
by A1,C0SP1:def 3
.= ((the addF of L3) || the carrier of L2) || the carrier of L1
by A2,C0SP1:def 3
.= (the addF of L3) || the carrier of L1 by A3,ZFMISC_1:96,RELAT_1:74;
A10: the multF of L1 = (the multF of L2) || the carrier of L1
by A1,C0SP1:def 3
.= ((the multF of L3) || the carrier of L2) || the carrier of L1
by A2,C0SP1:def 3
.= (the multF of L3) || the carrier of L1 by A3,ZFMISC_1:96,RELAT_1:74;
A11: 1.L1 = 1.L2 by A1,C0SP1:def 3 .=1.L3 by A2,C0SP1:def 3;
0.L1 = 0.L2 by A1,C0SP1:def 3 .=0.L3 by A2,C0SP1:def 3;
hence thesis by A8,A9,A10,A11,C0SP1:def 3;
end;
theorem Lm1:
F_Rat is Subfield of F_Complex by EC_PF_1:5,GAUSSINT:14,RING_3:48;
theorem Th3:
F_Rat is Subring of F_Complex by RING_3:43,Lm1;
theorem Th4:
INT.Ring is Subring of F_Complex by RING_3:47,Th3,Th1;
Lm5:
A is Subring of B implies In(0.A, B) = 0.B & In(1.A,B) = 1.B
proof
assume
A1: A is Subring of B; then
A2: In(0.A,B) = In(0.B,B) by C0SP1:def 3
.= 0.B by SUBSET_1:def 8;
In(1.A,B) = In(1.B,B) by A1,C0SP1:def 3
.= 1.B by SUBSET_1:def 8;
hence thesis by A2;
end;
Lm6:
for a be Element of A st A is Subring of B holds a is Element of B
proof
let a be Element of A;
assume A is Subring of B; then
the carrier of A c= the carrier of B by C0SP1:def 3;
hence thesis;
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:
for x, y be Element of B, x1, y1 be Element of A st A is Subring of B &
x = x1 & y = y1 holds x + y = x1 + y1
proof
let x, y be Element of B,
x1, y1 be Element of A;
assume A is Subring of B; then
the addF of A = (the addF of B) || the carrier of A by C0SP1:def 3;
hence thesis by FUNCT_1:49,ZFMISC_1:87;
end;
theorem Th9:
for x, y be Element of B, x1, y1 be Element of A st
A is Subring of B & x = x1 & y = y1 holds x * y = x1 * y1
proof
let x, y be Element of B, x1, y1 be Element of A;
assume A is Subring of B; then
the multF of A = (the multF of B) || the carrier of A by C0SP1:def 3;
hence thesis by FUNCT_1:49,ZFMISC_1:87;
end;
registration
let c be Complex;
reduce In(c,F_Complex) to c;
reducibility
proof
c in COMPLEX by XCMPLX_0:def 2;
then c is Element of F_Complex by COMPLFLD:def 1;
hence thesis by SUBSET_1:def 8;
end;
end;
begin
:: Define Extended eval Function for commutative rings A c= B
:: based upon POLYNOM4
definition
let A,B be Ring;
let p be Polynomial of A;
let x be Element of B;
func Ext_eval(p,x) -> Element of B means
:Def1:
ex F be FinSequence of B st it = Sum F & len F = len p
& for n be Element of NAT st n in dom F holds
F.n = In(p.(n-'1),B) * (power B).(x,n-'1);
existence
proof
deffunc G(Nat) = In(p.($1-'1),B)*(power B).(x,$1-'1);
consider F be FinSequence of B such that
A1: len F = len p and
A2: for n be Nat st n in dom F holds F.n = G(n) from FINSEQ_2:sch 1;
take y = Sum F;
take F;
thus y = Sum F & len F = len p by A1;
let n be Element of NAT;
assume n in dom F;
hence thesis by A2;
end;
uniqueness
proof
let y1,y2 be Element of B;
given F1 be FinSequence of B such that
A3: y1 = Sum F1 and
A4: len F1 = len p and
A5: for n be Element of NAT st n in dom F1 holds
F1.n = In(p.(n-'1),B)*(power B).(x,n-'1);
given F2 be FinSequence of B such that
A6: y2 = Sum F2 and
A7: len F2 = len p and
A8: for n be Element of NAT st n in dom F2 holds
F2.n = In(p.(n-'1),B)*(power B).(x,n-'1);
A9: dom F1 = Seg len p by A4,FINSEQ_1:def 3;
now
let n be Nat;
assume
A10: n in dom F1; then
A11: n in dom F2 by A7,A9,FINSEQ_1:def 3;
thus F1.n = In(p.(n-'1),B) *(power B).(x,n-'1) by A5,A10
.= F2.n by A8,A11;
end;
hence thesis by A3,A4,A6,A7,FINSEQ_2:9;
end;
end;
theorem Th11:
for n being Element of NAT, A,B be Ring, z be Element of A st
A is Subring of B holds
(power B).(In(z,B),n) = In((power A).(z,n),B)
proof
let n be Element of NAT, A,B be Ring, z be Element of A;
assume
A0: A is Subring of B; then
z is Element of B by Lm6; then
A2: In(z,B) = z by SUBSET_1:def 8;
A3: 1_A = 1_B by A0,C0SP1:def 3;
reconsider x = z as Element of B by A0,Lm6;
(power B).(In(z,B),n) = In((power A).(z,n),B)
proof
defpred P[Nat] means (power B).(In(z,B),$1) = In((power A).(z,$1),B);
A5: P[0]
proof
A6: In(1.A,B) = 1.B by A0,Lm5;
In((power A).(z,0),B) = 1.B by A3,GROUP_1:def 7,A6;
hence thesis by A3,GROUP_1:def 7;
end;
A7: for m be Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume
A9: P[m];
A10: (power A).(z,m) is Element of B by A0,Lm6;
A11: In((power A).(z,m),B) = (power A).(z,m)
by A10,SUBSET_1:def 8;
A12: (power A).(z,m+1) is Element of B by A0,Lm6;
(power B).(In(z,B),m+1)
= (power B).(In(z,B),m)* In(z,B) by GROUP_1:def 7
.= (power A).(z,m)*z by A0,A11,A2,Th9,A9
.= (power A).(z,m+1) by GROUP_1:def 7
.= In((power A).(z,m+1),B) by A12,SUBSET_1:def 8;
hence thesis;
end;
for m be Nat holds P[m] from NAT_1:sch 2(A5,A7);
hence thesis;
end;
hence thesis;
end;
theorem Th12:
for x1,x2 be Element of A st A is Subring of B holds
In(x1,B) + In(x2,B) = In(x1+x2,B)
proof
let x1,x2 be Element of A;
assume
A0: A is Subring of B; then
x1 is Element of B by Lm6; then
A2: In(x1,B) = x1 by SUBSET_1:def 8;
x2 is Element of B by A0,Lm6; then
A4: In(x2,B) = x2 by SUBSET_1:def 8;
x1 + x2 is Element of B by A0,Lm6; then
In(x1+x2,B) = x1+x2 by SUBSET_1:def 8
.= In(x1,B)+In(x2,B) by A0,A2,A4,Th8;
hence thesis;
end;
theorem Th13:
for x1,x2 be Element of A st A is Subring of B holds
In(x1,B) * In(x2,B) = In(x1*x2,B)
proof
let x1,x2 be Element of A;
assume
A0: A is Subring of B; then
x1 is Element of B by Lm6; then
A2: In(x1,B) = x1 by SUBSET_1:def 8;
x2 is Element of B by A0,Lm6; then
A4: In(x2,B) = x2 by SUBSET_1:def 8;
x1*x2 is Element of B by A0,Lm6; then
In(x1*x2,B) = x1*x2 by SUBSET_1:def 8
.= In(x1,B)*In(x2,B) by A0,A2,A4,Th9;
hence thesis;
end;
theorem Th14:
for F be FinSequence of A,
G be FinSequence of B
st A is Subring of B & F = G holds In(Sum F,B) = Sum G
proof
let F be FinSequence of A, G be FinSequence of B;
assume
A0: A is Subring of B;
defpred P[Nat] means
for F being FinSequence of A, G being FinSequence of B
st len F = $1 & F = G holds In(Sum F,B) = Sum G;
P1: P[0]
proof
let F be FinSequence of A,
G be FinSequence of B;
assume
A1: len F = 0 & F = G; then
A2: F = <*>the carrier of A;
A3: G = <*>the carrier of B by A1;
In(Sum F,B) = In(0.A,B) by A2,RLVECT_1:43
.= In(0.B,B) by A0,C0SP1:def 3 .= 0.B by SUBSET_1:def 8
.= Sum G by A3,RLVECT_1:43;
hence thesis;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A4: P[n];
let F be FinSequence of A,
G be FinSequence of B;
assume
A5: len F = n+1 & F = G;
reconsider F0 = F| n as FinSequence of A;
n+1 in Seg (n+1) by FINSEQ_1:4; then
A6: n+1 in dom F by A5,FINSEQ_1:def 3;
rng F c= the carrier of A; then
reconsider af = F.(n+1) as Element of A by A6,FUNCT_1:3;
A7: len F0 = n by FINSEQ_1:59,A5,NAT_1:11;
A8: len F = (len F0) + 1 by A5,FINSEQ_1:59,NAT_1:11;
A9: F0 = F | dom F0 by A7,FINSEQ_1:def 3;
reconsider G0 = G| n as FinSequence of B;
n+1 in Seg (n+1) by FINSEQ_1:4; then
A10: n+1 in dom G by A5,FINSEQ_1:def 3;
rng G c= the carrier of B; then
reconsider bf = G.(n+1) as Element of B by A10,FUNCT_1:3;
A11: len F0 = n & F0 = G0 by FINSEQ_1:59,A5,NAT_1:11;
G = G0^<*bf*> by A5,FINSEQ_3:55; then
Sum G = Sum G0 + bf by FVSUM_1:71
.= In(Sum F0,B)+ bf by A4,A11
.= In(Sum F0,B) + In(af,B) by A5,SUBSET_1:def 8
.= In(Sum F0 + af,B) by A0,Th12
.= In(Sum F,B) by A5,A8,A9,RLVECT_1:38;
hence thesis;
end;
for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
hence thesis;
end;
theorem Th15:
for n be Nat, x be Element of A, p be 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
let n be Nat,x be Element of A, p be Polynomial of A;
assume
A0: A is Subring of B; then
In(p.(n-'1) * (power A).(x,n-'1),B)
= In(p.(n-'1),B)*In((power A).(x,n-'1),B) by Th13
.= In(p.(n-'1),B)*(power B).(In(x,B),n -'1) by A0,Th11;
hence thesis;
end;
theorem Th16:
for x be Element of A, p be Polynomial of A st A is Subring of B holds
Ext_eval(p,In(x,B)) = In(eval(p,x),B)
proof
let x be Element of A, p be Polynomial of A;
assume
A0: A is Subring of B;
consider F1 be FinSequence of B such that
A1: Ext_eval(p,In(x,B)) = Sum F1 and
A2: len F1 = len p and
A3: for n be Element of NAT st n in dom F1 holds
F1.n = In(p.(n-'1),B) * (power B).(In(x,B),n-'1) by Def1;
consider F2 be FinSequence of A such that
A4: eval(p,x) = Sum F2 and
A5: len F2 = len p and
A6: for n be Element of NAT st n in dom F2 holds
F2.n = p.(n-'1) * (power A).(x,n-'1) by POLYNOM4:def 2;
F1 = F2
proof
A11: rng F2 c= the carrier of A;
A8: dom F1 = dom F2 by A2,A5,FINSEQ_3:29;
for k be Nat st k in dom F1 holds F1.k = F2.k
proof
let k be Nat;
assume
A10: k in dom F1; then
F2.k is Element of A by A8,FUNCT_1:3,A11; then
A13: F2.k is Element of B by A0,Lm6;
F1.k = In(p.(k-'1),B) * (power B).(In(x,B),k-'1) by A3,A10
.= In(p.(k-'1) * (power A).(x,k-'1),B) by A0,Th15
.= In(F2.k,B) by A6,A10,A8
.= F2.k by A13,SUBSET_1:def 8;
hence thesis;
end;
hence thesis by A2,A5,FINSEQ_3:29;
end;
hence thesis by A1,A4,A0,Th14;
end;
:: Modify POLYNOM4:17
theorem Th17:
for x be Element of B holds Ext_eval(0_.A,x) = 0.B
proof
let x be Element of B;
consider F be FinSequence of B such that
A1: Ext_eval(0_.A,x) = Sum F and
A2: len F = len 0_.A and
for n be Element of NAT st n in dom F holds
F.n = In((0_.A).(n-'1),B) * (power B).(x,n-'1) by Def1;
F = <*>the carrier of B by A2,POLYNOM4:3;
hence thesis by A1,RLVECT_1:43;
end;
:: Modify POLYNOM4:18
theorem Th18:
for A,B being non degenerated Ring
for x be Element of B st A is Subring of B holds
Ext_eval(1_.A,x) = 1.B
proof
let A,B be non degenerated Ring;
let x be Element of B;
assume
A0: A is Subring of B;
consider F be FinSequence of B such that
A1: Ext_eval(1_.A,x) = Sum F and
A2: len F = len 1_.A and
A3: for n be Element of NAT st n in dom F holds
F.n = In((1_.A).(n-'1),B)*(power B).(x,n-'1) by Def1;
len F = 1 by A2,POLYNOM4:4; then
A4: F.1 = In((1_.A).(1-'1),B) * (power B).(x,1-'1) by A3,FINSEQ_3:25
.= In((1_.A).(0),B) * (power B).(x,1-'1) by XREAL_1:232
.= In(1.A,B) * (power B).(x,1-'1) by POLYNOM3:30
.= 1.B * (power B).(x,1-'1) by A0,Lm5
.= (power B).(x,0) by XREAL_1:232 .= 1_B by GROUP_1:def 7 .= 1.B;
Sum F = Sum <*1.B*> by A2,POLYNOM4:4,FINSEQ_1:40,A4 .= 1.B by RLVECT_1:44;
hence thesis by A1;
end;
:: Modify POLYNOM4:19
theorem Th19:
for x be Element of B, p,q be Polynomial of A st A is Subring of B holds
Ext_eval(p+q,x) = Ext_eval(p,x) + Ext_eval(q,x)
proof
let x be Element of B, p,q be Polynomial of A;
assume
A0: A is Subring of B;
reconsider k = max(len p,len q) as Element of NAT;
A1: k - len p >= 0 by XREAL_1:48,XXREAL_0:25;
consider F1 be FinSequence of B such that
A2: Ext_eval(p,x) = Sum F1 and
A3: len F1 = len p and
A4: for n be Element of NAT st n in dom F1 holds
F1.n = In(p.(n-'1),B) * (power B).(x,n-'1) by Def1;
A5: len (F1 ^ ((k-'(len F1)) |-> 0.B))
= len p + len ((k-'(len p)) |-> 0.B) by A3,FINSEQ_1:22
.= len p + (k-'(len p)) by CARD_1:def 7
.= len p + (k-(len p)) by A1,XREAL_0:def 2 .= k;
A6: k - len q >= 0 by XREAL_1:48,XXREAL_0:25;
k >= len p & k >= len q by XXREAL_0:25; then
A7: k - len (p+q) >= 0 by POLYNOM4:6,XREAL_1:48;
consider F3 be FinSequence of B such that
A8: Ext_eval(p+q,x) = Sum F3 and
A9: len F3 = len (p+q) and
A10: for n be Element of NAT st n in dom F3 holds
F3.n = In((p+q).(n-'1),B) * (power B).(x,n-'1) by Def1;
A11: len (F3 ^ ((k-'(len F3)) |-> 0.B))
= len F3 + len((k-'(len F3)) |-> 0.B) by FINSEQ_1:22
.= len (p+q) + (k-'(len (p+q))) by CARD_1:def 7,A9
.= len (p+q) + (k-(len (p+q))) by A7,XREAL_0:def 2
.= k;
consider F2 be FinSequence of B such that
A12: Ext_eval(q,x) = Sum F2 and
A13: len F2 = len q and
A14: for n be Element of NAT st n in dom F2 holds
F2.n = In(q.(n-'1),B) * (power B).(x,n-'1) by Def1;
len (F2 ^ ((k-'(len F2)) |-> 0.B))
= len q + len ((k-'(len q)) |-> 0.B) by A13,FINSEQ_1:22
.= len q + (k-'(len q)) by CARD_1:def 7
.= len q + (k-(len q)) by A6,XREAL_0:def 2 .= k;
then reconsider
G1 = F1 ^ ((k-'(len F1)) |-> 0.B), G2 = F2 ^ ((k-'(len F2)) |->
0.B), G3 = F3 ^ ((k-'(len F3)) |-> 0.B)
as Element of k-tuples_on the carrier of B by A5,A11,FINSEQ_2:92;
now
let n be Nat;
assume
A15: n in Seg k; then
A16: 0+1 <= n by FINSEQ_1:1;
A17: n <= k by A15,FINSEQ_1:1;
per cases by XXREAL_0:1;
suppose
A18: len p > len q; then
k = len p by XXREAL_0:def 10; then
len(p+q) = len p by A18,POLYNOM4:7; then
A20: n in dom F3 by A9,A15,A18,XXREAL_0:def 10,FINSEQ_1:def 3;
A21: len G2 = k by CARD_1:def 7; then
A22: n in dom G2 by A15,FINSEQ_1:def 3; then
A23: G2/.n = G2.n by PARTFUN1:def 6;
len G1 = k by CARD_1:def 7; then
A24: n in dom G1 by A15,FINSEQ_1:def 3; then
A25: G1/.n = G1.n by PARTFUN1:def 6;
A26: n in dom F1 by A3,A15,A18,XXREAL_0:def 10,FINSEQ_1:def 3;
A27: G1/.n = G1.n by A24,PARTFUN1:def 6 .= F1.n by A26,FINSEQ_1:def 7
.= F1/.n by A26,PARTFUN1:def 6;
A28: F1.n = In(p.(n-'1),B)*(power B).(x,n-'1) by A4,A26;
now
per cases;
suppose
n <= len q; then
A29: n in dom F2 by A16,A13,FINSEQ_3:25; then
A30: F2.n = In(q.(n-'1),B)*(power B).(x,n-'1) by A14;
A31: G2/.n = G2.n by A22,PARTFUN1:def 6 .= F2.n by A29,FINSEQ_1:def 7
.= F2/.n by A29,PARTFUN1:def 6;
thus G3.n = F3.n by A20,FINSEQ_1:def 7
.= In((p+q).(n-'1),B)*(power B).(x,n-'1) by A10,A20
.= In((p.(n-'1) + q.(n-'1)),B)
* (power B).(x,n-'1) by NORMSP_1:def 2
.= ( In (p.(n-'1),B) + In( q.(n-'1),B))
* (power B).(x,n-'1) by A0,Th12
.= In(p.(n-'1),B)*(power B).(x,n-'1)
+ In(q.(n-'1),B)*(power B).(x,n-'1) by VECTSP_1:def 3
.= In(p.(n-'1),B)*(power B).(x,n-'1)
+ F2/.n by A29,A30,PARTFUN1:def 6
.= F1/.n + F2/.n by A26,A28,PARTFUN1:def 6
.= (G1 + G2).n by A15,A25,A23,A27,A31,FVSUM_1:18;
end;
suppose
A32: n > len q; then
A33: n >= len q+1 by NAT_1:13; then
n-1 >= len q by XREAL_1:19; then
A34: n-'1 >= len q by XREAL_0:def 2;
n-len F2 <= k-len F2 by A17,XREAL_1:9; then
A35: n-len F2 <= k-'len F2 by XREAL_0:def 2;
A36: n-len F2 >= 1 by A13,A33,XREAL_1:19; then
n-len F2 = n-'len F2 by XREAL_0:def 2; then
A37: n-len F2 in Seg (k-'len F2) by A36,A35;
n <= len G2 by A15,A21,FINSEQ_1:1; then
A38: G2/.n = ((k-'(len F2)) |-> 0.B).(n - len F2)
by A13,A23,A32,FINSEQ_1:24 .= 0.B by A37,FUNCOP_1:7;
thus G3.n = F3.n by A20,FINSEQ_1:def 7
.= In((p+q).(n-'1),B) * (power B).(x,n-'1) by A10,A20
.= In(p.(n-'1) + q.(n-'1),B) * (power B).(x,n-'1)
by NORMSP_1:def 2
.= In(p.(n-'1) + 0.A,B) * (power B).(x,n-'1) by A34,ALGSEQ_1:8
.= F1.n by A4,A26 .= G1/.n + 0.B by A26,A27,PARTFUN1:def 6
.= (G1 + G2).n by A15,A25,A23,A38,FVSUM_1:18;
end;
end;
hence G3.n = (G1 + G2).n;
end;
suppose
A39: len p < len q; then
k = len q by XXREAL_0:def 10; then
len(p+q) = len q by A39,POLYNOM4:7; then
A41: n in dom F3 by A9,A15,A39,XXREAL_0:def 10,FINSEQ_1:def 3;
A42: len G1 = k by CARD_1:def 7; then
A43: n in dom G1 by A15,FINSEQ_1:def 3; then
A44: G1/.n = G1.n by PARTFUN1:def 6;
len G2 = k by CARD_1:def 7; then
A45: n in dom G2 by A15,FINSEQ_1:def 3; then
A46: G2/.n = G2.n by PARTFUN1:def 6;
A47: n in dom F2 by A13,A15,A39,XXREAL_0:def 10,FINSEQ_1:def 3;
A48: G2/.n = G2.n by A45,PARTFUN1:def 6 .= F2.n by A47,FINSEQ_1:def 7
.= F2/.n by A47,PARTFUN1:def 6;
A49: F2.n = In(q.(n-'1),B)*(power B).(x,n-'1) by A14,A47;
now
per cases;
suppose n <= len p; then
A50: n in dom F1 by A16,A3,FINSEQ_3:25; then
A51: F1.n = In(p.(n-'1),B)*(power B).(x,n-'1) by A4;
A52: G1/.n = G1.n by A43,PARTFUN1:def 6 .= F1.n by A50,FINSEQ_1:def 7
.= F1/.n by A50,PARTFUN1:def 6;
thus G3.n = F3.n by A41,FINSEQ_1:def 7
.= In((p+q).(n-'1),B) * (power B).(x,n-'1) by A10,A41
.= In(p.(n-'1) + q.(n-'1),B) * (power B).(x,n-'1)
by NORMSP_1:def 2
.= ( In (p.(n-'1),B) + In( q.(n-'1),B))
* (power B).(x,n-'1) by A0,Th12
.= In(p.(n-'1),B)*(power B).(x,n-'1)
+ In(q.(n-'1),B)*(power B).(x,n-'1) by VECTSP_1:def 3
.= F1/.n + In(q.(n-'1),B)*(power B).(x,n-'1)
by A50,A51,PARTFUN1:def 6
.= F1/.n + F2/.n by A47,A49,PARTFUN1:def 6
.= (G1 + G2).n by A15,A44,A46,A48,A52,FVSUM_1:18;
end;
suppose
A53: n > len p; then
A54: n >= len p+1 by NAT_1:13;then
n-1 >= len p by XREAL_1:19; then
A55: n-'1 >= len p by XREAL_0:def 2;
n-len F1 <= k-len F1 by A17,XREAL_1:9; then
A56: n-len F1 <= k-'len F1 by XREAL_0:def 2;
A57: n-len F1 >= 1 by A3,A54,XREAL_1:19; then
n-len F1 = n-'len F1 by XREAL_0:def 2; then
A58: n-len F1 in Seg (k-'len F1) by A57,A56;
n <= len G1 by A15,A42,FINSEQ_1:1; then
A59: G1/.n = ((k-'(len F1)) |-> 0.B).(n-len F1) by A3,A44,A53,FINSEQ_1:24
.= 0.B by A58,FUNCOP_1:7;
thus G3.n = F3.n by A41,FINSEQ_1:def 7
.= In((p+q).(n-'1),B)*(power B).(x,n-'1) by A10,A41
.= In(p.(n-'1) + q.(n-'1),B) * (power B).(x,n-'1) by NORMSP_1:def 2
.= In(0.A + q.(n-'1),B) * (power B).(x,n-'1) by A55,ALGSEQ_1:8
.= F2.n by A14,A47
.= 0.B + G2/.n by A47,A48,PARTFUN1:def 6
.= (G1 + G2).n by A15,A44,A46,A59,FVSUM_1:18;
end;
end;
hence G3.n = (G1 + G2).n;
end;
suppose
A60: len p = len q;
len G2 = k by CARD_1:def 7; then
A61: n in dom G2 by A15,FINSEQ_1:def 3; then
A62: G2/.n = G2.n by PARTFUN1:def 6;
len G1 = k by CARD_1:def 7; then
A63: n in dom G1 by A15,FINSEQ_1:def 3; then
A64: G1/.n = G1.n by PARTFUN1:def 6;
A65: len G3 = k by CARD_1:def 7;
A66: n in dom F2 by A13,A15,A60,FINSEQ_1:def 3;
A67: n in dom F1 by A3,A15,A60,FINSEQ_1:def 3; then
A68: F1.n = In(p.(n-'1),B)*(power B).(x,n-'1) by A4;
A69: G1/.n = G1.n by A63,PARTFUN1:def 6 .= F1.n by A67,FINSEQ_1:def 7
.= F1/.n by A67,PARTFUN1:def 6;
now
per cases;
suppose
A70: n <= len (p+q);
A71: n in dom F2 by A13,A15,A60,FINSEQ_1:def 3; then
A72: F2.n = In(q.(n-'1),B)*(power B).(x,n-'1) by A14;
A73: G2/.n = G2.n by A61,PARTFUN1:def 6 .= F2.n by A71,FINSEQ_1:def 7
.= F2/.n by A71,PARTFUN1:def 6;
n in Seg len (p+q) by A16,A70; then
A74: n in dom F3 by A9,FINSEQ_1:def 3;
hence G3.n = F3.n by FINSEQ_1:def 7
.= In((p+q).(n-'1),B) * (power B).(x,n-'1) by A10,A74
.= In(p.(n-'1) + q.(n-'1),B)*(power B).(x,n-'1) by NORMSP_1:def 2
.= ( In (p.(n-'1),B) + In( q.(n-'1),B))
* (power B).(x,n-'1) by A0,Th12
.= In(p.(n-'1),B)*(power B).(x,n-'1)
+ In(q.(n-'1),B)*(power B).(x,n-'1) by VECTSP_1:def 3
.= In(p.(n-'1),B)*(power B).(x,n-'1) + F2/.n
by A71,A72,PARTFUN1:def 6
.= F1/.n + F2/.n by A67,A68,PARTFUN1:def 6
.= (G1 + G2).n by A15,A64,A62,A69,A73,FVSUM_1:18;
end;
suppose
A75: n > len (p+q); then
A76: n >= len (p+q)+1 by NAT_1:13; then
n-1 >= len (p+q)+1-1 by XREAL_1:9; then
A77: n-'1 >= len (p+q) by XREAL_0:def 2;
n-len F3 <= k-len F3 by A17,XREAL_1:9; then
A78: n-len F3 <= k-'len F3 by XREAL_0:def 2;
A79: G2.n = F2.n by A66,FINSEQ_1:def 7
.= In(q.(n-'1),B)*(power B).(x,n-'1) by A14,A66;
A80: G1.n = F1.n by A67,FINSEQ_1:def 7
.= In(p.(n-'1),B)*(power B).(x,n-'1) by A4,A67;
A81: n-len F3 >= 1 by A9,A76,XREAL_1:19; then
n-len F3 = n-'len F3 by XREAL_0:def 2; then
A82: n-len F3 in Seg (k-'len F3) by A81,A78;
n <= len G3 by A15,A65,FINSEQ_1:1;
hence
G3.n=((k-'(len F3)) |-> 0.B).(n-len F3) by A9,A75,FINSEQ_1:24
.= 0.B * (power B).(x,n-'1) by A82,FUNCOP_1:7
.= In(0.A,B)*(power B).(x,n-'1) by A0,Lm5
.= In((p+q).(n-'1),B) * (power B).(x,n-'1) by A77,ALGSEQ_1:8
.= In(p.(n-'1) + q.(n-'1),B) * (power B).(x,n-'1) by NORMSP_1:def 2
.= ( In (p.(n-'1),B) + In( q.(n-'1),B))
* (power B).(x,n-'1) by A0,Th12
.= In(p.(n-'1),B)*(power B).(x,n-'1)
+ In(q.(n-'1),B)*(power B).(x,n-'1) by VECTSP_1:def 3
.= (G1 + G2).n by A15,A80,A79,FVSUM_1:18;
end;
end;
hence G3.n = (G1 + G2).n;
end;
end;
then
A83: G3 = G1 + G2 by FINSEQ_2:119;
A84: Sum G3 = Sum F3 + Sum ((k-'(len F3)) |-> 0.B) by RLVECT_1:41
.= Sum F3 + 0.B by MATRIX_3:11 .= Sum F3;
A85: Sum G2 = Sum F2 + Sum ((k-'(len F2)) |-> 0.B) by RLVECT_1:41
.= Sum F2 + 0.B by MATRIX_3:11 .= Sum F2;
Sum G1 = Sum F1 + Sum ((k-'(len F1)) |-> 0.B) by RLVECT_1:41
.= Sum F1 + 0.B by MATRIX_3:11 .= Sum F1;
hence thesis by A2,A12,A8,A85,A84,A83,FVSUM_1:76;
end;
theorem Th20:
for p,q be Polynomial of A st A is Subring of B & len p > 0 & len q > 0
for x be 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
let p,q be Polynomial of A;
assume that
A0: A is Subring of B and
A1: len p > 0 and
A2: len q > 0;
A3: len q >= 0+1 by A2,NAT_1:13;
A5: len p >= 0+1 by A1,NAT_1:13;
A6: len p-1 = len p-'1 by A1,XREAL_0:def 2;
A7: len p + len q >= 0+(1+1) by A5,A3,XREAL_1:7;
reconsider i1=len p + len q - 1 as Element of NAT by A1,INT_1:3;
A9: i1-'1+1 = i1 by A7,XREAL_1:19,XREAL_1:235;
set LMp=Leading-Monomial(p), LMq=Leading-Monomial(q);
let x be Element of B;
consider F be FinSequence of B such that
A10: Ext_eval(LMp*'LMq,x) = Sum F and
A11: len F = len (LMp*'LMq) and
A12: for n be Element of NAT st n in dom F holds
F.n=In((LMp*'LMq).(n-'1),B)*(power B).(x,n-'1) by Def1;
consider r be FinSequence of A such that
A13: len r = i1-'1+1 and
A14: (LMp*'LMq).(i1-'1) = Sum r and
A15: for k be Element of NAT st k in dom r holds
r.k = LMp.(k-'1)*LMq.(i1-'1+1-'k) by POLYNOM3:def 9;
len p+0 <= len p+(len q-1) by A2,XREAL_1:7; then
len p in Seg len r by A5,A9,A13; then
A16: len p in dom r by FINSEQ_1:def 3;
i1-'len p = len p+(len q-1)-len p by A2,XREAL_0:def 2
.= len q-'1 by A2,XREAL_0:def 2; then
A17: r.(len p) = LMp.(len p-'1) * LMq.(len q-'1) by A9,A15,A16;
now
let i be Element of NAT;
assume that
A18: i in dom r and
A19: i <> len p;
i >= 0+1 by A18,FINSEQ_3:25; then
i-'1 = i-1 by XREAL_0:def 2; then
A20: i-'1 <> len p-'1 by A6,A19;
thus r/.i = r.i by A18,PARTFUN1:def 6
.= LMp.(i-'1) * LMq.(i1-'1+1-'i) by A15,A18
.= 0.A*LMq.(i1-'1+1-'i) by A20,POLYNOM4:def 1 .= 0.A;
end;
then
A21: Sum r = r/.(len p) by A16,POLYNOM2:3
.= LMp.(len p-'1) * LMq.(len q-'1) by A16,A17,PARTFUN1:def 6
.= p.(len p-'1) * LMq.(len q-'1) by POLYNOM4:def 1
.= p.(len p-'1) * q.(len q-'1) by POLYNOM4:def 1;
A22: len q-1 = len q-'1 by A2,XREAL_0:def 2;
A23: now
let i be Element of NAT;
assume that
A24: i in dom F and
A25: i <> i1;
consider r1 be FinSequence of A such that
A26: len r1 = i-'1+1 and
A27: (LMp*'LMq).(i-'1) = Sum r1 and
A28: for k be Element of NAT st k in dom r1 holds r1.k=LMp.(k-'1)*LMq.
(i-'1+1-'k) by POLYNOM3:def 9;
A29: i-'1+1 = i by A24,FINSEQ_3:25,XREAL_1:235;
A30: now
let j be Element of NAT;
assume
A31: j in dom r1; then
j >= 0+1 by FINSEQ_3:25; then
A32: j-'1 = j-1 by XREAL_0:def 2;
per cases;
suppose
j<>len p; then
A33: j-'1 <> len p-'1 by A6,A32;
thus r1.j = LMp.(j-'1)*LMq.(i-'1+1-'j) by A28,A31
.= 0.A*LMq.(i-'1+1-'j) by A33,POLYNOM4:def 1
.= 0.A;
end;
suppose
A34: j=len p;
j in Seg len r1 by A31,FINSEQ_1:def 3; then
i >= 0+j by A26,A29,FINSEQ_1:1; then
i-'len p = i-len p by A34,XREAL_1:19,XREAL_0:def 2; then
A35: i-'len p <> len q-'1 by A22,A25;
thus r1.j = LMp.(j-'1)*LMq.(i-'len p) by A28,A29,A31,A34
.= LMp.(j-'1)*0.A by A35,POLYNOM4:def 1 .= 0.A;
end;
end;
thus F/.i = F.i by A24,PARTFUN1:def 6
.= In(Sum r1,B)*(power B).(x,i-'1) by A12,A24,A27
.= In(0.A,B)*(power B).(x,i-'1) by A30,POLYNOM3:1
.= 0.B*(power B).(x,i-'1) by A0,Lm5
.= 0.B;
end;
A36: len p+len q-2 >= 0 by A7,XREAL_1:19;
len p+len q-(1+1) >= 0 by A7,XREAL_1:19; then
A37: i1-'1 = len p+len q-1-1 by XREAL_0:def 2
.= len p+len q-'2 by A36,XREAL_0:def 2;
per cases;
suppose (LMp*'LMq).(i1-'1) <> 0.A; then
len F >= i1 by A11,ALGSEQ_1:8,A9,NAT_1:13; then
A38: i1 in dom F by A7,XREAL_1:19,FINSEQ_3:25;
hence Ext_eval((Leading-Monomial(p))*'(Leading-Monomial(q)),x)
= F/.i1 by A10,A23,POLYNOM2:3
.= F.i1 by A38,PARTFUN1:def 6
.= In(p.(len p-'1)*q.(len q-'1),B)
*(power B).(x,len p+len q-'2) by A12,A14,A37,A21,A38;
end;
suppose
A39: (LMp*'LMq).(i1-'1) = 0.A;
now
let j be Nat;
assume j >= 0;
j in NAT by ORDINAL1:def 12;
then consider r1 be FinSequence of A such that
A40: len r1 = j+1 and
A41: (LMp*'LMq).j = Sum r1 and
A42: for k be Element of NAT st k in dom r1 holds r1.k = LMp.(k-'1)*
LMq.(j+1-'k) by POLYNOM3:def 9;
now
per cases;
suppose
j = i1-'1;
hence (LMp*'LMq).j = 0.A by A39;
end;
suppose
A43: j <> i1-'1;
now
let k be Element of NAT;
assume
A44: k in dom r1;
per cases;
suppose
A45: k-'1 <> len p-'1;
thus r1.k = LMp.(k-'1)*LMq.(j+1-'k) by A42,A44
.= 0.A*LMq.(j+1-'k) by A45,POLYNOM4:def 1 .= 0.A;
end;
suppose
A46: k-'1 = len p-'1;
A47: k in Seg len r1 by A44,FINSEQ_1:def 3;
0+1 <= k by A44,FINSEQ_3:25; then
A48: k-'1 = k-1 by XREAL_0:def 2;
0+k <= j+1 by A40,A47,FINSEQ_1:1; then
j+1-k >= 0 by XREAL_1:19; then
A49: j+1-'k = j-len p+1 by A6,A46,A48,XREAL_0:def 2;
A50: j-len p+1 <> i1-'1-len p+1 by A43;
thus r1.k = LMp.(k-'1)*LMq.(j+1-'k) by A42,A44
.= LMp.(k-'1)*0.A by A22,A9,A49,A50,POLYNOM4:def 1
.= 0.A;
end;
end;
hence (LMp*'LMq).j = 0.A by A41,POLYNOM3:1;
end;
end;
hence (LMp*'LMq).j = 0.A;
end; then
0 is_at_least_length_of (LMp*'LMq); then
len (LMp*'LMq) = 0 by ALGSEQ_1:def 3; then
A52: LMp*'LMq = 0_.A by POLYNOM4:5;
0.B = In(p.(len p-'1) * q.(len q-'1),B)
by A0,Lm5,A21,A14,A39;
hence thesis by Th17,A52;
end;
end;
theorem Th21:
for p be Polynomial of A for x be 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
let p be Polynomial of A;
let x be Element of B;
assume
A0: A is Subring of B;
set LMp=Leading-Monomial(p);
consider F be FinSequence of B such that
A1: Ext_eval(LMp,x) = Sum F and
A2: len F = len LMp and
A3: for n be Element of NAT st n in dom F holds
F.n = In(LMp.(n-'1),B)*(power B).(x,n-'1) by Def1;
A4: len F = len p by A2,POLYNOM4:15;
per cases;
suppose
A5: len p > 0; then
A7: len p >= 0+1 by NAT_1:13; then
A6: len p in dom F by A4,FINSEQ_3:25;
now
A8: len p-'1 = len p-1 by A5,XREAL_0:def 2;
let i be Element of NAT;
assume that
A9: i in dom F and
A10: i <> len p;
i >= 0+1 by A9,FINSEQ_3:25; then
i-'1 = i-1 by XREAL_0:def 2; then
A11: i-'1 <> len p-'1 by A10,A8;
thus F/.i = F.i by A9,PARTFUN1:def 6
.= In(LMp.(i-'1),B)*(power B).(x,i-'1) by A3,A9
.= In(0.A,B)*(power B).(x,i-'1) by A11,POLYNOM4:def 1
.= 0.B *(power B).(x,i-'1) by A0,Lm5
.= 0.B;
end;
then Sum F = F/.(len p) by A4,A7,FINSEQ_3:25,POLYNOM2:3
.= F.(len p) by A6,PARTFUN1:def 6
.= In(LMp.(len p-'1),B)*(power B).(x,len p-'1) by A3,A7,A4,FINSEQ_3:25;
hence thesis by A1,POLYNOM4:def 1;
end;
suppose
A12: len p = 0; then
A13: p = 0_.A by POLYNOM4:5;
LMp = 0_.A by A12,POLYNOM4:12;
hence Ext_eval(Leading-Monomial(p),x) =
0.B*(power B).(x,len p-'1) by Th17
.= In(0.A,B) *(power B).(x,len p-'1) by A0,Lm5
.= In(p.(len p-'1),B)*(power B).(x,len p-'1) by A13,FUNCOP_1:7;
end;
end;
::Modify POLYNOM_4:Lm3:
theorem Th22:
for B be comRing
for p,q be Polynomial of A for x be 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
let B be comRing;
let p,q be Polynomial of A;
let x be Element of B;
assume
A0: A is Subring of B;
per cases;
suppose
A1: len p <> 0 & len q <> 0; then
A2: len q >= 0+1 & len p >= 0+1 by NAT_1:13;
A3: len q-1 = len q-'1 & len p-1 = len p-'1 by A1,XREAL_0:def 2;
len p+len q >= 0+(1+1) by A2,XREAL_1:7; then
A4: len p+len q-'2 = len p+len q-2 by XREAL_1:19,XREAL_0:def 2;
A5: len p+len q-(1+1) = len p-1+(len q-1);
thus
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) by A0,A1,Th20
.= In(p.(len p-'1)*q.(len q-'1),B)
*((power B).(x,len p-'1)*(power B).(x,len q-'1)) by A3,A4,A5,POLYNOM2:1
.= In(p.(len p-'1),B)*In(q.(len q-'1),B)*
((power B).(x,len p-'1)*(power B).(x,len q-'1)) by A0,Th13
.= In(p.(len p-'1),B)*(In(q.(len q-'1),B)*
((power B).(x,len p-'1)*(power B).(x,len q-'1))) by GROUP_1:def 3
.= In(p.(len p-'1),B)*((power B).(x,len p-'1)*
(In(q.(len q-'1),B)*(power B).(x,len q-'1)))
by GROUP_1:def 3
.= In(p.(len p-'1),B)*(power B).(x,len p-'1)*
(In(q.(len q-'1),B)*(power B).(x,len q-'1)) by GROUP_1:def 3
.= In(p.(len p-'1),B)*(power B).(x,len p-'1) *
Ext_eval(Leading-Monomial(q),x) by A0,Th21
.= Ext_eval(Leading-Monomial(p),x)*Ext_eval(Leading-Monomial(q),x)
by A0,Th21;
end;
suppose
len p = 0; then
A6: Leading-Monomial(p) = 0_.A by POLYNOM4:12;
hence Ext_eval((Leading-Monomial(p))*'(Leading-Monomial(q)),x) =
Ext_eval(0_.A,x) by POLYNOM4:2
.= 0.B * Ext_eval(Leading-Monomial(q),x) by Th17
.= Ext_eval(Leading-Monomial(p),x)* Ext_eval(Leading-Monomial(q),x)
by A6,Th17;
end;
suppose
len q = 0;
then len Leading-Monomial(q) = 0 by POLYNOM4:15; then
A7: Leading-Monomial(q) = 0_.A by POLYNOM4:5;
hence Ext_eval((Leading-Monomial(p))*'(Leading-Monomial(q)),x)
= Ext_eval(0_.A,x) by POLYNOM3:34
.= Ext_eval(Leading-Monomial(p),x)*0.B by Th17
.= Ext_eval(Leading-Monomial(p),x)* Ext_eval(Leading-Monomial(q),x)
by A7,Th17;
end;
end;
:: Modify POLYNOM4:23
theorem Th15:
for B be comRing
for p,q be Polynomial of A for x be 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
let B be comRing;
let p1,q be Polynomial of A;
let x be Element of B;
assume
A0: A is Subring of B;
set p=Leading-Monomial(p1);
defpred P[Nat] means for q be Polynomial of A holds len q = $1 implies
Ext_eval(p*'q,x) = Ext_eval(p,x)*Ext_eval(q,x);
A1: for k be Nat st for n be Nat st n < k holds P[n] holds P[k]
proof
let k be Nat;
assume
A2: for n be Nat st n < k holds for q be Polynomial of A holds len q = n
implies Ext_eval(p*'q,x) = Ext_eval(p,x) * Ext_eval(q,x);
let q be Polynomial of A;
assume
A3: len q = k;
per cases;
suppose
A4: len q <> 0;
set LMq = Leading-Monomial(q);
consider r be Polynomial of A such that
A5: len r < len q and
A6: q = r+Leading-Monomial(q) and
for n be Element of NAT st n < len q-1 holds r.n = q.n
by A4,POLYNOM4:16;
thus Ext_eval(p*'q,x)=Ext_eval(p*'r+p*'LMq,x) by A6,POLYNOM3:31
.= Ext_eval(p*'r,x) + Ext_eval(p*'LMq,x) by A0,Th19
.= Ext_eval(p,x)*Ext_eval(r,x)+Ext_eval(p*'LMq,x) by A2,A3,A5
.= Ext_eval(p,x)*Ext_eval(r,x) + Ext_eval(p,x)*Ext_eval(LMq,x)
by A0,Th22
.= Ext_eval(p,x)*(Ext_eval(r,x) + Ext_eval(LMq,x))
by VECTSP_1:def 7
.= Ext_eval(p,x) * Ext_eval(q,x) by A0,A6,Th19;
end;
suppose
len q = 0; then
A7: q = 0_.A by POLYNOM4:5;
hence Ext_eval(p*'q,x) = Ext_eval(0_.A,x) by POLYNOM3:34
.= Ext_eval(p,x) * 0.B by Th17
.= Ext_eval(p,x) * Ext_eval(q,x) by A7,Th17;
end;
end;
A8: for n be Nat holds P[n] from NAT_1:sch 4(A1);
len q = len q;
hence thesis by A8;
end;
:: Modify POLYNOM4:24
theorem Th24:
for B be comRing
for p,q be Polynomial of A for x be Element of B st A is Subring of B
holds Ext_eval(p*'q,x) = Ext_eval(p,x) * Ext_eval(q,x)
proof
let B be comRing;
let p,q be Polynomial of A;
let x be Element of B;
assume
A0: A is Subring of B;
defpred P[Nat] means for p be Polynomial of A holds len p = $1
implies Ext_eval(p*'q,x) = Ext_eval(p,x)* Ext_eval(q,x);
A1: for k be Nat st for n be Nat st n < k holds P[n] holds P[k]
proof
let k be Nat;
assume
A2: for n be Nat st n < k holds for p be Polynomial of A holds len p =
n implies Ext_eval(p*'q,x) = Ext_eval(p,x) * Ext_eval(q,x);
let p be Polynomial of A;
assume
A3: len p = k;
per cases;
suppose
A4: len p <> 0;
set LMp = Leading-Monomial(p);
consider r be Polynomial of A such that
A5: len r < len p and
A6: p = r+Leading-Monomial(p) and
for n be Element of NAT st n < len p-1 holds r.n = p.n by A4,POLYNOM4:16;
thus Ext_eval(p*'q,x) = Ext_eval(r*'q+LMp*'q,x) by A6,POLYNOM3:32
.= Ext_eval(r*'q,x) + Ext_eval(LMp*'q,x) by A0,Th19
.= Ext_eval(r,x)*Ext_eval(q,x) + Ext_eval(LMp*'q,x) by A2,A3,A5
.= Ext_eval(r,x)*Ext_eval(q,x) + Ext_eval(LMp,x)*Ext_eval(q,x)
by A0,Th15
.= (Ext_eval(r,x)+Ext_eval(LMp,x))*Ext_eval(q,x) by VECTSP_1:def 7
.= Ext_eval(p,x) * Ext_eval(q,x) by A0,A6,Th19;
end;
suppose
len p = 0; then
A7: p = 0_.A by POLYNOM4:5;
hence Ext_eval(p*'q,x) = Ext_eval(0_.A,x) by POLYNOM4:2
.= 0.B * Ext_eval(q,x) by Th17
.= Ext_eval(p,x) * Ext_eval(q,x) by A7,Th17;
end;
end;
A8: for n be Nat holds P[n] from NAT_1:sch 4(A1);
len p = len p;
hence thesis by A8;
end;
:: modified POLYNOM5:37
theorem Th25:
for x be Element of B, z0 be Element of A
st A is Subring of B holds Ext_eval(<%z0%>,x) = In(z0,B)
proof
let x be Element of B, z0 be Element of A;
assume
A0: A is Subring of B;
consider F be FinSequence of B such that
A1: Ext_eval(<%z0%>,x) = Sum F and
A2: len F = len <%z0%> and
A3: for n be Element of NAT st n in dom F holds
F.n = In(<%z0%>.(n-'1),B)*(power B).(x,n-'1) by Def1;
per cases by A2,ALGSEQ_1:def 5,NAT_1:25;
suppose
A4: len F = 0;
A5: z0 = <%z0%>.0 by POLYNOM5:32 .= (0_.A).0 by A4,A2,POLYNOM4:5
.=0.A by FUNCOP_1:7;
Ext_eval(<%z0%>,x) = Ext_eval(0_.A,x) by A4,A2,POLYNOM4:5
.= 0.B by Th17
.= In(z0,B) by A5,A0,Lm5;
hence thesis;
end;
suppose
A6: len F = 1; then
A7: F.1 = In(<%z0%>.(1-'1),B)*(power B).(x,1-'1) by A3,FINSEQ_3:25
.=In( <%z0%>.0,B)*(power B).(x,1-'1) by XREAL_1:232
.= In( <%z0%>.0,B)*(power B).(x,0) by XREAL_1:232
.= In( z0,B) * (power B).(x,0) by POLYNOM5:32
.= In(z0,B) * 1_B by GROUP_1:def 7
.= In(z0,B);
Ext_eval(<%z0%>,x) = Sum <*In(z0,B)*> by A6,A7,FINSEQ_1:40,A1
.= In(z0,B) by RLVECT_1:44;
hence thesis;
end;
end;
:: modified POLYNOM5:44
theorem
for x be Element of B, z0,z1 be Element of A st A is Subring of B
holds Ext_eval(<%z0,z1%>,x) = In(z0,B)+In(z1,B)*x
proof
let x be Element of B, z0,z1 be Element of A;
assume
A0: A is Subring of B;
consider F be FinSequence of B such that
A1: Ext_eval(<%z0,z1%>,x) = Sum F and
A2: len F = len <%z0,z1%> and
A3: for n be Element of NAT st n in dom F holds
F.n = In(<%z0,z1%>.(n-'1),B)*(power B).(x,n-'1) by Def1;
len F = 0 or ... or len F = 2 by A2,POLYNOM5:39;
then per cases;
suppose
len F = 0; then
A4: <%z0,z1%> = 0_.A by A2,POLYNOM4:5;
hence Ext_eval(<%z0,z1%>,x)=0.B by Th17.=In(0.A,B) by A0,Lm5
.= In((0_.A).0,B) by FUNCOP_1:7
.= In(z0,B)+ 0.B * x by A4,POLYNOM5:38
.= In(z0,B) + In(0.A,B) *x by A0,Lm5
.= In(z0,B) + In((0_.A).1,B)*x by FUNCOP_1:7
.= In(z0,B)+ In(z1,B)*x by A4,POLYNOM5:38;
end;
suppose
A5: len F = 1;
then F.1 = In(<%z0,z1%>.(1-'1),B)*(power B).(x,1-'1) by A3,FINSEQ_3:25
.= In(<%z0,z1%>.0,B)* (power B).(x,1-'1) by XREAL_1:232
.= In(<%z0,z1%>.0,B)* (power B).(x,0) by XREAL_1:232
.= In(z0,B) * (power B).(x,0) by POLYNOM5:38
.= In(z0,B) * 1_B by GROUP_1:def 7
.= In(z0,B);
then F = <*In(z0,B)*> by A5,FINSEQ_1:40;
hence Ext_eval(<%z0,z1%>,x) = In(z0,B) + 0.B*x by A1,RLVECT_1:44
.= In(z0,B) + In(0.A,B) *x by A0,Lm5
.= In(z0,B) + In(<%z0,z1%>.1,B)*x by A2,A5,ALGSEQ_1:8
.= In(z0,B) + In(z1,B)*x by POLYNOM5:38;
end;
suppose
A6: len F = 2; then
A7: F.1 = In(<%z0,z1%>.(1-'1),B)*(power B).(x,1-'1) by A3,FINSEQ_3:25
.= In(<%z0,z1%>.0,B)* (power B).(x,1-'1) by XREAL_1:232
.= In(<%z0,z1%>.0,B)* (power B).(x,0) by XREAL_1:232
.= In(z0,B) * (power B).(x,0) by POLYNOM5:38
.= In(z0,B) * 1_B by GROUP_1:def 7
.= In(z0,B);
A8: 2-'1 = 2-1 by XREAL_0:def 2;
F.2 = In(<%z0,z1%>.(2-'1),B)*(power B).(x,2-'1) by A3,A6,FINSEQ_3:25
.= In(z1,B) * (power B).(x,1) by A8,POLYNOM5:38
.= In(z1,B) * x by GROUP_1:50;
then F = <* In(z0,B),In(z1,B)*x *> by A6,A7,FINSEQ_1:44;
hence thesis by A1,RLVECT_1:45;
end;
end;
begin
:: Definition of Integral Element over A in B
definition
let A,B be Ring;
let x be Element of B;
pred x is_integral_over A means
ex f be Polynomial of A st LC f = 1.A & Ext_eval(f,x) = 0.B;
end;
theorem Th27:
for A being non degenerated Ring
for a be Element of A st A is Subring of B holds
In(a,B) is_integral_over A
proof
let A be non degenerated Ring;
let a be Element of A;
assume
A0: A is Subring of B;
set p = <% -a, 1.A %>;
p.(len p -' 1) = p.(2-'1) by POLYNOM5:40 .= p.(2-1) by XREAL_1:233
.= p.1; then
A2: LC p = 1.A by POLYNOM5:38;
A3: eval(p,a) = -a + a by POLYNOM5:47
.= a - a .= 0.A by RLVECT_1:15;
Ext_eval(p,In(a,B)) = In(eval(p,a),B) by A0,Th16
.= 0.B by A0,Lm5,A3;
hence thesis by A2;
end;
definition
let A be non degenerated Ring, B be Ring;
assume
A0: A is Subring of B;
func integral_closure(A,B) -> non empty Subset of B equals
{z where z is Element of B: z is_integral_over A};
coherence
proof
set M ={z where z is Element of B: z is_integral_over A};
A1: now
let u be object;
assume u in M;
then ex z being Element of B st u = z & z is_integral_over A;
hence u in the carrier of B;
end;
In(0.A,B) is_integral_over A by A0,Th27; then
0.B is_integral_over A by A0,Lm5; then
0.B in M;
hence thesis by A1,TARSKI:def 3;
end;
end;
definition
let c be Complex;
attr c is algebraic means
ex x being Element of F_Complex st x = c & x is_integral_over F_Rat;
end;
definition
let x be Element of F_Complex;
redefine attr x is algebraic means :: redefines algebraic (ALGNUM_1, definition)
x is_integral_over F_Rat;
compatibility;
end;
definition
let c be Complex;
attr c is algebraic_integer means
ex x being Element of F_Complex st x = c & x is_integral_over INT.Ring;
end;
definition
let x be Element of F_Complex;
redefine attr x is algebraic_integer means :: redefines algebraic_integer (ALGNUM_1, definition)
x is_integral_over INT.Ring;
compatibility;
end;
notation
let x be Complex;
antonym x is transcendental for x is algebraic;
end;
registration
cluster rational -> algebraic for Complex;
coherence
proof
let c be Complex;
assume c is rational;
then reconsider c as Element of F_Rat by RAT_1:def 2;
take In(c,F_Complex);
thus thesis by Th3,Th27;
end;
end;
registration
cluster algebraic for Complex;
existence by GAUSSINT:14;
cluster algebraic for Element of F_Complex;
existence by Lm7;
end;
registration
cluster integer -> algebraic_integer for Complex;
coherence
proof
let c be Complex;
assume c is integer;
then reconsider c as Element of INT.Ring by INT_1:def 2;
take In(c,F_Complex);
thus thesis by Th4,Th27;
end;
end;
registration
cluster algebraic_integer for Complex;
existence by GAUSSINT:14;
cluster algebraic_integer for Element of F_Complex;
existence by Lm7;
end;
definition
let A,B be Ring;
let x be Element of B;
func Ann_Poly(x,A) -> non empty Subset of Polynom-Ring A equals
{p where p is Polynomial of A: Ext_eval(p,x) = 0.B};
coherence
proof
set M ={p where p is Polynomial of A:Ext_eval(p,x) = 0.B};
A1: now
let u be object;
assume u in M; then
ex p1 being Polynomial of A st u = p1 & Ext_eval(p1,x)=0.B;
hence u in the carrier of Polynom-Ring A by POLYNOM3:def 10;
end;
Ext_eval(0_.A,x) = 0.B by Th17; then
0_.A in M;
hence thesis by A1,TARSKI:def 3;
end;
end;
theorem Lm30:
for A,B be Ring, w be Element of B, 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
let A,B;
let w be Element of B;
let x,y be Element of Polynom-Ring A;
assume that
A0: A is Subring of B and
A1: x in Ann_Poly(w,A) and
A2: y in Ann_Poly(w,A);
reconsider x1=x, y1=y as Polynomial of A by POLYNOM3:def 10;
set M ={p where p is Polynomial of A:Ext_eval(p,w)=0.B};
consider x2 be Polynomial of A such that
A3: x2 = x1 and
A4: Ext_eval(x2,w)=0.B by A1;
consider y2 be Polynomial of A such that
A5: y2 = y1 and
A6: Ext_eval(y2,w)=0.B by A2;
A7: Ext_eval(x2 + y2,w) = Ext_eval(x1,w) + 0.B by A0,Th19,A6,A3
.= 0.B by A3,A4;
consider t be Polynomial of A such that
A8: t = x1+y1 and
A9: Ext_eval(t,w) = 0.B by A3,A5,A7;
x1+ y1 in M by A8,A9;
hence thesis by POLYNOM3:def 10;
end;
theorem Th31:
for B be comRing, z be Element of B, 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
let B be comRing;
let w be Element of B;
let p,x be Element of Polynom-Ring A;
assume that
A0: A is Subring of B and
A1: x in Ann_Poly(w,A);
set M ={p where p is Polynomial of A:Ext_eval(p,w)=0.B};
reconsider p1=p, x1=x as Polynomial of A by POLYNOM3:def 10;
consider x2 be Polynomial of A such that
A2: x2 = x1 and
A3: Ext_eval(x2,w)=0.B by A1;
Ext_eval(p1 *'x1,w) = Ext_eval(p1,w) * 0.B by A0,A2,A3,Th24.= 0.B;
then
consider t be Polynomial of A such that
A4: t = p1 *'x1 and
A5: Ext_eval(t,w) = 0.B;
p1 *'x1 in M by A4,A5;
hence thesis by POLYNOM3:def 10;
end;
theorem Lm32:
for B be comRing
for w be Element of B, 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
let B be comRing;
let w be Element of B;
let p,x be Element of Polynom-Ring A;
set M ={p where p is Polynomial of A:Ext_eval(p,w)=0.B};
reconsider p1=p, x1=x as Polynomial of A by POLYNOM3:def 10;
assume that
A0: A is Subring of B and
A1: x in Ann_Poly(w,A);
consider x2 be Polynomial of A such that
A2: x2 = x1 and
A3: Ext_eval(x2,w)=0.B by A1;
Ext_eval(x1*'p1,w) = Ext_eval(p1,w) * 0.B by A0,A2,A3,Th24
.= 0.B; then
consider t be Polynomial of A such that
A4: t = x1 *'p1 and
A5: Ext_eval(t,w) = 0.B;
x1 *'p1 in M by A4,A5;
hence thesis by POLYNOM3:def 10;
end;
theorem Th33:
for A be non degenerated Ring
for B be non degenerated comRing
for w be Element of B st A is Subring of B
holds Ann_Poly(w,A) is proper Ideal of Polynom-Ring A
proof
let A be non degenerated Ring;
let B be non degenerated comRing;
let w be Element of B;
assume
A0: A is Subring of B;
A1: Ann_Poly(w,A) is add-closed by A0,Lm30;
A2: Ann_Poly(w,A) is left-ideal by A0,Th31;
A3: Ann_Poly(w,A) is right-ideal by A0,Lm32;
Ann_Poly(w,A) is proper
proof
assume not Ann_Poly(w,A) is proper; then
A5: 1.Polynom-RingA in Ann_Poly(w,A);
A6: 1_.A in Ann_Poly(w,A) by A5,POLYNOM3:37;
A7: Ext_eval(1_.A,w)= 1.B by A0,Th18;
ex p be Polynomial of A st p = 1_.A & Ext_eval(p,w)= 0.B by A6;
hence contradiction by A7;
end;
hence thesis by A1,A2,A3;
end;
begin :: Properties of Polynomial Ring over PID.
reserve K, L for Field;
theorem Th34:
for K,L be Field, w be Element of L st K is Subring of L holds
ex g be Element of Polynom-Ring K st {g}-Ideal = Ann_Poly(w,K)
proof
let K,L;
let w be Element of L;
assume
A0: K is Subring of L;
A1: Polynom-Ring K is PID;
Ann_Poly(w,K) is Ideal of Polynom-Ring K by A0,Th33;
hence thesis by A1,IDEAL_1:def 27;
end;
theorem Th35:
for K,L be Field, z be Element of L st z is_integral_over K
holds Ann_Poly(z,K) <> {0.Polynom-Ring K}
proof
let K,L;
let z be Element of L;
assume
A1: z is_integral_over K;
set M = {p where p is Polynomial of K:Ext_eval(p,z)=0.L};
consider f be Polynomial of K such that
A2: LC f = 1.K and
A3: Ext_eval(f,z) = 0.L by A1;
not f in {0.Polynom-Ring K}
proof
assume
A5: f in {0.Polynom-Ring K};
reconsider f as Element of Polynom-Ring K by POLYNOM3:def 10;
f in {0.Polynom-Ring K}-Ideal by A5,IDEAL_1:47; then
f in the set of all 0.Polynom-Ring K*g
where g is Element of Polynom-Ring K by IDEAL_1:64; then
consider g1 being Element of Polynom-Ring K such that
A6: f = 0.Polynom-Ring K * g1;
reconsider g2 = g1 as Polynomial of K by POLYNOM3:def 10;
reconsider h2 = 0.Polynom-Ring K as Polynomial of K by POLYNOM3:def 10;
f = 0_.K by POLYNOM3:def 10,A6;
hence contradiction by FUNCOP_1:7,A2;
end;
hence thesis by A3;
end;
theorem Lm37:
for K be Field, p be Element of Polynom-Ring K st p <> 0_.K holds
p is non zero Element of the carrier of Polynom-Ring K
proof
let K;
let p be Element of Polynom-Ring K;
assume
A0: p <> 0_.K;
assume
A1: not(p is non zero Element of the carrier of Polynom-Ring K);
reconsider p as Element of the carrier of Polynom-Ring K;
p is zero by A1;
hence contradiction by A0;
end;
theorem Th38:
for K,L be Field, w be Element of L st K is Subring of L
holds Ann_Poly(w,K) is quasi-prime
proof
let K,L;
let w be Element of L;
assume
A0: K is Subring of L;
set M = {p where p is Polynomial of K:Ext_eval(p,w)=0.L};
for p, q being Element of Polynom-Ring K st p*q in Ann_Poly(w,K) holds
p in Ann_Poly(w,K) or q in Ann_Poly(w,K)
proof
let p, q be Element of Polynom-Ring K;
assume
A1: p*q in Ann_Poly(w,K);
reconsider p1=p, q1=q as Polynomial of K by POLYNOM3:def 10;
p1*'q1 in Ann_Poly(w,K) by A1,POLYNOM3:def 10; then
consider t be Polynomial of K such that
A5: t = p1*'q1 and
A6: Ext_eval(t,w)=0.L;
Ext_eval(p1,w) * Ext_eval(q1,w) = 0.L by A0,Th24,A6,A5;
then per cases by VECTSP_2:def 1;
suppose Ext_eval(p1,w)=0.L;
hence thesis;
end;
suppose Ext_eval(q1,w)=0.L;
hence thesis;
end;
end;
hence thesis by RING_1:def 1;
end;
theorem Th39:
for K,L be Field, w be Element of L st K is Subring of L &
w is_integral_over K holds Ann_Poly(w,K) is prime
proof
let K,L;
let w be Element of L;
assume K is Subring of L & w is_integral_over K;
then Ann_Poly(w,K) is proper quasi-prime by Th38,Th33;
hence thesis;
end;
theorem Th40:
for K,L be Field, z be Element of L st K is Subring of L &
z is_integral_over K
ex f be Element of Polynom-Ring K
st f <> 0_.K & {f}-Ideal = Ann_Poly(z,K) & f = NormPolynomial(f)
proof
let K,L be Field;
let z be Element of L;
assume that
A0: K is Subring of L and
A1: z is_integral_over K;
consider f be Element of Polynom-Ring K such that
A2: {f}-Ideal = Ann_Poly(z,K) by A0,Th34;
A3: f <> 0.Polynom-Ring K by A1,A2,Th35,IDEAL_1:47;
reconsider f as Element of Polynom-Ring K;
A4: f <> 0_.K by A3,POLYNOM3:def 10;
set g = NormPolynomial(f);
A7: {g}-Ideal = Ann_Poly(z,K) by A2,RING_4:27,RING_2:21;
g <> 0.Polynom-Ring K by A1,A7,Th35,IDEAL_1:47; then
A8: g <> 0_.K by POLYNOM3:def 10; then
A9: g is non zero Element of the carrier of Polynom-Ring K by Lm37;
A10:f is non zero Element of the carrier of Polynom-Ring K by A4,Lm37;
g = NormPolynomial(g) by A9,A10,RING_4:24;
hence thesis by A7,A8;
end;
theorem Th41:
for K,L be Field, z be Element of L,f,g be 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
let K,L be Field;
let z be Element of L;
let f,g be Element of Polynom-Ring K;
assume that
A1: z is_integral_over K and
A2: {f}-Ideal = Ann_Poly(z,K) and
A3: f = NormPolynomial(f) and
A4: {g}-Ideal = Ann_Poly(z,K) and
A5: g = NormPolynomial(g);
reconsider f as Element of the carrier of Polynom-Ring K;
NormPolynomial(f) <> 0.(Polynom-Ring K) by A3,A2,A1,Th35,IDEAL_1:47; then
f <> 0_.K by A3,POLYNOM3:def 10; then
A6: f is non zero Element of the carrier of Polynom-Ring K by Lm37;
reconsider g as Element of the carrier of Polynom-Ring K;
NormPolynomial(g) <> 0.(Polynom-Ring K) by A5,A4,A1,Th35,IDEAL_1:47; then
g <> 0_.K by A5,POLYNOM3:def 10; then
g is non zero Element of the carrier of Polynom-Ring K by Lm37;
hence thesis by A3,A6,A5,RING_2:21,RING_4:30,A4,A2;
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;
func minimal_polynom(z,K) -> Element of the carrier of Polynom-Ring K
means
:Def7:
it <> 0_.K & {it}-Ideal = Ann_Poly(z,K) & it = NormPolynomial(it);
existence by A1,A2,Th40;
uniqueness by Th41,A2;
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;
func deg_of_integral_element(z,K) -> Element of NAT equals
deg (minimal_polynom(z,K));
coherence
proof
set f = minimal_polynom(z,K);
A7: f is non zero by A1,A2,Def7;
reconsider f as Polynomial of K;
deg f <> -1 by A7; then
A8: len f <> 0;
len f + 1 > 0 + 1 by A8,XREAL_1:8; then
len f >= 1 by NAT_1:13;
hence thesis by INT_1:3;
end;
end;
definition
let A,B be Ring;
let x be Element of B;
func hom_Ext_eval(x,A) -> Function of Polynom-Ring A,B means :Def9:
for p be Polynomial of A holds it.p = Ext_eval(p,x);
existence
proof
defpred P[set,set] means ex p be Polynomial of A st p = $1 &
$2 = Ext_eval(p,x);
A1: for y be Element of the carrier of Polynom-Ring A
ex z be Element of B st P[y,z]
proof
let y be Element of the carrier of Polynom-Ring A;
reconsider p=y as Polynomial of A;
take Ext_eval(p,x);
take p;
thus thesis;
end;
consider f be Function of Polynom-Ring A, B such that
A2: for y be Element of Polynom-Ring A holds P[y,f.y]
from FUNCT_2:sch 3 (A1);
reconsider f as Function of Polynom-Ring A, B;
take f;
let p be Polynomial of A;
p in Polynom-Ring A by POLYNOM3:def 10; then
ex q be Polynomial of A st q = p & f.p = Ext_eval(q,x) by A2;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of Polynom-Ring A, B such that
A3: for p be Polynomial of A holds f1.p = Ext_eval(p,x) and
A4: for p be Polynomial of A holds f2.p = Ext_eval(p,x);
now
let y be Element of Polynom-Ring A;
reconsider p=y as Polynomial of A by POLYNOM3:def 10;
thus f1.y = Ext_eval(p,x) by A3 .= f2.y by A4;
end;
hence f1 = f2;
end;
end;
registration
let x be Element of F_Complex;
cluster hom_Ext_eval(x,F_Rat) -> unity-preserving additive multiplicative;
coherence
proof
thus (hom_Ext_eval(x,F_Rat)).(1_Polynom-Ring F_Rat)
= (hom_Ext_eval(x,F_Rat)).(1_.(F_Rat)) by POLYNOM3:37
.= Ext_eval(1_.(F_Rat),x) by Def9
.= 1_F_Complex by Th3,Th18;
hereby let a,b be Element of Polynom-Ring F_Rat;
reconsider p=a,q=b as Polynomial of F_Rat by POLYNOM3:def 10;
thus hom_Ext_eval(x,F_Rat).(a+b) = hom_Ext_eval(x,F_Rat).(p+q) by
POLYNOM3:def 10
.= Ext_eval(p+q,x) by Def9
.= Ext_eval(p,x) + Ext_eval(q,x) by Th3,Th19
.= hom_Ext_eval(x,F_Rat).a + Ext_eval(q,x) by Def9
.= hom_Ext_eval(x,F_Rat).a + hom_Ext_eval(x,F_Rat).b by Def9;
end;
hereby let a,b be Element of Polynom-Ring F_Rat;
reconsider p=a,q=b as Polynomial of F_Rat by POLYNOM3:def 10;
thus (hom_Ext_eval(x,F_Rat)).(a*b) = (hom_Ext_eval(x,F_Rat)).(p*'q)
by POLYNOM3:def 10
.= Ext_eval(p*'q,x) by Def9
.= Ext_eval(p,x)* Ext_eval(q,x) by Th3,Th24
.= (hom_Ext_eval(x,F_Rat)).a*Ext_eval(q,x) by Def9
.= (hom_Ext_eval(x,F_Rat)).a*(hom_Ext_eval(x,F_Rat)).b by Def9;
end;
end;
end;
theorem
for x be Element of F_Complex holds
F_Complex is (Polynom-Ring F_Rat)-homomorphic
proof
let x be Element of F_Complex;
hom_Ext_eval(x,F_Rat) is RingHomomorphism;
hence thesis;
end;
theorem Lm45:
for x be Element of B, z be object st z in rng hom_Ext_eval(x,A)
holds z in B;
definition
let x be Element of F_Complex;
func FQ(x) -> Subset of F_Complex equals
rng hom_Ext_eval(x,F_Rat);
coherence;
end;
registration
let x be Element of F_Complex;
cluster FQ(x) -> non empty;
coherence;
end;
theorem Lm46:
for x,z1,z2 be Element of F_Complex st
z1 in FQ(x) & z2 in FQ(x) holds z1 + z2 in FQ(x)
proof
let x,z1,z2 be Element of F_Complex;
assume that
A1: z1 in FQ(x) and
A2: z2 in FQ(x);
consider f1 be object such that
A3: f1 in dom hom_Ext_eval(x,F_Rat) and
A4: z1 = hom_Ext_eval(x,F_Rat).f1 by A1,FUNCT_1:def 3;
consider f2 be object such that
A5: f2 in dom hom_Ext_eval(x,F_Rat) and
A6: z2 = hom_Ext_eval(x,F_Rat).f2 by A2,FUNCT_1:def 3;
A7: dom hom_Ext_eval(x,F_Rat) =
the carrier of Polynom-Ring F_Rat by FUNCT_2:def 1;
reconsider g1 = f1, g2 = f2 as Polynomial of F_Rat
by A3,A5,POLYNOM3:def 10;
A8: z1 + z2 = Ext_eval(g1,x) + hom_Ext_eval(x,F_Rat).f2 by Def9,A6,A4
.= Ext_eval(g1,x) + Ext_eval(g2,x) by Def9
.= Ext_eval(g1+g2,x) by Th3,Th19
.= hom_Ext_eval(x,F_Rat).(g1+g2) by Def9;
set g = g1+g2;
g in dom hom_Ext_eval(x,F_Rat) by A7,POLYNOM3:def 10;
hence thesis by A8,FUNCT_1:def 3;
end;
theorem Lm47:
for x,z1,z2 be Element of F_Complex st
z1 in FQ(x) & z2 in FQ(x) holds z1 * z2 in FQ(x)
proof
let x,z1,z2 be Element of F_Complex;
assume that
A1: z1 in FQ(x) and
A2: z2 in FQ(x);
consider f1 be object such that
A3: f1 in dom hom_Ext_eval(x,F_Rat) and
A4: z1 = hom_Ext_eval(x,F_Rat).f1 by A1,FUNCT_1:def 3;
consider f2 be object such that
A5: f2 in dom hom_Ext_eval(x,F_Rat) and
A6: z2 = hom_Ext_eval(x,F_Rat).f2 by A2,FUNCT_1:def 3;
A7: dom hom_Ext_eval(x,F_Rat) =
the carrier of Polynom-Ring F_Rat by FUNCT_2:def 1;
reconsider g1 = f1, g2 = f2 as Polynomial of F_Rat by A3,A5,POLYNOM3:def 10;
A8: z1 * z2 = Ext_eval(g1,x) * hom_Ext_eval(x,F_Rat).f2 by Def9,A6,A4
.= Ext_eval(g1,x) * Ext_eval(g2,x) by Def9
.= Ext_eval(g1*'g2,x) by Th3,Th24
.= hom_Ext_eval(x,F_Rat).(g1*'g2) by Def9;
set g = g1*'g2;
g in dom hom_Ext_eval(x,F_Rat) by A7,POLYNOM3:def 10;
hence thesis by A8,FUNCT_1:def 3;
end;
theorem Lm48:
for x be Element of F_Complex, a be Element of F_Rat holds
a in FQ(x)
proof
let x be Element of F_Complex;
let a be Element of F_Rat;
reconsider f = <% a %> as Polynomial of F_Rat;
A2: dom hom_Ext_eval(x,F_Rat) =
the carrier of Polynom-Ring F_Rat by FUNCT_2:def 1;
A3: Ext_eval(f,x) = In(a,F_Complex) by Th3,Th25;
reconsider f as Element of Polynom-Ring F_Rat by POLYNOM3:def 10;
In(a,F_Complex) = hom_Ext_eval(x,F_Rat).f by A3,Def9;
hence thesis by A2,FUNCT_1:def 3;
end;
definition
let x be Element of F_Complex;
func FQ_add(x) -> BinOp of FQ(x) equals
addcomplex || FQ(x);
correctness
proof
set ad = addcomplex||FQ(x);
set theCFComplex = the carrier of F_Complex;
A0: [:FQ(x),FQ(x):] c= [:theCFComplex,theCFComplex:];
theCFComplex = COMPLEX by COMPLFLD:def 1; then
[:FQ(x),FQ(x):] c= dom (addcomplex) by A0,FUNCT_2:def 1; then
A1: dom ad = [:FQ(x),FQ(x):] by RELAT_1:62;
for z be object st z in [:FQ(x),FQ(x):] holds ad. z in FQ(x)
proof
let z be object such that
A2: z in [:FQ(x),FQ(x):];
consider a, b be object such that
A3: a in FQ(x) and
A4: b in FQ(x) and
A5: z = [a,b] by A2,ZFMISC_1:def 2;
reconsider x1 = a, y1 = b as Element of theCFComplex by A3,A4;
ad.z = addcomplex.(a,b) by A2,A5,FUNCT_1:49
.= x1+y1 by BINOP_2:def 3;
hence ad.z in FQ(x) by A3,A4,Lm46;
end;
hence thesis by A1,FUNCT_2:3;
end;
end;
definition
let x be Element of F_Complex;
func FQ_mult(x) -> BinOp of FQ(x) equals
multcomplex || FQ(x);
correctness
proof
set mult = multcomplex||FQ(x);
set theCFComplex = the carrier of F_Complex;
A0: theCFComplex = COMPLEX by COMPLFLD:def 1;
[:FQ(x),FQ(x):] c= [:COMPLEX,COMPLEX:] by A0; then
[:FQ(x),FQ(x):] c= dom(multcomplex) by FUNCT_2:def 1; then
A1: dom mult = [:FQ(x),FQ(x):] by RELAT_1:62;
for z be object st z in [:FQ(x),FQ(x):] holds mult.z in FQ(x)
proof
let z be object such that
A2: z in [:FQ(x),FQ(x):];
consider x1,y1 be object such that
A3: x1 in FQ(x) & y1 in FQ(x) & z = [x1,y1] by A2,ZFMISC_1:def 2;
reconsider x2 = x1, y2 = y1 as Element of theCFComplex by A3;
mult.z = multcomplex.(x2,y2) by A2,A3,FUNCT_1:49
.= x2*y2 by BINOP_2:def 5;
hence mult.z in FQ(x) by A3,Lm47;
end;
hence thesis by A1,FUNCT_2:3;
end;
end;
theorem Th49:
for x be Element of F_Complex, z, w be Element of FQ(x) holds
(FQ_add(x)).(z,w) = z+w
proof
let x be Element of F_Complex;
let z, w be Element of FQ(x);
thus (FQ_add(x)).(z,w) = addcomplex.(z,w) by FUNCT_1:49,ZFMISC_1:87
.= z+w by BINOP_2:def 3;
end;
theorem Th50:
for x be Element of F_Complex, z, w be Element of FQ(x) holds
(FQ_mult(x)).(z,w) = z*w
proof
let x be Element of F_Complex;
let z, w be Element of FQ(x);
thus (FQ_mult(x)).(z,w) = multcomplex.(z,w) by FUNCT_1:49,ZFMISC_1:87
.= z*w by BINOP_2:def 5;
end;
theorem Lm52: :::?????
for x be Element of F_Complex holds
In(1.F_Complex, FQ(x)) = 1.F_Complex
proof
let x be Element of F_Complex;
1.F_Complex = 1.F_Rat by C0SP1:def 3,Th3;
hence thesis by Lm48,SUBSET_1:def 8;
end;
theorem Lm53:
In(-1.F_Rat,F_Complex) = -1.F_Complex
proof
1.F_Complex + In(-1.F_Rat,F_Complex)
= In(1.F_Rat,F_Complex) + In(-1.F_Rat,F_Complex) by Lm5,Th3
.= In(0.F_Rat,F_Complex)
.= 0.F_Complex by Lm5,Th3;
hence thesis by RLVECT_1:def 10;
end;
definition
let x be Element of F_Complex;
func FQ_Ring(x) -> strict non empty doubleLoopStr equals
doubleLoopStr(# FQ(x), FQ_add(x), FQ_mult(x),In(1.F_Complex,FQ(x)),
In(0.F_Complex,FQ(x)) #);
coherence;
end;
theorem Th54:
for x be Element of F_Complex holds FQ_Ring(x) is Ring
proof
let x be Element of F_Complex;
reconsider ZS = doubleLoopStr(# FQ(x),FQ_add(x),FQ_mult(x),
In(1.F_Complex,FQ(x)),In(0.F_Complex,FQ(x)) #) as non empty doubleLoopStr;
A1:for v, w being Element of ZS holds v + w = w + v
proof
let v, w be Element of ZS;
v in F_Complex & w in F_Complex by Lm45; then
reconsider v1 = v, w1 = w as Element of F_Complex;
thus v + w = w1 + v1 by Th49
.= w + v by Th49;
end;
A2: for u, v, w being Element of ZS holds (u + v) + w = u + (v + w)
proof
let u, v, w be Element of ZS;
u in F_Complex & v in F_Complex & w in F_Complex by Lm45; then
reconsider u1 = u, v1 = v, w1 = w as Element of F_Complex;
A3: u + v = u1+v1 by Th49;
A4: v + w = v1+w1 by Th49;
thus (u + v) + w = u1+v1+w1 by Th49,A3
.= u1+(v1+w1)
.= u+(v+w) by Th49,A4;
end;
A5: for v being Element of ZS holds v + 0.ZS = v
proof
let v be Element of ZS;
A6: 0.ZS = 0.F_Complex by Lm48,Lm7,SUBSET_1:def 8;
0.ZS in F_Complex & v in F_Complex by Lm45; then
reconsider v1 = v as Element of F_Complex;
thus v + 0.ZS = v1 + 0.F_Complex by Th49,A6 .= v;
end;
A7: for v being Element of ZS holds v is right_complementable
proof
let v be Element of ZS;
v in F_Complex by Lm45; then
reconsider v1 = v as Element of F_Complex;
A8: (-1.F_Complex) * v1 = -(1.F_Complex * v1) by VECTSP_1:9
.= -v1;
reconsider w1 = -1.F_Complex as Element of ZS by Lm48,Lm53;
A10: w1 * v = (-1.F_Complex ) * v1 by Th50;
take w1*v;
thus v + (w1*v) = v1 + ((-1.F_Complex ) * v1) by A10,Th49
.= 0.F_Complex by RLVECT_1:5,A8 .= 0.ZS by Lm48,Lm7,SUBSET_1:def 8;
end;
A11: for a, b, v being Element of ZS holds (a + b) * v = a * v + b * v
proof
let a, b, v be Element of ZS;
a in F_Complex & b in F_Complex & v in F_Complex by Lm45; then
reconsider a1 = a, b1 = b, v1 = v as Element of F_Complex;
A12: a+b in FQ(x);
reconsider ab = a+b as Element of F_Complex by A12;
A13: a1*v1 = a*v & (b1*v1 = b*v) by Th50;
thus (a + b) * v = ab * v1 by Th50
.= (a1 + b1) * v1 by Th49
.= a1*v1 + b1*v1
.= a*v + b*v by A13,Th49;
end;
A14: for a, v, w being Element of ZS
holds a * (v + w) = a * v + a * w & (v + w)*a = v*a + w*a
proof
let a, v, w be Element of ZS;
a in F_Complex & v in F_Complex & w in F_Complex by Lm45; then
reconsider a1 = a, v1 = v, w1 = w as Element of F_Complex;
A15: v+w in FQ(x);
reconsider vw = (v+w) as Element of F_Complex by A15;
A16: (a1*v1 = a*v) & (a1*w1 = a*w) by Th50;
thus a * (v + w) = a1 * vw by Th50
.= a1 * (v1 + w1) by Th49
.= a1*v1 + a1*w1
.= a*v + a*w by A16,Th49;
thus (v + w) * a = v*a + w*a by A11;
end;
A17: for a, b, v being Element of ZS holds (a * b) * v = a * (b * v)
proof
let a, b, v be Element of ZS;
a in F_Complex & b in F_Complex & v in F_Complex by Lm45; then
reconsider a1 = a, b1 = b, v1 = v as Element of F_Complex;
A18: a*b in FQ(x) & b*v in FQ(x);
reconsider ab = (a*b), bv = (b*v) as Element of F_Complex by A18;
thus (a * b) * v = ab * v1 by Th50
.= (a1 * b1) * v1 by Th50
.= a1 * (b1 * v1)
.= a1 * bv by Th50
.= a * (b * v) by Th50;
end;
for v being Element of ZS holds v *1.ZS = v & 1.ZS * v = v
proof
let v be Element of ZS;
A19: 1.ZS = 1.F_Complex by Lm52;
v in F_Complex by Lm45; then
reconsider v1 = v as Element of F_Complex;
thus v * 1.ZS = v1 * 1.F_Complex by A19,Th50
.= v;
thus 1.ZS * v = 1.F_Complex * v1 by A19,Th50
.= v;
end;
hence thesis by A1,A2,A5,A7,A14,A17,VECTSP_1:def 6,def 7,
GROUP_1:def 3,RLVECT_1:def 2,def 3,def 4,ALGSTR_0:def 16;
end;
registration
let x be Element of F_Complex;
cluster FQ_Ring(x) -> Abelian add-associative right_zeroed
right_complementable associative well-unital distributive;
coherence by Th54;
end;
registration
let z be Element of F_Complex;
cluster FQ_Ring(z) -> domRing-like commutative non degenerated;
coherence
proof
set X = FQ_Ring(z);
thus X is domRing-like
proof
for x, y being Element of X holds
x*y = 0.X implies x = 0.X or y = 0.X
proof
let x, y be Element of X;
x in F_Complex & y in F_Complex by Lm45; then
reconsider x1 = x, y1 = y as Element of F_Complex;
assume
A1: x*y = 0.X;
A2: 0.X = 0.F_Complex by Lm48,Lm7,SUBSET_1:def 8; then
x1*y1 = 0.F_Complex by A1,Th50;
hence thesis by A2,VECTSP_1:12;
end;
hence thesis by VECTSP_2:def 1;
end;
A3: 0.FQ_Ring(z) = 0.F_Complex by Lm48,Lm7,SUBSET_1:def 8;
thus X is commutative
proof
let v, w be Element of FQ_Ring(z);
v in F_Complex & w in F_Complex by Lm45; then
reconsider v1=v, w1=w as Element of F_Complex;
thus v * w = v1 * w1 by Th50
.= w * v by Th50;
end;
thus thesis by Lm52,A3;
end;
end;
Lm55:
for x be Element of F_Complex holds
the carrier of F_Rat c= the carrier of FQ_Ring(x) by Lm48;
theorem Lm56:
for x be Element of F_Complex holds
[:RAT,RAT:] c= [:FQ(x),FQ(x):] & [:FQ(x),FQ(x):] c= [:COMPLEX,COMPLEX:]
proof
let x be Element of F_Complex;
A1: the carrier of F_Rat c= the carrier of FQ_Ring(x) by Lm48;
A2: FQ(x) c= the carrier of F_Complex;
FQ(x) c= COMPLEX by A2,COMPLFLD:def 1;
hence thesis by A1,ZFMISC_1:96;
end;
theorem Lm57:
for x be Element of F_Complex holds
the addF of F_Rat = (the addF of FQ_Ring(x))||RAT
proof
let x be Element of F_Complex;
thus the addF of F_Rat =
addcomplex|[:RAT,RAT:] by ZFMISC_1:96,RELAT_1:74,
VECTSP_1:def 5,RING_3:2,GAUSSINT:13
.= (the addF of FQ_Ring(x))||RAT by Lm56,RELAT_1:74;
end;
theorem Lm58:
for x be Element of F_Complex holds
the multF of F_Rat = (the multF of FQ_Ring(x))||RAT
proof
let x be Element of F_Complex;
thus the multF of F_Rat
= multcomplex|[:RAT,RAT:] by ZFMISC_1:96,RELAT_1:74,
VECTSP_1:def 5,RING_3:3,GAUSSINT:13
.= (the multF of FQ_Ring(x))||RAT by Lm56,RELAT_1:74;
end;
theorem
for x be Element of F_Complex holds F_Rat is Subring of FQ_Ring(x)
proof
let x be Element of F_Complex;
A1: the addF of F_Rat = (the addF of FQ_Ring(x))||the carrier of F_Rat
by Lm57;
A2: the multF of F_Rat = (the multF of FQ_Ring(x))||the carrier of F_Rat
by Lm58;
A3: 1.FQ_Ring(x) = 1.F_Complex by Lm52 .= 1.F_Rat by C0SP1:def 3,Th3;
0.FQ_Ring(x) = 0.F_Rat by Lm48,Lm7,SUBSET_1:def 8;
hence thesis by Lm55,A1,A2,A3,C0SP1:def 3;
end;
theorem Th80:
for f,g be 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
let f,g be Element of Polynom-Ring K;
assume that
A1: f <> 0.Polynom-Ring K and
A2: {f}-Ideal is prime and
A4: not g in {f}-Ideal;
assume
A5: {f,g}-Ideal <> the carrier of Polynom-Ring K;
Polynom-Ring K is PID; then
consider h be Element of Polynom-Ring K such that
A7: {f,g}-Ideal = {h}-Ideal by IDEAL_1:def 27;
A8: {f}-Ideal c= {h}-Ideal & {g}-Ideal c= {h}-Ideal by A7,IDEAL_1:69;
consider s be Element of Polynom-Ring K such that
A9: f = h*s by RING_2:19,A8,GCD_1:def 1;
consider t be Element of Polynom-Ring K such that
A11:g = h*t by RING_2:19,A8,GCD_1:def 1;
f is non zero Element of Polynom-Ring K by A1,STRUCT_0:def 12; then
A13:f is prime by A2,RING_2:24;
per cases by A9,A13;
suppose f divides s; then
consider u be Element of Polynom-Ring K such that
A16: s = f*u by GCD_1:def 1;
A17: f = f*(u*h) by GROUP_1:def 3,A9,A16;
reconsider v = u*h as Element of Polynom-Ring K;
f * 1.Polynom-Ring K - f*v = 0.Polynom-Ring K by RLVECT_1:5,A17;
then
f * (1.Polynom-Ring K -v) = 0.Polynom-Ring K by VECTSP_1:11; then
1.Polynom-Ring K + (-v)=0.Polynom-Ring K by A1,VECTSP_2:def 1; then
h divides 1.Polynom-Ring K by VECTSP_1:19,GCD_1:def 1; then
A27: h is Unit of Polynom-Ring K by GCD_1:def 20;
[#] Polynom-Ring K = the carrier of Polynom-Ring K;
hence contradiction by A5,A7,A27,RING_2:20;
end;
suppose f divides h; then
consider v be Element of Polynom-Ring K such that
A31: h = f*v by GCD_1:def 1;
g = f*(v*t) by A11,A31,GROUP_1:def 3;
hence contradiction by A4,GCD_1:def 1,RING_2:18;
end;
end;
theorem Th81:
for f,g be Element of Polynom-Ring K holds
f <> 0.Polynom-Ring K & {f}-Ideal is prime &
not g in {f}-Ideal implies {f}-Ideal,{g}-Ideal are_co-prime
proof
let f,g be Element of Polynom-Ring K;
{f,g}-Ideal = {f}-Ideal + {g}-Ideal by IDEAL_1:76;
hence thesis by Th80;
end;
theorem Lm62:
for x be Element of F_Complex,a be Element of FQ_Ring(x)
ex g be Element of Polynom-Ring F_Rat st a = hom_Ext_eval(x,F_Rat).g
proof
let x be Element of F_Complex;
let a be Element of FQ_Ring(x);
ex g1 be object st g1 in dom hom_Ext_eval(x,F_Rat) &
a = hom_Ext_eval(x,F_Rat).g1 by FUNCT_1:def 3;
hence thesis;
end;
theorem Th83:
for x,a be Element of F_Complex st a <> 0.F_Complex &
a in the carrier of FQ_Ring(x)
ex g be Element of Polynom-Ring F_Rat
st not g in Ann_Poly(x,F_Rat) & a = hom_Ext_eval(x,F_Rat).g
proof
let x,a be Element of F_Complex;
set M = {p where p is Polynomial of F_Rat:Ext_eval(p,x)=0.F_Complex};
assume that
A1: a <> 0.F_Complex and
A2: a in the carrier of FQ_Ring(x);
consider g be Element of Polynom-Ring F_Rat such that
A3: a = hom_Ext_eval(x,F_Rat).g by A2,Lm62;
take g;
thus not g in Ann_Poly(x,F_Rat)
proof
assume g in Ann_Poly(x,F_Rat);
then consider g1 be Polynomial of F_Rat such that
A5: g1 = g and
A6: Ext_eval(g1,x)=0.F_Complex;
thus contradiction by A1,A6,A3,A5,Def9;
end;
thus thesis by A3;
end;
theorem Th84:
for x,a be Element of F_Complex st x is algebraic & a <> 0.F_Complex &
a in the carrier of FQ_Ring(x)
ex f,g be 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
let x,a be Element of F_Complex;
assume that
A1: x is algebraic and
A2: a <> 0.F_Complex and
A3: a in the carrier of FQ_Ring(x);
consider f be Element of Polynom-Ring F_Rat such that
A4: {f}-Ideal = Ann_Poly(x,F_Rat) by Th34,Th3;
consider g be Element of Polynom-Ring F_Rat such that
A5: not(g in Ann_Poly(x,F_Rat)) and
A6: a = hom_Ext_eval(x,F_Rat).g by Th83,A2,A3;
A7: {f}-Ideal is prime by A4,A1,Th3,Th39;
A8: f <> 0.Polynom-Ring F_Rat by A1,A4,Th35,IDEAL_1:47;
{f}-Ideal,{g}-Ideal are_co-prime by A4,A5,A7,A8,Th81;
hence thesis by A4,A5,A6;
end;
theorem Th85:
for x,a be Element of F_Complex st x is algebraic & a <> 0.F_Complex &
a in the carrier of FQ_Ring(x) holds
ex b be Element of F_Complex st b in the carrier of FQ_Ring(x)
& a*b = 1.F_Complex
proof
let x,a be Element of F_Complex;
set COPolynomFRat = the carrier of Polynom-Ring F_Rat;
set M = {h where h is Polynomial of F_Rat:Ext_eval(h,x)=0.F_Complex};
assume that
A1: x is algebraic and
A2: a <> 0.F_Complex and
A3: a in the carrier of FQ_Ring(x);
consider f,g be Element of Polynom-Ring F_Rat such that
A4: {f}-Ideal = Ann_Poly(x,F_Rat) and
not(g in Ann_Poly(x,F_Rat)) and
A6: a = hom_Ext_eval(x,F_Rat).g and
A7: {f}-Ideal,{g}-Ideal are_co-prime by A1,A2,A3,Th84;
1.Polynom-Ring F_Rat in {f}-Ideal+{g}-Ideal by A7; then
1.Polynom-Ring F_Rat in {p+q where p,q is Element of Polynom-Ring F_Rat:
p in {f}-Ideal & q in {g}-Ideal} by IDEAL_1:def 19; then
consider p,q be Element of Polynom-Ring F_Rat such that
A10: 1.Polynom-Ring F_Rat = p+q and
A11: p in {f}-Ideal and
A12: q in {g}-Ideal;
A14: {g}-Ideal = the set of all g*s where s is Element of Polynom-Ring F_Rat
by IDEAL_1:64;
consider s be Element of Polynom-Ring F_Rat such that
A15: q = g * s by A12,A14;
reconsider p1=p,q1=q, g1=g,s1=s as Polynomial of F_Rat
by POLYNOM3:def 10;
A16: p+q = p1+q1 by POLYNOM3:def 10;
consider p2 be Polynomial of F_Rat such that
A17: p2 = p and
A18: Ext_eval(p2,x)=0.F_Complex by A4,A11;
set b = Ext_eval(s1,x);
A20: b = hom_Ext_eval(x,F_Rat).s1 by Def9;
A21: dom hom_Ext_eval(x,F_Rat) = the carrier of Polynom-Ring F_Rat
by FUNCT_2:def 1;
A22: b in the carrier of FQ_Ring(x) by A20,A21,FUNCT_1:def 3;
1.F_Complex = Ext_eval(1_.(F_Rat),x) by Th3,Th18
.= Ext_eval(p1+q1,x) by A10,POLYNOM3:def 10,A16
.= 0.F_Complex + Ext_eval(q1,x) by A17,A18,Th3,Th19
.= Ext_eval(g1 *'s1,x) by A15,POLYNOM3:def 10
.= Ext_eval(g1,x) * Ext_eval(s1,x) by Th3,Th24
.= a*b by A6,Def9;
hence thesis by A22;
end;
theorem
for x be Element of F_Complex st x is algebraic holds FQ_Ring(x) is Field
proof
let x be Element of F_Complex;
assume
A1: x is algebraic;
for a be Element of FQ_Ring(x) st a <> 0.FQ_Ring(x) holds
a is left_invertible
proof
let a be Element of FQ_Ring(x);
assume a <> 0.FQ_Ring(x); then
A4: a <> 0.F_Complex by SUBSET_1:def 8;
a in FQ(x); then
reconsider y = a as Element of F_Complex;
consider b be Element of F_Complex such that
A5: b in the carrier of FQ_Ring(x) and
A6: y*b = 1.F_Complex by A1,A4,Th85;
reconsider a1=y,b1 = b as Element of FQ_Ring(x) by A5;
b1*a1 = 1.F_Complex by A6,Th50
.= 1.FQ_Ring(x) by Lm52;
hence thesis;
end;
then FQ_Ring(x) is almost_left_invertible;
hence FQ_Ring(x) is Field;
end;