set p = X^2+X+1 ;
set F = FAdj ((Z/ 2),{alpha});
H:
embField (canHomP X^2+X+1) is FieldExtension of FAdj ((Z/ 2),{alpha})
by FIELD_4:7;
( alpha in {alpha} & {alpha} is Subset of (FAdj ((Z/ 2),{alpha})) )
by TARSKI:def 1, FIELD_6:35;
then reconsider a = alpha as Element of (FAdj ((Z/ 2),{alpha})) ;
alpha " = a "
by FIELD_6:18;
then reconsider ai = alpha " as Element of (FAdj ((Z/ 2),{alpha})) ;
C:
( rpoly (1,alpha) = rpoly (1,a) & rpoly (1,(alpha ")) = rpoly (1,ai) )
by H, FIELD_4:21;
reconsider q = (rpoly (1,a)) *' (rpoly (1,ai)) as Element of the carrier of (Polynom-Ring (FAdj ((Z/ 2),{alpha}))) by POLYNOM3:def 10;
B:
X^2+X+1 = (1. (FAdj ((Z/ 2),{alpha}))) * ((rpoly (1,a)) *' (rpoly (1,ai)))
by lemZ2, H, C, FIELD_4:17;
( rpoly (1,a) is Ppoly of FAdj ((Z/ 2),{alpha}) & rpoly (1,ai) is Ppoly of FAdj ((Z/ 2),{alpha}) )
by RING_5:51;
then
(rpoly (1,a)) *' (rpoly (1,ai)) is Ppoly of FAdj ((Z/ 2),{alpha})
by RING_5:52;
then A:
X^2+X+1 splits_in FAdj ((Z/ 2),{alpha})
by B, FIELD_4:def 5;
now for E being FieldExtension of Z/ 2 st X^2+X+1 splits_in E & E is Subfield of FAdj ((Z/ 2),{alpha}) holds
E == FAdj ((Z/ 2),{alpha})let E be
FieldExtension of
Z/ 2;
( X^2+X+1 splits_in E & E is Subfield of FAdj ((Z/ 2),{alpha}) implies E == FAdj ((Z/ 2),{alpha}) )assume D0:
(
X^2+X+1 splits_in E &
E is
Subfield of
FAdj (
(Z/ 2),
{alpha}) )
;
E == FAdj ((Z/ 2),{alpha})then D3:
FAdj (
(Z/ 2),
{alpha}) is
E -extending
by FIELD_4:7;
D4:
Roots (
(FAdj ((Z/ 2),{alpha})),
X^2+X+1)
c= the
carrier of
E
by D3, D0, A, FIELD_8:27;
alpha in Roots (
(FAdj ((Z/ 2),{alpha})),
X^2+X+1)
by lemZ2roots, TARSKI:def 2;
then
alpha in the
carrier of
E
by D4;
then D1:
{alpha} c= the
carrier of
E
by TARSKI:def 1;
D2:
E is
Subfield of
embField (canHomP X^2+X+1)
by D0, EC_PF_1:5;
Z/ 2 is
Subfield of
E
by FIELD_4:7;
then
FAdj (
(Z/ 2),
{alpha}) is
Subfield of
E
by D1, D2, FIELD_6:37;
hence
E == FAdj (
(Z/ 2),
{alpha})
by D0, FIELD_7:def 2;
verum end;
hence
FAdj ((Z/ 2),{alpha}) is SplittingField of X^2+X+1
by A, FIELD_8:def 1; verum