let F be Field; for E being FieldExtension of F
for K being b1 -extending FieldExtension of F
for T1 being finite F -algebraic Subset of E
for T2 being Subset of K st T1 = T2 holds
FAdj (F,T1) = FAdj (F,T2)
let E be FieldExtension of F; for K being E -extending FieldExtension of F
for T1 being finite F -algebraic Subset of E
for T2 being Subset of K st T1 = T2 holds
FAdj (F,T1) = FAdj (F,T2)
let K be E -extending FieldExtension of F; for T1 being finite F -algebraic Subset of E
for T2 being Subset of K st T1 = T2 holds
FAdj (F,T1) = FAdj (F,T2)
let T1 be finite F -algebraic Subset of E; for T2 being Subset of K st T1 = T2 holds
FAdj (F,T1) = FAdj (F,T2)
let T2 be Subset of K; ( T1 = T2 implies FAdj (F,T1) = FAdj (F,T2) )
assume AS:
T1 = T2
; FAdj (F,T1) = FAdj (F,T2)
defpred S1[ Nat] means for T1 being finite F -algebraic Subset of E
for T2 being Subset of K st card T1 = $1 & T1 = T2 holds
FAdj (F,T1) = FAdj (F,T2);
A:
S1[ 0 ]
proof
now for T1 being finite F -algebraic Subset of E
for T2 being Subset of K st card T1 = 0 & T1 = T2 holds
FAdj (F,T1) = FAdj (F,T2)let T1 be
finite F -algebraic Subset of
E;
for T2 being Subset of K st card T1 = 0 & T1 = T2 holds
FAdj (F,T1) = FAdj (F,T2)let T2 be
Subset of
K;
( card T1 = 0 & T1 = T2 implies FAdj (F,T1) = FAdj (F,T2) )assume
(
card T1 = 0 &
T1 = T2 )
;
FAdj (F,T1) = FAdj (F,T2)then
(
T1 = {} &
T2 = {} )
;
then A1:
(
T1 is
Subset of
F &
T2 is
Subset of
F )
by XBOOLE_1:2;
then doubleLoopStr(# the
carrier of
(FAdj (F,T1)), the
addF of
(FAdj (F,T1)), the
multF of
(FAdj (F,T1)), the
OneF of
(FAdj (F,T1)), the
ZeroF of
(FAdj (F,T1)) #) =
doubleLoopStr(# the
carrier of
F, the
addF of
F, the
multF of
F, the
OneF of
F, the
ZeroF of
F #)
by FIELD_7:def 1, FIELD_7:3
.=
doubleLoopStr(# the
carrier of
(FAdj (F,T2)), the
addF of
(FAdj (F,T2)), the
multF of
(FAdj (F,T2)), the
OneF of
(FAdj (F,T2)), the
ZeroF of
(FAdj (F,T2)) #)
by A1, FIELD_7:def 1, FIELD_7:3
;
hence
FAdj (
F,
T1)
= FAdj (
F,
T2)
;
verum end;
hence
S1[
0 ]
;
verum
end;
B:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume B0:
S1[
k]
;
S1[k + 1]B1:
E is
Subfield of
K
by FIELD_4:7;
then B2:
the
carrier of
E c= the
carrier of
K
by EC_PF_1:def 1;
now for T1 being finite F -algebraic Subset of E
for T2 being Subset of K st card T1 = k + 1 & T1 = T2 holds
FAdj (F,T1) = FAdj (F,T2)let T1 be
finite F -algebraic Subset of
E;
for T2 being Subset of K st card T1 = k + 1 & T1 = T2 holds
FAdj (F,T1) = FAdj (F,T2)let T2 be
Subset of
K;
( card T1 = k + 1 & T1 = T2 implies FAdj (F,T1) = FAdj (F,T2) )assume C0:
(
card T1 = k + 1 &
T1 = T2 )
;
FAdj (F,T1) = FAdj (F,T2)then reconsider U1 =
T1 as non
empty finite Subset of
E ;
set a = the
Element of
U1;
reconsider V1 =
T1 \ { the Element of U1} as
finite F -algebraic Subset of
E ;
reconsider V2 =
T2 \ { the Element of U1} as
Subset of
K ;
then
{ the Element of U1} c= T1
;
then C1:
T1 = V1 \/ { the Element of U1}
by XBOOLE_1:45;
the
Element of
U1 in { the Element of U1}
by TARSKI:def 1;
then
not the
Element of
U1 in V1
by XBOOLE_0:def 5;
then C2:
card T1 = (card V1) + 1
by C1, CARD_2:41;
then
{ the Element of U1} c= T2
;
then C3:
T2 = V2 \/ { the Element of U1}
by XBOOLE_1:45;
C4:
FAdj (
F,
V1)
= FAdj (
F,
V2)
by B0, C0, C2;
reconsider b = the
Element of
U1 as
Element of
K by B2;
consider p being non
zero Polynomial of
F such that B:
Ext_eval (
p, the
Element of
U1)
= 0. E
by FIELD_6:43;
reconsider p =
p as non
zero Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
Ext_eval (
p,
b) =
0. E
by B, FIELD_6:11
.=
0. K
by B1, EC_PF_1:def 1
;
then reconsider b =
b as
F -algebraic Element of
K by FIELD_6:43;
reconsider E1 =
E as
F -extending FieldExtension of
F by FIELD_4:7;
reconsider E2 =
K as
F -extending FieldExtension of
F by FIELD_4:7;
consider p being non
zero Polynomial of
F such that B:
Ext_eval (
p, the
Element of
U1)
= 0. E
by FIELD_6:43;
reconsider p =
p as non
zero Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
the
carrier of
(Polynom-Ring F) c= the
carrier of
(Polynom-Ring (FAdj (F,V1)))
by FIELD_4:10;
then reconsider q =
p as
Element of the
carrier of
(Polynom-Ring (FAdj (F,V1))) ;
C:
Polynom-Ring F is
Subring of
Polynom-Ring (FAdj (F,V1))
by FIELD_4:def 1;
then reconsider q =
q as non
zero Element of the
carrier of
(Polynom-Ring (FAdj (F,V1))) ;
Ext_eval (
q, the
Element of
U1)
= 0. E1
by B, FIELD_7:15;
then reconsider a1 = the
Element of
U1 as
FAdj (
F,
V1)
-algebraic Element of
E1 by FIELD_6:43;
consider p being non
zero Polynomial of
F such that B:
Ext_eval (
p,
b)
= 0. K
by FIELD_6:43;
reconsider p =
p as non
zero Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
the
carrier of
(Polynom-Ring F) c= the
carrier of
(Polynom-Ring (FAdj (F,V2)))
by FIELD_4:10;
then reconsider q =
p as
Element of the
carrier of
(Polynom-Ring (FAdj (F,V2))) ;
C:
Polynom-Ring F is
Subring of
Polynom-Ring (FAdj (F,V2))
by FIELD_4:def 1;
then reconsider q =
q as non
zero Element of the
carrier of
(Polynom-Ring (FAdj (F,V2))) ;
Ext_eval (
q,
b)
= 0. E2
by B, FIELD_7:15;
then reconsider b1 =
b as
FAdj (
F,
V2)
-algebraic Element of
E2 by FIELD_6:43;
thus FAdj (
F,
T1) =
FAdj (
(FAdj (F,V1)),
{a1})
by C1, FIELD_7:34
.=
FAdj (
(FAdj (F,V2)),
{b1})
by C4, FIELD_10:9
.=
FAdj (
F,
T2)
by C3, FIELD_7:34
;
verum end; hence
S1[
k + 1]
;
verum end;
I:
for k being Nat holds S1[k]
from NAT_1:sch 2(A, B);
consider n being Nat such that
H:
card T1 = n
;
thus
FAdj (F,T1) = FAdj (F,T2)
by H, AS, I; verum