let R be strict Field; for E being FieldExtension of R
for T being Subset of E holds
( FAdj (R,T) = R iff T is Subset of R )
let S be FieldExtension of R; for T being Subset of S holds
( FAdj (R,T) = R iff T is Subset of R )
let T be Subset of S; ( FAdj (R,T) = R iff T is Subset of R )
set P = FAdj (R,T);
X:
( R is Subring of R & R is Subring of S )
by FIELD_4:def 1, LIOUVIL2:18;
X1:
( R is Subfield of R & R is Subfield of S )
by FIELD_4:7, FIELD_4:1;
now ( T is Subset of R implies FAdj (R,T) = R )assume B0:
T is
Subset of
R
;
FAdj (R,T) = Rthen B1:
the
carrier of
R = the
carrier of
(FAdj (R,T))
by Z, TARSKI:2;
B2:
1. (FAdj (R,T)) =
1. S
by dFA
.=
1. R
by X, C0SP1:def 3
;
B3:
0. (FAdj (R,T)) =
0. S
by dFA
.=
0. R
by X, C0SP1:def 3
;
B4: the
addF of
(FAdj (R,T)) =
the
addF of
S || (carrierFA T)
by dFA
.=
the
addF of
S || the
carrier of
R
by B1, dFA
.=
the
addF of
R
by X, C0SP1:def 3
;
the
multF of
(FAdj (R,T)) =
the
multF of
S || (carrierFA T)
by dFA
.=
the
multF of
S || the
carrier of
R
by B1, dFA
.=
the
multF of
R
by X, C0SP1:def 3
;
hence
FAdj (
R,
T)
= R
by Z, TARSKI:2, B5, B2, B3, B4;
verum end;
hence
( FAdj (R,T) = R iff T is Subset of R )
by FAt; verum