let K be Field; for F being K -monomorphic Field
for f being Monomorphism of K,F
for E being Field st E = embField f holds
K is Subfield of E
let F be K -monomorphic Field; for f being Monomorphism of K,F
for E being Field st E = embField f holds
K is Subfield of E
let f be Monomorphism of K,F; for E being Field st E = embField f holds
K is Subfield of E
let E be Field; ( E = embField f implies K is Subfield of E )
A2:
[#] (embField f) = carr f
by defemb;
assume A1:
E = embField f
; K is Subfield of E
then
[#] E = carr f
by defemb;
then A3:
[#] K c= [#] E
by XBOOLE_0:def 3;
A4:
dom the addF of E = [:([#] E),([#] E):]
by FUNCT_2:def 1;
set g1 = the addF of K;
set g2 = the addF of E | [:([#] K),([#] K):];
A5: dom ( the addF of E | [:([#] K),([#] K):]) =
(dom the addF of E) /\ [:([#] K),([#] K):]
by RELAT_1:61
.=
[:([#] K),([#] K):]
by A3, ZFMISC_1:96, XBOOLE_1:28, A4
.=
dom the addF of K
by FUNCT_2:def 1
;
now for x being set st x in dom the addF of K holds
the addF of K . x = ( the addF of E | [:([#] K),([#] K):]) . xlet x be
set ;
( x in dom the addF of K implies the addF of K . x = ( the addF of E | [:([#] K),([#] K):]) . x )assume
x in dom the
addF of
K
;
the addF of K . x = ( the addF of E | [:([#] K),([#] K):]) . xthen consider x1,
x2 being
object such that A6:
(
x1 in [#] K &
x2 in [#] K &
x = [x1,x2] )
by ZFMISC_1:def 2;
reconsider a =
x1,
b =
x2 as
Element of
K by A6;
A7:
[a,b] in [:([#] K),([#] K):]
by ZFMISC_1:def 2;
reconsider a1 =
x1,
b1 =
x2 as
Element of
(embField f) by A6, A2, XBOOLE_0:def 3;
( the addF of E || ([#] K)) . (
a,
b) =
a1 + b1
by A1, A7, FUNCT_1:49
.=
a + b
by Lm7
;
hence
the
addF of
K . x = ( the addF of E | [:([#] K),([#] K):]) . x
by A6;
verum end;
then A8:
the addF of K = the addF of E || ([#] K)
by A5;
set g1 = the multF of K;
set g2 = the multF of E | [:([#] K),([#] K):];
A9:
dom the multF of E = [:([#] E),([#] E):]
by FUNCT_2:def 1;
A10: dom ( the multF of E | [:([#] K),([#] K):]) =
(dom the multF of E) /\ [:([#] K),([#] K):]
by RELAT_1:61
.=
[:([#] K),([#] K):]
by A3, ZFMISC_1:96, XBOOLE_1:28, A9
.=
dom the multF of K
by FUNCT_2:def 1
;
now for x being set st x in dom the multF of K holds
the multF of K . x = ( the multF of E | [:([#] K),([#] K):]) . xlet x be
set ;
( x in dom the multF of K implies the multF of K . x = ( the multF of E | [:([#] K),([#] K):]) . x )assume
x in dom the
multF of
K
;
the multF of K . x = ( the multF of E | [:([#] K),([#] K):]) . xthen consider x1,
x2 being
object such that A11:
(
x1 in [#] K &
x2 in [#] K &
x = [x1,x2] )
by ZFMISC_1:def 2;
reconsider a =
x1,
b =
x2 as
Element of
K by A11;
A12:
[a,b] in [:([#] K),([#] K):]
by ZFMISC_1:def 2;
reconsider a1 =
x1,
b1 =
x2 as
Element of
(embField f) by A11, A2, XBOOLE_0:def 3;
( the multF of E || ([#] K)) . (
a,
b) =
a1 * b1
by A1, A12, FUNCT_1:49
.=
a * b
by Lm11
;
hence
the
multF of
K . x = ( the multF of E | [:([#] K),([#] K):]) . x
by A11;
verum end;
then A13:
the multF of K = the multF of E || ([#] K)
by A10;
( 1. E = 1. K & 0. E = 0. K )
by defemb, A1;
hence
K is Subfield of E
by A3, A8, A13, EC_PF_1:def 1; verum