let F be Field; for E being FieldExtension of F
for T being Subset of E holds
( RAdj (F,T) = FAdj (F,T) iff RAdj (F,T) is Field )
let E be FieldExtension of F; for T being Subset of E holds
( RAdj (F,T) = FAdj (F,T) iff RAdj (F,T) is Field )
let T be Subset of E; ( RAdj (F,T) = FAdj (F,T) iff RAdj (F,T) is Field )
set Pf = FAdj (F,T);
set Pr = RAdj (F,T);
now ( RAdj (F,T) is Field implies FAdj (F,T) = RAdj (F,T) )assume
RAdj (
F,
T) is
Field
;
FAdj (F,T) = RAdj (F,T)then reconsider Prf =
RAdj (
F,
T) as
Field ;
F is
Subring of
Prf
by RAsub;
then A:
F is
Subfield of
Prf
by FIELD_5:13;
B:
Prf is
Subfield of
E
by FIELD_5:13;
T is
Subset of
Prf
by RAt;
then
FAdj (
F,
T) is
Subfield of
Prf
by A, B, FAsub2;
then C:
FAdj (
F,
T) is
Subring of
Prf
by FIELD_5:12;
RAdj (
F,
T) is
Subring of
FAdj (
F,
T)
by RF;
hence
FAdj (
F,
T)
= RAdj (
F,
T)
by C, RE;
verum end;
hence
( RAdj (F,T) = FAdj (F,T) iff RAdj (F,T) is Field )
; verum