let F be Field; :: thesis: for E1, E2 being FieldExtension of F st E1,E2 are_isomorphic_over F holds
E2,E1 are_isomorphic_over F
let E1, E2 be FieldExtension of F; :: thesis: ( E1,E2 are_isomorphic_over F implies E2,E1 are_isomorphic_over F )
F is Subring of E1 by FIELD_4:def 1;
then H1: the carrier of F c= the carrier of E1 by C0SP1:def 3;
assume E1,E2 are_isomorphic_over F ; :: thesis: E2,E1 are_isomorphic_over F
then consider f being Function of E1,E2 such that
A: f is F -isomorphism ;
B: ( f is F -fixing & f is isomorphism ) by A;
C: ( f is one-to-one & f is onto & rng f = the carrier of E2 ) by A, FUNCT_2:def 3;
then reconsider g = f " as Function of E2,E1 by FUNCT_2:25;
now :: thesis: for a being Element of F holds g . a = a
let a be Element of F; :: thesis: g . a = a
H2: dom f = the carrier of E1 by FUNCT_2:def 1;
H3: a in the carrier of E1 by H1;
thus g . a = g . (f . a) by B
.= a by H2, H3, A, FUNCT_1:34 ; :: thesis: verum
end;
then D: g is F -fixing ;
H4: ( f is additive & f is multiplicative & f is unity-preserving ) by A;
H5: g is additive
proof
now :: thesis: for a, b being Element of E2 holds (g . a) + (g . b) = g . (a + b)
let a, b be Element of E2; :: thesis: (g . a) + (g . b) = g . (a + b)
consider x being object such that
A2: ( x in the carrier of E1 & a = f . x ) by C, FUNCT_2:11;
reconsider x = x as Element of E1 by A2;
consider y being object such that
A3: ( y in the carrier of E1 & b = f . y ) by C, FUNCT_2:11;
reconsider y = y as Element of E1 by A3;
thus (g . a) + (g . b) = x + (g . (f . y)) by A2, A3, A, FUNCT_2:26
.= x + y by A, FUNCT_2:26
.= g . (f . (x + y)) by A, FUNCT_2:26
.= g . (a + b) by H4, A2, A3 ; :: thesis: verum
end;
hence g is additive ; :: thesis: verum
end;
H6: g is multiplicative
proof
now :: thesis: for a, b being Element of E2 holds (g . a) * (g . b) = g . (a * b)
let a, b be Element of E2; :: thesis: (g . a) * (g . b) = g . (a * b)
consider x being object such that
A2: ( x in the carrier of E1 & a = f . x ) by C, FUNCT_2:11;
reconsider x = x as Element of E1 by A2;
consider y being object such that
A3: ( y in the carrier of E1 & b = f . y ) by C, FUNCT_2:11;
reconsider y = y as Element of E1 by A3;
thus (g . a) * (g . b) = x * (g . (f . y)) by A, A2, A3, FUNCT_2:26
.= x * y by A, FUNCT_2:26
.= g . (f . (x * y)) by A, FUNCT_2:26
.= g . (a * b) by H4, A2, A3 ; :: thesis: verum
end;
hence g is multiplicative ; :: thesis: verum
end;
F: g is unity-preserving by H4, FUNCT_2:26;
now :: thesis: for x being object holds
( x in rng g iff x in the carrier of E1 )
let x be object ; :: thesis: ( x in rng g iff x in the carrier of E1 )
H7: now :: thesis: ( x in rng g implies x in the carrier of E1 )
assume H8: x in rng g ; :: thesis: x in the carrier of E1
rng g c= the carrier of E1 by RELAT_1:def 19;
hence x in the carrier of E1 by H8; :: thesis: verum
end;
now :: thesis: ( x in the carrier of E1 implies x in rng g )
assume x in the carrier of E1 ; :: thesis: x in rng g
then reconsider x1 = x as Element of E1 ;
f . x1 in the carrier of E2 ;
then A9: f . x1 in dom g by FUNCT_2:def 1;
g . (f . x1) = x1 by A, FUNCT_2:26;
hence x in rng g by A9, FUNCT_1:def 3; :: thesis: verum
end;
hence ( x in rng g iff x in the carrier of E1 ) by H7; :: thesis: verum
end;
then g is onto by TARSKI:2;
then g is F -isomorphism by D, F, H5, H6;
hence E2,E1 are_isomorphic_over F ; :: thesis: verum