let F be Field; for E being FieldExtension of F
for L being F -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E)) holds unionField (S,f,E) is Subfield of E
let E be FieldExtension of F; for L being F -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E)) holds unionField (S,f,E) is Subfield of E
let L be F -monomorphic Field; for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E)) holds unionField (S,f,E) is Subfield of E
let f be Monomorphism of F,L; for S being non empty ascending Subset of (Ext_Set (f,E)) holds unionField (S,f,E) is Subfield of E
let S be non empty ascending Subset of (Ext_Set (f,E)); unionField (S,f,E) is Subfield of E
set K = unionField (S,f,E);
H: the carrier of (unionField (S,f,E)) =
unionCarrier (S,f,E)
by duf
.=
union { the carrier of (p `1) where p is Element of S : verum }
;
A:
the carrier of (unionField (S,f,E)) c= the carrier of E
proof
now for o being object st o in the carrier of (unionField (S,f,E)) holds
o in the carrier of Elet o be
object ;
( o in the carrier of (unionField (S,f,E)) implies o in the carrier of E )assume
o in the
carrier of
(unionField (S,f,E))
;
o in the carrier of Ethen consider Y being
set such that A1:
(
o in Y &
Y in { the carrier of (p `1) where p is Element of S : verum } )
by H, TARSKI:def 4;
consider p being
Element of
S such that A2:
Y = the
carrier of
(p `1)
by A1;
p in Ext_Set (
f,
E)
;
then consider K being
Element of
SubFields E,
g being
Function of
K,
L such that A3:
(
p = [K,g] & ex
K1 being
FieldExtension of
F ex
g1 being
Function of
K1,
L st
(
K1 = K &
g1 = g &
g1 is
monomorphism &
g1 is
f -extending ) )
;
p `1 is
Subfield of
E
by A3, subfie;
then
the
carrier of
(p `1) c= the
carrier of
E
by EC_PF_1:def 1;
hence
o in the
carrier of
E
by A1, A2;
verum end;
hence
the
carrier of
(unionField (S,f,E)) c= the
carrier of
E
;
verum
end;
B:
the addF of (unionField (S,f,E)) = the addF of E || the carrier of (unionField (S,f,E))
proof
set aF = the
addF of
(unionField (S,f,E));
set aK = the
addF of
E || the
carrier of
(unionField (S,f,E));
B1:
dom ( the addF of E || the carrier of (unionField (S,f,E))) =
(dom the addF of E) /\ [: the carrier of (unionField (S,f,E)), the carrier of (unionField (S,f,E)):]
by RELAT_1:61
.=
[: the carrier of E, the carrier of E:] /\ [: the carrier of (unionField (S,f,E)), the carrier of (unionField (S,f,E)):]
by FUNCT_2:def 1
.=
[: the carrier of (unionField (S,f,E)), the carrier of (unionField (S,f,E)):]
by A, XBOOLE_1:28, ZFMISC_1:96
.=
dom the
addF of
(unionField (S,f,E))
by FUNCT_2:def 1
;
now for x being object st x in dom the addF of (unionField (S,f,E)) holds
the addF of (unionField (S,f,E)) . x = ( the addF of E || the carrier of (unionField (S,f,E))) . xlet x be
object ;
( x in dom the addF of (unionField (S,f,E)) implies the addF of (unionField (S,f,E)) . b1 = ( the addF of E || the carrier of (unionField (S,f,E))) . b1 )assume
x in dom the
addF of
(unionField (S,f,E))
;
the addF of (unionField (S,f,E)) . b1 = ( the addF of E || the carrier of (unionField (S,f,E))) . b1then consider a,
b being
object such that B3:
(
a in the
carrier of
(unionField (S,f,E)) &
b in the
carrier of
(unionField (S,f,E)) &
x = [a,b] )
by ZFMISC_1:def 2;
reconsider a =
a,
b =
b as
Element of
(unionField (S,f,E)) by B3;
consider Y1 being
set such that C1:
(
a in Y1 &
Y1 in { the carrier of (p `1) where p is Element of S : verum } )
by H, TARSKI:def 4;
consider pa being
Element of
S such that B4:
Y1 = the
carrier of
(pa `1)
by C1;
consider Y2 being
set such that C2:
(
b in Y2 &
Y2 in { the carrier of (p `1) where p is Element of S : verum } )
by H, TARSKI:def 4;
consider pb being
Element of
S such that B5:
Y2 = the
carrier of
(pb `1)
by C2;
pa in Ext_Set (
f,
E)
;
then consider U being
Element of
SubFields E,
g being
Function of
U,
L such that A3:
(
pa = [U,g] & ex
K1 being
FieldExtension of
F ex
g1 being
Function of
K1,
L st
(
K1 = U &
g1 = g &
g1 is
monomorphism &
g1 is
f -extending ) )
;
AS1:
pa `1 is
Subfield of
E
by A3, subfie;
pb in Ext_Set (
f,
E)
;
then consider U being
Element of
SubFields E,
g being
Function of
U,
L such that A3:
(
pb = [U,g] & ex
K1 being
FieldExtension of
F ex
g1 being
Function of
K1,
L st
(
K1 = U &
g1 = g &
g1 is
monomorphism &
g1 is
f -extending ) )
;
AS2:
pb `1 is
Subfield of
E
by A3, subfie;
per cases
( pa <= pb or pb <= pa )
by dasc;
suppose
pa <= pb
;
the addF of (unionField (S,f,E)) . b1 = ( the addF of E || the carrier of (unionField (S,f,E))) . b1then reconsider a1 =
a,
b1 =
b as
Element of
(pb `1) by C1, C2, B4, B5, lem1a;
B4:
the
addF of
(pb `1) = the
addF of
E || the
carrier of
(pb `1)
by AS2, EC_PF_1:def 1;
B5:
[a1,b1] in [: the carrier of (pb `1), the carrier of (pb `1):]
by ZFMISC_1:def 2;
B6:
[a,b] in [: the carrier of (unionField (S,f,E)), the carrier of (unionField (S,f,E)):]
by ZFMISC_1:def 2;
thus the
addF of
(unionField (S,f,E)) . x =
a + b
by B3
.=
a1 + b1
by lem4a
.=
the
addF of
E . (
a,
b)
by B4, B5, FUNCT_1:49
.=
( the addF of E || the carrier of (unionField (S,f,E))) . x
by B3, B6, FUNCT_1:49
;
verum end; suppose
pb <= pa
;
the addF of (unionField (S,f,E)) . b1 = ( the addF of E || the carrier of (unionField (S,f,E))) . b1then reconsider a1 =
a,
b1 =
b as
Element of
(pa `1) by C1, C2, B4, B5, lem1a;
B4:
the
addF of
(pa `1) = the
addF of
E || the
carrier of
(pa `1)
by AS1, EC_PF_1:def 1;
B5:
[a1,b1] in [: the carrier of (pa `1), the carrier of (pa `1):]
by ZFMISC_1:def 2;
B6:
[a1,b1] in [: the carrier of (unionField (S,f,E)), the carrier of (unionField (S,f,E)):]
by ZFMISC_1:def 2;
thus the
addF of
(unionField (S,f,E)) . x =
a + b
by B3
.=
a1 + b1
by lem4a
.=
the
addF of
E . (
a1,
b1)
by B4, B5, FUNCT_1:49
.=
( the addF of E || the carrier of (unionField (S,f,E))) . x
by B3, B6, FUNCT_1:49
;
verum end; end;
hence
the
addF of
(unionField (S,f,E)) = the
addF of
E || the
carrier of
(unionField (S,f,E))
by B1;
verum
end;
C:
the multF of (unionField (S,f,E)) = the multF of E || the carrier of (unionField (S,f,E))
proof
set aF = the
multF of
(unionField (S,f,E));
set aK = the
multF of
E || the
carrier of
(unionField (S,f,E));
B1:
dom ( the multF of E || the carrier of (unionField (S,f,E))) =
(dom the multF of E) /\ [: the carrier of (unionField (S,f,E)), the carrier of (unionField (S,f,E)):]
by RELAT_1:61
.=
[: the carrier of E, the carrier of E:] /\ [: the carrier of (unionField (S,f,E)), the carrier of (unionField (S,f,E)):]
by FUNCT_2:def 1
.=
[: the carrier of (unionField (S,f,E)), the carrier of (unionField (S,f,E)):]
by A, XBOOLE_1:28, ZFMISC_1:96
.=
dom the
multF of
(unionField (S,f,E))
by FUNCT_2:def 1
;
now for x being object st x in dom the multF of (unionField (S,f,E)) holds
the multF of (unionField (S,f,E)) . x = ( the multF of E || the carrier of (unionField (S,f,E))) . xlet x be
object ;
( x in dom the multF of (unionField (S,f,E)) implies the multF of (unionField (S,f,E)) . b1 = ( the multF of E || the carrier of (unionField (S,f,E))) . b1 )assume
x in dom the
multF of
(unionField (S,f,E))
;
the multF of (unionField (S,f,E)) . b1 = ( the multF of E || the carrier of (unionField (S,f,E))) . b1then consider a,
b being
object such that B3:
(
a in the
carrier of
(unionField (S,f,E)) &
b in the
carrier of
(unionField (S,f,E)) &
x = [a,b] )
by ZFMISC_1:def 2;
reconsider a =
a,
b =
b as
Element of
(unionField (S,f,E)) by B3;
consider Y1 being
set such that C1:
(
a in Y1 &
Y1 in { the carrier of (p `1) where p is Element of S : verum } )
by H, TARSKI:def 4;
consider pa being
Element of
S such that B4:
Y1 = the
carrier of
(pa `1)
by C1;
consider Y2 being
set such that C2:
(
b in Y2 &
Y2 in { the carrier of (p `1) where p is Element of S : verum } )
by H, TARSKI:def 4;
consider pb being
Element of
S such that B5:
Y2 = the
carrier of
(pb `1)
by C2;
pa in Ext_Set (
f,
E)
;
then consider U being
Element of
SubFields E,
g being
Function of
U,
L such that A3:
(
pa = [U,g] & ex
K1 being
FieldExtension of
F ex
g1 being
Function of
K1,
L st
(
K1 = U &
g1 = g &
g1 is
monomorphism &
g1 is
f -extending ) )
;
AS1:
pa `1 is
Subfield of
E
by A3, subfie;
pb in Ext_Set (
f,
E)
;
then consider U being
Element of
SubFields E,
g being
Function of
U,
L such that A3:
(
pb = [U,g] & ex
K1 being
FieldExtension of
F ex
g1 being
Function of
K1,
L st
(
K1 = U &
g1 = g &
g1 is
monomorphism &
g1 is
f -extending ) )
;
AS2:
pb `1 is
Subfield of
E
by A3, subfie;
per cases
( pa <= pb or pb <= pa )
by dasc;
suppose
pa <= pb
;
the multF of (unionField (S,f,E)) . b1 = ( the multF of E || the carrier of (unionField (S,f,E))) . b1then reconsider a1 =
a,
b1 =
b as
Element of
(pb `1) by C1, C2, B4, B5, lem1a;
B4:
the
multF of
(pb `1) = the
multF of
E || the
carrier of
(pb `1)
by AS2, EC_PF_1:def 1;
B5:
[a1,b1] in [: the carrier of (pb `1), the carrier of (pb `1):]
by ZFMISC_1:def 2;
B6:
[a,b] in [: the carrier of (unionField (S,f,E)), the carrier of (unionField (S,f,E)):]
by ZFMISC_1:def 2;
thus the
multF of
(unionField (S,f,E)) . x =
a * b
by B3
.=
a1 * b1
by lem4a
.=
the
multF of
E . (
a,
b)
by B4, B5, FUNCT_1:49
.=
( the multF of E || the carrier of (unionField (S,f,E))) . x
by B3, B6, FUNCT_1:49
;
verum end; suppose
pb <= pa
;
the multF of (unionField (S,f,E)) . b1 = ( the multF of E || the carrier of (unionField (S,f,E))) . b1then reconsider a1 =
a,
b1 =
b as
Element of
(pa `1) by C1, C2, B4, B5, lem1a;
B4:
the
multF of
(pa `1) = the
multF of
E || the
carrier of
(pa `1)
by AS1, EC_PF_1:def 1;
B5:
[a1,b1] in [: the carrier of (pa `1), the carrier of (pa `1):]
by ZFMISC_1:def 2;
B6:
[a1,b1] in [: the carrier of (unionField (S,f,E)), the carrier of (unionField (S,f,E)):]
by ZFMISC_1:def 2;
thus the
multF of
(unionField (S,f,E)) . x =
a * b
by B3
.=
a1 * b1
by lem4a
.=
the
multF of
E . (
a1,
b1)
by B4, B5, FUNCT_1:49
.=
( the multF of E || the carrier of (unionField (S,f,E))) . x
by B3, B6, FUNCT_1:49
;
verum end; end;
hence
the
multF of
(unionField (S,f,E)) = the
multF of
E || the
carrier of
(unionField (S,f,E))
by B1;
verum
end;
set p = the Element of S;
the Element of S in Ext_Set (f,E)
;
then consider U being Element of SubFields E, g being Function of U,L such that
A3:
( the Element of S = [U,g] & ex K1 being FieldExtension of F ex g1 being Function of K1,L st
( K1 = U & g1 = g & g1 is monomorphism & g1 is f -extending ) )
;
AS3:
the Element of S `1 is Subfield of E
by A3, subfie;
D: 1. (unionField (S,f,E)) =
1. ( the Element of S `1)
by lem5a
.=
1. E
by AS3, EC_PF_1:def 1
;
0. (unionField (S,f,E)) =
0. ( the Element of S `1)
by lem5a
.=
0. E
by AS3, EC_PF_1:def 1
;
hence
unionField (S,f,E) is Subfield of E
by A, B, C, D, EC_PF_1:def 1; verum