let F be Field; :: thesis: for E1, E2, E3 being FieldExtension of F st E1,E2 are_isomorphic_over F & E2,E3 are_isomorphic_over F holds
E1,E3 are_isomorphic_over F
let E1, E2, E3 be FieldExtension of F; :: thesis: ( E1,E2 are_isomorphic_over F & E2,E3 are_isomorphic_over F implies E1,E3 are_isomorphic_over F )
assume AS: ( E1,E2 are_isomorphic_over F & E2,E3 are_isomorphic_over F ) ; :: thesis: E1,E3 are_isomorphic_over F
consider f being Function of E1,E2 such that
A: f is F -isomorphism by AS;
consider g being Function of E2,E3 such that
B: g is F -isomorphism by AS;
C: ( f is F -fixing & f is isomorphism ) by A;
D: ( f is one-to-one & f is onto & rng f = the carrier of E2 ) by A, FUNCT_2:def 3;
E: ( g is F -fixing & g is isomorphism ) by B;
F: ( g is one-to-one & g is onto & rng g = the carrier of E3 ) by B, FUNCT_2:def 3;
H0: dom (g * f) = the carrier of E1
proof
H1: for o being object st o in dom (g * f) holds
o in the carrier of E1 ;
now :: thesis: for o being object st o in the carrier of E1 holds
o in dom (g * f)
let o be object ; :: thesis: ( o in the carrier of E1 implies o in dom (g * f) )
assume H2: o in the carrier of E1 ; :: thesis: o in dom (g * f)
then reconsider x = o as Element of E1 ;
( o in dom f & f . x in the carrier of E2 ) by H2, FUNCT_2:def 1;
then ( o in dom f & f . o in dom g ) by FUNCT_2:def 1;
hence o in dom (g * f) by FUNCT_1:11; :: thesis: verum
end;
hence dom (g * f) = the carrier of E1 by H1, TARSKI:2; :: thesis: verum
end;
rng (g * f) = the carrier of E3 by D, F, FUNCT_2:14;
then reconsider h = g * f as Function of E1,E3 by H0, FUNCT_2:2;
K: h is onto by D, F, FUNCT_2:14;
h is F -fixing
proof
F is Subring of E1 by FIELD_4:def 1;
then H3: the carrier of F c= the carrier of E1 by C0SP1:def 3;
now :: thesis: for a being Element of F holds h . a = a
let a be Element of F; :: thesis: h . a = a
thus h . a = g . (f . a) by H0, H3, FUNCT_1:12
.= g . a by C
.= a by E ; :: thesis: verum
end;
hence h is F -fixing ; :: thesis: verum
end;
then h is F -isomorphism by A, B, K;
hence E1,E3 are_isomorphic_over F ; :: thesis: verum