set F = FAdj (F_Rat,{zeta});
set V = VecSp ((FAdj (F_Rat,{zeta})),F_Rat);
A:
the carrier of (FAdj (F_Rat,{zeta})) = the carrier of (VecSp ((FAdj (F_Rat,{zeta})),F_Rat))
by FIELD_4:def 6;
( {zeta} is Subset of (FAdj (F_Rat,{zeta})) & zeta in {zeta} )
by FIELD_6:35, TARSKI:def 1;
then reconsider e = 1. F_Complex, z = zeta as Element of (VecSp ((FAdj (F_Rat,{zeta})),F_Rat)) by A, FIELD_6:def 6;
e = 1
by COMPLEX1:def 4, COMPLFLD:def 1;
then C:
Lin {e,z} = ModuleStr(# the carrier of (VecSp ((FAdj (F_Rat,{zeta})),F_Rat)), the addF of (VecSp ((FAdj (F_Rat,{zeta})),F_Rat)), the ZeroF of (VecSp ((FAdj (F_Rat,{zeta})),F_Rat)), the lmult of (VecSp ((FAdj (F_Rat,{zeta})),F_Rat)) #)
by baseZ, VECTSP_7:def 3;
now not sqrt 2 in the carrier of (FAdj (F_Rat,{zeta}))assume
sqrt 2
in the
carrier of
(FAdj (F_Rat,{zeta}))
;
contradictionthen
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
FAdj (
F_Rat,
{zeta})
by FIELD_6:36;
1. F_Complex = 1. (FAdj (F_Rat,{zeta}))
by EC_PF_1:def 1;
then E1:
[(l . e),e] in [: the carrier of F_Rat, the carrier of (FAdj (F_Rat,{zeta})):]
by ZFMISC_1:def 2;
the
carrier of
F_Rat c= the
carrier of
(FAdj (F_Rat,{zeta}))
by E0, EC_PF_1:def 1;
then E2:
[: the carrier of F_Rat, the carrier of (FAdj (F_Rat,{zeta})):] c= [: the carrier of (FAdj (F_Rat,{zeta})), the carrier of (FAdj (F_Rat,{zeta})):]
by ZFMISC_1:96;
thus (l . e) * e =
( the multF of (FAdj (F_Rat,{zeta})) | [: the carrier of F_Rat, the carrier of (FAdj (F_Rat,{zeta})):]) . (
(l . e),
e)
by FIELD_4:def 6
.=
the
multF of
(FAdj (F_Rat,{zeta})) . (
(l . e),
e)
by E1, FUNCT_1:49
.=
( the multF of F_Complex || the carrier of (FAdj (F_Rat,{zeta}))) . (
(l . e),
e)
by EC_PF_1:def 1
.=
a * (1. F_Complex)
by E2, E1, FUNCT_1:49
.=
a
;
verum
end;
F:
(l . z) * z = b * zeta
proof
F0:
F_Rat is
Subfield of
FAdj (
F_Rat,
{zeta})
by FIELD_6:36;
(
{zeta} is
Subset of
(FAdj (F_Rat,{zeta})) &
zeta in {zeta} )
by FIELD_6:35, TARSKI:def 1;
then F1:
[(l . z),z] in [: the carrier of F_Rat, the carrier of (FAdj (F_Rat,{zeta})):]
by ZFMISC_1:def 2;
the
carrier of
F_Rat c= the
carrier of
(FAdj (F_Rat,{zeta}))
by F0, EC_PF_1:def 1;
then F2:
[: the carrier of F_Rat, the carrier of (FAdj (F_Rat,{zeta})):] c= [: the carrier of (FAdj (F_Rat,{zeta})), the carrier of (FAdj (F_Rat,{zeta})):]
by ZFMISC_1:96;
thus (l . z) * z =
( the multF of (FAdj (F_Rat,{zeta})) | [: the carrier of F_Rat, the carrier of (FAdj (F_Rat,{zeta})):]) . (
(l . z),
z)
by FIELD_4:def 6
.=
the
multF of
(FAdj (F_Rat,{zeta})) . (
(l . z),
z)
by F1, FUNCT_1:49
.=
( the multF of F_Complex || the carrier of (FAdj (F_Rat,{zeta}))) . (
(l . z),
z)
by EC_PF_1:def 1
.=
b * zeta
by F2, F1, FUNCT_1:49
;
verum
end;
(
a in FAdj (
F_Rat,
{zeta}) &
b * zeta in FAdj (
F_Rat,
{zeta}) )
proof
F_Rat is
Subfield of
FAdj (
F_Rat,
{zeta})
by FIELD_6:36;
then G2:
the
carrier of
F_Rat c= the
carrier of
(FAdj (F_Rat,{zeta}))
by EC_PF_1:def 1;
hence
a in FAdj (
F_Rat,
{zeta})
;
b * zeta in FAdj (F_Rat,{zeta})
G3:
FAdj (
F_Rat,
{zeta}) is
Subring of
F_Complex
by FIELD_5:12;
(
{zeta} is
Subset of
(FAdj (F_Rat,{zeta})) &
zeta in {zeta} )
by TARSKI:def 1, FIELD_6:35;
then reconsider u =
zeta ,
v =
b as
Element of
(FAdj (F_Rat,{zeta})) by G2;
v * u = b * zeta
by G3, FIELD_6:16;
hence
b * zeta in FAdj (
F_Rat,
{zeta})
;
verum
end;
then G:
[a,(b * zeta)] in [: the carrier of (FAdj (F_Rat,{zeta})), the carrier of (FAdj (F_Rat,{zeta})):]
by ZFMISC_1:def 2;
((l . e) * e) + ((l . z) * z) =
the
addF of
(FAdj (F_Rat,{zeta})) . (
a,
(b * zeta))
by E, F, FIELD_4:def 6
.=
( the addF of F_Complex || the carrier of (FAdj (F_Rat,{zeta}))) . (
a,
(b * zeta))
by EC_PF_1:def 1
.=
a + (b * zeta)
by G, FUNCT_1:49
;
hence
sqrt 2
= a + (b * zeta)
by C1, VECTSP_6:18;
verum
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;
verum end;
hence
sqrt 2 is not Element of (FAdj (F_Rat,{zeta}))
; verum