let F be Field; for E being F -algebraic FieldExtension of F
for L being algebraic-closed F -monomorphic Field
for f being Monomorphism of F,L ex g being Function of E,L st
( g is monomorphism & g is f -extending )
let E be F -algebraic FieldExtension of F; for L being algebraic-closed F -monomorphic Field
for f being Monomorphism of F,L ex g being Function of E,L st
( g is monomorphism & g is f -extending )
let L be algebraic-closed F -monomorphic Field; for f being Monomorphism of F,L ex g being Function of E,L st
( g is monomorphism & g is f -extending )
let f be Monomorphism of F,L; ex g being Function of E,L st
( g is monomorphism & g is f -extending )
set S = Ext_Set (f,E);
set R = { [p,q] where p, q is Element of Ext_Set (f,E) : p <= q } ;
now for o being object st o in { [p,q] where p, q is Element of Ext_Set (f,E) : p <= q } holds
ex y, z being object st o = [y,z]let o be
object ;
( o in { [p,q] where p, q is Element of Ext_Set (f,E) : p <= q } implies ex y, z being object st o = [y,z] )assume
o in { [p,q] where p, q is Element of Ext_Set (f,E) : p <= q }
;
ex y, z being object st o = [y,z]then consider p,
q being
Element of
Ext_Set (
f,
E)
such that A:
(
o = [p,q] &
p <= q )
;
thus
ex
y,
z being
object st
o = [y,z]
by A;
verum end;
then reconsider R = { [p,q] where p, q is Element of Ext_Set (f,E) : p <= q } as Relation by RELAT_1:def 1;
B:
field R = Ext_Set (f,E)
I1:
R is_reflexive_in field R
I2:
R is_transitive_in field R
proof
now for x, y, z being object st x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R holds
[x,z] in Rlet x,
y,
z be
object ;
( x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R implies [x,z] in R )assume I3:
(
x in field R &
y in field R &
z in field R &
[x,y] in R &
[y,z] in R )
;
[x,z] in Rthen consider p,
q being
Element of
Ext_Set (
f,
E)
such that I4:
(
[p,q] = [x,y] &
p <= q )
;
consider q1,
r being
Element of
Ext_Set (
f,
E)
such that I5:
(
[q1,r] = [y,z] &
q1 <= r )
by I3;
I6:
(
p = x &
q = y &
q1 = y &
r = z )
by I4, I5, XTUPLE_0:1;
then
p <= r
by I4, I5, po3;
hence
[x,z] in R
by I6;
verum end;
hence
R is_transitive_in field R
by RELAT_2:def 8;
verum
end;
I3:
R is_antisymmetric_in field R
proof
now for x, y being object st x in field R & y in field R & [x,y] in R & [y,x] in R holds
x = ylet x,
y be
object ;
( x in field R & y in field R & [x,y] in R & [y,x] in R implies x = y )assume I3:
(
x in field R &
y in field R &
[x,y] in R &
[y,x] in R )
;
x = ythen consider p,
q being
Element of
Ext_Set (
f,
E)
such that I4:
(
[p,q] = [x,y] &
p <= q )
;
consider q1,
p1 being
Element of
Ext_Set (
f,
E)
such that I5:
(
[q1,p1] = [y,x] &
q1 <= p1 )
by I3;
(
p = x &
q = y &
q1 = y &
p1 = x )
by I4, I5, XTUPLE_0:1;
hence
x = y
by I4, I5, po2;
verum end;
hence
R is_antisymmetric_in field R
by RELAT_2:def 4;
verum
end;
then reconsider R = R as reflexive antisymmetric transitive Relation by I1, I2, RELAT_2:def 9, RELAT_2:def 16, RELAT_2:def 12;
A:
R partially_orders Ext_Set (f,E)
by I1, I2, I3, B;
then
Ext_Set (f,E) has_upper_Zorn_property_wrt R
;
then consider U being set such that
Z:
U is_maximal_in R
by A, B, ORDERS_1:63;
reconsider U = U as Element of Ext_Set (f,E) by Z, B;
U in Ext_Set (f,E)
;
then consider W being Element of SubFields E, h being Function of W,L such that
H1:
( U = [W,h] & ex W1 being FieldExtension of F ex h1 being Function of W1,L st
( W1 = W & h1 = h & h1 is monomorphism & h1 is f -extending ) )
;
consider W1 being FieldExtension of F, h1 being Function of W1,L such that
H2:
( W1 = W & h1 = h & h1 is monomorphism & h1 is f -extending )
by H1;
reconsider W = W as FieldExtension of F by H2;
I1:
W is Subfield of E
by subfie;
then I2:
the carrier of W c= the carrier of E
by EC_PF_1:def 1;
now for a being Element of E holds a in the carrier of Wlet a be
Element of
E;
a in the carrier of Wassume A1:
not
a in the
carrier of
W
;
contradictionreconsider E1 =
E as
FieldExtension of
F ;
reconsider E1 =
E1 as
W -extending FieldExtension of
F by I1, FIELD_4:7;
reconsider E1 =
E1 as
W -algebraic FieldExtension of
W by FIELD_7:40;
reconsider a =
a as
W -algebraic Element of
E1 ;
set V =
FAdj (
W,
{a});
I3:
FAdj (
W,
{a}) is
Element of
SubFields E
by subfie;
reconsider L1 =
L as
algebraic-closed W -monomorphic Field by H2, RING_3:def 3;
reconsider h1 =
h1 as
Monomorphism of
W,
L1 by H2;
consider r being
Function of
(FAdj (W,{a})),
L such that A2:
(
r is
monomorphism &
r is
h1 -extending )
by lift1;
reconsider V =
FAdj (
W,
{a}) as
W -extending FieldExtension of
F ;
reconsider r =
r as
Function of
V,
L ;
[V,r] in Ext_Set (
f,
E)
then reconsider T =
[V,r] as
Element of
Ext_Set (
f,
E) ;
U <= T
by H2, H1, A2;
then A5:
[U,T] in R
;
(
{a} is
Subset of
V &
a in {a} )
by FIELD_6:35, TARSKI:def 1;
then
the
carrier of
W <> the
carrier of
V
by A1;
then
U <> T
by H1, XTUPLE_0:1;
hence
contradiction
by B, A5, Z;
verum end;
then C:
the carrier of E c= the carrier of W
;
then G:
the carrier of E = the carrier of W
by I2, XBOOLE_0:def 10;
set E1 = doubleLoopStr(# the carrier of E, the addF of E, the multF of E, the OneF of E, the ZeroF of E #);
M:
( doubleLoopStr(# the carrier of E, the addF of E, the multF of E, the OneF of E, the ZeroF of E #) is strict & W is strict )
by subfie;
D:
doubleLoopStr(# the carrier of E, the addF of E, the multF of E, the OneF of E, the ZeroF of E #) = W
proof
D1: the
addF of
doubleLoopStr(# the
carrier of
E, the
addF of
E, the
multF of
E, the
OneF of
E, the
ZeroF of
E #) =
the
addF of
E || the
carrier of
E
.=
the
addF of
W
by I1, G, EC_PF_1:def 1
;
D2: the
multF of
doubleLoopStr(# the
carrier of
E, the
addF of
E, the
multF of
E, the
OneF of
E, the
ZeroF of
E #) =
the
multF of
E || the
carrier of
E
.=
the
multF of
W
by I1, G, EC_PF_1:def 1
;
D3:
1. doubleLoopStr(# the
carrier of
E, the
addF of
E, the
multF of
E, the
OneF of
E, the
ZeroF of
E #) =
1. E
.=
1. W
by I1, EC_PF_1:def 1
;
0. doubleLoopStr(# the
carrier of
E, the
addF of
E, the
multF of
E, the
OneF of
E, the
ZeroF of
E #) =
0. E
.=
0. W
by I1, EC_PF_1:def 1
;
hence
doubleLoopStr(# the
carrier of
E, the
addF of
E, the
multF of
E, the
OneF of
E, the
ZeroF of
E #)
= W
by C, M, D1, D2, D3, I2, XBOOLE_0:def 10;
verum
end;
then reconsider h2 = h1 as Function of doubleLoopStr(# the carrier of E, the addF of E, the multF of E, the OneF of E, the ZeroF of E #),L by H2;
doubleLoopStr(# the carrier of E, the addF of E, the multF of E, the OneF of E, the ZeroF of E #) == E
by lemug1;
then consider i being Function of E,doubleLoopStr(# the carrier of E, the addF of E, the multF of E, the OneF of E, the ZeroF of E #) such that
E:
( i = id E & i is isomorphism )
by FIELD_7:1;
reconsider g = h2 * i as Function of E,L ;
K:
g is linear
by E, H2, D, RINGCAT1:1;
then
g is f -extending
;
hence
ex g being Function of E,L st
( g is monomorphism & g is f -extending )
by K; verum