let K, F be Field; ( K,F are_disjoint implies ( F is K -monomorphic iff ex E being Field st
( E,F are_isomorphic & K is Subfield of E ) ) )
assume AS:
K,F are_disjoint
; ( F is K -monomorphic iff ex E being Field st
( E,F are_isomorphic & K is Subfield of E ) )
now ( ex E being Field st
( E,F are_isomorphic & K is Subfield of E ) implies F is K -monomorphic )assume
ex
E being
Field st
(
E,
F are_isomorphic &
K is
Subfield of
E )
;
F is K -monomorphic then consider E being
Field such that A:
(
E,
F are_isomorphic &
K is
Subfield of
E )
;
K is
Subring of
E
by A, RING_3:43;
then consider m being
Function of
K,
E such that B:
(
m is
RingHomomorphism &
m is
monomorphism )
by RING_3:def 3, RING_3:71;
consider i being
Function of
E,
F such that C:
i is
RingIsomorphism
by A, QUOFIELD:def 23;
set f =
i * m;
i * m is
linear
by B, C, RINGCAT1:1;
hence
F is
K -monomorphic
by B, C, RING_3:def 3;
verum end;
hence
( F is K -monomorphic iff ex E being Field st
( E,F are_isomorphic & K is Subfield of E ) )
by AS, Th16; verum