:: Splitting Fields for the Rational Polynomials X^2-2, X^2+X+1, X^3-1, and
:: X^3-2
:: by Christoph Schwarzweller and Sara Burgoa
::
:: Received April 30, 2022
:: Copyright (c) 2022-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 ARYTM_3, VECTSP_1, TARSKI, ABIAN, STRUCT_0, SUBSET_1, SUPINF_2,
NAT_1, MESFUNC1, C0SP1, FUNCT_4, CARD_3, POLYNOM1, POLYNOM2, POLYNOM3,
RLVECT_3, EC_PF_1, HURWITZ, FINSEQ_1, PREPOWER, FUNCT_1, RELAT_1, CARD_1,
SQUARE_1, XBOOLE_0, NUMBERS, POLYNOM5, GROUP_1, COMPTRIG, RAT_1,
AFINSQ_1, GLIB_000, FDIFF_1, CAT_1, YELLOW_8, RATFUNC1, RING_2, ALGNUM_1,
ARYTM_1, FOMODEL1, FINSET_1, NEWTON, XXREAL_0, GAUSSINT, COMPLFLD,
RING_3, RING_5, FIELD_6, XCMPLX_0, FIELD_8, REALALG2, INT_1, FIELD_4,
FUNCT_7, COMPLEX1, FIELD_7, ALGSEQ_1, FIELD_9, FIELD_10, RLVECT_2,
ZFMISC_1, ALGSTR_0, REALSET1, ORDINAL4;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELSET_1, REALSET1, ZFMISC_1,
FUNCT_1, ORDINAL1, FUNCT_2, STRUCT_0, NUMBERS, CARD_1, ENUMSET1, BINOP_1,
XCMPLX_0, XXREAL_0, NAT_1, NAT_D, SQUARE_1, COMPTRIG, INT_1, FUNCT_7,
FINSET_1, POLYNOM4, ALGSEQ_1, FINSEQ_1, FINSEQ_4, ABIAN, POLYNOM3, RAT_1,
POLYNOM5, NEWTON, PREPOWER, GROUP_1, BINOM, O_RING_1, COMPLEX1, ALGSTR_0,
RLVECT_1, HURWITZ, VECTSP_1, VECTSP_6, VECTSP_7, C0SP1, EC_PF_1,
RATFUNC1, GAUSSINT, COMPLFLD, RING_2, RING_3, RING_4, RING_5, ALGNUM_1,
FIELD_4, FIELD_5, FIELD_6, FIELD_7, FIELD_8, FIELD_9;
constructors BINOP_1, REAL_1, FINSOP_1, POLYNOM3, FUNCT_4, ORDINAL1, NAT_1,
ALGSTR_0, POLYNOM4, XBOOLE_0, RELSET_1, ARYTM_3, RLVECT_1, ABIAN,
FUNCT_7, FINSEQ_1, CARD_1, FINSET_1, GAUSSINT, RATFUNC1, O_RING_1, GCD_1,
GROUP_1, GROUP_4, BINOM, MEMBERED, RING_3, FINSEQ_4, PREPOWER, REALSET1,
EC_PF_1, ALGSEQ_1, RING_2, NEWTON, RING_4, FUNCOP_1, ALGNUM_1, SQUARE_1,
POLYNOM5, POLYNOM1, VECTSP_7, VECTSP_6, RING_5, COMPLFLD, COMPLEX1,
RAT_1, NAT_D, BINOP_2, INT_1, FIELD_4, FIELD_5, FIELD_6, FIELD_7,
FIELD_8, FIELD_9;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM4,
SQUARE_1, RAT_1, REALSET1, RLVECT_1, FUNCT_1, CARD_1, NEWTON, FINSET_1,
RATFUNC1, GAUSSINT, COMPLFLD, COMPLEX1, RING_4, RING_5, ABIAN, POLYNOM3,
POLYNOM5, ALGNUM_1, FIELD_4, FIELD_5, FIELD_6, FIELD_7, FIELD_9;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities REALSET1, XCMPLX_0, BINOP_1, STRUCT_0, ALGSTR_0, VECTSP_1, FIELD_6,
POLYNOM3;
expansions STRUCT_0, TARSKI, FUNCT_1, ALGSEQ_1;
theorems VECTSP_2, RLVECT_1, FUNCT_2, TARSKI, EC_PF_1, POLYNOM4, GAUSSINT,
RATFUNC1, POLYNOM5, RING_4, RING_5, HURWITZ, XREAL_1, INT_1, BINOM,
NAT_1, XBOOLE_0, FUNCT_7, FIELD_4, ALGSEQ_1, FUNCOP_1, POLYNOM3,
ALGNUM_1, RAT_1, XXREAL_0, XBOOLE_1, ORDINAL1, XREAL_0, FIELD_6, GROUP_1,
NUMBERS, COMPLFLD, COMPTRIG, XCMPLX_0, PREPOWER, SQUARE_1, NEWTON,
ENUMSET1, XCMPLX_1, ABIAN, FIELD_5, O_RING_1, FIELD_7, FIELD_8, FINSEQ_3,
FINSEQ_4, CARD_2, COMPLEX1, VECTSP_6, IRRAT_1, VECTSP_7, NAT_2, C0SP1,
VECTSP_1, FUNCT_1, FINSEQ_1, RING_3, INT_2, ZFMISC_1, FIELD_9;
begin :: Preliminaries
definition
let L be non empty doubleLoopStr;
let a,b,c be Element of L;
redefine func {a,b,c} -> Subset of L; :: redefines { (ENUMSET1, definition)
coherence
proof
now let o be object;
assume o in {a,b,c}; then
per cases by ENUMSET1:def 1;
suppose o = a;
hence o in the carrier of L;
end;
suppose o = b;
hence o in the carrier of L;
end;
suppose o = c;
hence o in the carrier of L;
end;
end;
then {a,b,c} c= the carrier of L;
hence thesis;
end;
end;
registration
let i be Integer;
cluster i|^3 -> integer;
coherence
proof
i|^(2+1) = i|^(1+1) * i by NEWTON:6 .= (i|^1 * i) * i by NEWTON:6;
hence thesis;
end;
end;
registration
let i be even Integer;
cluster i|^3 -> even;
coherence
proof
i|^(2+1) = i|^(1+1) * i by NEWTON:6 .= (i|^1 * i) * i by NEWTON:6;
hence thesis;
end;
end;
registration
let i be odd Integer;
cluster i|^3 -> odd;
coherence
proof
i|^(2+1) = i|^(1+1) * i by NEWTON:6 .= (i|^1 * i) * i by NEWTON:6;
hence thesis;
end;
end;
theorem lemcontr2:
for r,s being Complex holds (r * s) |^ 3 = (r |^ 3) * (s |^ 3)
proof
let r,s be Complex;
thus (r * s) |^ 3
= (r * s) |^ (2+1)
.= (r * s) |^ (1+1) * (r * s) by NEWTON:6
.= ((r * s)|^ 1 * (r * s)) * (r * s) by NEWTON:6
.= ((r|^1 * r) * r) * ((s * s) * s)
.= (r |^(1+1) * r) * ((s * s) * s) by NEWTON:6
.= r |^(2+1) * ((s|^1 * s) * s) by NEWTON:6
.= r |^(2+1) * (s|^(1+1) * s) by NEWTON:6
.= (r |^ 3) * (s |^ 3) by NEWTON:6;
end;
theorem lemcontr1:
for r being Rational holds r|^3 >= 0 iff r >= 0
proof
let r be Rational;
r|^3 = r|^(2 + 1)
.= r|^(1+1) * r by NEWTON:6
.= (r|^1 * r) * r by NEWTON:6
.= (r * r) * r;
hence thesis;
end;
theorem lemcontr:
not ex r being Rational st r|^3 = 2
proof
now assume ex r being Rational st r|^3 = 2; then
consider r being Rational such that A1: r|^3 = 2;
consider i being Integer, n being Nat such that
A3: n <> 0 and
A4: r = i / n and
A5: for i1 being Integer, n1 being Nat
st n1 <> 0 & r = i1 / n1 holds n <= n1 by RAT_1:9;
A6: i = r * n by A3,A4,XCMPLX_1:87;
r >= 0 by A1,lemcontr1;
then reconsider m = i as Element of NAT by A6,INT_1:3;
A7: m|^3 = 2 * n|^3 by A1,A6,lemcontr2;
then m is even;
then consider m1 being Nat such that
A8: m = 2 * m1 by ABIAN:def 2;
n|^3 = ((2 * m1)|^3) / 2 by A7,A8
.= ((2 |^ (2+1)) * (m1 |^ 3)) / 2 by lemcontr2
.= (((2|^2 * 2) * (m1 |^ 3))) / 2 by NEWTON:6
.= 2|^(1+1) * m1|^3
.= (2|^1 * 2) * m1|^3 by NEWTON:6
.= 2 * (2|^1 * m1|^3);
then n is even;
then consider n1 being Nat such that
A9: n = 2 * n1 by ABIAN:def 2;
reconsider n1 as Element of NAT by ORDINAL1:def 12;
A10: m1/n1 = r by A4,A8,A9,XCMPLX_1:91;
A11: n1 <> 0 by A3,A9;
then 2 * n1 > 1 * n1 by XREAL_1:98;
hence contradiction by A5,A9,A11,A10;
end;
hence thesis;
end;
registration
cluster 3-Root 2 -> non rational;
coherence
proof
(3-Root 2)|^3 = 2 by PREPOWER:def 2;
hence thesis by lemcontr;
end;
end;
theorem lemfinset:
for X1,X2 being finite set st X1 c= X2 & card X1 = card X2 holds X1 = X2
proof
let X1,X2 be finite set;
assume AS: X1 c= X2 & card X1 = card X2;
then card (X2 \ X1) = card X2 - card X1 by CARD_2:44 .= 0 by AS;
then X2 \ X1 = {};
then X2 c= X1 by XBOOLE_1:37;
hence thesis by AS,XBOOLE_0:def 10;
end;
registration
let F be Field;
cluster linear for Element of the carrier of Polynom-Ring F;
existence
proof
reconsider p = rpoly(1,0.F) as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
take p;
deg p = 1 by HURWITZ:27;
hence thesis by FIELD_5:def 1;
end;
cluster non linear non constant for Element of the carrier of Polynom-Ring F;
existence
proof
reconsider p = rpoly(2,0.F) as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
take p;
deg p = 2 by HURWITZ:27;
hence thesis by FIELD_5:def 1,RING_4:def 4;
end;
end;
theorem thirred2:
for F being Field
for p being Element of the carrier of Polynom-Ring F st deg p = 2
holds p is reducible iff p is with_roots
proof
let F be Field, p be Element of the carrier of Polynom-Ring F;
assume A: deg p = 2; then
reconsider p as
non linear non constant Element of the carrier of Polynom-Ring F
by FIELD_5:def 1,RING_4:def 4;
now assume B0: p is reducible;
p <> 0_.(F) & not p is Unit of Polynom-Ring F; then
consider q being Element of the carrier of Polynom-Ring F such that
B1: q divides p & 1 <= deg q & deg q < deg p by B0,RING_4:41;
consider r being Polynomial of F such that
B2: p = q *' r by B1,RING_4:1;
B3: deg q is Element of NAT by B1,INT_1:3;
1 <= deg q & deg q < 1 + 1 by B1,A; then
1 <= deg q & deg q <= 1 by B3,NAT_1:13; then
q is linear by XXREAL_0:1,FIELD_5:def 1;
hence p is with_roots by B2;
end;
hence thesis;
end;
theorem thirred:
for F being Field
for p being Element of the carrier of Polynom-Ring F st deg p = 3
holds p is reducible iff p is with_roots
proof
let F be Field, p be Element of the carrier of Polynom-Ring F;
assume A: deg p = 3; then
reconsider p as
non linear non constant Element of the carrier of Polynom-Ring F
by FIELD_5:def 1,RING_4:def 4;
now assume B0: p is reducible;
p <> 0_.(F) & not p is Unit of Polynom-Ring F; then
consider q being Element of the carrier of Polynom-Ring F such that
B1: q divides p & 1 <= deg q & deg q < deg p by B0,RING_4:41;
consider r being Polynomial of F such that
B2: p = q *' r by B1,RING_4:1;
B3: deg q is Element of NAT by B1,INT_1:3;
q <> 0_.(F) & r <> 0_.(F) by B2; then
B4: deg p = deg q + deg r by B2,HURWITZ:23;
B5: deg q < 2 + 1 by B1,A;
deg q <= 2 implies deg q = 0 or ... or deg q = 2 by B3; then
per cases by B5,B3,NAT_1:13;
suppose deg q = 0;
hence p is with_roots by B1;
end;
suppose deg q = 1; then
q is linear by FIELD_5:def 1;
hence p is with_roots by B2;
end;
suppose deg q = 2; then
r is linear by B4,A,FIELD_5:def 1;
hence p is with_roots by B2;
end;
end;
hence thesis;
end;
begin :: More on Field Extensions
registration
cluster F_Complex -> F_Rat-extending;
coherence;
end;
registration
cluster F_Rat-membered for Element of F_Real;
existence
proof
take 0.F_Real;
thus thesis;
end;
cluster non F_Rat-membered for Element of F_Real;
existence
proof
consider o being object such that
A: o in REAL & not o in RAT by NUMBERS:2,XBOOLE_0:6;
reconsider c = o as Element of F_Real by A;
thus thesis by A,FIELD_7:def 5,GAUSSINT:def 14;
end;
cluster F_Real-membered for Element of F_Complex;
existence
proof
take 0.F_Complex;
thus thesis;
end;
cluster non F_Real-membered for Element of F_Complex;
existence
proof
consider o being object such that
A: o in COMPLEX & not o in REAL by NUMBERS:1,XBOOLE_0:6;
reconsider c = o as Element of F_Complex by A,COMPLFLD:def 1;
c is non F_Real-membered by A,FIELD_7:def 5;
hence thesis;
end;
cluster F_Rat-membered for Element of F_Complex;
existence
proof
take 0.F_Complex;
thus thesis;
end;
cluster non F_Rat-membered for Element of F_Complex;
existence
proof
consider o being object such that
A: o in COMPLEX & not o in RAT by NUMBERS:3,XBOOLE_0:6;
reconsider c = o as Element of F_Complex by A,COMPLFLD:def 1;
c is non F_Rat-membered by A,FIELD_7:def 5,GAUSSINT:def 14;
hence thesis;
end;
end;
theorem mmo:
for F being Field,
E being FieldExtension of F,
K being E-extending FieldExtension of F
for p being Element of the carrier of Polynom-Ring F,
q being Element of the carrier of Polynom-Ring E
st p = q holds Roots(K,p) = Roots(K,q)
proof
let F be Field, E be FieldExtension of F,
K be E-extending FieldExtension of F;
let p be Element of the carrier of Polynom-Ring F,
q be Element of the carrier of Polynom-Ring E;
H: Roots(K,p) = {a where a is Element of K : a is_a_root_of p,K} &
Roots(K,q) = {a where a is Element of K : a is_a_root_of q,K}
by FIELD_4:def 4;
assume AS: p = q;
Z: now let o be object;
assume o in Roots(K,p); then
consider a being Element of K such that
A: o = a & a is_a_root_of p,K by H;
Ext_eval(q,a) = Ext_eval(p,a) by AS,FIELD_8:6 .= 0.K by A,FIELD_4:def 2;
then a is_a_root_of q,K by FIELD_4:def 2;
hence o in Roots(K,q) by A,H;
end;
now let o be object;
assume o in Roots(K,q); then
consider a being Element of K such that
B: o = a & a is_a_root_of q,K by H;
Ext_eval(p,a) = Ext_eval(q,a) by AS,FIELD_8:6 .= 0.K by B,FIELD_4:def 2;
then a is_a_root_of p,K by FIELD_4:def 2;
hence o in Roots(K,p) by B,H;
end;
hence thesis by Z,TARSKI:2;
end;
bb0:
for F being Field
for E being FieldExtension of F,
K being F-extending FieldExtension of E
for a being Element of E,
b being Element of K st b = a
holds the carrier of RAdj(F,{a}) = the carrier of RAdj(F,{b})
proof
let R be Field, S be FieldExtension of R, T be R-extending FieldExtension of S;
let a be Element of S, b be Element of T;
assume AS: b = a;
A: the carrier of RAdj(R,{a}) =
the set of all Ext_eval(p,a) where p is Polynomial of R by FIELD_6:45;
B: the carrier of RAdj(R,{b}) =
the set of all Ext_eval(p,b) where p is Polynomial of R by FIELD_6:45;
C: now let o be object;
assume o in the carrier of RAdj(R,{a}); then
consider p being Polynomial of R such that
D1: o = Ext_eval(p,a) by A;
p is Element of the carrier of Polynom-Ring R by POLYNOM3:def 10;
then o = Ext_eval(p,b) by D1,AS,FIELD_7:14;
hence o in the carrier of RAdj(R,{b}) by B;
end;
now let o be object;
assume o in the carrier of RAdj(R,{b}); then
consider p being Polynomial of R such that
D1: o = Ext_eval(p,b) by B;
p is Element of the carrier of Polynom-Ring R by POLYNOM3:def 10;
then o = Ext_eval(p,a) by D1,AS,FIELD_7:14;
hence o in the carrier of RAdj(R,{a}) by A;
end;
hence thesis by C,TARSKI:2;
end;
theorem bb1:
for F being Field
for E being FieldExtension of F,
K being F-extending FieldExtension of E
for a being Element of E,
b being Element of K st b = a holds RAdj(F,{a}) = RAdj(F,{b})
proof
let R be Field, S be FieldExtension of R, T be R-extending FieldExtension of S;
let a be Element of S, b be Element of T;
assume AS: b = a;
S is Subring of T by FIELD_4:def 1;
then RAdj(R,{a}) is Subring of T by ALGNUM_1:1;
hence thesis by AS,bb0,FIELD_6:14;
end;
bba:
for F being Field
for E being FieldExtension of F,
K being F-extending FieldExtension of E
for a being F-algebraic Element of E,
b being F-algebraic Element of K st b = a
holds the carrier of FAdj(F,{a}) = the carrier of FAdj(F,{b})
proof
let F be Field;
let E be FieldExtension of F, K be F-extending FieldExtension of E;
let a be F-algebraic Element of E, b be F-algebraic Element of K;
assume AS: b = a;
FAdj(F,{a}) = RAdj(F,{a}) by FIELD_6:56
.= RAdj(F,{b}) by AS,bb1 .= FAdj(F,{b}) by FIELD_6:56;
hence thesis;
end;
theorem mmk:
for F being Field
for E being FieldExtension of F,
K being F-extending FieldExtension of E
for a being F-algebraic Element of E,
b being F-algebraic Element of K st b = a holds FAdj(F,{a}) = FAdj(F,{b})
proof
let F be Field;
let E be FieldExtension of F, K be F-extending FieldExtension of E;
let a be F-algebraic Element of E, b be F-algebraic Element of K;
assume AS: b = a;
E is Subfield of K by FIELD_4:7;
then FAdj(F,{a}) is Subfield of K by EC_PF_1:5;
hence thesis by AS,bba,EC_PF_1:8;
end;
theorem mmv:
for F being Field,
E being FieldExtension of F,
K being E-extending FieldExtension of F
for a being F-algebraic Element of E,
b being F-algebraic Element of K st a = b holds MinPoly(a,F) = MinPoly(b,F)
proof
let F be Field, E be FieldExtension of F,
K be E-extending FieldExtension of F;
let a be F-algebraic Element of E, b be F-algebraic Element of K;
H: E is Subfield of K by FIELD_4:7;
assume a = b; then
Ext_eval(MinPoly(a,F),b) = Ext_eval(MinPoly(a,F),a) by FIELD_7:14
.= 0.E by FIELD_6:52
.= 0.K by H,EC_PF_1:def 1;
hence thesis by FIELD_6:52;
end;
theorem mmu:
for F being Field
for E being F-finite FieldExtension of F
for a being Element of E holds deg MinPoly(a,F) divides deg(E,F)
proof
let F be Field, E be F-finite FieldExtension of F, a be Element of E;
set K = FAdj(F,{a});
reconsider E1 = E as K-finite F-extending FieldExtension of K
by FIELD_4:7,FIELD_7:31;
deg(E1,F) = deg(E1,K) * deg(K,F) by FIELD_7:30
.= deg(E1,K) * deg MinPoly(a,F) by FIELD_6:67;
hence thesis by INT_1:def 3;
end;
registration
let F be Field,
E be FieldExtension of F;
let T1,T2 be Subset of E;
cluster FAdj(F,T1\/T2) -> FAdj(F,T1)-extending FAdj(F,T2)-extending;
coherence
proof
FAdj(F,T1) is Subfield of FAdj(F,T1\/T2) by XBOOLE_1:7,FIELD_7:10;
hence FAdj(F,T1\/T2) is FAdj(F,T1)-extending by FIELD_4:7;
FAdj(F,T2) is Subfield of FAdj(F,T1\/T2) by XBOOLE_1:7,FIELD_7:10;
hence FAdj(F,T1\/T2) is FAdj(F,T2)-extending by FIELD_4:7;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
let a,b be Element of E;
cluster FAdj(F,{a,b}) -> FAdj(F,{a})-extending FAdj(F,{b})-extending;
coherence
proof
{a} c= {a,b}
proof
now let o be object;
assume o in {a};
then o = a by TARSKI:def 1;
hence o in {a,b} by TARSKI:def 2;
end;
hence thesis;
end;
then FAdj(F,{a}) is Subfield of FAdj(F,{a,b}) by FIELD_7:10;
hence FAdj(F,{a,b}) is FAdj(F,{a})-extending by FIELD_4:7;
{b} c= {a,b}
proof
now let o be object;
assume o in {b};
then o = b by TARSKI:def 1;
hence o in {a,b} by TARSKI:def 2;
end;
hence thesis;
end;
then FAdj(F,{b}) is Subfield of FAdj(F,{a,b}) by FIELD_7:10;
hence FAdj(F,{a,b}) is FAdj(F,{b})-extending by FIELD_4:7;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
let a,b,c be Element of E;
cluster FAdj(F,{a,b,c}) -> FAdj(F,{a,b})-extending FAdj(F,{a,c})-extending
FAdj(F,{b,c})-extending;
coherence
proof
{a,b} c= {a,b,c}
proof
now let o be object;
assume o in {a,b}; then
per cases by TARSKI:def 2;
suppose o = a;
hence o in {a,b,c} by ENUMSET1:def 1;
end;
suppose o = b;
hence o in {a,b,c} by ENUMSET1:def 1;
end;
end;
hence thesis;
end;
then FAdj(F,{a,b}) is Subfield of FAdj(F,{a,b,c}) by FIELD_7:10;
hence FAdj(F,{a,b,c}) is FAdj(F,{a,b})-extending by FIELD_4:7;
{a,c} c= {a,b,c}
proof
now let o be object;
assume o in {a,c}; then
per cases by TARSKI:def 2;
suppose o = a;
hence o in {a,b,c} by ENUMSET1:def 1;
end;
suppose o = c;
hence o in {a,b,c} by ENUMSET1:def 1;
end;
end;
hence thesis;
end;
then FAdj(F,{a,c}) is Subfield of FAdj(F,{a,b,c}) by FIELD_7:10;
hence FAdj(F,{a,b,c}) is FAdj(F,{a,c})-extending by FIELD_4:7;
{b,c} c= {a,b,c}
proof
now let o be object;
assume o in {b,c}; then
per cases by TARSKI:def 2;
suppose o = b;
hence o in {a,b,c} by ENUMSET1:def 1;
end;
suppose o = c;
hence o in {a,b,c} by ENUMSET1:def 1;
end;
end;
hence thesis;
end;
then FAdj(F,{b,c}) is Subfield of FAdj(F,{a,b,c}) by FIELD_7:10;
hence FAdj(F,{a,b,c}) is FAdj(F,{b,c})-extending by FIELD_4:7;
end;
end;
LL0:
0_.(F_Rat)+*(0,-2)+*(3,1).0 = -2 &
0_.(F_Rat)+*(0,-2)+*(3,1).1 = 0 &
0_.(F_Rat)+*(0,-2)+*(3,1).2 = 0 &
0_.(F_Rat)+*(0,-2)+*(3,1).3 = 1 &
for n being Nat st n >= 4 holds 0_.(F_Rat)+*(0,-2)+*(3,1).n = 0
proof
set L = F_Rat, f = 0_.(F_Rat)+*(0,-2)+*(3,1);
A1: 0 in dom 0_.(L);
thus f.0 = (0_.(L)+*(0,-2)).0 by FUNCT_7:32
.= -2 by A1,FUNCT_7:31;
thus f.1 = (0_.(L)+*(0,-2)).1 by FUNCT_7:32
.= (0_.(L)).1 by FUNCT_7:32
.= 0 by GAUSSINT:def 14;
thus f.2 = (0_.(L)+*(0,-2)).2 by FUNCT_7:32
.= (0_.(L)).2 by FUNCT_7:32
.= 0 by GAUSSINT:def 14;
3 in NAT & dom(0_.(F_Rat)+*(0,-2)) = dom 0_.(F_Rat) by FUNCT_7:30;
hence f.3 = 1 by FUNCT_7:31;
let n be Nat;
assume
A4: n >= 4; then
n >= 1+1+1+1; then
n > 0+1+1+1 by NAT_1:13;
hence f.n = (0_.(L)+*(0,-2)).n by FUNCT_7:32
.= (0_.(L)).n by A4,FUNCT_7:32
.= 0 by ORDINAL1:def 12,FUNCOP_1:7,GAUSSINT:def 14;
end;
lemI: for z being Element of F_Complex
holds z|^3 = z * z^2 & z|^2 = z^2 & z|^2 = z * z
proof
let z be Element of F_Complex;
thus z * z^2
= z * (z * z) by O_RING_1:def 1
.= z * (z|^1 * z) by BINOM:8
.= z * (z|^1 * z|^1) by BINOM:8
.= z * z|^(1+1) by BINOM:10
.= z|^1 * z|^2 by BINOM:8
.= z|^(2+1) by BINOM:10
.= z|^3;
z * z = z|^1 * z by BINOM:8
.= z|^1 * z|^1 by BINOM:8
.= z|^(1+1) by BINOM:10;
hence thesis by O_RING_1:def 1;
end;
LL01:
0_.(F_Rat)+*(0,-1)+*(3,1).0 = -1 &
0_.(F_Rat)+*(0,-1)+*(3,1).1 = 0 &
0_.(F_Rat)+*(0,-1)+*(3,1).2 = 0 &
0_.(F_Rat)+*(0,-1)+*(3,1).3 = 1 &
for n being Nat st n >= 4 holds 0_.(F_Rat)+*(0,-1)+*(3,1).n = 0
proof
set L = F_Rat, f = 0_.(F_Rat)+*(0,-1)+*(3,1);
A1: 0 in dom 0_.(L);
thus f.0 = (0_.(L)+*(0,-1)).0 by FUNCT_7:32
.= -1 by A1,FUNCT_7:31;
thus f.1 = (0_.(L)+*(0,-1)).1 by FUNCT_7:32
.= (0_.(L)).1 by FUNCT_7:32
.= 0 by GAUSSINT:def 14;
thus f.2 = (0_.(L)+*(0,-1)).2 by FUNCT_7:32
.= (0_.(L)).2 by FUNCT_7:32
.= 0 by GAUSSINT:def 14;
3 in NAT & dom(0_.(F_Rat)+*(0,-1)) = dom 0_.(F_Rat) by FUNCT_7:30;
hence f.3 = 1 by FUNCT_7:31;
let n be Nat;
assume
A4: n >= 4; then
n >= 1+1+1+1; then
n > 0+1+1+1 by NAT_1:13;
hence f.n = (0_.(L)+*(0,-1)).n by FUNCT_7:32
.= (0_.(L)).n by A4,FUNCT_7:32
.= 0 by ORDINAL1:def 12,FUNCOP_1:7,GAUSSINT:def 14;
end;
begin :: The Rational Polynomials X^2-2, X^3-1, X^2+X+1 and X^3-2
definition
func X^2-2 -> Element of the carrier of Polynom-Ring F_Rat equals
<%-(1.F_Rat+1.F_Rat),0.F_Rat,1.F_Rat%>;
coherence by POLYNOM3:def 10;
func X^3-1 -> Element of the carrier of Polynom-Ring F_Rat equals
0_.(F_Rat)+*(0,-1)+*(3,1);
coherence
proof
set f = 0_.(F_Rat)+*(0,-1)+*(3,1);
H: dom f = dom(0_.(F_Rat)+*(0,-1)) by FUNCT_7:30
.= dom(0_.(F_Rat)) by FUNCT_7:30
.= NAT;
now let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
i <= 3 implies i = 0 or ... or i = 3; then
per cases;
suppose i = 0;
hence f.x in the carrier of F_Rat by LL01,RAT_1:def 2,GAUSSINT:def 14;
end;
suppose i = 1;
hence f.x in the carrier of F_Rat by LL01,GAUSSINT:def 14;
end;
suppose i = 2;
hence f.x in the carrier of F_Rat by LL01,GAUSSINT:def 14;
end;
suppose i = 3;
hence f.x in the carrier of F_Rat by LL01,GAUSSINT:def 14;
end;
suppose i > 3;
then i >= 3 + 1 by NAT_1:13;
then f.i = 0.F_Rat by LL01,GAUSSINT:def 14;
hence f.x in the carrier of F_Rat;
end;
end;
then reconsider f as sequence of the carrier of F_Rat by H,FUNCT_2:3;
f is finite-Support by LL01,GAUSSINT:def 14;
hence thesis by POLYNOM3:def 10;
end;
func X^3-2 -> Element of the carrier of Polynom-Ring F_Rat equals
0_.(F_Rat)+*(0,-2)+*(3,1);
coherence
proof
set f = 0_.(F_Rat)+*(0,-2)+*(3,1);
H: dom f = dom(0_.(F_Rat)+*(0,-2)) by FUNCT_7:30
.= dom(0_.(F_Rat)) by FUNCT_7:30
.= NAT;
now let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
i <= 3 implies i = 0 or ... or i = 3; then
per cases;
suppose i = 0;
hence f.x in the carrier of F_Rat by LL0,RAT_1:def 2,GAUSSINT:def 14;
end;
suppose i = 1;
hence f.x in the carrier of F_Rat by LL0,GAUSSINT:def 14;
end;
suppose i = 2;
hence f.x in the carrier of F_Rat by LL0,GAUSSINT:def 14;
end;
suppose i = 3;
hence f.x in the carrier of F_Rat by LL0,GAUSSINT:def 14;
end;
suppose i > 3;
then i >= 3 + 1 by NAT_1:13;
then f.i = 0.F_Rat by LL0,GAUSSINT:def 14;
hence f.x in the carrier of F_Rat;
end;
end;
then reconsider f as sequence of the carrier of F_Rat by H,FUNCT_2:3;
f is finite-Support by LL0,GAUSSINT:def 14;
hence thesis by POLYNOM3:def 10;
end;
func X^2+X+1 -> Element of the carrier of Polynom-Ring F_Rat equals
<%1.F_Rat,1.F_Rat,1.F_Rat%>;
coherence by POLYNOM3:def 10;
end;
definition
func 2-Root(2) -> non zero Element of F_Real equals
sqrt 2;
coherence
proof
reconsider t = sqrt 2 as Element of F_Real by XREAL_0:def 1;
t is non zero by SQUARE_1:24;
hence thesis;
end;
func 3-Root(2) -> non zero Element of F_Real equals
3-Root 2;
coherence
proof
reconsider t = 3-Root 2 as Element of F_Real by XREAL_0:def 1;
t is non zero;
hence thesis;
end;
func 2-CRoot(2) -> non zero Element of F_Complex equals
sqrt 2;
coherence
proof
reconsider t = sqrt 2 as Element of F_Real by XREAL_0:def 1;
B: F_Real is Subfield of F_Complex by FIELD_4:7; then
the carrier of F_Real c= the carrier of F_Complex by EC_PF_1:def 1; then
reconsider t as Element of F_Complex;
sqrt 2 <> 0.F_Real by SQUARE_1:24; then
t is non zero by B,EC_PF_1:def 1;
hence thesis;
end;
func 3-CRoot(2) -> non zero Element of F_Complex equals
3-Root 2;
coherence
proof
reconsider t = 3-Root 2 as Element of F_Real by XREAL_0:def 1;
B: F_Real is Subfield of F_Complex by FIELD_4:7; then
the carrier of F_Real c= the carrier of F_Complex by EC_PF_1:def 1; then
reconsider t as Element of F_Complex;
3-Root 2 <> 0.F_Real; then
t is non zero by B,EC_PF_1:def 1;
hence thesis;
end;
func sqrt(-3) -> non zero Element of F_Complex equals
<i> * (sqrt 3);
coherence
proof
<i> * (sqrt 3) in COMPLEX by XCMPLX_0:def 2; then
reconsider t = <i> * (sqrt 3) as Element of F_Complex by COMPLFLD:def 1;
<i> * (sqrt 3) <> 0 by SQUARE_1:25; then
t is non zero by COMPLFLD:def 1;
hence thesis;
end;
func zeta -> non zero Element of F_Complex equals
(-1 + <i> * (sqrt 3)) / 2;
coherence
proof
the carrier of F_Complex = COMPLEX by COMPLFLD:def 1; then
reconsider z = (-1+<i>*(sqrt 3))/2 as Element of F_Complex by XCMPLX_0:def 2;
H: (sqrt 3) / 2 <> 0 by SQUARE_1:24;
z = (-1/2) + <i> * ((sqrt 3) / 2); then
Im z = (sqrt 3) / 2 by COMPLEX1:12; then
z <> 0c by H; then
z is non zero by COMPLFLD:def 1;
hence thesis;
end;
end;
LL1: len X^3-2 = 4 & len X^3-1 = 4
proof
now let m be Nat;
assume B: m is_at_least_length_of X^3-2;
now assume m < 4; then
m < 3 + 1;
hence contradiction by B,LL0,GAUSSINT:def 14,NAT_1:13;
end;
hence 4 <= m;
end;
hence len X^3-2 = 4 by LL0,GAUSSINT:def 14,ALGSEQ_1:def 2,ALGSEQ_1:def 3;
now let m be Nat;
assume B: m is_at_least_length_of X^3-1;
now assume m < 4; then
m < 3 + 1;
hence contradiction by B,LL01,GAUSSINT:def 14,NAT_1:13;
end;
hence 4 <= m;
end;
hence thesis by LL01,GAUSSINT:def 14,ALGSEQ_1:def 2,ALGSEQ_1:def 3;
end;
LL:
deg X^3-2 = 3 & deg X^3-1 = 3 & deg X^2+X+1 = 2 & deg X^2-2 = 2
proof
thus 3 = (len X^3-2) - 1 by LL1 .= deg X^3-2 by HURWITZ:def 2;
thus 3 = (len X^3-1) - 1 by LL1 .= deg X^3-1 by HURWITZ:def 2;
1.F_Rat <> 0.F_Rat;
hence deg X^2+X+1 = 2 by FIELD_9:18;
thus deg X^2-2 = 2 by FIELD_9:18;
end;
LL3:
for x being Element of F_Rat holds eval(X^3-2,x) = x|^3 - 2
proof
let x be Element of F_Rat;
set p = X^3-2, R = F_Rat, t = -(1.R + 1.R);
consider F be FinSequence of the carrier of F_Rat such that
A1: eval(p,x) = Sum F and
A2: len F = len p and
A3: for n be Element of NAT st n in dom F
holds F.n = p.(n-'1) * (power R).(x,n-'1) by POLYNOM4:def 2;
A5: F.1 = p.(1-'1) * (power R).(x,1-'1) by A3,A2,LL1,FINSEQ_3:25
.= p.0 * (power R).(x,1-'1) by XREAL_1:232
.= p.0 * (power R).(x,0) by XREAL_1:232
.= t * 1_R by GROUP_1:def 7,LL0,GAUSSINT:def 14;
A6: 2-'1 = 2-1 by XREAL_0:def 2;
A7: F.2 = 0.R * (power R).(x,1)
by A6,LL0,A3,A2,LL1,FINSEQ_3:25,GAUSSINT:def 14;
A8: 3-'1 = 3-1 by XREAL_0:def 2;
A9: F.3 = 0.R * (power R).(x,2)
by A8,LL0,A3,A2,LL1,FINSEQ_3:25,GAUSSINT:def 14;
A10: 4-'1 = 4-1 by XREAL_0:def 2;
A11: F.4 = p.(4-'1) * (power R).(x,4-'1) by A3,A2,LL1,FINSEQ_3:25
.= x|^3 by A10,LL0,BINOM:def 2;
F = <*t,0.R,0.R,x|^3*> by A2,LL1,A5,A7,A9,A11,FINSEQ_4:76
.= <*t,0.R,0.R*> ^ <*x|^3*> by FINSEQ_4:74;
hence eval(p,x)
= Sum <*t,0.R,0.R*> + Sum <*x|^3*> by A1,RLVECT_1:41
.= Sum <*t,0.R,0.R*> + x|^3 by RLVECT_1:44
.= x|^3 - 2 by GAUSSINT:def 14,RLVECT_1:72;
end;
LL31:
for x being Element of F_Rat holds eval(X^3-1,x) = x|^3 - 1
proof
let x be Element of F_Rat;
set p = X^3-1, R = F_Rat, t = -1.R;
consider F be FinSequence of the carrier of F_Rat such that
A1: eval(p,x) = Sum F and
A2: len F = len p and
A3: for n be Element of NAT st n in dom F
holds F.n = p.(n-'1) * (power R).(x,n-'1) by POLYNOM4:def 2;
A5: F.1 = p.(1-'1) * (power R).(x,1-'1) by A3,A2,LL1,FINSEQ_3:25
.= p.0 * (power R).(x,1-'1) by XREAL_1:232
.= p.0 * (power R).(x,0) by XREAL_1:232
.= t * 1_R by GROUP_1:def 7,LL01,GAUSSINT:def 14;
A6: 2-'1 = 2-1 by XREAL_0:def 2;
A7: F.2 = 0.R * (power R).(x,1)
by A6,LL01,A3,A2,LL1,FINSEQ_3:25,GAUSSINT:def 14;
A8: 3-'1 = 3-1 by XREAL_0:def 2;
A9: F.3 = 0.R * (power R).(x,2)
by A8,LL01,A3,A2,LL1,FINSEQ_3:25,GAUSSINT:def 14;
A10: 4-'1 = 4-1 by XREAL_0:def 2;
A11: F.4 = p.(4-'1) * (power R).(x,4-'1) by A3,A2,LL1,FINSEQ_3:25
.= x|^3 by A10,LL01,BINOM:def 2;
F = <*t,0.R,0.R,x|^3*> by A2,LL1,A5,A7,A9,A11,FINSEQ_4:76
.= <*t,0.R,0.R*> ^ <*x|^3*> by FINSEQ_4:74;
hence eval(p,x)
= Sum <*t,0.R,0.R*> + Sum <*x|^3*> by A1,RLVECT_1:41
.= Sum <*t,0.R,0.R*> + x|^3 by RLVECT_1:44
.= x|^3 - 1 by GAUSSINT:def 14,RLVECT_1:72;
end;
LL32:
for x being Element of F_Rat holds eval(X^2+X+1,x) = x|^2 + x + 1
proof
let x be Element of F_Rat;
H: x^2 = x * x by O_RING_1:def 1
.= x|^1 * x by BINOM:8
.= x|^1 * x|^1 by BINOM:8
.= x|^(1+1) by BINOM:10;
eval(<%1.F_Rat,1.F_Rat,1.F_Rat%>,x)
= 1.F_Rat + (1.F_Rat) * x + (1.F_Rat) * x^2 by FIELD_9:20;
hence thesis by H,GAUSSINT:def 14;
end;
LKX2:
for x being Element of F_Rat holds eval(X^2-2,x) = x|^2 - 2
proof
set t = -(1.F_Rat+1.F_Rat);
let x be Element of F_Rat;
H: x^2 = x * x by O_RING_1:def 1
.= x|^1 * x by BINOM:8
.= x|^1 * x|^1 by BINOM:8
.= x|^(1+1) by BINOM:10;
eval(<%t,0.F_Rat,1.F_Rat%>,x)
= t + (0.F_Rat) * x + (1.F_Rat) * x^2 by FIELD_9:20;
hence thesis by H,GAUSSINT:def 14;
end;
LKX2ext:
for z being Element of F_Real holds Ext_eval(X^2-2,z) = z|^2 - 2
proof
let x be Element of F_Real;
set R = F_Real, p = X^2-2, t = -(1.R+1.R);
F_Rat is Subring of F_Real by FIELD_4:def 1; then
J: 1.F_Rat = 1.R by C0SP1:def 3;
consider F being FinSequence of the carrier of F_Real such that
A1: Ext_eval(X^2-2,x) = Sum F and
A2: len F = len p and
A3: for n be Element of NAT st n in dom F holds
F.n = In(p.(n-'1),R) * (power R).(x,n-'1) by ALGNUM_1:def 1;
B1: p.0 = t by J,FIELD_9:16;
B2: p.1 = 0.R by GAUSSINT:def 14,FIELD_9:16;
B3: p.2 = 1.R by GAUSSINT:def 14,FIELD_9:16;
BB: deg p = 2 by FIELD_9:18;
B0: deg p = len p - 1 by HURWITZ:def 2; then
B4: len F = 3 by A2,BB; then
A5: F.1 = In(p.(1-'1),R) * (power R).(x,1-'1) by A3,FINSEQ_3:25
.= In(p.0,R) * (power R).(x,1-'1) by XREAL_1:232
.= p.0 * (power R).(x,0) by XREAL_1:232
.= t * 1_R by B1,GROUP_1:def 7;
A6: 2-'1 = 2-1 by XREAL_0:def 2;
A7: F.2 = In(p.(2-'1),R) * (power R).(x,2-'1) by B4,A3,FINSEQ_3:25
.= 0.R * x|^1 by B2,A6;
A8: 3-'1 = 3-1 by XREAL_0:def 2;
A9: F.3 = In(p.(3-'1),R)*(power R).(x,3-'1) by B0,A3,A2,BB,FINSEQ_3:25
.= x|^2 by B3,A8,BINOM:def 2;
F = <*t,0.R,x|^2*> by B0,A2,BB,A5,A7,A9,FINSEQ_1:45;
hence Ext_eval(p,x)
= t + 0.R + x|^2 by A1,RLVECT_1:46
.= x |^ 2 - 2; :: by H,COMPLFLD:8,COMPLEX1:def 4;
end;
lem3:
for r being Rational, a being Element of F_Rat st a = r holds a|^3 = r|^3
proof
let r be Rational, a be Element of F_Rat;
assume A: a = r;
B: a|^3 = a|^(2+1)
.= a|^2 * a|^1 by BINOM:10
.= a|^(1+1) * a by BINOM:8
.= (a|^1 * a|^1) * a by BINOM:10
.= (a * a|^1) * a by BINOM:8
.= (a * a) * a by BINOM:8;
r|^3 = r|^(2+1)
.= r|^(1+1) * r by NEWTON:6
.= (r|^1 * r) * r by NEWTON:6
.= (r * r) * r;
hence thesis by A,B;
end;
R32: 3-Root(2) |^ 3 = 2
proof
A: (3-Root 2) |^ (1+1)
= ((3-Root 2) |^ 1) * (3-Root 2) by NEWTON:6
.= ((1_F_Real) * 3-Root(2)) * 3-Root(2)
.= (power(F_Real).(3-Root(2),0) * 3-Root(2)) * 3-Root(2)
by GROUP_1:def 7
.= power(F_Real).(3-Root(2),0+1) * 3-Root(2) by GROUP_1:def 7
.= power(F_Real).(3-Root(2),1+1) by GROUP_1:def 7;
(3-Root 2) |^ (2+1)
= power(F_Real).(3-Root(2),2) * (3-Root(2)) by A,NEWTON:6
.= power(F_Real).(3-Root(2),2+1) by GROUP_1:def 7
.= 3-Root(2) |^ 3 by BINOM:def 2;
hence thesis by PREPOWER:def 2;
end;
LL2:
Ext_eval(X^3-2,3-Root(2)) = 0.F_Real
proof
set R = F_Real, p = X^3-2, x = 3-Root(2), t = -(1.R + 1.R);
consider F being FinSequence of the carrier of F_Real such that
A1: Ext_eval(X^3-2,x) = Sum F and
A2: len F = len p and
A3: for n be Element of NAT st n in dom F holds
F.n = In(p.(n-'1),R) * (power R).(x,n-'1) by ALGNUM_1:def 1;
A5: F.1 = In(p.(1-'1),R) * (power R).(x,1-'1) by A3,A2,LL1,FINSEQ_3:25
.= In(p.0,R) * (power R).(x,1-'1) by XREAL_1:232
.= p.0 * (power R).(x,0) by XREAL_1:232
.= t * 1_R by GROUP_1:def 7,LL0;
A6: 2-'1 = 2-1 by XREAL_0:def 2;
A7: F.2 = In(p.(2-'1),R) * (power R).(x,2-'1) by A3,A2,LL1,FINSEQ_3:25
.= 0.R * (power R).(x,1) by A6,LL0;
A8: 3-'1 = 3-1 by XREAL_0:def 2;
A9: F.3 = In(p.(3-'1),R) * (power R).(x,3-'1) by A3,A2,LL1,FINSEQ_3:25
.= 0.R * (power R).(x,2) by A8,LL0;
A10: 4-'1 = 4-1 by XREAL_0:def 2;
A11: F.4 = In(p.(4-'1),R) * (power R).(x,4-'1) by A3,A2,LL1,FINSEQ_3:25
.= x|^3 by A10,LL0,BINOM:def 2;
F = <*t,0.R,0.R,x|^3*> by A2,LL1,A5,A7,A9,A11,FINSEQ_4:76
.= <*t,0.R,0.R*> ^ <*x|^3*> by FINSEQ_4:74;
hence Ext_eval(p,x)
= Sum <*t,0.R,0.R*> + Sum <*x|^3*> by A1,RLVECT_1:41
.= Sum <*t,0.R,0.R*> + x|^3 by RLVECT_1:44
.= x|^3 + t by RLVECT_1:72
.= 0.R by R32;
end;
LZ23: zeta|^2 <> 1 & zeta|^3 = 1 & zeta|^2 = -zeta - 1
proof
H: (sqrt 3) / 2 <> 0 by SQUARE_1:24;
I: zeta|^2 = zeta * zeta by lemI;
zeta = (-1/2) + <i> * ((sqrt 3) / 2); then
A: Re(zeta) = (-1/2) & Im(zeta) = (sqrt 3) / 2 by COMPLEX1:12; then
B: Re(zeta * zeta)
= (-1/2)^2 - ((sqrt 3) / 2)^2 by COMPLEX1:16
.= (-1/2)^2 - ((sqrt 3) / 2) * ((sqrt 3) / 2) by SQUARE_1:def 1
.= (-1/2)^2 - ((sqrt 3) * (sqrt 3)) / (2 * 2)
.= (-1/2)^2 - ((sqrt 3)^2) / (2 * 2) by SQUARE_1:def 1
.= (-1/2)^2 - (3 / (2*2)) by SQUARE_1:def 2
.= (-1/2) * (-1/2) - (3 / (2*2)) by SQUARE_1:def 1
.= -1/2;
C: Im(zeta * zeta) = 2 * ((-1/2) * ((sqrt 3) / 2)) by A,COMPLEX1:16
.= -(sqrt 3) / 2;
hence zeta|^2 <> 1 by I,H;
J: (sqrt 3)^2 = 3 by SQUARE_1:def 2;
D: zeta|^(2+1) = zeta|^2 * zeta|^1 by BINOM:10
.= (zeta * zeta) * zeta by I,BINOM:8; then
E: Re(zeta|^3)
= (-1/2) * (-1/2) - ((sqrt 3)/2) * (-(sqrt 3)/2) by C,B,A,COMPLEX1:9
.= (-1/2) * (-1/2) - (-((sqrt 3) * (sqrt 3))) / (2 * 2)
.= (-1/2) * (-1/2) - ((-((sqrt 3)^2)) / (2 * 2)) by SQUARE_1:def 1
.= 1 by J;
Im(zeta|^3)
= (-1/2) * ((sqrt 3)/2) + (-1/2) * (-(sqrt 3)/2) by D,C,B,A,COMPLEX1:9
.= 0;
hence zeta|^3 = 1 by E,COMPLEX1:6,COMPLEX1:3,COMPLEX1:def 4;
reconsider z = zeta as Complex;
Re(-z) = -(-1/2) & Im(-z) = -((sqrt 3) / 2) by A,COMPLEX1:17; then
H: Re(-z - 1r) = -(-1/2) - 1 by COMPLEX1:6,COMPLEX1:19 .= -(1/2);
Im(-z - 1r) = Im(-z) - 0 by COMPLEX1:6,COMPLEX1:19;
hence zeta|^2 = -zeta-1 by I,H,A,COMPLEX1:17,B,C,COMPLEX1:3,COMPLEX1:def 4;
end;
lem3c:
for r being Complex,
a being Element of F_Complex st a = r holds a|^3 = r|^3
proof
let r be Complex, a be Element of F_Complex;
assume A: a = r;
B: a|^3 = a|^(2+1)
.= a|^2 * a|^1 by BINOM:10
.= a|^(1+1) * a by BINOM:8
.= (a|^1 * a|^1) * a by BINOM:10
.= (a * a|^1) * a by BINOM:8
.= (a * a) * a by BINOM:8;
r|^3 = r|^(2+1)
.= r|^(1+1) * r by NEWTON:6
.= (r|^1 * r) * r by NEWTON:6
.= (r * r) * r;
hence thesis by A,B;
end;
LL33:
Ext_eval(X^3-1,zeta) = 0.F_Complex
proof
set R = F_Complex, p = X^3-1, x = zeta, t = - 1.R;
A0: t = -1 by COMPLFLD:8,COMPLEX1:def 4;
consider F being FinSequence of the carrier of F_Complex such that
A1: Ext_eval(X^3-1,x) = Sum F and
A2: len F = len p and
A3: for n be Element of NAT st n in dom F holds
F.n = In(p.(n-'1),R) * (power R).(x,n-'1) by ALGNUM_1:def 1;
A5: F.1 = In(p.(1-'1),R) * (power R).(x,1-'1) by A3,A2,LL1,FINSEQ_3:25
.= In(p.0,R) * (power R).(x,1-'1) by XREAL_1:232
.= p.0 * (power R).(x,0) by XREAL_1:232
.= t * 1_R by A0,GROUP_1:def 7,LL01;
A6: 2-'1 = 2-1 by XREAL_0:def 2;
A7: F.2 = In(p.(2-'1),R) * (power R).(x,2-'1) by A3,A2,LL1,FINSEQ_3:25
.= 0.R * (power R).(x,1) by A6,LL01,COMPLFLD:def 1;
A8: 3-'1 = 3-1 by XREAL_0:def 2;
A9: F.3 = In(p.(3-'1),R) * (power R).(x,3-'1) by A3,A2,LL1,FINSEQ_3:25
.= 0.R * (power R).(x,2) by A8,LL01,COMPLFLD:def 1;
A10: 4-'1 = 4-1 by XREAL_0:def 2;
A11: F.4 = In(p.(4-'1),R) * (power R).(x,4-'1) by A3,A2,LL1,FINSEQ_3:25
.= x|^3 by A10,LL01,BINOM:def 2;
F = <*t,0.R,0.R,x|^3*> by A2,LL1,A5,A7,A9,A11,FINSEQ_4:76
.= <*t,0.R,0.R*> ^ <*x|^3*> by FINSEQ_4:74;
hence Ext_eval(p,x)
= Sum <*t,0.R,0.R*> + Sum <*x|^3*> by A1,RLVECT_1:41
.= Sum <*t,0.R,0.R*> + x|^3 by RLVECT_1:44
.= zeta |^ 3 - 1 by A0,RLVECT_1:72
.= 0.R by LZ23,COMPLFLD:def 1;
end;
evalext11:
for z being Element of F_Complex holds Ext_eval(X^2+X+1,z) = z|^2 + z + 1
proof
let x be Element of F_Complex;
set R = F_Complex, p = X^2+X+1, t = 1.R;
consider F being FinSequence of the carrier of F_Complex such that
A1: Ext_eval(X^2+X+1,x) = Sum F and
A2: len F = len p and
A3: for n be Element of NAT st n in dom F holds
F.n = In(p.(n-'1),R) * (power R).(x,n-'1) by ALGNUM_1:def 1;
B1: p.0 = 1 by GAUSSINT:def 14,FIELD_9:16
.= 1.R by COMPLEX1:def 4,COMPLFLD:def 1;
B2: p.1 = 1 by GAUSSINT:def 14,FIELD_9:16
.= 1.R by COMPLEX1:def 4,COMPLFLD:def 1;
B3: p.2 = 1 by GAUSSINT:def 14,FIELD_9:16
.= 1.R by COMPLEX1:def 4,COMPLFLD:def 1;
1.F_Rat <> 0.F_Rat; then
BB: deg p = 2 by FIELD_9:18;
B0: deg p = len p - 1 by HURWITZ:def 2; then
B4: len F = 3 by A2,BB; then
A5: F.1 = In(p.(1-'1),R) * (power R).(x,1-'1) by A3,FINSEQ_3:25
.= In(p.0,R) * (power R).(x,1-'1) by XREAL_1:232
.= p.0 * (power R).(x,0) by XREAL_1:232
.= 1.R * 1_R by B1,GROUP_1:def 7;
A6: 2-'1 = 2-1 by XREAL_0:def 2;
A7: F.2 = In(p.(2-'1),R) * (power R).(x,2-'1) by B4,A3,FINSEQ_3:25
.= x|^1 by B2,A6,BINOM:def 2
.= x by BINOM:8;
A8: 3-'1 = 3-1 by XREAL_0:def 2;
A9: F.3 = In(p.(3-'1),R)*(power R).(x,3-'1) by B0,A3,A2,BB,FINSEQ_3:25
.= x|^2 by B3,A8,BINOM:def 2;
F = <*1.R,x,x|^2*> by B0,A2,BB,A5,A7,A9,FINSEQ_1:45;
hence Ext_eval(p,x)
= 1.R + x + x|^2 by A1,RLVECT_1:46
.= x |^ 2 + x + 1 by COMPLFLD:8,COMPLEX1:def 4;
end;
rootz:
Roots(F_Complex,X^2+X+1) = {zeta, zeta^2}
proof
set F = F_Complex, p = X^2+X+1;
set M = {zeta, zeta^2};
F_Real is Subfield of F by FIELD_4:7; then
the carrier of F_Real c= the carrier of F_Complex by EC_PF_1:def 1; then
reconsider r = 3-Root(2) as Element of F_Complex;
reconsider z = zeta as Complex;
H: Roots(F,p) = {a where a is Element of F : a is_a_root_of p,F}
by FIELD_4:def 4;
K: zeta|^2 = zeta * zeta by lemI;
K1: (zeta^2)|^2 = (zeta^2)|^(1+1)
.= ((zeta^2)|^1) * (zeta^2)|^1 by BINOM:10
.= (zeta^2)|^1 * (zeta^2) by BINOM:8
.= (zeta^2) * (zeta^2) by BINOM:8;
zeta = (-1/2) + <i> * ((sqrt 3) / 2); then
D1: Re(zeta) = (-1/2) & Im(zeta) = (sqrt 3) / 2 by COMPLEX1:12; then
D2: Re(zeta * zeta)
= (-1/2)^2 - ((sqrt 3) / 2)^2 by COMPLEX1:16
.= (-1/2)^2 - ((sqrt 3) / 2) * ((sqrt 3) / 2) by SQUARE_1:def 1
.= (-1/2)^2 - ((sqrt 3) * (sqrt 3)) / (2 * 2)
.= (-1/2)^2 - ((sqrt 3)^2) / (2 * 2) by SQUARE_1:def 1
.= (-1/2)^2 - (3 / (2*2)) by SQUARE_1:def 2
.= (-1/2) * (-1/2) - (3 / (2*2)) by SQUARE_1:def 1
.= -1/2;
D3: Im(zeta * zeta) = 2 * ((-1/2) * ((sqrt 3) / 2)) by D1,COMPLEX1:16
.= -(sqrt 3) / 2;
now let o be object;
assume B: o in {zeta, zeta^2}; then
reconsider c = o as Element of F_Complex;
per cases by B,TARSKI:def 2;
suppose E0: o = zeta;
E1: Re(zeta+1)
= (-1/2) + Re 1r by D1,COMPLEX1:8,COMPLEX1:def 4
.= 1/2 by COMPLEX1:6;
E2: Im(zeta+1)
= (sqrt 3) / 2 + Im 1r by D1,COMPLEX1:8,COMPLEX1:def 4
.= (sqrt 3) / 2 by COMPLEX1:6;
E3: Re(zeta|^2 + (zeta + 1))
= (-1/2) + 1/2 by K,D2,E1,COMPLEX1:8 .= 0;
E4: Im(zeta|^2 + (zeta + 1))
= -(sqrt 3) / 2 + (sqrt 3) / 2 by K,D3,E2,COMPLEX1:8 .= 0;
E5: zeta|^2 + zeta + 1 = 0c by E3,E4,COMPLEX1:4,COMPLEX1:3;
Ext_eval(p,c)
= zeta|^2 + zeta + 1 by E0,evalext11
.= 0.F by E5,COMPLFLD:def 1;
then c is_a_root_of p,F by FIELD_4:def 2;
hence o in Roots(F,p) by H;
end;
suppose E0: o = zeta^2;
F: (zeta^2)|^2
= (zeta^2) * (zeta * zeta) by K1,O_RING_1:def 1
.= (zeta * zeta) * (zeta * zeta) by O_RING_1:def 1;
E1: Re(zeta * zeta + 1)
= -1/2 + Re 1r by D2,COMPLEX1:8,COMPLEX1:def 4
.= 1/2 by COMPLEX1:6;
E2: Im(zeta * zeta + 1)
= -(sqrt 3) / 2 + Im 1r by D3,COMPLEX1:8,COMPLEX1:def 4
.= -(sqrt 3) / 2 by COMPLEX1:6;
E3: Re((zeta * zeta) * (zeta * zeta))
= (-1/2) * (-1/2) - (-(sqrt 3) / 2) * (-(sqrt 3) / 2)
by D2,D3,COMPLEX1:9
.= 1/4 - ((sqrt 3) * (sqrt 3)) / (2 * 2)
.= 1/4 - ((sqrt 3)^2) / (2 * 2) by SQUARE_1:def 1
.= 1/4 - 3/4 by SQUARE_1:def 2
.= -(1/2);
E4: Im((zeta * zeta) * (zeta * zeta))
= (-1/2) * (-(sqrt 3) / 2) + (-1/2) * (-(sqrt 3) / 2)
by D2,D3,COMPLEX1:9
.= (sqrt 3) / 2;
E5: Re((zeta * zeta) * (zeta * zeta) + (zeta * zeta + 1))
= 1/2 + -(1/2) by E1,E3,COMPLEX1:8 .= 0;
E6: Im((zeta * zeta) * (zeta * zeta) + (zeta * zeta + 1))
= (sqrt 3) / 2 + -(sqrt 3) / 2 by E2,E4,COMPLEX1:8 .= 0;
E7: (zeta * zeta) * (zeta * zeta) + zeta * zeta + 1 = 0c
by E5,E6,COMPLEX1:4,COMPLEX1:3;
Ext_eval(p,c)
= (zeta^2)|^2 + zeta^2 + 1 by E0,evalext11
.= (zeta^2)|^2 + zeta * zeta + 1 by O_RING_1:def 1
.= 0.F by F,E7,COMPLFLD:def 1;
then c is_a_root_of p,F by FIELD_4:def 2;
hence o in Roots(F,p) by H;
end;
end; then
B: M c= Roots(F_Complex,X^2+X+1);
the carrier of Polynom-Ring F_Rat c= the carrier of Polynom-Ring F
by FIELD_4:10; then
reconsider q = X^2+X+1 as Element of the carrier of Polynom-Ring F_Complex;
reconsider qq = q as non zero Element of the carrier of Polynom-Ring F_Rat;
1.F_Rat <> 0.F_Rat; then
H: 2= deg X^2+X+1 by FIELD_9:18 .= deg q by FIELD_4:20; then
reconsider q as non constant Element of the carrier of Polynom-Ring F_Complex
by RING_4:def 4;
C: card M = 2
proof
now assume D6: zeta = zeta^2;
zeta|^(2+1) = zeta|^2 * zeta|^1 by BINOM:10
.= zeta|^2 * zeta by BINOM:8
.= zeta|^2 by D6,K,O_RING_1:def 1;
hence contradiction by LZ23;
end;
hence thesis by CARD_2:57;
end;
D: card Roots(F_Complex,X^2+X+1) = 2
proof
F: card(Roots q) <= 2 by H,RING_5:22;
G: 2 <= card Roots(F_Complex,qq) by C,B,NAT_1:43;
Roots(F_Complex,X^2+X+1) = Roots q by FIELD_7:13;
hence thesis by F,G,XXREAL_0:1;
end;
thus thesis by B,C,D,lemfinset;
end;
leng:
for R being Field
for p,q being Polynomial of R holds len(p*'q) <= len p + len q -' 1
proof
let R be Field; let p,q be Polynomial of R;
len p + len q -' 1 is_at_least_length_of p*'q
proof
now let i be Nat;
i in NAT by ORDINAL1:def 12;
then consider r be FinSequence of the carrier of R such that
A2: len r = i+1 and
A3: (p*'q).i = Sum r and
A4: for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * q.(i
+1-'k) by POLYNOM3:def 9;
assume i >= len p + len q -' 1;
then i >= len p + len q - 1 by XREAL_0:def 2;
then i+1 >= len p + len q by XREAL_1:20;
then
A5: -len p >= -(i+1 - len q) by XREAL_1:24,XREAL_1:19;
now
let k be Element of NAT;
assume
A6: k in dom r;
then
A7: r.k = p.(k-'1) * q.(i+1-'k) by A4;
k in Seg len r by A6,FINSEQ_1:def 3;
then
A8: k <= i+1 by A2,FINSEQ_1:1;
per cases;
suppose
k-'1 < len p;
then k-1 < len p by XREAL_0:def 2;
then -(k-1) > -len p by XREAL_1:24;
then 1-k > len q - (i+1) by A5,XXREAL_0:2;
then i+1+(1-k) > len q by XREAL_1:19;
then i+1-k+1 > len q;
then i+1-'k+1 > len q by A8,XREAL_1:48,XREAL_0:def 2;
then q.(i+1-'k) = 0.R by NAT_1:13,ALGSEQ_1:8;
hence r.k = 0.R by A7;
end;
suppose
k-'1 >= len p;
then p.(k-'1) = 0.R by ALGSEQ_1:8;
hence r.k = 0.R by A7;
end;
end;
hence (p*'q).i = 0.R by A3,POLYNOM3:1;
end;
hence thesis;
end;
hence thesis by ALGSEQ_1:def 3;
end;
lemX3:
X^3-1 = X-(1.F_Rat) * X^2+X+1
proof
set F = F_Rat;
reconsider p1 = X-(1.F), p2 = X^2+X+1, q = X^3-1 as Polynomial of F;
J: 5 -' 1 = 5 - 1 by XREAL_0:def 2;
L: 4 -' 1 = 4 - 1 by XREAL_0:def 2; then
K: 2 -' 1 = 2 - 1 & 3 -' 1 = 3 - 1 & 3 -' 2 = 3 - 2 & 4 -' 1 = 3 &
4 -' 2 = 4 - 2 by XREAL_0:def 2;
A: dom(p1*'p2) = NAT by FUNCT_2:def 1 .= dom q by FUNCT_2:def 1;
now let o be object;
assume o in dom q;
then reconsider i = o as Element of NAT;
consider r being FinSequence of the carrier of F such that
B1: len r = i+1 & (p1*'p2).i = Sum r &
for k being Element of NAT st k in dom r
holds r.k = p1.(k-'1) * p2.(i+1-'k) by POLYNOM3:def 9;
i <= 3 implies i = 0 or ... or i = 3; then
per cases;
suppose C: i = 0;
then B2: r = <*r.1*> by B1,FINSEQ_1:40;
then dom r = {1} by FINSEQ_1:2,FINSEQ_1:38;
then 1 in dom r by TARSKI:def 1;
then r.1 = p1.(1-'1) * p2.(0+1-'1) by C,B1
.= p1.(1-'1) * p2.0 by NAT_2:8
.= p1.0 * p2.0 by NAT_2:8
.= rpoly(1,1.F).0 * p2.0 by FIELD_9:def 2
.= (-power(F).(1.F,1)) * p2.0 by HURWITZ:25
.= (-((1.F)|^1)) * p2.0 by BINOM:def 2
.= (-(1.F)) * p2.0 by BINOM:8
.= (-1.F) * 1.F by FIELD_9:16;
hence (p1*'p2).o = q.o by B1,C,LL01,GAUSSINT:13,B2,RLVECT_1:44;
end;
suppose C: i = 1;
then B3: r = <*r.1,r.2*> by B1,FINSEQ_1:44;
B4: dom r = {1,2} by B1,C,FINSEQ_1:def 3,FINSEQ_1:2;
then 1 in dom r by TARSKI:def 2;
then B5: r.1 = p1.(1-'1) * p2.(1+1-'1) by C,B1
.= p1.0 * p2.1 by K,NAT_2:8
.= rpoly(1,1.F).0 * p2.1 by FIELD_9:def 2
.= (-power(F).(1.F,1)) * p2.1 by HURWITZ:25
.= (-((1.F)|^1)) * p2.1 by BINOM:def 2
.= (-(1.F)) * p2.1 by BINOM:8
.= (-(1.F)) * 1.F by FIELD_9:16;
2 in dom r by B4,TARSKI:def 2;
then r.2 = p1.(2-'1) * p2.(1+1-'2) by C,B1
.= p1.1 * p2.0 by K,NAT_2:8
.= rpoly(1,1.F).1 * p2.0 by FIELD_9:def 2
.= 1_F_Rat * p2.0 by HURWITZ:25
.= 1.F_Rat by FIELD_9:16;
then Sum r = -(1.F) + 1.F by B3,B5,RLVECT_1:45 .= 0;
hence (p1*'p2).o = q.o by B1,C,LL01;
end;
suppose C: i = 2;
then B3: r = <*r.1,r.2,r.3*> by B1,FINSEQ_1:45;
B4: dom r = Seg 3 by B1,C,FINSEQ_1:def 3
.= Seg 2 \/ {2+1} by FINSEQ_1:9
.= {1,2,3} by FINSEQ_1:2,ENUMSET1:3;
then 1 in dom r by ENUMSET1:def 1;
then B5: r.1 = p1.(1-'1) * p2.(2+1-'1) by C,B1
.= p1.0 * p2.2 by K,NAT_2:8
.= p1.0 * 1.F by FIELD_9:16
.= rpoly(1,1.F).0 by FIELD_9:def 2
.= (-power(F).(1.F,1)) by HURWITZ:25
.= (-((1.F)|^1)) by BINOM:def 2
.= (-(1.F)) by BINOM:8;
2 in dom r by B4,ENUMSET1:def 1;
then B6: r.2 = p1.1 * p2.1 by K,C,B1
.= p1.1 * 1.F by FIELD_9:16
.= rpoly(1,1.F).1 by FIELD_9:def 2
.= 1_F_Rat by HURWITZ:25
.= 1.F_Rat;
3 in dom r by B4,ENUMSET1:def 1;
then r.3 = p1.2 * p2.(2+1-'3) by K,C,B1
.= rpoly(1,1.F).2 * p2.(2+1-'3) by FIELD_9:def 2
.= 0.F * p2.(2+1-'3) by HURWITZ:26;
then Sum r = (-(1.F)) + 1.F + 0.F by B3,B5,B6,RLVECT_1:46 .= 0;
hence (p1*'p2).o = q.o by B1,C,LL01;
end;
suppose C: i = 3;
then B3: r = <*r.1,r.2,r.3,r.4*> by B1,FINSEQ_4:76;
B4: dom r = Seg 4 by B1,C,FINSEQ_1:def 3
.= Seg 3 \/ {3+1} by FINSEQ_1:9
.= (Seg 2 \/ {2+1}) \/ {4} by FINSEQ_1:9
.= {1,2,3} \/ {4} by FINSEQ_1:2,ENUMSET1:3
.= {1,2,3,4} by ENUMSET1:6;
then 1 in dom r by ENUMSET1:def 2;
then B5: r.1 = p1.(1-'1) * p2.(3+1-'1) by C,B1
.= p1.0 * p2.3 by L,NAT_2:8
.= p1.0 * 0.F by FIELD_9:16;
2 in dom r by B4,ENUMSET1:def 2;
then B6: r.2 = p1.1 * p2.2 by K,C,B1
.= p1.1 * 1.F by FIELD_9:16
.= rpoly(1,1.F).1 by FIELD_9:def 2
.= 1_F_Rat by HURWITZ:25
.= 1.F_Rat;
3 in dom r by B4,ENUMSET1:def 2;
then B7: r.3 = p1.2 * p2.(3+1-'3) by K,C,B1
.= rpoly(1,1.F).2 * p2.(3+1-'3) by FIELD_9:def 2
.= 0.F * p2.(3+1-'3) by HURWITZ:26;
4 in dom r by B4,ENUMSET1:def 2;
then r.4 = p1.3 * p2.(3+1-'4) by L,C,B1
.= rpoly(1,1.F).3 * p2.(3+1-'4) by FIELD_9:def 2
.= 0.F * p2.(3+1-'4) by HURWITZ:26;
then r = <*(0.F),(1.F),(0.F)*> ^ <*(0.F)*> by B3,B5,B6,B7,FINSEQ_4:74;
then Sum r
= Sum <*(0.F),(1.F),(0.F)*> + Sum <*(0.F)*> by RLVECT_1:41
.= Sum <*(0.F),(1.F),(0.F)*> + 0.F by RLVECT_1:44
.= 1 by RLVECT_1:72,GAUSSINT:13;
hence (p1*'p2).o = q.o by B1,C,LL01;
end;
suppose C: i > 3;
C0: deg q = len q - 1 by HURWITZ:def 2;
C1: i >= 3 + 1 by C,NAT_1:13;
then E: q.i = 0.F by C0,LL,ALGSEQ_1:8;
p1 = rpoly(1,1.F) by FIELD_9:def 2; then
C2: deg p1 = 1 & deg p2 = 2 by LL,HURWITZ:27;
F: deg p1 = len p1 - 1 & deg p2 = len p2 - 1 by HURWITZ:def 2;
len(p1*'p2) <= len p1 + len p2 -' 1 by leng;
hence (p1*'p2).o = q.o by J,F,C2,C1,XXREAL_0:2,E,ALGSEQ_1:8;
end;
end;
then q = p1 *' p2 by A .= X-(1.F) * X^2+X+1 by POLYNOM3:def 10;
hence thesis;
end;
evalext1:
for z being Element of F_Complex holds Ext_eval(X^3-1,z) = z|^3 - 1
proof
let x be Element of F_Complex;
set R = F_Complex, p = X^3-1, t = - 1.R;
A0: t = -1 by COMPLFLD:8,COMPLEX1:def 4;
consider F being FinSequence of the carrier of F_Complex such that
A1: Ext_eval(X^3-1,x) = Sum F and
A2: len F = len p and
A3: for n be Element of NAT st n in dom F holds
F.n = In(p.(n-'1),R) * (power R).(x,n-'1) by ALGNUM_1:def 1;
A5: F.1 = In(p.(1-'1),R) * (power R).(x,1-'1) by A3,A2,LL1,FINSEQ_3:25
.= In(p.0,R) * (power R).(x,1-'1) by XREAL_1:232
.= p.0 * (power R).(x,0) by XREAL_1:232
.= t * 1_R by A0,GROUP_1:def 7,LL01;
A6: 2-'1 = 2-1 by XREAL_0:def 2;
A7: F.2 = In(p.(2-'1),R) * (power R).(x,2-'1) by A3,A2,LL1,FINSEQ_3:25
.= 0.R * (power R).(x,1) by A6,LL01,COMPLFLD:def 1;
A8: 3-'1 = 3-1 by XREAL_0:def 2;
A9: F.3 = In(p.(3-'1),R) * (power R).(x,3-'1) by A3,A2,LL1,FINSEQ_3:25
.= 0.R * (power R).(x,2) by A8,LL01,COMPLFLD:def 1;
A10: 4-'1 = 4-1 by XREAL_0:def 2;
A11: F.4 = In(p.(4-'1),R) * (power R).(x,4-'1) by A3,A2,LL1,FINSEQ_3:25
.= x|^3 by A10,LL01,BINOM:def 2;
F = <*t,0.R,0.R,x|^3*> by A2,LL1,A5,A7,A9,A11,FINSEQ_4:76
.= <*t,0.R,0.R*> ^ <*x|^3*> by FINSEQ_4:74;
hence Ext_eval(p,x)
= Sum <*t,0.R,0.R*> + Sum <*x|^3*> by A1,RLVECT_1:41
.= Sum <*t,0.R,0.R*> + x|^3 by RLVECT_1:44
.= x |^ 3 - 1 by A0,RLVECT_1:72;
end;
lemCRo:
for z being Element of the carrier of F_Complex holds
Ext_eval(X^3-1,z) = 0.F_Complex iff z is CRoot of 3,1
proof
let z be Element of the carrier of F_Complex;
reconsider z1 = z as Complex;
A: now assume Ext_eval(X^3-1,z) = 0.F_Complex; then
z|^3 - 1 = 0.F_Complex by evalext1 .= 0 by COMPLFLD:def 1; then
1 = z1|^3 by lem3c;
hence z is CRoot of 3,1 by COMPTRIG:def 2;
end;
now assume z is CRoot of 3,1; then
1 = z1|^3 by COMPTRIG:def 2 .= z|^3 by lem3c;
hence Ext_eval(X^3-1,z)
= 1 - 1 by evalext1 .= 0.F_Complex by COMPLFLD:def 1;
end;
hence thesis by A;
end;
lemCRo2:
zeta is CRoot of 3,1 & zeta^2 is CRoot of 3,1
proof
reconsider z = zeta as Complex;
zeta|^(1+1) = zeta * zeta by lemI; then
A: zeta|^2 = z^2 by SQUARE_1:def 1;
B: zeta|^2 = zeta^2 by lemI;
zeta|^3 = z|^3 by lem3c;
hence zeta is CRoot of 3,1 by LZ23,COMPTRIG:def 2;
(z^2)|^3 = (z * z)|^3 by SQUARE_1:def 1
.= (z|^3) * (z|^3) by NEWTON:7
.= (z|^3)^2 by SQUARE_1:def 1
.= 1^2 by LZ23,lem3c
.= 1 * 1 by SQUARE_1:def 1;
hence zeta^2 is CRoot of 3,1 by A,B,COMPTRIG:def 2;
end;
lemroots3:
Roots(F_Complex,X^3-1) = {1, zeta, zeta^2}
proof
set F = F_Complex, p = X^3-1;
set M = {1, zeta, zeta^2};
reconsider z = zeta as Complex;
H: Roots(F,p) = {a where a is Element of F : a is_a_root_of p,F}
by FIELD_4:def 4;
Z: 1 = 1.F by COMPLFLD:def 1,COMPLEX1:def 4;
now let o be object;
assume B: o in {1, zeta, zeta^2}; then
reconsider c = o as Element of F_Complex by Z,ENUMSET1:def 1;
per cases by B,ENUMSET1:def 1;
suppose E0: o = 1;
Ext_eval(X^3-1,1.F) = (1.F)|^3 - 1 by evalext1
.= (1.F)|^(2+1) - 1.F by Z
.= (1.F)|^2 * (1.F)|^1 - 1.F by BINOM:10
.= (1.F)|^(1+1) * (1.F) - 1.F by BINOM:8
.= (1.F)|^1 * (1.F)|^1 - 1.F by BINOM:10
.= (1.F)|^1 * (1.F) - 1.F by BINOM:8
.= 1.F - 1.F by BINOM:8
.= 0.F by RLVECT_1:5; then
1.F is_a_root_of p,F by FIELD_4:def 2;
hence o in Roots(F,p) by H,E0,Z;
end;
suppose E0: o = zeta;
Ext_eval(X^3-1,zeta) = 0.F by lemCRo,lemCRo2; then
zeta is_a_root_of p,F by FIELD_4:def 2;
hence o in Roots(F,p) by H,E0;
end;
suppose E0: o = zeta^2;
Ext_eval(X^3-1,zeta^2) = 0.F by lemCRo,lemCRo2; then
zeta^2 is_a_root_of p,F by FIELD_4:def 2;
hence o in Roots(F,p) by H,E0;
end;
end; then
B: M c= Roots(F_Complex,X^3-1);
the carrier of Polynom-Ring F_Rat c= the carrier of Polynom-Ring F
by FIELD_4:10; then
reconsider q = X^3-1 as Element of the carrier of Polynom-Ring F_Complex;
H: deg q = 3 by LL,FIELD_4:20; then
reconsider q as non constant Element of the carrier of Polynom-Ring F_Complex
by RING_4:def 4;
G: Roots(F_Complex,X^3-1) = Roots q by FIELD_7:13;
E1: zeta <> 0.F;
C: card M = 3
proof
D0: zeta = (-1/2) + <i> * ((sqrt 3) / 2); then
Re(zeta) = (-1/2) & Im(zeta) = (sqrt 3) / 2 by COMPLEX1:12; then
D2: Im(zeta * zeta) = 2 * ((-1/2) * ((sqrt 3) / 2)) by COMPLEX1:16
.= -(sqrt 3) / 2;
D3: (sqrt 3) / 2 <> 0 by SQUARE_1:24;
C1: zeta <> 1 by D0,COMPLEX1:12,COMPLEX1:6,COMPLEX1:def 4;
C2: now assume 1 = zeta^2;
then zeta * zeta = 1.F by Z,O_RING_1:def 1 .= 1r by COMPLFLD:def 1;
hence contradiction by D2,D3,COMPLEX1:6;
end;
C3: now assume zeta = zeta^2;
then zeta * 1.F = zeta * zeta by O_RING_1:def 1;
then zeta = 1.F by E1,VECTSP_2:8 .= 1r by COMPLFLD:def 1;
hence contradiction by D0,COMPLEX1:12,COMPLEX1:6;
end;
thus thesis by C1,C2,C3,CARD_2:58;
end;
D: card Roots(F_Complex,X^3-1) = 3
proof
F: card(Roots q) <= 3 by H,RING_5:22;
G1: 3 <= card(Roots q) by C,G,B,NAT_1:43;
Roots(F_Complex,X^3-1) = Roots q by FIELD_7:13;
hence thesis by F,G1,XXREAL_0:1;
end;
thus thesis by G,B,C,D,lemfinset;
end;
lemlem:
not zeta in REAL & not zeta^2 in REAL
proof
H: zeta * zeta = zeta^2 by O_RING_1:def 1;
D0: (sqrt 3) / 2 <> 0 by SQUARE_1:24;
zeta = (-1/2) + <i> * ((sqrt 3) / 2); then
Re(zeta) = (-1/2) & Im(zeta) = (sqrt 3) / 2 by COMPLEX1:12; then
Im(zeta * zeta) = 2 * ((-1/2) * ((sqrt 3) / 2)) by COMPLEX1:16
.= -(sqrt 3) / 2;
hence thesis by H,D0;
end;
registration
cluster X^2-2 -> monic purely_quadratic irreducible;
coherence
proof
set p = X^2-2, F = F_Rat;
thus X^2-2 is monic;
thus X^2-2 is purely_quadratic;
now assume X^2-2 is with_roots; then
consider a being Element of F_Rat such that
A: a is_a_root_of X^2-2 by POLYNOM5:def 8;
reconsider r = a as Rational;
0.F_Rat = eval(X^2-2,a) by A,POLYNOM5:def 7
.= a|^2 - 2 by LKX2; then
B: 2 = a|^(1+1) by GAUSSINT:def 14
.= a|^1 * a|^1 by BINOM:10
.= a * a|^1 by BINOM:8
.= r * r by BINOM:8
.= r^2 by SQUARE_1:def 1;
per cases;
suppose r >= 0; then
r = sqrt 2 by B,SQUARE_1:def 2;
hence contradiction by INT_2:28,IRRAT_1:1;
end;
suppose L: r <= 0;
(-r)^2 = r^2 by SQUARE_1:3; then
(-r) = sqrt 2 by L,B,SQUARE_1:def 2;
hence contradiction by INT_2:28,IRRAT_1:1;
end;
end;
hence X^2-2 is irreducible by LL,thirred2;
end;
cluster X^3-2 -> monic non constant irreducible;
coherence
proof
set p = X^3-2, F = F_Rat;
LC p = p.(4-'1) by LL1,RATFUNC1:def 6
.= p.(4-1) by XREAL_0:def 2
.= 1.F by LL0,GAUSSINT:def 14;
hence X^3-2 is monic by RATFUNC1:def 7;
thus X^3-2 is non constant by LL,RING_4:def 4;
now assume X^3-2 is with_roots; then
consider a being Element of F_Rat such that
A: a is_a_root_of X^3-2 by POLYNOM5:def 8;
reconsider r = a as Rational;
0.F_Rat = eval(X^3-2,a) by A,POLYNOM5:def 7
.= a|^3 - 2 by LL3; then
2 = r|^3 by lem3,GAUSSINT:def 14;
hence contradiction by lemcontr;
end;
hence X^3-2 is irreducible by LL,thirred;
end;
cluster X^3-1 -> monic non constant reducible;
coherence
proof
set p = X^3-1, F = F_Rat;
LC p = p.(4-'1) by LL1,RATFUNC1:def 6
.= p.(4-1) by XREAL_0:def 2
.= 1.F by LL01,GAUSSINT:def 14;
hence X^3-1 is monic by RATFUNC1:def 7;
thus X^3-1 is non constant by LL,RING_4:def 4;
eval(X^3-1,1.F) = (1.F)|^3 - 1 by LL31
.= (1|^3) - 1 by lem3,GAUSSINT:def 14
.= 0.F by GAUSSINT:def 14;
then X^3-1 is with_roots by POLYNOM5:def 7,POLYNOM5:def 8;
hence X^3-1 is reducible by LL,thirred;
end;
cluster X^2+X+1 -> monic quadratic irreducible;
coherence
proof
set p = X^2+X+1, F = F_Rat;
1.F_Rat <> 0.F_Rat; then
H: deg p = 2 by FIELD_9:18;
thus X^2+X+1 is monic;
thus X^2+X+1 is quadratic;
I: Roots X^2+X+1 c= Roots(F_Complex,X^2+X+1) by FIELD_4:28;
F_Rat is Subfield of F_Real by FIELD_4:7; then
K: the carrier of F_Rat c= the carrier of F_Real by EC_PF_1:def 1;
now assume X^2+X+1 is with_roots; then
consider a being Element of F_Rat such that
A: a is_a_root_of X^2+X+1 by POLYNOM5:def 8;
a in Roots X^2+X+1 by A,POLYNOM5:def 10; then
per cases by I,rootz,TARSKI:def 2;
suppose a = zeta;
hence contradiction by lemlem,K;
end;
suppose a = zeta^2;
hence contradiction by lemlem,K;
end;
end;
hence X^2+X+1 is irreducible by H,thirred2;
end;
end;
registration
cluster 2-Root(2) -> non (F_Rat)-membered F_Rat-algebraic;
coherence
proof
not sqrt 2 in RAT by INT_2:28,IRRAT_1:1;
hence 2-Root(2) is non (F_Rat)-membered by GAUSSINT:def 14,FIELD_7:def 5;
Ext_eval(X^2-2,2-Root(2))
= (2-Root(2))|^(1+1) - 2 by LKX2ext
.= (2-Root(2))|^1 * (2-Root(2))|^1 - 2 by BINOM:10
.= (2-Root(2)) * (2-Root(2))|^1 - 2 by BINOM:8
.= (2-Root(2)) * (2-Root(2)) - 2 by BINOM:8
.= (sqrt 2)^2 - 2 by SQUARE_1:def 1
.= 2 - 2 by SQUARE_1:def 2
.= 0.F_Real;
hence thesis by FIELD_6:43;
end;
cluster 2-CRoot(2) -> non (F_Rat)-membered F_Rat-algebraic;
coherence
proof
not sqrt 2 in RAT by INT_2:28,IRRAT_1:1;
hence 2-CRoot(2) is non (F_Rat)-membered by FIELD_7:def 5,GAUSSINT:def 14;
Ext_eval(X^2-2,2-CRoot(2))
= Ext_eval(X^2-2,2-Root(2)) by FIELD_7:14
.= (2-Root(2))|^(1+1) - 2 by LKX2ext
.= (2-Root(2))|^1 * (2-Root(2))|^1 - 2 by BINOM:10
.= (2-Root(2)) * (2-Root(2))|^1 - 2 by BINOM:8
.= (2-Root(2)) * (2-Root(2)) - 2 by BINOM:8
.= (sqrt 2)^2 - 2 by SQUARE_1:def 1
.= 2 - 2 by SQUARE_1:def 2
.= 0.F_Complex by COMPLFLD:def 1;
hence thesis by FIELD_6:43;
end;
cluster 3-Root(2) -> non (F_Rat)-membered F_Rat-algebraic;
coherence
proof
not 3-Root(2) in the carrier of F_Rat;
hence 3-Root(2) is non (F_Rat)-membered by FIELD_7:def 5;
thus thesis by LL2,FIELD_6:43;
end;
cluster 3-CRoot(2) -> non (F_Rat)-membered F_Rat-algebraic;
coherence
proof
not 3-Root(2) in the carrier of F_Rat;
hence 3-CRoot(2) is non (F_Rat)-membered by FIELD_7:def 5;
Ext_eval(X^3-2,3-CRoot(2))
= Ext_eval(X^3-2,3-Root(2)) by FIELD_7:14
.= 0.F_Complex by LL2,COMPLFLD:def 1;
hence thesis by FIELD_6:43;
end;
cluster zeta -> non (F_Real)-membered F_Rat-algebraic;
coherence
proof
B: (sqrt 3) / 2 <> 0 by SQUARE_1:24;
(-1 + <i> * (sqrt 3)) / 2 = (-1)/2 + <i> * ((sqrt 3) / 2);
then Im zeta <> 0 by B,COMPLEX1:12;
then not zeta in the carrier of F_Real;
hence zeta is non (F_Real)-membered by FIELD_7:def 5;
thus thesis by LL33,FIELD_6:43;
end;
cluster zeta^2 -> non (F_Real)-membered F_Rat-algebraic;
coherence
proof
H: (sqrt 3) / 2 <> 0 by SQUARE_1:24;
I: zeta * zeta = zeta^2 by O_RING_1:def 1;
zeta = (-1/2) + <i> * ((sqrt 3) / 2); then
Re(zeta) = (-1/2) & Im(zeta) = (sqrt 3) / 2 by COMPLEX1:12; then
Im(zeta * zeta) = 2 * ((-1/2) * ((sqrt 3) / 2)) by COMPLEX1:16
.= -(sqrt 3) / 2; then
not zeta * zeta in the carrier of F_Real by H;
hence thesis by I,FIELD_7:def 5;
end;
end;
registration
cluster FAdj(F_Rat,{3-Root(2)}) -> (F_Rat)-finite;
coherence;
cluster FAdj(F_Rat,{3-CRoot(2),zeta}) -> (F_Rat)-finite;
coherence;
end;
llsplit1:
for F being Field holds F is algebraic-closed implies
for p being non constant Polynomial of F holds p splits_in F
proof
let F be Field;
assume B: F is algebraic-closed;
now let p be non constant Polynomial of F;
reconsider p1 = p as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
deg p1 > 0 by RATFUNC1:def 2; then
reconsider p1 = p as non constant
Element of the carrier of Polynom-Ring F
by RING_4:def 4;
set q = NormPolynomial p1;
deg q = deg p by RING_4:27,RING_4:29; then
reconsider q as non constant monic Polynomial of F
by RING_4:def 4,RATFUNC1:def 2;
reconsider q as Ppoly of F by B,RING_5:70;
C: LC p <> 0.F;
q = (LC p)" * p by RING_4:23; then
LC p * q = ((LC p) * (LC p)") * p by RING_4:11
.= ((LC p)" * (LC p)) * p by GROUP_1:def 12
.= (1.F) * p by C,VECTSP_1:def 10
.= p;
hence p splits_in F by FIELD_4:def 5;
end;
hence thesis;
end;
LLsplit:
X^3-2 splits_in F_Complex & X^3-1 splits_in F_Complex &
X^2+X+1 splits_in F_Complex
proof
reconsider p = X^3-2 as Polynomial of F_Complex by FIELD_4:8;
X^3-2 is Element of the carrier of Polynom-Ring F_Rat &
p is Element of the carrier of Polynom-Ring F_Complex by POLYNOM3:def 10; then
deg p = 3 by LL,FIELD_4:20; then
reconsider p as non constant Polynomial of F_Complex by RATFUNC1:def 2;
consider a being non zero Element of F_Complex, q being Ppoly of F_Complex
such that B: p = a * q by llsplit1,FIELD_4:def 5;
thus X^3-2 splits_in F_Complex by B,FIELD_4:def 5;
reconsider p = X^3-1 as Polynomial of F_Complex by FIELD_4:8;
X^3-1 is Element of the carrier of Polynom-Ring F_Rat &
p is Element of the carrier of Polynom-Ring F_Complex by POLYNOM3:def 10; then
deg p = 3 by LL,FIELD_4:20; then
reconsider p as non constant Polynomial of F_Complex by RATFUNC1:def 2;
consider a being non zero Element of F_Complex, q being Ppoly of F_Complex
such that B: p = a * q by llsplit1,FIELD_4:def 5;
thus X^3-1 splits_in F_Complex by B,FIELD_4:def 5;
reconsider p = X^2+X+1 as Polynomial of F_Complex by FIELD_4:8;
A: deg X^2+X+1 = 2 by FIELD_9:def 4;
X^2+X+1 is Element of the carrier of Polynom-Ring F_Rat &
p is Element of the carrier of Polynom-Ring F_Complex by POLYNOM3:def 10; then
deg p = 2 by A,FIELD_4:20; then
reconsider p as non constant Polynomial of F_Complex by RATFUNC1:def 2;
consider a being non zero Element of F_Complex, q being Ppoly of F_Complex
such that B: p = a * q by llsplit1,FIELD_4:def 5;
thus X^2+X+1 splits_in F_Complex by B,FIELD_4:def 5;
end;
registration
cluster F_Real -> FAdj(F_Rat,{2-Root(2)})-extending;
coherence by FIELD_4:7;
cluster F_Real -> FAdj(F_Rat,{3-Root(2)})-extending;
coherence by FIELD_4:7;
cluster F_Complex -> FAdj(F_Rat,{2-Root(2)})-extending;
coherence;
cluster F_Complex -> FAdj(F_Rat,{3-Root(2)})-extending;
coherence;
cluster F_Complex -> FAdj(F_Rat,{3-CRoot(2),zeta})-extending;
coherence by FIELD_4:7;
end;
theorem
zeta = (-1/2) + <i> * ((sqrt 3) / 2);
theorem
zeta^2 = (-1/2) - <i> * (sqrt 3) / 2
proof
zeta = (-1/2) + <i> * ((sqrt 3) / 2); then
A: Re(zeta) = (-1/2) & Im(zeta) = (sqrt 3) / 2 by COMPLEX1:12; then
B: Re(zeta * zeta)
= (-1/2)^2 - ((sqrt 3) / 2)^2 by COMPLEX1:16
.= (-1/2)^2 - ((sqrt 3) / 2) * ((sqrt 3) / 2) by SQUARE_1:def 1
.= (-1/2)^2 - ((sqrt 3) * (sqrt 3)) / (2 * 2)
.= (-1/2)^2 - ((sqrt 3)^2) / (2 * 2) by SQUARE_1:def 1
.= (-1/2)^2 - (3 / (2*2)) by SQUARE_1:def 2
.= (-1/2) * (-1/2) - (3 / (2*2)) by SQUARE_1:def 1
.= -1/2;
C: Im(zeta * zeta) = 2 * ((-1/2) * ((sqrt 3) / 2)) by A,COMPLEX1:16
.= -(sqrt 3) / 2;
Re((-1/2) + <i> * (-(sqrt 3) / 2)) = -1/2 &
Im((-1/2) + <i> * (-(sqrt 3) / 2)) = (-(sqrt 3) / 2) by COMPLEX1:12; then
zeta * zeta = (-1/2) + <i> * (-(sqrt 3) / 2) by B,C,COMPLEX1:3;
hence thesis by O_RING_1:def 1;
end;
theorem
zeta|^2 <> 1 & zeta|^3 = 1 & zeta|^2 = -zeta - 1 by LZ23;
theorem
zeta is CRoot of 3,1 & zeta^2 is CRoot of 3,1 by lemCRo2;
theorem
3-Root(2) |^ 3 = 2 by R32;
theorem
X^3-1 = X-(1.F_Rat) * X^2+X+1 by lemX3;
theorem
deg X^2-2 = 2 & deg X^3-2 = 3 & deg X^3-1 = 3 & deg X^2+X+1 = 2 by LL;
theorem
for x being Element of F_Rat holds eval(X^2-2,x) = x|^2 - 2 by LKX2;
theorem
for x being Element of F_Rat holds eval(X^3-1,x) = x|^3 - 1 by LL31;
theorem
for x being Element of F_Rat holds eval(X^2+X+1,x) = x|^2 + x + 1 by LL32;
theorem
for x being Element of F_Rat holds eval(X^3-2,x) = x|^3 - 2 by LL3;
theorem
for r being Element of F_Real holds Ext_eval(X^2-2,r) = r|^2 - 2 by LKX2ext;
theorem
for z being Element of F_Complex holds Ext_eval(X^3-1,z) = z|^3 - 1
by evalext1;
theorem
for z being Element of F_Complex holds Ext_eval(X^2+X+1,z) = z|^2 + z + 1
by evalext11;
theorem evalext2:
for z being Element of F_Complex holds Ext_eval(X^3-2,z) = z|^3 - 2
proof
let x be Element of F_Complex;
set R = F_Complex, p = X^3-2, t = -(1.R + 1.R);
A0: t = -(1 + 1) by COMPLFLD:8,COMPLEX1:def 4;
consider F being FinSequence of the carrier of F_Complex such that
A1: Ext_eval(X^3-2,x) = Sum F and
A2: len F = len p and
A3: for n be Element of NAT st n in dom F holds
F.n = In(p.(n-'1),R) * (power R).(x,n-'1) by ALGNUM_1:def 1;
A5: F.1 = In(p.(1-'1),R) * (power R).(x,1-'1) by A3,A2,LL1,FINSEQ_3:25
.= In(p.0,R) * (power R).(x,1-'1) by XREAL_1:232
.= p.0 * (power R).(x,0) by XREAL_1:232
.= p.0 * 1_R by GROUP_1:def 7
.= t by LL0;
A6: 2-'1 = 2-1 by XREAL_0:def 2;
A7: F.2 = In(p.(2-'1),R) * (power R).(x,2-'1) by A3,A2,LL1,FINSEQ_3:25
.= 0.R * (power R).(x,1) by COMPLFLD:7,A6,LL0;
A8: 3-'1 = 3-1 by XREAL_0:def 2;
A9: F.3 = In(p.(3-'1),R) * (power R).(x,3-'1) by A3,A2,LL1,FINSEQ_3:25
.= 0.R * (power R).(x,2) by COMPLFLD:7,A8,LL0;
A10: 4-'1 = 4-1 by XREAL_0:def 2;
A11: F.4 = In(p.(4-'1),R) * (power R).(x,4-'1) by A3,A2,LL1,FINSEQ_3:25
.= x|^3 by A10,LL0,BINOM:def 2;
F = <*t,0.R,0.R,x|^3*> by A2,LL1,A5,A7,A9,A11,FINSEQ_4:76
.= <*t,0.R,0.R*> ^ <*x|^3*> by FINSEQ_4:74;
hence Ext_eval(p,x)
= Sum <*t,0.R,0.R*> + Sum <*x|^3*> by A1,RLVECT_1:41
.= Sum <*t,0.R,0.R*> + x|^3 by RLVECT_1:44
.= x |^ 3 - 2 by A0,RLVECT_1:72;
end;
theorem
for z being Element of the carrier of F_Complex holds
Ext_eval(X^3-1,z) = 0.F_Complex iff z is CRoot of 3,1 by lemCRo;
theorem
Discriminant X^2+X+1 = -3
proof
A1: (1+1) '*' 1.F_Rat
= (1 '*' 1.F_Rat) + (1 '*' 1.F_Rat) by RING_3:62
.= (1 '*' 1.F_Rat) + 1.F_Rat by RING_3:60
.= 1.F_Rat + 1.F_Rat by RING_3:60
.= 2 by GAUSSINT:13;
A2: (2+2) '*' 1.F_Rat
= (2 '*' 1.F_Rat) + (2 '*' 1.F_Rat) by RING_3:62
.= 4 by A1;
thus Discriminant X^2+X+1
= (1.F_Rat)^2 - 4 '*' (1.F_Rat) by FIELD_9:def 10
.= -3 by A2,GAUSSINT:13;
end;
theorem
FAdj(F_Rat,{zeta}) = FAdj(F_Rat,{sqrt(-3)})
proof
set F = FAdj(F_Rat,{sqrt(-3)});
A: F_Rat is Subfield of FAdj(F_Rat,{sqrt(-3)}) by FIELD_6:36;
{zeta} is Subset of FAdj(F_Rat,{sqrt(-3)})
proof
now let o be object;
assume o in {zeta}; then
B1: o = zeta by TARSKI:def 1;
B2: {sqrt(-3)} is Subset of FAdj(F_Rat,{sqrt(-3)}) by FIELD_6:35;
sqrt(-3) in {sqrt(-3)} by TARSKI:def 1; then
reconsider sqt = sqrt(-3) as Element of FAdj(F_Rat,{sqrt(-3)}) by B2;
B3: F is Subring of F_Complex by FIELD_5:12; then
B4: 1.F_Complex = 1.F & 1 = 1.F_Complex
by COMPLEX1:def 4,COMPLFLD:def 1,C0SP1:def 3; then
B5: -1.F_Complex = -1.F & -1 = -1.F_Complex by B3,FIELD_6:17;
B6: (-1) + <i> * (sqrt 3) = (-1.F_Complex) + sqrt(-3) &
(-1.F_Complex) + sqrt(-3) = (-1.F) + sqt by B3,B5,FIELD_6:15;
set t = 1.F_Complex + 1.F_Complex;
B9: t" = 2" by B4,COMPLFLD:5,COMPLFLD:9;
B10: t = 1.F + 1.F by B4,B3,FIELD_6:15;
t is non zero by COMPLFLD:9; then
B11: t" = (1.F + 1.F)" by B10,FIELD_6:18;
((-1) + <i> * (sqrt 3)) * 2"
= ((-1.F_Complex) + sqrt(-3)) * t" by B9,B4
.= ((-1.F) + sqt) * (1.F + 1.F)" by B3,B6,B11,FIELD_6:16;
hence o in the carrier of FAdj(F_Rat,{sqrt(-3)}) by B1;
end;
hence thesis by TARSKI:def 3;
end; then
C: FAdj(F_Rat,{zeta}) is Subfield of FAdj(F_Rat,{sqrt(-3)}) by A,FIELD_6:37;
set F = FAdj(F_Rat,{zeta});
A: F_Rat is Subfield of FAdj(F_Rat,{zeta}) by FIELD_6:36;
{sqrt(-3)} is Subset of FAdj(F_Rat,{zeta})
proof
now let o be object;
assume o in {sqrt(-3)}; then
B1: o = sqrt(-3) by TARSKI:def 1;
B2: {zeta} is Subset of FAdj(F_Rat,{zeta}) by FIELD_6:35;
zeta in {zeta} by TARSKI:def 1; then
reconsider zet = zeta as Element of FAdj(F_Rat,{zeta}) by B2;
B3: F is Subring of F_Complex by FIELD_5:12; then
B4: 1.F_Complex = 1.F & 1 = 1.F_Complex
by COMPLEX1:def 4,COMPLFLD:def 1,C0SP1:def 3;
set t = 1.F_Complex + 1.F_Complex;
t = 1.F + 1.F by B3,B4,FIELD_6:15; then
t * zeta = (1.F + 1.F) * zet by B3,FIELD_6:16; then
t * zeta + 1.F_Complex = (1.F + 1.F) * zet + 1.F by B3,B4,FIELD_6:15;
hence o in the carrier of FAdj(F_Rat,{zeta}) by B1,B4;
end;
hence thesis by TARSKI:def 3;
end; then
FAdj(F_Rat,{sqrt(-3)}) is Subfield of FAdj(F_Rat,{zeta}) by A,FIELD_6:37;
hence thesis by C,FIELD_7:def 2,FIELD_7:2;
end;
begin :: A Splitting Field of X^2-2
theorem mp:
MinPoly(2-Root(2),F_Rat) = X^2-2
proof
Ext_eval(X^2-2,2-Root(2))
= (2-Root(2))|^(1+1) - 2 by LKX2ext
.= (2-Root(2))|^1 * (2-Root(2))|^1 - 2 by BINOM:10
.= (2-Root(2)) * (2-Root(2))|^1 - 2 by BINOM:8
.= (2-Root(2)) * (2-Root(2)) - 2 by BINOM:8
.= (sqrt 2)^2 - 2 by SQUARE_1:def 1
.= 2 - 2 by SQUARE_1:def 2
.= 0.F_Real;
hence thesis by FIELD_6:52;
end;
theorem
deg(FAdj(F_Rat,{2-Root(2)}),F_Rat) = 2 by LL,mp,FIELD_6:67;
theorem
{ 1, sqrt 2 } is Basis of VecSp(FAdj(F_Rat,{2-Root(2)}),F_Rat)
proof
set F = F_Rat;
B: now let o be object;
assume o in Base 2-Root(2); then
consider n being Element of NAT such that
B1: o = 2-Root(2)|^n & n < deg MinPoly(2-Root(2),F);
n < 1 + 1 by LL,B1,mp; then
n <= 1 by NAT_1:13; then
per cases by NAT_1:25;
suppose n = 0;
then o = 1_F_Real by B1,BINOM:8;
hence o in {1, sqrt 2} by TARSKI:def 2;
end;
suppose n = 1;
then o = 2-Root(2) by B1,BINOM:8;
hence o in {1, sqrt 2} by TARSKI:def 2;
end;
end;
now let o be object;
assume o in {1, sqrt 2}; then
per cases by TARSKI:def 2;
suppose o = 1;
then o = 1_F_Real
.= 2-Root(2)|^0 by BINOM:8;
hence o in Base 2-Root(2) by LL,mp;
end;
suppose o = sqrt 2;
then o = 2-Root(2)|^1 by BINOM:8;
hence o in Base 2-Root(2) by LL,mp;
end;
end;
then Base 2-Root(2) = {1, sqrt 2} by B,TARSKI:2;
hence thesis by FIELD_6:65;
end;
theorem
Roots X^2-2 = {};
theorem
not X^2-2 splits_in F_Rat
proof
now assume X^2-2 splits_in F_Rat; then
consider a being non zero Element of F_Rat, q being Ppoly of F_Rat such that
A: X^2-2 = a * q by FIELD_4:def 5;
thus contradiction by A;
end;
hence thesis;
end;
theorem 2splitb:
Roots(F_Real,X^2-2) = {2-Root(2), -2-Root(2)}
proof
set F = F_Real, p = X^2-2;
set M = {2-Root(2), -2-Root(2)};
H: Roots(F,p) = {a where a is Element of F : a is_a_root_of p,F}
by FIELD_4:def 4;
now let o be object;
assume B: o in {2-Root(2), -2-Root(2)}; then
reconsider c = o as Element of F_Real;
per cases by B,TARSKI:def 2;
suppose E0: o = 2-Root(2);
Ext_eval(p,c)
= 2-Root(2)|^(1+1) - 2 by E0,LKX2ext
.= (2-Root(2)|^1 * 2-Root(2)|^1) - 2 by BINOM:10
.= (2-Root(2)|^1 * 2-Root(2)) - 2 by BINOM:8
.= (2-Root(2) * 2-Root(2)) - 2 by BINOM:8
.= (sqrt 2)^2 - 2 by SQUARE_1:def 1
.= 2 - 2 by SQUARE_1:def 2
.= 0.F;
then c is_a_root_of p,F by FIELD_4:def 2;
hence o in Roots(F,p) by H;
end;
suppose E0: o = -2-Root(2);
Ext_eval(p,c)
= (-2-Root(2))|^(1+1) - 2 by E0,LKX2ext
.= ((-2-Root(2))|^1 * (-2-Root(2))|^1) - 2 by BINOM:10
.= ((-2-Root(2))|^1 * (-2-Root(2))) - 2 by BINOM:8
.= ((-2-Root(2)) * (-2-Root(2))) - 2 by BINOM:8
.= (2-Root(2) * 2-Root(2)) - 2
.= (sqrt 2)^2 - 2 by SQUARE_1:def 1
.= 2 - 2 by SQUARE_1:def 2
.= 0.F;
then c is_a_root_of p,F by FIELD_4:def 2;
hence o in Roots(F,p) by H;
end;
end; then
B: M c= Roots(F_Real,X^2-2);
the carrier of Polynom-Ring F_Rat c= the carrier of Polynom-Ring F
by FIELD_4:10; then
reconsider q = X^2-2 as Element of the carrier of Polynom-Ring F;
reconsider qq = q as non zero Element of the carrier of Polynom-Ring F_Rat;
H: 2= deg X^2-2 by FIELD_9:18 .= deg q by FIELD_4:20; then
reconsider q as non constant Element of the carrier of Polynom-Ring F_Real
by RING_4:def 4;
C: card M = 2 by CARD_2:57,SQUARE_1:19;
D: card Roots(F_Real,X^2-2) = 2
proof
F: card(Roots q) <= 2 by H,RING_5:22;
G: 2 <= card Roots(F_Real,qq) by C,B,NAT_1:43;
Roots(F_Real,X^2-2) = Roots q by FIELD_7:13;
hence thesis by F,G,XXREAL_0:1;
end;
thus thesis by B,C,D,lemfinset;
end;
theorem 2splita:
X^2-2 = X-2-Root(2) * X+2-Root(2)
proof
set F = F_Real, a = 2-Root(2), b = -2-Root(2);
A: X-a = rpoly(1,a) by FIELD_9:def 2 .= <%-a, 1.F%> by RING_5:10;
B: X-b = rpoly(1,b) by FIELD_9: def 2 .= <%-b, 1.F%> by RING_5:10;
C: X-b = rpoly(1,-2-Root(2)) by FIELD_9:def 2 .= X+2-Root(2) by FIELD_9:def 3;
D: (X-a) * (X-b) = <%-a, 1.F%> *' <%-b, 1.F%> by A,B,POLYNOM3:def 10
.= <%(-a)*(-b),(1.F)*(-b)+(1.F)*(-a),(1.F)*(1.F)%> by FIELD_9:24
.= <%a*b,-b+-a,1.F%>;
H: a * b = -((sqrt 2) * (sqrt 2))
.= -((sqrt 2)^2) by SQUARE_1:def 1
.= -(1.F_Rat + 1.F_Rat) by SQUARE_1:def 2,GAUSSINT:def 14;
the carrier of Polynom-Ring F_Rat c= the carrier of Polynom-Ring F
by FIELD_4:10; then
X^2-2 in the carrier of Polynom-Ring F; then
reconsider p = X^2-2 as Polynomial of F by POLYNOM3:def 10;
E: dom p = NAT by FUNCT_2:def 1
.= dom <%a*b,-b+-a,1.F%> by FUNCT_2:def 1;
now let o be object;
assume o in dom <%a*b,-b+-a,1.F%>;
then reconsider i = o as Element of NAT;
i <= 2 implies i = 0 or ... or i = 2; then
per cases;
suppose C: i = 0; then
<%a*b,-b+-a,1.F%>.i = a * b by FIELD_9:16
.= p.i by C,H,FIELD_9:16;
hence <%a*b,-b+-a,1.F%>.o = p.o;
end;
suppose C: i = 1; then
<%a*b,-b+-a,1.F%>.i = -b + -a by FIELD_9:16
.= p.i by C,FIELD_9:16,GAUSSINT:def 14;
hence <%a*b,-b+-a,1.F%>.o = p.o;
end;
suppose C: i = 2; then
<%a*b,-b+-a,1.F%>.i = 1.F by FIELD_9:16
.= p.i by C,FIELD_9:16,GAUSSINT:def 14;
hence <%a*b,-b+-a,1.F%>.o = p.o;
end;
suppose i > 2; then
C1: i >= 2 + 1 by NAT_1:13; then
<%a*b,-b+-a,1.F%>.i = 0.F by FIELD_9:16
.= p.i by C1,FIELD_9:16,GAUSSINT:def 14;
hence <%a*b,-b+-a,1.F%>.o = p.o;
end;
end;
then p = <%a*b,-b+-a,1.F%> by E
.= (X-2-Root(2)) * (X+2-Root(2)) by C,D;
hence thesis;
end;
theorem 2split:
FAdj(F_Rat,{2-Root(2)}) is SplittingField of X^2-2
proof
set F = FAdj(F_Rat,{2-Root(2)});
C: X-2-Root(2) = rpoly(1,2-Root(2)) & X+2-Root(2) = rpoly(1,-2-Root(2))
by FIELD_9:def 2,FIELD_9:def 3;
rpoly(1,2-Root(2)) is Ppoly of F_Real &
rpoly(1,-2-Root(2)) is Ppoly of F_Real by RING_5:51; then
A: rpoly(1,2-Root(2)) *' rpoly(1,-2-Root(2)) is Ppoly of F_Real by RING_5:52;
X^2-2 = 1.F_Real * (rpoly(1,2-Root(2)) *' rpoly(1,-2-Root(2)))
by C,POLYNOM3:def 10,2splita; then
D: X^2-2 splits_in F_Real by A,FIELD_4:def 5;
{2-Root(2), -2-Root(2)} c= the carrier of F
proof
2-Root(2) in {2-Root(2)} & {2-Root(2)} is Subset of F
by FIELD_6:35,TARSKI:def 1; then
reconsider a = 2-Root(2) as Element of F;
H: F is Subring of F_Real by FIELD_5:12;
now let o be object;
assume o in {2-Root(2), -2-Root(2)}; then
per cases by TARSKI:def 2;
suppose o = 2-Root(2);
then o = a;
hence o in the carrier of F;
end;
suppose o = -2-Root(2);
then o = -a by H,FIELD_6:17;
hence o in the carrier of F;
end;
end;
hence thesis;
end; then
B: X^2-2 splits_in F by D,2splitb,FIELD_8:27;
now let E be FieldExtension of F_Rat;
assume C: X^2-2 splits_in E & E is Subfield of F; then
E: F is E-extending & E is Subfield of F_Real by EC_PF_1:5,FIELD_4:7;
F: F_Rat is Subfield of E by FIELD_4:7;
{2-Root(2)} is Subset of E
proof
G: Roots(F_Real,X^2-2) c= the carrier of E by E,D,C,FIELD_8:27;
2-Root(2) in Roots(F_Real,X^2-2) by 2splitb,TARSKI:def 2; then
2-Root(2) in the carrier of E by G;
then {2-Root(2)} c= the carrier of E by TARSKI:def 1;
hence thesis;
end;
then F is Subfield of E by F,E,FIELD_6:37;
hence E == F by C,FIELD_7:def 2;
end;
hence F is SplittingField of X^2-2 by B,FIELD_8:def 1;
end;
theorem nnn:
not 3-Root(2) is Element of FAdj(F_Rat,{2-Root(2)})
proof
H: MinPoly(3-Root(2),F_Rat) = X^3-2 by LL2,FIELD_6:52;
now assume 3-Root(2) is Element of FAdj(F_Rat,{2-Root(2)}); then
reconsider a = 3-Root(2) as Element of FAdj(F_Rat,{2-Root(2)});
I: deg MinPoly(a,F_Rat) = 3 by H,LL,mmv;
deg(FAdj(F_Rat,{2-Root(2)}),F_Rat) = 2 by LL,mp,FIELD_6:67;
hence contradiction by I,mmu,INT_2:27;
end;
hence thesis;
end;
theorem
not F_Real is SplittingField of X^2-2
proof
set F = FAdj(F_Rat,{2-Root(2)});
now assume A: F_Real is SplittingField of X^2-2;
X^2-2 splits_in F by 2split,FIELD_8:def 1; then
F_Real == F by A,FIELD_8:def 1; then
F_Real is Subfield of F by FIELD_7:def 2; then
the carrier of F_Real c= the carrier of F by EC_PF_1:def 1;
hence contradiction by nnn;
end;
hence thesis;
end;
theorem
not F_Complex is SplittingField of X^2-2
proof
set F = FAdj(F_Rat,{2-Root(2)});
H: F is Subfield of F_Complex by FIELD_4:7;
now assume A: F_Complex is SplittingField of X^2-2;
X^2-2 splits_in F by 2split,FIELD_8:def 1; then
F_Complex == F by H,A,FIELD_8:def 1; then
F_Complex is Subfield of F by FIELD_7:def 2; then
the carrier of F_Complex c= the carrier of F by EC_PF_1:def 1;
hence contradiction by nnn;
end;
hence thesis;
end;
begin :: A Splitting Field of X^3-1 and X^2+X+1
theorem
Roots X^3-1 = {1}
proof
A: now let o be object;
assume o in {1}; then
B: o = 1.F_Rat by TARSKI:def 1,GAUSSINT:13;
eval(X^3-1,1.F_Rat)
= (1.F_Rat)|^(2+1) - 1.F_Rat by LL31,GAUSSINT:13
.= ((1.F_Rat)|^2 * (1.F_Rat)|^1) - 1.F_Rat by BINOM:10
.= ((1.F_Rat)|^(1+1) * 1.F_Rat) - 1.F_Rat by BINOM:8
.= ((1.F_Rat)|^1 * (1.F_Rat)|^1) - 1.F_Rat by BINOM:10
.= ((1.F_Rat)|^1 * 1.F_Rat) - 1.F_Rat by BINOM:8
.= (1.F_Rat * 1.F_Rat) - 1.F_Rat by BINOM:8
.= 0.F_Rat by RLVECT_1:15; then
1.F_Rat is_a_root_of X^3-1 by POLYNOM5:def 7;
hence o in Roots X^3-1 by B,POLYNOM5:def 10;
end;
H: Roots(F_Complex,X^3-1) =
{a where a is Element of F_Complex : a is_a_root_of X^3-1,F_Complex}
by FIELD_4:def 4;
now let o be object;
assume C: o in Roots X^3-1; then
reconsider a = o as Element of F_Rat;
F_Rat is Subfield of F_Complex by FIELD_4:7; then
the carrier of F_Rat c= the carrier of F_Complex by EC_PF_1:def 1; then
reconsider c = a as Element of F_Complex;
G: a is_a_root_of X^3-1 by C,POLYNOM5:def 10;
0.F_Complex = 0.F_Rat by GAUSSINT:13,COMPLFLD:def 1
.= eval(X^3-1,a) by G,POLYNOM5:def 7
.= Ext_eval(X^3-1,c) by FIELD_6:10;
then c is_a_root_of X^3-1,F_Complex by FIELD_4:def 2;
then D: a in {1, zeta, zeta^2} by H,lemroots3;
F_Rat is Subfield of F_Real by FIELD_4:7; then
E: the carrier of F_Rat c= the carrier of F_Real by EC_PF_1:def 1;
now assume a <> 1; then
per cases by D,ENUMSET1:def 1;
suppose a = zeta;
hence contradiction by E,FIELD_7:def 5;
end;
suppose a = zeta^2;
hence contradiction by E,FIELD_7:def 5;
end;
end;
hence o in {1} by TARSKI:def 1;
end;
hence thesis by A,TARSKI:2;
end;
theorem
Roots X^2+X+1 = {};
theorem minpzeta:
MinPoly(zeta,F_Rat) = X^2+X+1
proof
H: Roots(F_Complex,X^2+X+1) =
{a where a is Element of F_Complex : a is_a_root_of X^2+X+1,F_Complex}
by FIELD_4:def 4;
zeta in Roots(F_Complex,X^2+X+1) by rootz,TARSKI:def 2;
then consider a being Element of F_Complex such that
I: a = zeta & a is_a_root_of X^2+X+1,F_Complex by H;
Ext_eval(X^2+X+1,zeta) = 0.F_Complex by I,FIELD_4:def 2;
hence thesis by FIELD_6:52;
end;
theorem
Roots(F_Complex,X^3-1) = {1, zeta, zeta^2} by lemroots3;
theorem
Roots(F_Complex,X^2+X+1) = {zeta, zeta^2} by rootz;
theorem
not X^3-1 splits_in F_Rat
proof
I: F_Rat is FieldExtension of F_Rat by FIELD_4:6;
F_Rat is Subfield of F_Real by FIELD_4:7; then
K: the carrier of F_Rat c= the carrier of F_Real by EC_PF_1:def 1;
now assume X^3-1 splits_in F_Rat; then
A: {1, zeta, zeta^2} c= the carrier of F_Rat
by lemroots3,I,LLsplit,FIELD_8:27;
zeta in {1, zeta, zeta^2} by ENUMSET1:def 1;
hence contradiction by A,K,FIELD_7:def 5;
end;
hence thesis;
end;
theorem
not X^3-1 splits_in F_Real
proof
now assume X^3-1 splits_in F_Real; then
A: {1, zeta, zeta^2} c= the carrier of F_Real
by lemroots3,LLsplit,FIELD_8:27;
zeta in {1, zeta, zeta^2} by ENUMSET1:def 1;
hence contradiction by A,FIELD_7:def 5;
end;
hence thesis;
end;
theorem
not X^2+X+1 splits_in F_Rat
proof
I: F_Rat is FieldExtension of F_Rat by FIELD_4:6;
F_Rat is Subfield of F_Real by FIELD_4:7; then
K: the carrier of F_Rat c= the carrier of F_Real by EC_PF_1:def 1;
now assume X^2+X+1 splits_in F_Rat; then
A: {zeta, zeta^2} c= the carrier of F_Rat by rootz,I,LLsplit,FIELD_8:27;
zeta in {zeta, zeta^2} by TARSKI:def 2;
hence contradiction by A,K,FIELD_7:def 5;
end;
hence thesis;
end;
theorem
not X^2+X+1 splits_in F_Real
proof
now assume X^2+X+1 splits_in F_Real; then
A: {zeta, zeta^2} c= the carrier of F_Real by rootz,LLsplit,FIELD_8:27;
zeta in {zeta, zeta^2} by TARSKI:def 2;
hence contradiction by A,FIELD_7:def 5;
end;
hence thesis;
end;
theorem lemX3a:
X^2+X+1 = X-zeta * X-(zeta^2)
proof
set F = F_Complex;
the carrier of Polynom-Ring F_Rat c= the carrier of Polynom-Ring F
by FIELD_4:10; then
X^2+X+1 is Element of the carrier of Polynom-Ring F; then
reconsider q = X^2+X+1 as Polynomial of F;
reconsider p1 = X-zeta, p2 = X-(zeta^2) as Polynomial of F;
L: 4 -' 1 = 4 - 1 by XREAL_0:def 2; then
K: 2 -' 1 = 2 - 1 & 3 -' 1 = 3 - 1 & 3 -' 2 = 3 - 2 & 4 -' 1 = 3 &
4 -' 2 = 4 - 2 by XREAL_0:def 2;
A: dom(p1*'p2) = NAT by FUNCT_2:def 1 .= dom q by FUNCT_2:def 1;
B: zeta|^2 = zeta^2 by lemI;
D0: q.0 = 1.F_Rat & q.1 = 1.F_Rat & q.2 = 1.F_Rat by FIELD_9:16;
1 = 1.F by COMPLFLD:def 1,COMPLEX1:def 4; then
-zeta - 1 = -zeta - 1.F; then
D2: -(-zeta - 1) = -(-zeta - 1.F)
.= 1.F + --zeta
.= zeta + 1.F;
now let o be object;
assume o in dom q;
then reconsider i = o as Element of NAT;
consider r being FinSequence of the carrier of F such that
B1: len r = i+1 & (p1*'p2).i = Sum r &
for k being Element of NAT st k in dom r
holds r.k = p1.(k-'1) * p2.(i+1-'k) by POLYNOM3:def 9;
i <= 2 implies i = 0 or ... or i = 2; then
per cases;
suppose C: i = 0;
then B2: r = <*r.1*> by B1,FINSEQ_1:40;
then dom r = {1} by FINSEQ_1:2,FINSEQ_1:38;
then 1 in dom r by TARSKI:def 1;
then r.1 = p1.(1-'1) * p2.(0+1-'1) by C,B1
.= p1.(1-'1) * p2.0 by NAT_2:8
.= p1.0 * p2.0 by NAT_2:8
.= rpoly(1,zeta).0 * p2.0 by FIELD_9:def 2
.= (-power(F).(zeta,1)) * p2.0 by HURWITZ:25
.= (-(zeta|^1)) * p2.0 by BINOM:def 2
.= (-zeta) * p2.0 by BINOM:8
.= (-zeta) * rpoly(1,zeta^2).0 by FIELD_9:def 2
.= (-zeta) * (-power(F).(zeta^2,1)) by HURWITZ:25
.= (-zeta) * (-(zeta^2|^1)) by BINOM:def 2
.= (-zeta) * (-(zeta|^2)) by B,BINOM:8
.= zeta * zeta|^2
.= zeta|^2 * zeta|^1 by BINOM:8
.= zeta|^(2+1) by BINOM:10
.= 1.F_Complex by LZ23,COMPLEX1:def 4,COMPLFLD:def 1;
hence (p1*'p2).o = 1.F_Complex by B1,B2,RLVECT_1:44
.= q.o by C,D0,GAUSSINT:13,COMPLEX1:def 4,COMPLFLD:def 1;
end;
suppose C: i = 1;
then B3: r = <*r.1,r.2*> by B1,FINSEQ_1:44;
B4: dom r = {1,2} by B1,C,FINSEQ_1:def 3,FINSEQ_1:2;
then 1 in dom r by TARSKI:def 2;
then B5: r.1 = p1.(1-'1) * p2.(1+1-'1) by C,B1
.= p1.0 * p2.1 by K,NAT_2:8
.= rpoly(1,zeta).0 * p2.1 by FIELD_9:def 2
.= (-power(F).(zeta,1)) * p2.1 by HURWITZ:25
.= (-(zeta|^1)) * p2.1 by BINOM:def 2
.= (-zeta) * p2.1 by BINOM:8
.= (-zeta) * rpoly(1,zeta^2).1 by FIELD_9:def 2
.= (-zeta) * 1_F by HURWITZ:25
.= -zeta;
2 in dom r by B4,TARSKI:def 2;
then r.2 = p1.(2-'1) * p2.(1+1-'2) by C,B1
.= p1.1 * p2.0 by K,NAT_2:8
.= rpoly(1,zeta).1 * p2.0 by FIELD_9:def 2
.= 1_F * p2.0 by HURWITZ:25
.= rpoly(1,zeta^2).0 by FIELD_9:def 2
.= -power(F).(zeta^2,1) by HURWITZ:25
.= -(zeta^2|^1) by BINOM:def 2
.= zeta + 1.F by D2,B,LZ23,BINOM:8;
then Sum r = -zeta + (zeta + 1.F) by B3,B5,RLVECT_1:45
.= (-zeta + zeta) + 1.F
.= 0.F + 1.F;
hence (p1*'p2).o = q.o
by C,D0,B1,COMPLFLD:def 1,GAUSSINT:13,COMPLEX1:def 4;
end;
suppose C: i = 2;
then B3: r = <*r.1,r.2,r.3*> by B1,FINSEQ_1:45;
B4: dom r = Seg 3 by B1,C,FINSEQ_1:def 3
.= Seg 2 \/ {2+1} by FINSEQ_1:9
.= {1,2,3} by FINSEQ_1:2,ENUMSET1:3;
then 1 in dom r by ENUMSET1:def 1;
then B5: r.1 = p1.(1-'1) * p2.(2+1-'1) by C,B1
.= p1.0 * p2.2 by K,NAT_2:8
.= p1.0 * rpoly(1,zeta^2).2 by FIELD_9:def 2
.= p1.0 * 0.F by HURWITZ:26;
2 in dom r by B4,ENUMSET1:def 1;
then B6: r.2 = p1.1 * p2.1 by K,C,B1
.= rpoly(1,zeta).1 * p2.1 by FIELD_9:def 2
.= 1_F * p2.1 by HURWITZ:25
.= rpoly(1,zeta^2).1 by FIELD_9:def 2
.= 1_F by HURWITZ:25;
3 in dom r by B4,ENUMSET1:def 1;
then r.3 = p1.2 * p2.(2+1-'3) by K,C,B1
.= rpoly(1,zeta).2 * p2.(2+1-'3) by FIELD_9:def 2
.= 0.F * p2.(2+1-'3) by HURWITZ:26;
then Sum r = 0.F + 1.F + 0.F by B3,B5,B6,RLVECT_1:46 .= 1.F;
hence (p1*'p2).o = q.o
by C,D0,B1,COMPLFLD:def 1,GAUSSINT:13,COMPLEX1:def 4;
end;
suppose i > 2; then
C1: i >= 2 + 1 by NAT_1:13;
then E: q.i = 0.F_Rat by FIELD_9:16
.= 0.F by GAUSSINT:13,COMPLFLD:def 1;
p1 = rpoly(1,zeta) & p2 = rpoly(1,zeta^2) by FIELD_9:def 2; then
C2: deg p1 = 1 & deg p2 = 1 by HURWITZ:27;
C3: deg p1 = len p1 - 1 & deg p2 = len p2 - 1 by HURWITZ:def 2;
len(p1*'p2) <= len p1 + len p2 -' 1 by leng;
hence (p1*'p2).o = q.o by C2,C3,E,L,C1,XXREAL_0:2,ALGSEQ_1:8;
end;
end;
then q = p1 *' p2 by A .= X-zeta * X-(zeta^2) by POLYNOM3:def 10;
hence thesis;
end;
theorem
X^3-1 = X-(1.F_Complex) * X-zeta * X-(zeta^2)
proof
reconsider q = X^2+X+1 as Polynomial of F_Rat;
reconsider p = X-zeta * X-(zeta^2) as Polynomial of F_Complex
by POLYNOM3:def 10;
B: X-(1.F_Complex) = rpoly(1,1.F_Complex) by FIELD_9:def 2;
C: X-(1.F_Rat) = rpoly(1,1.F_Rat) by FIELD_9:def 2;
1.F_Rat = 1.F_Complex by GAUSSINT:13,COMPLEX1:def 4,COMPLFLD:def 1; then
A: X-(1.F_Complex) = X-(1.F_Rat) by B,C,FIELD_4:21;
thus X^3-1 = rpoly(1,1.F_Rat) *' q by C,lemX3,POLYNOM3:def 10
.= rpoly(1,1.F_Complex) *' p by A,B,C,FIELD_4:17,lemX3a
.= X-(1.F_Complex) * (X-zeta * X-(zeta^2)) by B,POLYNOM3:def 10
.= X-(1.F_Complex) * X-zeta * X-(zeta^2) by GROUP_1:def 3;
end;
theorem Xsplit:
FAdj(F_Rat,{zeta}) is SplittingField of X^2+X+1
proof
set F = FAdj(F_Rat,{zeta});
Roots(F_Complex,X^2+X+1) c= the carrier of F
proof
A1: {zeta} is Subset of F by FIELD_6:35;
zeta in {zeta} by TARSKI:def 1; then
reconsider b = zeta as Element of F by A1;
A3: F is Subring of F_Complex by FIELD_5:12;
now let o be object;
assume o in Roots(F_Complex,X^2+X+1); then
per cases by rootz,TARSKI:def 2;
suppose o = zeta;
then o = b;
hence o in the carrier of F;
end;
suppose o = zeta^2;
then o = zeta * zeta by O_RING_1:def 1
.= b * b by A3,FIELD_6:16;
hence o in the carrier of F;
end;
end;
hence thesis;
end; then
B: X^2+X+1 splits_in F by LLsplit,FIELD_8:27;
now let E be FieldExtension of F_Rat;
assume C: X^2+X+1 splits_in E & E is Subfield of F; then
E: E is Subfield of F_Complex by EC_PF_1:5;
D: F_Rat is Subfield of E by FIELD_4:7;
{zeta} is Subset of E
proof
F_Complex is E-extending by E,FIELD_4:7; then
A1: Roots(F_Complex,X^2+X+1) c= the carrier of E by LLsplit,C,FIELD_8:27;
zeta in Roots(F_Complex,X^2+X+1) by rootz,TARSKI:def 2; then
zeta in the carrier of E by A1;
then {zeta} c= the carrier of E by TARSKI:def 1;
hence thesis;
end;
then F is Subfield of E by D,E,FIELD_6:37;
hence E == F by C,FIELD_7:def 2;
end;
hence F is SplittingField of X^2+X+1 by B,FIELD_8:def 1;
end;
theorem Ysplit:
FAdj(F_Rat,{zeta}) is SplittingField of X^3-1
proof
set F = FAdj(F_Rat,{zeta});
Roots(F_Complex,X^3-1) c= the carrier of F
proof
A1: {zeta} is Subset of F by FIELD_6:35;
zeta in {zeta} by TARSKI:def 1; then
reconsider b = zeta as Element of F by A1;
A3: F is Subring of F_Complex by FIELD_5:12;
A4: zeta^2 = zeta * zeta by O_RING_1:def 1
.= b * b by A3,FIELD_6:16;
now let o be object;
assume o in Roots(F_Complex,X^3-1); then
per cases by lemroots3,ENUMSET1:def 1;
suppose o = 1;
then o = 1.F_Complex by COMPLEX1:def 4,COMPLFLD:def 1
.= 1.F by EC_PF_1:def 1;
hence o in the carrier of F;
end;
suppose o = zeta;
then o = b;
hence o in the carrier of F;
end;
suppose o = zeta^2;
hence o in the carrier of F by A4;
end;
end;
hence thesis;
end; then
B: X^3-1 splits_in F by LLsplit,FIELD_8:27;
now let E be FieldExtension of F_Rat;
assume C: X^3-1 splits_in E & E is Subfield of F; then
E: E is Subfield of F_Complex by EC_PF_1:5;
D: F_Rat is Subfield of E by FIELD_4:7;
{zeta} is Subset of E
proof
F_Complex is E-extending by E,FIELD_4:7; then
A1: Roots(F_Complex,X^3-1) c= the carrier of E by LLsplit,C,FIELD_8:27;
zeta in Roots(F_Complex,X^3-1) by lemroots3,ENUMSET1:def 1; then
zeta in the carrier of E by A1;
then {zeta} c= the carrier of E by TARSKI:def 1;
hence thesis;
end;
then F is Subfield of E by D,E,FIELD_6:37;
hence E == F by C,FIELD_7:def 2;
end;
hence F is SplittingField of X^3-1 by B,FIELD_8:def 1;
end;
theorem
deg(FAdj(F_Rat,{zeta}),F_Rat) = 2 by minpzeta,LL,FIELD_6:67;
theorem baseZ:
{1, zeta} is Basis of VecSp(FAdj(F_Rat,{zeta}),F_Rat)
proof
set F = F_Rat;
B: now let o be object;
assume o in Base zeta; then
consider n being Element of NAT such that
B1: o = zeta|^n & n < deg MinPoly(zeta,F);
n < 1 + 1 by LL,B1,minpzeta; then
n <= 1 by NAT_1:13; then
per cases by NAT_1:25;
suppose n = 0;
then o = 1_F_Complex by B1,BINOM:8;
then o = 1 by COMPLEX1:def 4,COMPLFLD:def 1;
hence o in {1, zeta} by TARSKI:def 2;
end;
suppose n = 1;
then o = zeta by B1,BINOM:8;
hence o in {1, zeta} by TARSKI:def 2;
end;
end;
now let o be object;
assume o in {1, zeta}; then
per cases by TARSKI:def 2;
suppose o = 1;
then o = 1_F_Complex by COMPLEX1:def 4,COMPLFLD:def 1
.= zeta|^0 by BINOM:8;
hence o in Base zeta by LL,minpzeta;
end;
suppose o = zeta;
then o = zeta|^1 by BINOM:8;
hence o in Base zeta by LL,minpzeta;
end;
end;
then Base zeta = {1, zeta} by B,TARSKI:2;
hence thesis by FIELD_6:65;
end;
theorem ns2:
not sqrt 2 is Element of FAdj(F_Rat,{zeta})
proof
set F = FAdj(F_Rat,{zeta}), V = VecSp(F,F_Rat);
A: the carrier of F = the carrier of V by FIELD_4:def 6;
{zeta} is Subset of F & zeta in {zeta} by FIELD_6:35,TARSKI:def 1; then
reconsider e = 1.F_Complex, z = zeta as Element of V by A,FIELD_6:def 6;
e = 1 by COMPLEX1:def 4,COMPLFLD:def 1; then
C: Lin{e,z} = the ModuleStr of V by baseZ,VECTSP_7:def 3;
now assume sqrt 2 in the carrier of FAdj(F_Rat,{zeta}); then
sqrt 2 in Lin{e,z} by FIELD_4:def 6,C; then
consider l being Linear_Combination of {e,z} such that
C1: sqrt 2 = Sum l by VECTSP_7:7;
F_Rat is Subfield of F_Complex by FIELD_4:7; then
the carrier of F_Rat c= the carrier of F_Complex by EC_PF_1:def 1; then
reconsider a = l.e, b = l.z as Element of F_Complex;
C2: sqrt 2 = a + b * zeta
proof
E: l.e * e = a
proof
E0: F_Rat is Subfield of F by FIELD_6:36;
1.F_Complex = 1.F by EC_PF_1:def 1; then
E1: [l.e,e] in [:the carrier of F_Rat,the carrier of F:]
by ZFMISC_1:def 2;
the carrier of F_Rat c= the carrier of F by E0,EC_PF_1:def 1; then
E2: [:the carrier of F_Rat,the carrier of F:] c=
[:the carrier of F,the carrier of F:] by ZFMISC_1:96;
thus l.e * e
= ((the multF of F)|[:the carrier of F_Rat,the carrier of F:]).(l.e,e)
by FIELD_4:def 6
.= (the multF of F).(l.e,e) by E1,FUNCT_1:49
.= ((the multF of F_Complex)||(the carrier of F)).(l.e,e)
by EC_PF_1:def 1
.= a * 1.F_Complex by E2,E1,FUNCT_1:49 .= a;
end;
F: l.z * z = b * zeta
proof
F0: F_Rat is Subfield of F by FIELD_6:36;
{zeta} is Subset of F & zeta in {zeta} by FIELD_6:35,TARSKI:def 1;
then
F1: [l.z,z] in [:the carrier of F_Rat,the carrier of F:]
by ZFMISC_1:def 2;
the carrier of F_Rat c= the carrier of F by F0,EC_PF_1:def 1; then
F2: [:the carrier of F_Rat,the carrier of F:] c=
[:the carrier of F,the carrier of F:] by ZFMISC_1:96;
thus l.z * z
= ((the multF of F)|[:the carrier of F_Rat,the carrier of F:]).(l.z,z)
by FIELD_4:def 6
.= (the multF of F).(l.z,z) by F1,FUNCT_1:49
.= ((the multF of F_Complex)||(the carrier of F)).(l.z,z)
by EC_PF_1:def 1
.= b * zeta by F2,F1,FUNCT_1:49;
end;
a in F & b * zeta in F
proof
F_Rat is Subfield of F by FIELD_6:36; then
G2: the carrier of F_Rat c= the carrier of F by EC_PF_1:def 1;
hence a in F;
G3: F is Subring of F_Complex by FIELD_5:12;
{zeta} is Subset of F & zeta in {zeta} by TARSKI:def 1,FIELD_6:35;
then reconsider u = zeta, v = b as Element of F by G2;
v * u = b * zeta by G3,FIELD_6:16;
hence b * zeta in F;
end; then
G: [a,b*zeta] in [:the carrier of F,the carrier of F:] by ZFMISC_1:def 2;
l.e * e + l.z * z
= (the addF of F).(a,b*zeta) by E,F,FIELD_4:def 6
.= ((the addF of F_Complex)||(the carrier of F)).(a,b*zeta)
by EC_PF_1:def 1
.= a + b * zeta by G,FUNCT_1:49;
hence thesis by C1,VECTSP_6:18;
end;
C4: sqrt 2 = (a + b * (-1/2)) + <i> * (b * (sqrt 3) / 2) by C2; then
Im(a + b * zeta) = b * (sqrt 3) / 2 by COMPLEX1:12; then
b * (sqrt 3) / 2 = 0 by C2;
hence contradiction by C4,INT_2:28,IRRAT_1:1;
end;
hence thesis;
end;
theorem
not F_Complex is SplittingField of X^2+X+1
proof
set F = FAdj(F_Rat,{zeta});
now assume A: F_Complex is SplittingField of X^2+X+1;
X^2+X+1 splits_in F by Xsplit,FIELD_8:def 1; then
F_Complex == F by A,FIELD_8:def 1; then
F_Complex is Subfield of F by FIELD_7:def 2; then
D: the carrier of F_Complex c= the carrier of F by EC_PF_1:def 1;
F_Real is Subfield of F_Complex by FIELD_4:7; then
the carrier of F_Real c= the carrier of F_Complex by EC_PF_1:def 1;
hence contradiction by D,ns2;
end;
hence thesis;
end;
theorem
not F_Complex is SplittingField of X^3-1
proof
set F = FAdj(F_Rat,{zeta});
now assume A: F_Complex is SplittingField of X^3-1;
X^3-1 splits_in F by Ysplit,FIELD_8:def 1; then
F_Complex == F by A,FIELD_8:def 1; then
F_Complex is Subfield of F by FIELD_7:def 2; then
D: the carrier of F_Complex c= the carrier of F by EC_PF_1:def 1;
F_Real is Subfield of F_Complex by FIELD_4:7; then
the carrier of F_Real c= the carrier of F_Complex by EC_PF_1:def 1;
hence contradiction by D,ns2;
end;
hence thesis;
end;
begin :: A Splitting Field of X^3-2
theorem minpolzeta:
MinPoly(3-Root(2),F_Rat) = X^3-2 by LL2,FIELD_6:52;
theorem
deg(FAdj(F_Rat,{3-Root(2)}),F_Rat) = 3 by LL,minpolzeta,FIELD_6:67;
theorem bas3R:
{ 1, 3-Root(2), 3-Root(2)^2 }
is Basis of VecSp(FAdj(F_Rat,{3-Root(2)}),F_Rat)
proof
set F = F_Rat, M = { 1.F_Real, 3-Root(2), 3-Root(2)^2 };
B: now let o be object;
assume o in Base 3-Root(2); then
consider n being Element of NAT such that
B1: o = 3-Root(2)|^n & n < deg MinPoly(3-Root(2),F);
B2: n < 2 + 1 by LL,B1,LL2,FIELD_6:52;
n <= 2 implies n = 0 or ... or n = 2; then
per cases by B2,NAT_1:13;
suppose n = 0;
then o = 1_F_Real by B1,BINOM:8;
hence o in M by ENUMSET1:def 1;
end;
suppose n = 1;
then o = 3-Root(2) by B1,BINOM:8;
hence o in M by ENUMSET1:def 1;
end;
suppose n = 2;
then o = 3-Root(2)|^(1+1) by B1
.= 3-Root(2)|^1 * 3-Root(2)|^1 by BINOM:10
.= 3-Root(2)|^1 * 3-Root(2) by BINOM:8
.= 3-Root(2) * 3-Root(2) by BINOM:8
.= 3-Root(2)^2 by O_RING_1:def 1;
hence o in M by ENUMSET1:def 1;
end;
end;
now let o be object;
assume o in M; then
per cases by ENUMSET1:def 1;
suppose o = 1.F_Real;
then o = 1_F_Real .= 3-Root(2)|^0 by BINOM:8;
hence o in Base 3-Root(2) by LL,minpolzeta;
end;
suppose o = 3-Root(2);
then o = 3-Root(2)|^1 by BINOM:8;
hence o in Base 3-Root(2) by LL,minpolzeta;
end;
suppose o = 3-Root(2)^2;
then o = 3-Root(2) * 3-Root(2) by O_RING_1:def 1
.= 3-Root(2)|^1 * 3-Root(2) by BINOM:8
.= 3-Root(2)|^1 * 3-Root(2)|^1 by BINOM:8
.= 3-Root(2)|^(1+1) by BINOM:10;
hence o in Base 3-Root(2) by LL,minpolzeta;
end;
end;
then Base 3-Root(2) = M by B,TARSKI:2;
hence thesis by FIELD_6:65;
end;
theorem
Roots X^3-2 = {}
proof
Roots X^3-2 <> {} implies X^3-2 is with_roots;
hence thesis by LL,thirred;
end;
theorem
not X^3-2 splits_in F_Rat
proof
now assume X^3-2 splits_in F_Rat; then
consider a being non zero Element of F_Rat, q being Ppoly of F_Rat such that
A: X^3-2 = a * q by FIELD_4:def 5;
thus contradiction by A,thirred,LL;
end;
hence thesis;
end;
lemroots:
Roots(F_Complex,X^3-2) = {3-Root(2), 3-Root(2) * zeta, 3-Root(2) * zeta^2}
proof
set F = F_Complex, p = X^3-2;
set M = {3-Root(2), 3-Root(2) * zeta, 3-Root(2) * zeta^2};
I: F_Real is Subfield of F by FIELD_4:7;
reconsider r = 3-Root(2) as Element of F_Complex;
reconsider z = zeta as Complex;
H: Roots(F,p) = {a where a is Element of F : a is_a_root_of p,F}
by FIELD_4:def 4;
K: zeta^2 = zeta * zeta by O_RING_1:def 1
.= z^2 by SQUARE_1:def 1;
L: (z^2)|^3 = (z * z)|^3 by SQUARE_1:def 1
.= (z|^3) * (z|^3) by NEWTON:7
.= (z|^3)^2 by SQUARE_1:def 1
.= 1^2 by LZ23,lem3c
.= 1 * 1 by SQUARE_1:def 1;
now let o be object;
assume B: o in {r, r * zeta, r * zeta^2}; then
reconsider c = o as Element of F_Complex;
per cases by B,ENUMSET1:def 1;
suppose o = r; then
Ext_eval(p,c) = Ext_eval(p,3-Root(2)) by FIELD_7:14
.= 0.F by I,LL2,EC_PF_1:def 1;
then c is_a_root_of p,F by FIELD_4:def 2;
hence o in Roots(F,p) by H;
end;
suppose o = r * zeta; then
Ext_eval(p,c) = (r * zeta)|^3 - 2 by evalext2
.= ((3-Root 2) * z)|^3 - 2 by lem3c
.= (((3-Root 2)|^3) * (z|^3)) - 2 by lemcontr2
.= (2 * (z|^3)) - 2 by PREPOWER:def 2
.= (2 * 1) - 2 by LZ23,lem3c
.= 0.F_Real
.= 0.F by I,EC_PF_1:def 1;
then c is_a_root_of p,F by FIELD_4:def 2;
hence o in Roots(F,p) by H;
end;
suppose o = r * zeta^2; then
Ext_eval(p,c) = (r * zeta^2)|^3 - 2 by evalext2
.= ((3-Root 2) * z^2)|^3 - 2 by K,lem3c
.= (((3-Root 2)|^3) * ((z^2)|^3)) - 2 by lemcontr2
.= (2 * 1) - 2 by L,PREPOWER:def 2
.= 0.F_Real
.= 0.F by I,EC_PF_1:def 1;
then c is_a_root_of p,F by FIELD_4:def 2;
hence o in Roots(F,p) by H;
end;
end; then
B: M c= Roots(F_Complex,X^3-2);
the carrier of Polynom-Ring F_Rat c= the carrier of Polynom-Ring F
by FIELD_4:10; then
reconsider q = X^3-2 as Element of the carrier of Polynom-Ring F_Complex;
H: deg q = 3 by LL,FIELD_4:20; then
reconsider q as non constant Element of the carrier of Polynom-Ring F_Complex
by RING_4:def 4;
C: card M = 3
proof
zeta = (-1/2) + <i> * ((sqrt 3) / 2); then
Re(zeta) = (-1/2) & Im(zeta) = (sqrt 3) / 2 by COMPLEX1:12; then
D2: Im(zeta * zeta) = 2 * ((-1/2) * ((sqrt 3) / 2)) by COMPLEX1:16
.= -(sqrt 3) / 2;
D3: (sqrt 3) / 2 <> 0 by SQUARE_1:24;
D4: r <> 0.F & zeta <> 0.F;
C1: now assume r = r * zeta;
then r * 1.F = r * zeta;
hence contradiction by D4,VECTSP_2:8;
end;
C2: now assume r = r * zeta^2;
then r * 1.F = r * (zeta * zeta) by O_RING_1:def 1;
then zeta * zeta = 1.F by D4,VECTSP_2:8 .= 1r by COMPLFLD:def 1;
hence contradiction by D2,D3,COMPLEX1:6;
end;
C3: now assume r * zeta = r * zeta^2;
then zeta = zeta^2 by D4,VECTSP_2:8
.= zeta * zeta by O_RING_1:def 1;
then zeta * 1.F = zeta * zeta;
hence contradiction by D4,VECTSP_2:8;
end;
thus thesis by C1,C2,C3,CARD_2:58;
end;
D: card Roots(F_Complex,X^3-2) = 3
proof
F: card(Roots q) <= 3 by H,RING_5:22;
G: 3 <= card Roots(F_Complex,X^3-2) by C,B,NAT_1:43;
Roots(F_Complex,X^3-2) = Roots q by FIELD_7:13;
hence thesis by F,G,XXREAL_0:1;
end;
thus thesis by B,C,D,lemfinset;
end;
lemnotsplit:
not 3-Root(2) * zeta in REAL & not 3-Root(2) * zeta^2 in REAL
proof
zeta = (-1/2) + <i> * ((sqrt 3) / 2); then
D1: Re(zeta) = (-1/2) & Im(zeta) = (sqrt 3) / 2 by COMPLEX1:12; then
D2: Im(zeta * zeta) = 2 * ((-1/2) * ((sqrt 3) / 2)) by COMPLEX1:16
.= -(sqrt 3) / 2;
D3: (sqrt 3) / 2 <> 0 by SQUARE_1:24;
D4: zeta^2 = zeta * zeta by O_RING_1:def 1;
D5: Im 3-Root(2) = 0 & 3-Root(2) <> 0;
Im(3-Root(2) * zeta)
= (Re 3-Root(2)) * ((sqrt 3)/2) + Re zeta * 0 by D1,D5,COMPLEX1:9
.= 3-Root(2) * ((sqrt 3)/2) by COMPLEX1:def 1;
hence not 3-Root(2) * zeta in REAL by D5,D3;
Im(3-Root(2) * zeta^2)
= (Re 3-Root(2)) * (-(sqrt 3)/2) + Re zeta^2 * 0 by D2,D4,D5,COMPLEX1:9
.= 3-Root(2) * (-(sqrt 3)/2) by COMPLEX1:def 1;
hence thesis by D5,D3;
end;
theorem
Roots(FAdj(F_Rat,{3-Root(2)}),X^3-2) = {3-Root(2)}
proof
set F = FAdj(F_Rat,{3-Root(2)});
H0: F is Subfield of F_Complex &
the carrier of F c= the carrier of F_Real by FIELD_4:7,EC_PF_1:def 1;
H1: Roots(F,X^3-2) = {a where a is Element of F :
a is_a_root_of X^3-2,F} by FIELD_4:def 4;
H2: Roots(F_Complex,X^3-2) = {a where a is Element of F_Complex :
a is_a_root_of X^3-2,F_Complex} by FIELD_4:def 4;
H3: {3-Root(2)} is Subset of the carrier of F by FIELD_6:35;
3-Root(2) in {3-Root(2)} by TARSKI:def 1; then
reconsider z = 3-Root(2) as Element of F by H3;
A: now let o be object;
assume o in {3-Root(2)}; then
A1: o = 3-Root(2) by TARSKI:def 1;
Ext_eval(X^3-2,z) = Ext_eval(X^3-2,3-Root(2)) by FIELD_7:14
.= 0.F by LL2,FIELD_6:def 6; then
z is_a_root_of X^3-2,F by FIELD_4:def 2;
hence o in Roots(F,X^3-2) by A1,H1;
end;
now let o be object;
assume o in Roots(F,X^3-2); then
consider a being Element of F such that
B1: o = a & a is_a_root_of X^3-2,F by H1;
the carrier of F c= the carrier of F_Complex by H0,EC_PF_1:def 1; then
reconsider z = a as Element of F_Complex;
0.F = Ext_eval(X^3-2,a) by B1,FIELD_4:def 2
.= Ext_eval(X^3-2,z) by FIELD_6:11; then
0.F_Complex = Ext_eval(X^3-2,z) by H0,EC_PF_1:def 1; then
z is_a_root_of X^3-2,F_Complex by FIELD_4:def 2; then
B2: z in Roots(F_Complex,X^3-2) by H2;
now assume z <> 3-Root(2); then
per cases by B2,lemroots,ENUMSET1:def 1;
suppose z = 3-Root(2) * zeta;
hence contradiction by H0,lemnotsplit;
end;
suppose z = 3-Root(2) * zeta^2;
hence contradiction by H0,lemnotsplit;
end;
end;
hence o in {3-Root(2)} by B1,TARSKI:def 1;
end;
hence thesis by A,TARSKI:2;
end;
theorem
not X^3-2 splits_in FAdj(F_Rat,{3-Root(2)})
proof
set F = FAdj(F_Rat,{3-Root(2)});
B: the carrier of F c= the carrier of F_Real by EC_PF_1:def 1;
now assume X^3-2 splits_in F; then
Roots(F,X^3-2) = {3-Root(2), 3-Root(2) * zeta, 3-Root(2) * zeta^2}
by LLsplit,FIELD_8:29,lemroots; then
3-Root(2) * zeta in Roots(F,X^3-2) by ENUMSET1:def 1;
hence contradiction by B,lemnotsplit;
end;
hence thesis;
end;
theorem
Roots(F_Real,X^3-2) = {3-Root(2)}
proof
H0: F_Real is Subfield of F_Complex by FIELD_4:7;
H1: Roots(F_Real,X^3-2) = {a where a is Element of F_Real :
a is_a_root_of X^3-2,F_Real} by FIELD_4:def 4;
H2: Roots(F_Complex,X^3-2) = {a where a is Element of F_Complex :
a is_a_root_of X^3-2,F_Complex} by FIELD_4:def 4;
A: now let o be object;
assume o in {3-Root(2)}; then
A1: o = 3-Root(2) by TARSKI:def 1;
3-Root(2) is_a_root_of X^3-2,F_Real by LL2,FIELD_4:def 2;
hence o in Roots(F_Real,X^3-2) by A1,H1;
end;
now let o be object;
assume o in Roots(F_Real,X^3-2); then
consider a being Element of F_Real such that
B1: o = a & a is_a_root_of X^3-2,F_Real by H1;
the carrier of F_Real c= the carrier of F_Complex by H0,EC_PF_1:def 1; then
reconsider z = a as Element of F_Complex;
0.F_Real = Ext_eval(X^3-2,a) by B1,FIELD_4:def 2
.= Ext_eval(X^3-2,z) by FIELD_6:11; then
0.F_Complex = Ext_eval(X^3-2,z) by H0,EC_PF_1:def 1; then
z is_a_root_of X^3-2,F_Complex by FIELD_4:def 2; then
B2: z in Roots(F_Complex,X^3-2) by H2;
now assume z <> 3-Root(2); then
per cases by B2,lemroots,ENUMSET1:def 1;
suppose z = 3-Root(2) * zeta;
hence contradiction by lemnotsplit;
end;
suppose z = 3-Root(2) * zeta^2;
hence contradiction by lemnotsplit;
end;
end;
hence o in {3-Root(2)} by B1,TARSKI:def 1;
end;
hence thesis by A,TARSKI:2;
end;
theorem
not X^3-2 splits_in F_Real
proof
now assume X^3-2 splits_in F_Real; then
Roots(F_Real,X^3-2) = {3-Root(2), 3-Root(2) * zeta, 3-Root(2) * zeta^2}
by LLsplit,FIELD_8:29,lemroots; then
3-Root(2) * zeta in Roots(F_Real,X^3-2) by ENUMSET1:def 1;
hence contradiction by lemnotsplit;
end;
hence thesis;
end;
theorem
Roots(F_Complex,X^3-2) = {3-Root(2), 3-Root(2) * zeta, 3-Root(2) * zeta^2}
by lemroots;
theorem
X^3-2 = X-(3-CRoot(2)) * X-(3-CRoot(2) * zeta) * X-(3-CRoot(2) * zeta^2)
proof
set F = F_Complex;
set a = 3-CRoot(2) * zeta, b = 3-CRoot(2) * zeta^2, c = 3-CRoot(2);
A: X-a = rpoly(1,a) by FIELD_9:def 2 .= <%-a, 1.F%> by RING_5:10;
B: X-b = rpoly(1,b) by FIELD_9: def 2 .= <%-b, 1.F%> by RING_5:10;
C: X-c = rpoly(1,c) by FIELD_9: def 2 .= <%-c, 1.F%> by RING_5:10;
D: (X-a) * (X-b) = <%-a, 1.F%> *' <%-b, 1.F%> by A,B,POLYNOM3:def 10
.= <%(-a)*(-b),(1.F)*(-b)+(1.F)*(-a),(1.F)*(1.F)%> by FIELD_9:24
.= <%a*b,-b+-a,1.F%> by VECTSP_1:10;
H1: a * b
= (3-CRoot(2) * 3-CRoot(2)) * (zeta * zeta^2)
.= (3-CRoot(2) * 3-CRoot(2)) * zeta|^3 by lemI
.= 3-Root(2)|^1 * 3-Root(2) by LZ23,BINOM:8
.= 3-Root(2)|^1 * 3-Root(2)|^1 by BINOM:8
.= 3-Root(2)|^(1+1) by BINOM:10;
H4: 1 = 1.F by COMPLFLD:def 1,COMPLEX1:def 4; then
H5: -2 = -(1.F + 1.F);
1 = 1.F by COMPLEX1:def 4,COMPLFLD:def 1; then
H6: -1 = -1.F;
zeta^2 + zeta = zeta|^(1+1) + zeta by lemI; then
b + a
= 3-CRoot(2) * (-1.F + (-zeta + zeta)) by H6,LZ23
.= 3-CRoot(2) * (-1.F + 0.F)
.= -(3-CRoot(2) * 1.F) by VECTSP_1:8
.= -3-Root(2); then
H6: --3-Root(2) = -(b+a) .= -b + -a;
reconsider p1 = X-c as Polynomial of F;
p1 *' <%a*b,-b+-a,1.F%> = X^3-2
proof
J: 5 -' 1 = 5 - 1 by XREAL_0:def 2;
L: 4 -' 1 = 4 - 1 by XREAL_0:def 2; then
K: 2 -' 1 = 2 - 1 & 3 -' 1 = 3 - 1 & 3 -' 2 = 3 - 2 & 4 -' 1 = 3 &
4 -' 2 = 4 - 2 by XREAL_0:def 2;
the carrier of Polynom-Ring F_Rat c=
the carrier of Polynom-Ring F by FIELD_4:10; then
X^3-2 is Element of the carrier of Polynom-Ring F; then
reconsider q = X^3-2 as Polynomial of F;
set p2 = <%a*b,-b+-a,1.F%>;
A: dom(p1*'p2) = NAT by FUNCT_2:def 1 .= dom q by FUNCT_2:def 1;
now let o be object;
assume o in dom q;
then reconsider i = o as Element of NAT;
consider r being FinSequence of the carrier of F such that
B1: len r = i+1 & (p1*'p2).i = Sum r &
for k being Element of NAT st k in dom r
holds r.k = p1.(k-'1) * p2.(i+1-'k) by POLYNOM3:def 9;
i <= 3 implies i = 0 or ... or i = 3; then
per cases;
suppose C1: i = 0;
then B2: r = <*r.1*> by B1,FINSEQ_1:40;
then dom r = {1} by FINSEQ_1:2,FINSEQ_1:38;
then 1 in dom r by TARSKI:def 1;
then r.1 = p1.(1-'1) * p2.(0+1-'1) by C1,B1
.= p1.(1-'1) * p2.0 by NAT_2:8
.= p1.0 * p2.0 by NAT_2:8
.= p1.0 * (a * b) by FIELD_9:16
.= (-c) * (a * b) by C,POLYNOM5:38
.= -(3-Root(2) * 3-Root(2)|^2) by H1
.= -(3-Root(2)|^2 * 3-Root(2)|^1) by BINOM:8
.= -(3-Root(2)|^(2+1)) by BINOM:10
.= -(1.F + 1.F) by H4,R32;
hence (p1*'p2).o = q.o by H5,C1,LL0,B1,B2,RLVECT_1:44;
end;
suppose C1: i = 1;
then B3: r = <*r.1,r.2*> by B1,FINSEQ_1:44;
B4: dom r = {1,2} by B1,C1,FINSEQ_1:def 3,FINSEQ_1:2;
then 1 in dom r by TARSKI:def 2;
then B5: r.1 = p1.(1-'1) * p2.(1+1-'1) by C1,B1
.= p1.0 * p2.1 by K,NAT_2:8
.= (-c) * p2.1 by C,POLYNOM5:38
.= (-c) * (-b+-a) by FIELD_9:16;
2 in dom r by B4,TARSKI:def 2;
then r.2 = p1.(2-'1) * p2.(1+1-'2) by C1,B1
.= p1.1 * p2.0 by K,NAT_2:8
.= 1.F * p2.0 by C,POLYNOM5:38
.= 1.F * (a * b) by FIELD_9:16;
then Sum r = (-c) * (-b+-a) + (a * b) by B3,B5,RLVECT_1:45
.= -(3-Root(2) * 3-Root(2)) + 3-Root(2)|^2 by H6,H1
.= -(3-Root(2)|^1 * 3-Root(2)) + 3-Root(2)|^2 by BINOM:8
.= -(3-Root(2)|^1 * 3-Root(2)|^1) + 3-Root(2)|^2 by BINOM:8
.= -3-Root(2)|^(1+1) + 3-Root(2)|^2 by BINOM:10
.= 0;
hence (p1*'p2).o = q.o by B1,C1,LL0;
end;
suppose C1: i = 2;
then B3: r = <*r.1,r.2,r.3*> by B1,FINSEQ_1:45;
B4: dom r = Seg 3 by B1,C1,FINSEQ_1:def 3
.= Seg 2 \/ {2+1} by FINSEQ_1:9
.= {1,2,3} by FINSEQ_1:2,ENUMSET1:3;
then 1 in dom r by ENUMSET1:def 1;
then B5: r.1 = p1.(1-'1) * p2.(2+1-'1) by C1,B1
.= p1.0 * p2.2 by K,NAT_2:8
.= p1.0 * 1.F by FIELD_9:16
.= -c by C,POLYNOM5:38;
2 in dom r by B4,ENUMSET1:def 1;
then B6: r.2 = p1.1 * p2.1 by K,C1,B1
.= 1.F * p2.1 by C,POLYNOM5:38
.= -b+-a by FIELD_9:16;
3 in dom r by B4,ENUMSET1:def 1;
then r.3 = p1.2 * p2.(2+1-'3) by K,C1,B1
.= 0.F * p2.(2+1-'3) by C,POLYNOM5:38;
then Sum r = -c + (-b + -a) + 0.F by B3,B5,B6,RLVECT_1:46
.= 0 by H6;
hence (p1*'p2).o = q.o by B1,C1,LL0;
end;
suppose C1: i = 3;
then B3: r = <*r.1,r.2,r.3,r.4*> by B1,FINSEQ_4:76;
B4: dom r = Seg 4 by B1,C1,FINSEQ_1:def 3
.= Seg 3 \/ {3+1} by FINSEQ_1:9
.= (Seg 2 \/ {2+1}) \/ {4} by FINSEQ_1:9
.= {1,2,3} \/ {4} by FINSEQ_1:2,ENUMSET1:3
.= {1,2,3,4} by ENUMSET1:6;
then 1 in dom r by ENUMSET1:def 2;
then B5: r.1 = p1.(1-'1) * p2.(3+1-'1) by C1,B1
.= p1.0 * p2.3 by L,NAT_2:8
.= p1.0 * 0.F by FIELD_9:16;
2 in dom r by B4,ENUMSET1:def 2;
then B6: r.2 = p1.1 * p2.2 by K,C1,B1
.= p1.1 * 1.F by FIELD_9:16
.= 1.F by C,POLYNOM5:38;
3 in dom r by B4,ENUMSET1:def 2;
then B7: r.3 = p1.2 * p2.(3+1-'3) by K,C1,B1
.= 0.F * p2.(3+1-'3) by C,POLYNOM5:38;
4 in dom r by B4,ENUMSET1:def 2;
then r.4 = p1.3 * p2.(3+1-'4) by L,C1,B1
.= 0.F * p2.(3+1-'4) by C,POLYNOM5:38;
then r = <*(0.F),(1.F),(0.F)*> ^ <*(0.F)*> by B3,B5,B6,B7,FINSEQ_4:74;
then Sum r
= Sum <*(0.F),(1.F),(0.F)*> + Sum <*(0.F)*> by RLVECT_1:41
.= Sum <*(0.F),(1.F),(0.F)*> + 0.F by RLVECT_1:44
.= 0.F + 1.F + 0.F by RLVECT_1:46
.= 1 by COMPLFLD:def 1,COMPLEX1:def 4;
hence (p1*'p2).o = q.o by B1,C1,LL0;
end;
suppose C11: i > 3;
reconsider q1 = q as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
CC: deg q1 = 3 by LL,FIELD_4:20;
C0: deg q = len q - 1 by HURWITZ:def 2;
C1: i >= 3 + 1 by C11,NAT_1:13;
then E: q.i = 0.F by CC,C0,ALGSEQ_1:8;
1.F <> 0.F; then
C2: len p1 = 2 & deg p2 = 2 by C,POLYNOM5:40,FIELD_9:18;
C3: deg p2 = len p2 - 1 by HURWITZ:def 2;
len(p1*'p2) <= len p1 + len p2 -' 1 by leng;
hence (p1*'p2).o = q.o by J,E,C1,C3,C2,XXREAL_0:2,ALGSEQ_1:8;
end;
end;
hence thesis by A;
end;
then X-c * ((X-a) * (X-b)) = X^3-2 by D,POLYNOM3:def 10;
hence thesis by GROUP_1:def 3;
end;
theorem 32split:
FAdj(F_Rat,{3-CRoot(2), zeta}) is SplittingField of X^3-2
proof
set F = FAdj(F_Rat,{3-CRoot(2), zeta});
Roots(F_Complex,X^3-2) c= the carrier of F
proof
A1: {3-CRoot(2),zeta} is Subset of F by FIELD_6:35;
3-Root(2) in {3-CRoot(2), zeta} &
zeta in {3-CRoot(2), zeta} by TARSKI:def 2; then
reconsider a = 3-Root(2), b = zeta as Element of F by A1;
A3: F is Subring of F_Complex by FIELD_4:def 1;
A5: zeta * zeta = b * b by A3,FIELD_6:16;
now let o be object;
assume o in Roots(F_Complex,X^3-2); then
per cases by lemroots,ENUMSET1:def 1;
suppose o = 3-Root(2);
then o = a;
hence o in the carrier of F;
end;
suppose o = 3-Root(2) * zeta;
then o = 3-CRoot(2) * zeta
.= a * b by A3,FIELD_6:16;
hence o in the carrier of F;
end;
suppose o = 3-Root(2) * zeta^2;
then o = 3-CRoot(2) * (zeta * zeta) by O_RING_1:def 1
.= a * (b * b) by A3,A5,FIELD_6:16;
hence o in the carrier of F;
end;
end;
hence thesis;
end; then
B: X^3-2 splits_in F by LLsplit,FIELD_8:27;
now let E be FieldExtension of F_Rat;
assume C: X^3-2 splits_in E & E is Subfield of F; then
E: E is Subfield of F_Complex by EC_PF_1:5; then
F: E is Subring of F_Complex by FIELD_5:12;
D: F_Rat is Subfield of E by FIELD_4:7;
{3-CRoot(2),zeta} is Subset of E
proof
F_Complex is E-extending by E,FIELD_4:7; then
A1: Roots(F_Complex,X^3-2) c= the carrier of E by LLsplit,C,FIELD_8:27;
3-Root(2) in Roots(F_Complex,X^3-2) &
3-CRoot(2) * zeta in Roots(F_Complex,X^3-2)
by lemroots,ENUMSET1:def 1; then
reconsider a = 3-Root(2),
b = 3-CRoot(2) * zeta as Element of E by A1;
A3: 3-CRoot(2) is non zero;
a" = 3-CRoot(2)" by E,FIELD_6:18; then
A4: a" * b = 3-CRoot(2)" * (3-CRoot(2) * zeta) by F,FIELD_6:16
.= (3-CRoot(2)" * 3-CRoot(2)) * zeta
.= 1.F_Complex * zeta by A3,VECTSP_2:9;
now let o be object;
assume o in {3-CRoot(2),zeta}; then
per cases by TARSKI:def 2;
suppose o = 3-CRoot(2); then
o = a;
hence o in the carrier of E;
end;
suppose o = zeta;
hence o in the carrier of E by A4;
end;
end;
then {3-CRoot(2),zeta} c= the carrier of E;
hence thesis;
end;
then F is Subfield of E by D,E,FIELD_6:37;
hence E == F by C,FIELD_7:def 2;
end;
hence F is SplittingField of X^3-2 by B,FIELD_8:def 1;
end;
registration
cluster F_Complex -> FAdj(F_Rat,{3-CRoot(2)})-extending;
coherence;
cluster FAdj(F_Rat,{3-CRoot(2),zeta}) -> FAdj(F_Rat,{3-CRoot(2)})-extending;
coherence;
end;
registration
cluster zeta -> FAdj(F_Rat,{3-CRoot(2)})-algebraic;
coherence
proof
set K = FAdj(F_Rat,{3-CRoot(2)});
the carrier of Polynom-Ring F_Rat c=
the carrier of Polynom-Ring K by FIELD_4:10; then
reconsider p = X^2+X+1 as Element of the carrier of Polynom-Ring K;
deg p = 2 by LL,FIELD_4:20; then
reconsider p as non constant Element of the carrier of Polynom-Ring K
by RING_4:def 4;
H: Roots(F_Complex,X^2+X+1) =
{a where a is Element of F_Complex : a is_a_root_of X^2+X+1,F_Complex}
by FIELD_4:def 4;
zeta in Roots(F_Complex,X^2+X+1) by rootz,TARSKI:def 2;
then consider a being Element of F_Complex such that
I: a = zeta & a is_a_root_of X^2+X+1,F_Complex by H;
0.F_Complex = Ext_eval(X^2+X+1,zeta) by I,FIELD_4:def 2
.= Ext_eval(p,zeta) by FIELD_8:6;
hence thesis by FIELD_6:43;
end;
end;
theorem mmm:
MinPoly(zeta,FAdj(F_Rat,{3-CRoot(2)})) = X^2+X+1
proof
set K = FAdj(F_Rat,{3-CRoot(2)});
K = FAdj(F_Rat,{3-Root(2)}) by mmk; then
K: the carrier of K c= the carrier of F_Real by EC_PF_1:def 1;
the carrier of Polynom-Ring F_Rat c=
the carrier of Polynom-Ring K by FIELD_4:10; then
reconsider p = X^2+X+1 as Element of the carrier of Polynom-Ring K;
M: deg p = 2 by LL,FIELD_4:20; then
reconsider p as non constant Element of the carrier of Polynom-Ring K
by RING_4:def 4;
L: F_Rat is Subfield of K by FIELD_4:7;
LC p = LC X^2+X+1 by FIELD_8:5
.= 1.F_Rat by RATFUNC1:def 7
.= 1.K by L,EC_PF_1:def 1; then
A: p is monic by RATFUNC1:def 7;
B: now assume p is reducible;
then p is with_roots by M,thirred2; then
consider a being Element of K such that
C: a is_a_root_of p by POLYNOM5:def 8;
Y: Roots p c= Roots(F_Complex,p) by FIELD_4:28;
Z: Roots(F_Complex,p) = {zeta, zeta^2} by rootz,mmo;
a in Roots p by C,POLYNOM5:def 10; then
per cases by Z,Y,TARSKI:def 2;
suppose a = zeta;
hence contradiction by lemlem,K;
end;
suppose a = zeta^2;
hence contradiction by lemlem,K;
end;
end;
H: Roots(F_Complex,X^2+X+1) =
{a where a is Element of F_Complex : a is_a_root_of X^2+X+1,F_Complex}
by FIELD_4:def 4;
zeta in Roots(F_Complex,X^2+X+1) by rootz,TARSKI:def 2;
then consider a being Element of F_Complex such that
I: a = zeta & a is_a_root_of X^2+X+1,F_Complex by H;
0.F_Complex = Ext_eval(X^2+X+1,zeta) by I,FIELD_4:def 2
.= Ext_eval(p,zeta) by FIELD_8:6;
hence thesis by A,B,FIELD_6:52;
end;
theorem mml:
deg(FAdj(F_Rat,{3-CRoot(2),zeta}), FAdj(F_Rat,{3-CRoot(2)})) = 2
proof
set K = FAdj(F_Rat,{3-CRoot(2)});
the carrier of Polynom-Ring F_Rat c=
the carrier of Polynom-Ring K by FIELD_4:10; then
reconsider p = X^2+X+1 as Element of the carrier of Polynom-Ring K;
A: FAdj(F_Rat,{3-CRoot(2), zeta})
= FAdj(F_Rat,{3-CRoot(2)}\/{zeta}) by ENUMSET1:1
.= FAdj(K,{zeta}) by FIELD_7:35;
deg p = 2 by LL,FIELD_4:20;
hence thesis by A,mmm,FIELD_6:67;
end;
theorem baszeta:
{ 1, zeta } is Basis of
VecSp(FAdj(F_Rat,{3-CRoot(2),zeta}), FAdj(F_Rat,{3-CRoot(2)}))
proof
set F = FAdj(F_Rat,{3-CRoot(2), zeta}), K = FAdj(F_Rat,{3-CRoot(2)});
C: FAdj(F_Rat,{3-CRoot(2), zeta})
= FAdj(F_Rat,{3-CRoot(2)}\/{zeta}) by ENUMSET1:1
.= FAdj(K,{zeta}) by FIELD_7:35;
reconsider z = zeta as K-algebraic Element of F_Complex;
H: deg MinPoly(z,K) = 2 by mmm,LL,FIELD_4:20;
B: now let o be object;
assume o in Base z; then
consider n being Element of NAT such that
B1: o = z|^n & n < deg MinPoly(z,K);
n < 1 + 1 by mmm,LL,FIELD_4:20,B1; then
n <= 1 by NAT_1:13; then
per cases by NAT_1:25;
suppose n = 0;
then o = 1_F_Complex by B1,BINOM:8;
then o = 1 by COMPLEX1:def 4,COMPLFLD:def 1;
hence o in {1, z} by TARSKI:def 2;
end;
suppose n = 1;
then o = z by B1,BINOM:8;
hence o in {1, z} by TARSKI:def 2;
end;
end;
now let o be object;
assume o in {1, z}; then
per cases by TARSKI:def 2;
suppose o = 1;
then o = 1_F_Complex by COMPLEX1:def 4,COMPLFLD:def 1
.= z|^0 by BINOM:8;
hence o in Base z by H;
end;
suppose o = z;
then o = z|^1 by BINOM:8;
hence o in Base z by H;
end;
end; then
Base z = {1, z} by B,TARSKI:2;
hence thesis by C,FIELD_6:65;
end;
theorem grad6:
deg(FAdj(F_Rat,{3-CRoot(2),zeta}), F_Rat) = 6
proof
set F = FAdj(F_Rat,{3-CRoot(2), zeta}), K = FAdj(F_Rat,{3-CRoot(2)});
A: deg(FAdj(F_Rat,{3-Root(2)}),F_Rat) = 3 by LL,minpolzeta,FIELD_6:67;
B: K = FAdj(F_Rat,{3-Root(2)}) by mmk;
FAdj(F_Rat,{3-CRoot(2), zeta})
= FAdj(F_Rat,{3-CRoot(2)}\/{zeta}) by ENUMSET1:1
.= FAdj(K,{zeta}) by FIELD_7:35; then
deg(F,F_Rat) = deg(F,K) * deg(K,F_Rat) by FIELD_7:30
.= 6 by A,B,mml;
hence thesis;
end;
theorem
{ 1, 3-Root(2), 3-Root(2)^2, zeta, 3-Root(2) * zeta, 3-Root(2)^2 * zeta }
is Basis of VecSp(FAdj(F_Rat,{3-CRoot(2),zeta}),F_Rat)
proof
set F = FAdj(F_Rat,{3-CRoot(2), zeta}), K = FAdj(F_Rat,{3-CRoot(2)});
B: K = FAdj(F_Rat,{3-Root(2)}) by mmk;
C: FAdj(F_Rat,{3-CRoot(2), zeta})
= FAdj(F_Rat,{3-CRoot(2)}\/{zeta}) by ENUMSET1:1
.= FAdj(K,{zeta}) by FIELD_7:35;
set M = {1,3-Root(2),3-Root(2)^2,zeta,3-Root(2)*zeta,3-Root(2)^2*zeta};
reconsider B1 = {1,3-Root(2),3-Root(2)^2} as Basis of VecSp(K,F_Rat)
by B,bas3R;
reconsider B2 = {1,zeta} as Basis of VecSp(F,K) by baszeta;
E: Base(B1,B2) = {a*b where a,b is Element of F : a in B1 & b in B2}
by FIELD_7:def 7;
Base(B1,B2) = M
proof
E1: now let o be object;
assume o in M; then
per cases by ENUMSET1:def 4;
suppose E0: o = 1;
set a = 1.F, b = 1.F;
E1: a = 1.F_Complex & b = 1.F_Complex by EC_PF_1:def 1; then
a = 1 & b = 1 by COMPLEX1:def 4,COMPLFLD:def 1; then
E2: a in B1 & b in B2 by ENUMSET1:def 1,TARSKI:def 2;
a * b = 1 by E1,COMPLEX1:def 4,COMPLFLD:def 1;
hence o in Base(B1,B2) by E,E2,E0;
end;
suppose E0: o = 3-Root(2);
{3-CRoot(2), zeta} is Subset of F &
3-Root(2) in {3-CRoot(2), zeta} by TARSKI:def 2,FIELD_6:35; then
reconsider a = 3-Root(2) as Element of F;
set b = 1.F;
b = 1.F_Complex by EC_PF_1:def 1
.= 1 by COMPLEX1:def 4,COMPLFLD:def 1; then
E1: a in B1 & b in B2 by ENUMSET1:def 1,TARSKI:def 2;
a * b = 3-Root(2);
hence o in Base(B1,B2) by E,E1,E0;
end;
suppose E0: o = 3-Root(2)^2;
{3-CRoot(2), zeta} is Subset of F &
3-CRoot(2) in {3-CRoot(2), zeta} by TARSKI:def 2,FIELD_6:35; then
reconsider c = 3-CRoot(2) as Element of F;
F is Subring of F_Complex by FIELD_5:12; then
A: 3-CRoot(2) * 3-CRoot(2) = c * c by FIELD_6:16;
3-Root(2)^2 = 3-Root(2) * 3-Root(2) by O_RING_1:def 1
.= 3-CRoot(2) * 3-CRoot(2); then
reconsider a = 3-Root(2)^2 as Element of F by A;
set b = 1.F;
b = 1.F_Complex by EC_PF_1:def 1
.= 1 by COMPLEX1:def 4,COMPLFLD:def 1; then
E1: a in B1 & b in B2 by ENUMSET1:def 1,TARSKI:def 2;
a * b = 3-Root(2)^2;
hence o in Base(B1,B2) by E,E1,E0;
end;
suppose E0: o = zeta;
{3-CRoot(2), zeta} is Subset of F &
zeta in {3-CRoot(2), zeta} by TARSKI:def 2,FIELD_6:35; then
reconsider b = zeta as Element of F;
set a = 1.F;
a = 1.F_Complex by EC_PF_1:def 1
.= 1 by COMPLEX1:def 4,COMPLFLD:def 1; then
E1: a in B1 & b in B2 by ENUMSET1:def 1,TARSKI:def 2;
a * b = zeta;
hence o in Base(B1,B2) by E,E1,E0;
end;
suppose E0: o = 3-Root(2)*zeta;
{3-CRoot(2), zeta} is Subset of F &
zeta in {3-CRoot(2), zeta} &
3-Root(2) in {3-CRoot(2), zeta} by TARSKI:def 2,FIELD_6:35; then
reconsider a = 3-Root(2), b = zeta as Element of F;
E1: a in B1 & b in B2 by ENUMSET1:def 1,TARSKI:def 2;
F is Subring of F_Complex by FIELD_5:12; then
a * b = 3-CRoot(2) * zeta by FIELD_6:16;
hence o in Base(B1,B2) by E,E1,E0;
end;
suppose E0: o = 3-Root(2)^2*zeta;
A: {3-CRoot(2), zeta} is Subset of F &
zeta in {3-CRoot(2), zeta} &
3-Root(2) in {3-CRoot(2), zeta} by TARSKI:def 2,FIELD_6:35; then
reconsider c = 3-CRoot(2) as Element of F;
F is Subring of F_Complex by FIELD_5:12; then
B: 3-CRoot(2) * 3-CRoot(2) = c * c by FIELD_6:16;
C: 3-Root(2)^2 = 3-Root(2) * 3-Root(2) by O_RING_1:def 1
.= 3-CRoot(2) * 3-CRoot(2); then
reconsider a = 3-Root(2)^2, b = zeta as Element of F by A,B;
E1: a in B1 & b in B2 by ENUMSET1:def 1,TARSKI:def 2;
F is Subring of F_Complex by FIELD_5:12; then
a * b = (3-CRoot(2) * 3-CRoot(2)) * zeta by C,FIELD_6:16;
hence o in Base(B1,B2) by C,E,E1,E0;
end;
end;
now let o be object;
assume o in Base(B1,B2); then
consider a,b being Element of F such that
E0: o = a * b & a in B1 & b in B2 by E;
per cases by E0,ENUMSET1:def 1;
suppose E1: a = 1;
per cases by E0,TARSKI:def 2;
suppose b = 1; then
E2: a = 1.F_Complex & b = 1.F_Complex
by E1,COMPLEX1:def 4,COMPLFLD:def 1;
F is Subring of F_Complex by FIELD_5:12; then
a * b = 1.F_Complex * 1.F_Complex by E2,FIELD_6:16
.= 1 by COMPLEX1:def 4,COMPLFLD:def 1;
hence o in M by E0,ENUMSET1:def 4;
end;
suppose E2: b = zeta;
E3: a = 1.F_Complex by E1,COMPLEX1:def 4,COMPLFLD:def 1;
F is Subring of F_Complex by FIELD_5:12; then
a * b = 1.F_Complex * zeta by E2,E3,FIELD_6:16 .= zeta;
hence o in M by E0,ENUMSET1:def 4;
end;
end;
suppose E1: a = 3-Root(2);
per cases by E0,TARSKI:def 2;
suppose b = 1; then
E2: b = 1.F_Complex by COMPLEX1:def 4,COMPLFLD:def 1;
F is Subring of F_Complex by FIELD_5:12; then
a * b = 3-CRoot(2) * 1.F_Complex by E1,E2,FIELD_6:16
.= 3-Root(2);
hence o in M by E0,ENUMSET1:def 4;
end;
suppose E2: b = zeta;
F is Subring of F_Complex by FIELD_5:12; then
a * b = 3-CRoot(2) * zeta by E1,E2,FIELD_6:16;
hence o in M by E0,ENUMSET1:def 4;
end;
end;
suppose E1: a = 3-Root(2)^2;
per cases by E0,TARSKI:def 2;
suppose b = 1; then
E2: b = 1.F_Complex by COMPLEX1:def 4,COMPLFLD:def 1;
E3: F is Subring of F_Complex by FIELD_5:12;
E4: 3-Root(2)^2 = 3-Root(2) * 3-Root(2) by O_RING_1:def 1
.= 3-CRoot(2) * 3-CRoot(2); then
a * b = (3-CRoot(2) * 3-CRoot(2)) * 1.F_Complex
by E1,E2,E3,FIELD_6:16
.= 3-Root(2)^2 by E4;
hence o in M by E0,ENUMSET1:def 4;
end;
suppose E2: b = zeta;
E3: F is Subring of F_Complex by FIELD_5:12;
E4: 3-Root(2)^2 = 3-Root(2) * 3-Root(2) by O_RING_1:def 1
.= 3-CRoot(2) * 3-CRoot(2); then
a * b = (3-CRoot(2) * 3-CRoot(2)) * zeta by E1,E2,E3,FIELD_6:16
.= 3-Root(2)^2 * zeta by E4;
hence o in M by E0,ENUMSET1:def 4;
end;
end;
end;
hence thesis by E1,TARSKI:2;
end;
hence thesis by C,FIELD_7:29;
end;
registration
cluster F_Complex -> FAdj(F_Rat,{2-CRoot(2)})-extending;
coherence by FIELD_4:7;
cluster F_Complex -> FAdj(F_Rat,{2-CRoot(2),zeta})-extending;
coherence by FIELD_4:7;
cluster FAdj(F_Rat,{2-CRoot(2),zeta}) -> FAdj(F_Rat,{2-CRoot(2)})-extending;
coherence;
cluster FAdj(F_Rat,{3-CRoot(2),zeta,2-CRoot(2)}) ->
FAdj(F_Rat,{2-CRoot(2),zeta})-extending;
coherence;
end;
registration
cluster zeta -> FAdj(F_Rat,{2-CRoot(2)})-algebraic;
coherence
proof
set K = FAdj(F_Rat,{2-CRoot(2)});
the carrier of Polynom-Ring F_Rat c=
the carrier of Polynom-Ring K by FIELD_4:10; then
reconsider p = X^2+X+1 as Element of the carrier of Polynom-Ring K;
deg p = 2 by LL,FIELD_4:20; then
reconsider p as non constant Element of the carrier of Polynom-Ring K
by RING_4:def 4;
H: Roots(F_Complex,X^2+X+1) =
{a where a is Element of F_Complex : a is_a_root_of X^2+X+1,F_Complex}
by FIELD_4:def 4;
zeta in Roots(F_Complex,X^2+X+1) by rootz,TARSKI:def 2;
then consider a being Element of F_Complex such that
I: a = zeta & a is_a_root_of X^2+X+1,F_Complex by H;
0.F_Complex = Ext_eval(X^2+X+1,zeta) by I,FIELD_4:def 2
.= Ext_eval(p,zeta) by FIELD_8:6;
hence thesis by FIELD_6:43;
end;
cluster 3-CRoot(2) -> FAdj(F_Rat,{2-CRoot(2),zeta})-algebraic;
coherence
proof
set K = FAdj(F_Rat,{2-CRoot(2),zeta});
the carrier of Polynom-Ring F_Rat c=
the carrier of Polynom-Ring K by FIELD_4:10; then
reconsider p = X^3-2 as Element of the carrier of Polynom-Ring K;
deg p = 3 by LL,FIELD_4:20; then
reconsider p as non constant Element of the carrier of Polynom-Ring K
by RING_4:def 4;
now let r be Element of F_Real, a be Element of F_Complex;
assume A: a = r;
B: a|^3 = a|^(2+1)
.= a|^2 * a|^1 by BINOM:10
.= a|^(1+1) * a by BINOM:8
.= (a|^1 * a|^1) * a by BINOM:10
.= (a * a|^1) * a by BINOM:8
.= (a * a) * a by BINOM:8;
r|^3 = r|^(2+1)
.= r|^2 * r|^1 by BINOM:10
.= r|^(1+1) * r by BINOM:8
.= (r|^1 * r|^1) * r by BINOM:10
.= (r * r|^1) * r by BINOM:8
.= (r * r) * r by BINOM:8;
hence a|^3 = r|^3 by A,B;
end; then
H: 3-CRoot(2)|^3 = 2 by R32;
Ext_eval(p,3-CRoot(2))
= Ext_eval(X^3-2,3-CRoot(2)) by FIELD_7:15
.= 3-CRoot(2)|^3 - 2 by evalext2
.= 0.F_Complex by H,COMPLFLD:def 1;
hence thesis by FIELD_6:43;
end;
end;
registration
cluster FAdj(F_Rat,{3-CRoot(2),zeta,2-CRoot(2)}) ->
FAdj(F_Rat,{2-CRoot(2),zeta})-finite;
coherence
proof
FAdj(F_Rat,{3-CRoot(2),zeta,2-CRoot(2)})
= FAdj(F_Rat,{zeta,2-CRoot(2),3-CRoot(2)}) by ENUMSET1:59
.= FAdj(F_Rat,{zeta,2-CRoot(2)}\/{3-CRoot(2)}) by ENUMSET1:3
.= FAdj(FAdj(F_Rat,{2-CRoot(2),zeta}),{3-CRoot(2)}) by FIELD_7:34;
hence thesis;
end;
end;
theorem mmmz:
MinPoly(zeta,FAdj(F_Rat,{2-CRoot(2)})) = X^2+X+1
proof
set K = FAdj(F_Rat,{2-CRoot(2)});
K = FAdj(F_Rat,{2-Root(2)}) by mmk; then
K: the carrier of K c= the carrier of F_Real by EC_PF_1:def 1;
the carrier of Polynom-Ring F_Rat c=
the carrier of Polynom-Ring K by FIELD_4:10; then
reconsider p = X^2+X+1 as Element of the carrier of Polynom-Ring K;
M: deg p = 2 by LL,FIELD_4:20; then
reconsider p as non constant Element of the carrier of Polynom-Ring K
by RING_4:def 4;
L: F_Rat is Subfield of K by FIELD_4:7;
LC p = LC X^2+X+1 by FIELD_8:5
.= 1.F_Rat by RATFUNC1:def 7
.= 1.K by L,EC_PF_1:def 1; then
A: p is monic by RATFUNC1:def 7;
B: now assume p is reducible;
then p is with_roots by M,thirred2; then
consider a being Element of K such that
C: a is_a_root_of p by POLYNOM5:def 8;
Y: Roots p c= Roots(F_Complex,p) by FIELD_4:28;
Z: Roots(F_Complex,p) = {zeta, zeta^2} by rootz,mmo;
a in Roots p by C,POLYNOM5:def 10; then
per cases by Z,Y,TARSKI:def 2;
suppose a = zeta;
hence contradiction by lemlem,K;
end;
suppose a = zeta^2;
hence contradiction by lemlem,K;
end;
end;
H: Roots(F_Complex,X^2+X+1) =
{a where a is Element of F_Complex : a is_a_root_of X^2+X+1,F_Complex}
by FIELD_4:def 4;
zeta in Roots(F_Complex,X^2+X+1) by rootz,TARSKI:def 2;
then consider a being Element of F_Complex such that
I: a = zeta & a is_a_root_of X^2+X+1,F_Complex by H;
0.F_Complex = Ext_eval(X^2+X+1,zeta) by I,FIELD_4:def 2
.= Ext_eval(p,zeta) by FIELD_8:6;
hence thesis by A,B,FIELD_6:52;
end;
theorem mmmza:
deg(FAdj(F_Rat,{2-CRoot(2), zeta}), FAdj(F_Rat,{2-CRoot(2)})) = 2
proof
set K = FAdj(F_Rat,{2-CRoot(2)});
the carrier of Polynom-Ring F_Rat c=
the carrier of Polynom-Ring K by FIELD_4:10; then
reconsider p = X^2+X+1 as Element of the carrier of Polynom-Ring K;
A: FAdj(F_Rat,{2-CRoot(2), zeta})
= FAdj(F_Rat,{2-CRoot(2)}\/{zeta}) by ENUMSET1:1
.= FAdj(K,{zeta}) by FIELD_7:35;
deg p = 2 by LL,FIELD_4:20;
hence thesis by A,mmmz,FIELD_6:67;
end;
theorem grad4:
deg(FAdj(F_Rat,{2-CRoot(2),zeta}),F_Rat) = 4
proof
set F = FAdj(F_Rat,{2-CRoot(2), zeta}), K = FAdj(F_Rat,{2-CRoot(2)});
A: X^2-2 = MinPoly(2-CRoot(2),F_Rat) by mp,mmv;
F = FAdj(F_Rat,{2-CRoot(2)}\/{zeta}) by ENUMSET1:1
.= FAdj(K,{zeta}) by FIELD_7:35;
hence deg(F,F_Rat) = deg(F,K) * deg(K,F_Rat) by FIELD_7:30
.= 2 * 2 by A,LL,FIELD_6:67,mmmza
.= 4;
end;
theorem ff:
not sqrt 2 is Element of FAdj(F_Rat,{3-CRoot(2),zeta})
proof
set F = FAdj(F_Rat,{3-CRoot(2),zeta}), K = FAdj(F_Rat,{2-CRoot(2),zeta});
now assume sqrt 2 is Element of FAdj(F_Rat,{3-CRoot(2),zeta}); then
reconsider a = sqrt 2 as Element of F;
{a} is Subset of F; then
FAdj(F_Rat,{3-CRoot(2),zeta})
= FAdj(F,{2-CRoot(2)}) by FIELD_7:2,FIELD_7:3
.= FAdj(F_Rat,{3-CRoot(2),zeta}\/{2-CRoot(2)}) by FIELD_7:34
.= FAdj(F_Rat,{3-CRoot(2),zeta,2-CRoot(2)}) by ENUMSET1:3; then
C: 6 = deg(FAdj(F_Rat,{3-CRoot(2),zeta,2-CRoot(2)}),K) * 4
by grad4,grad6,FIELD_7:30;
now let n be Integer, k be Nat;
assume C3: k <> 0 & 3/2 = n/k;
then (3/2) * k = (n/k) * k .= n * k* k" .= n by C3,XCMPLX_1:203;
then C4: 3 * k = n * 2;
C5: 3 = 2 * 1 + 1;
now assume 2 > k;
then k is trivial by NAT_2:29;
then per cases by NAT_2:def 1;
suppose k = 0;
hence contradiction by C3;
end;
suppose k = 1;
hence contradiction by C5,C4;
end;
end;
hence 2 <= k;
end; then
denominator(3/2) = 2 by RAT_1:def 3;
hence contradiction by C,RAT_1:21;
end;
hence thesis;
end;
theorem
not F_Complex is SplittingField of X^3-2
proof
set F = FAdj(F_Rat,{3-CRoot(2), zeta});
now assume A: F_Complex is SplittingField of X^3-2;
X^3-2 splits_in F by 32split,FIELD_8:def 1; then
F_Complex == F by A,FIELD_8:def 1; then
F_Complex is Subfield of F by FIELD_7:def 2; then
the carrier of F_Complex c= the carrier of F by EC_PF_1:def 1;
hence contradiction by ff;
end;
hence thesis;
end;