let F be Field; for E being FieldExtension of F
for a being Element of E holds FAdj (F,{a,(- a)}) = FAdj (F,{a})
let E be FieldExtension of F; for a being Element of E holds FAdj (F,{a,(- a)}) = FAdj (F,{a})
let a be Element of E; FAdj (F,{a,(- a)}) = FAdj (F,{a})
Y:
FAdj (F,{a}) is Subfield of FAdj (F,{a,(- a)})
by FIELD_7:10, ZFMISC_1:7;
now for o being object st o in the carrier of (FAdj (F,{a,(- a)})) holds
o in the carrier of (FAdj (F,{a}))let o be
object ;
( o in the carrier of (FAdj (F,{a,(- a)})) implies o in the carrier of (FAdj (F,{a})) )assume A:
o in the
carrier of
(FAdj (F,{a,(- a)}))
;
o in the carrier of (FAdj (F,{a})) the
carrier of
(FAdj (F,{a,(- a)})) =
carrierFA {a,(- a)}
by FIELD_6:def 6
.=
{ x where x is Element of E : for U being Subfield of E st F is Subfield of U & {a,(- a)} is Subset of U holds
x in U }
;
then consider oe being
Element of
E such that C:
(
oe = o & ( for
U being
Subfield of
E st
F is
Subfield of
U &
{a,(- a)} is
Subset of
U holds
oe in U ) )
by A;
the
carrier of
(FAdj (F,{a})) =
carrierFA {a}
by FIELD_6:def 6
.=
{ x where x is Element of E : for U being Subfield of E st F is Subfield of U & {a} is Subset of U holds
x in U }
;
hence
o in the
carrier of
(FAdj (F,{a}))
by C, D;
verum end;
then
the carrier of (FAdj (F,{a,(- a)})) c= the carrier of (FAdj (F,{a}))
;
then
FAdj (F,{a,(- a)}) is Subfield of FAdj (F,{a})
by EC_PF_1:6;
hence
FAdj (F,{a,(- a)}) = FAdj (F,{a})
by Y, EC_PF_1:4; verum