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))
for p being Element of S holds p `1 is Subfield of unionField (S,f,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))
for p being Element of S holds p `1 is Subfield of unionField (S,f,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))
for p being Element of S holds p `1 is Subfield of unionField (S,f,E)
let f be Monomorphism of F,L; for S being non empty ascending Subset of (Ext_Set (f,E))
for p being Element of S holds p `1 is Subfield of unionField (S,f,E)
let S be non empty ascending Subset of (Ext_Set (f,E)); for p being Element of S holds p `1 is Subfield of unionField (S,f,E)
let p be Element of S; p `1 is Subfield of unionField (S,f,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 }
;
J:
the carrier of (p `1) in { the carrier of (p `1) where p is Element of S : verum }
;
then A:
the carrier of (p `1) c= the carrier of (unionField (S,f,E))
by H, ZFMISC_1:74;
B:
the addF of (p `1) = the addF of (unionField (S,f,E)) || the carrier of (p `1)
proof
set aF = the
addF of
(p `1);
set aK = the
addF of
(unionField (S,f,E)) || the
carrier of
(p `1);
B1:
dom ( the addF of (unionField (S,f,E)) || the carrier of (p `1)) =
(dom the addF of (unionField (S,f,E))) /\ [: the carrier of (p `1), the carrier of (p `1):]
by RELAT_1:61
.=
[: the carrier of (unionField (S,f,E)), the carrier of (unionField (S,f,E)):] /\ [: the carrier of (p `1), the carrier of (p `1):]
by FUNCT_2:def 1
.=
[: the carrier of (p `1), the carrier of (p `1):]
by A, ZFMISC_1:96, XBOOLE_1:28
;
now for x being object st x in dom the addF of (p `1) holds
the addF of (p `1) . x = ( the addF of (unionField (S,f,E)) || the carrier of (p `1)) . xlet x be
object ;
( x in dom the addF of (p `1) implies the addF of (p `1) . x = ( the addF of (unionField (S,f,E)) || the carrier of (p `1)) . x )assume B2:
x in dom the
addF of
(p `1)
;
the addF of (p `1) . x = ( the addF of (unionField (S,f,E)) || the carrier of (p `1)) . xthen consider a,
b being
object such that B3:
(
a in the
carrier of
(p `1) &
b in the
carrier of
(p `1) &
x = [a,b] )
by ZFMISC_1:def 2;
reconsider a =
a,
b =
b as
Element of
(p `1) by B3;
reconsider y =
a,
z =
b as
Element of
(unionField (S,f,E)) by A;
thus the
addF of
(p `1) . x =
a + b
by B3
.=
y + z
by lem4a
.=
( the addF of (unionField (S,f,E)) || the carrier of (p `1)) . x
by B3, B2, FUNCT_1:49
;
verum end;
hence
the
addF of
(p `1) = the
addF of
(unionField (S,f,E)) || the
carrier of
(p `1)
by B1, FUNCT_2:def 1;
verum
end;
C:
the multF of (p `1) = the multF of (unionField (S,f,E)) || the carrier of (p `1)
proof
set mF = the
multF of
(p `1);
set mK = the
multF of
(unionField (S,f,E)) || the
carrier of
(p `1);
B1:
dom ( the multF of (unionField (S,f,E)) || the carrier of (p `1)) =
(dom the multF of (unionField (S,f,E))) /\ [: the carrier of (p `1), the carrier of (p `1):]
by RELAT_1:61
.=
[: the carrier of (unionField (S,f,E)), the carrier of (unionField (S,f,E)):] /\ [: the carrier of (p `1), the carrier of (p `1):]
by FUNCT_2:def 1
.=
[: the carrier of (p `1), the carrier of (p `1):]
by A, ZFMISC_1:96, XBOOLE_1:28
;
now for x being object st x in dom the multF of (p `1) holds
the multF of (p `1) . x = ( the multF of (unionField (S,f,E)) || the carrier of (p `1)) . xlet x be
object ;
( x in dom the multF of (p `1) implies the multF of (p `1) . x = ( the multF of (unionField (S,f,E)) || the carrier of (p `1)) . x )assume B2:
x in dom the
multF of
(p `1)
;
the multF of (p `1) . x = ( the multF of (unionField (S,f,E)) || the carrier of (p `1)) . xthen consider a,
b being
object such that B3:
(
a in the
carrier of
(p `1) &
b in the
carrier of
(p `1) &
x = [a,b] )
by ZFMISC_1:def 2;
reconsider a =
a,
b =
b as
Element of
(p `1) by B3;
reconsider y =
a,
z =
b as
Element of
(unionField (S,f,E)) by A;
thus the
multF of
(p `1) . x =
a * b
by B3
.=
y * z
by lem4a
.=
( the multF of (unionField (S,f,E)) || the carrier of (p `1)) . x
by B3, B2, FUNCT_1:49
;
verum end;
hence
the
multF of
(p `1) = the
multF of
(unionField (S,f,E)) || the
carrier of
(p `1)
by B1, FUNCT_2:def 1;
verum
end;
( 1. (p `1) = 1. (unionField (S,f,E)) & 0. (unionField (S,f,E)) = 0. (p `1) )
by lem5a;
hence
p `1 is Subfield of unionField (S,f,E)
by H, J, ZFMISC_1:74, B, C, EC_PF_1:def 1; verum