let F be Field; for E being FieldExtension of F
for T being Subset of E holds RAdj (F,T) is Subring of FAdj (F,T)
let E be FieldExtension of F; for T being Subset of E holds RAdj (F,T) is Subring of FAdj (F,T)
let T be Subset of E; RAdj (F,T) is Subring of FAdj (F,T)
set Pf = FAdj (F,T);
set Pr = RAdj (F,T);
A: 1. (RAdj (F,T)) =
1. E
by dRA
.=
1. (FAdj (F,T))
by dFA
;
B: 0. (RAdj (F,T)) =
0. E
by dRA
.=
0. (FAdj (F,T))
by dFA
;
then C:
the carrier of (RAdj (F,T)) c= the carrier of (FAdj (F,T))
;
then Y:
[: the carrier of (RAdj (F,T)), the carrier of (RAdj (F,T)):] c= [: the carrier of (FAdj (F,T)), the carrier of (FAdj (F,T)):]
by ZFMISC_1:96;
D: the addF of (FAdj (F,T)) || the carrier of (RAdj (F,T)) =
( the addF of E || (carrierFA T)) || the carrier of (RAdj (F,T))
by dFA
.=
( the addF of E || the carrier of (FAdj (F,T))) || the carrier of (RAdj (F,T))
by dFA
.=
the addF of E || the carrier of (RAdj (F,T))
by Y, FUNCT_1:51
.=
the addF of E || (carrierRA T)
by dRA
.=
the addF of (RAdj (F,T))
by dRA
;
the multF of (FAdj (F,T)) || the carrier of (RAdj (F,T)) =
( the multF of E || (carrierFA T)) || the carrier of (RAdj (F,T))
by dFA
.=
( the multF of E || the carrier of (FAdj (F,T))) || the carrier of (RAdj (F,T))
by dFA
.=
the multF of E || the carrier of (RAdj (F,T))
by Y, FUNCT_1:51
.=
the multF of E || (carrierRA T)
by dRA
.=
the multF of (RAdj (F,T))
by dRA
;
hence
RAdj (F,T) is Subring of FAdj (F,T)
by A, B, C, D, C0SP1:def 3; verum