let F1 be Field; :: thesis: for F2 being F1 -homomorphic F1 -isomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
(Psi (a,b,h,p)) . a = b
let F2 be F1 -homomorphic F1 -isomorphic Field; :: thesis: for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
(Psi (a,b,h,p)) . a = b
let h be Isomorphism of F1,F2; :: thesis: for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
(Psi (a,b,h,p)) . a = b
let E1 be FieldExtension of F1; :: thesis: for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
(Psi (a,b,h,p)) . a = b
let E2 be FieldExtension of F2; :: thesis: for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
(Psi (a,b,h,p)) . a = b
let a be Element of E1; :: thesis: for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
(Psi (a,b,h,p)) . a = b
let b be Element of E2; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
(Psi (a,b,h,p)) . a = b
let p be irreducible Element of the carrier of (Polynom-Ring F1); :: thesis: ( Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 implies (Psi (a,b,h,p)) . a = b )
assume AS: ( Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 ) ; :: thesis: (Psi (a,b,h,p)) . a = b
F1 is Subfield of E1 by FIELD_4:7;
then I1: 0. E1 = 0. F1 by EC_PF_1:def 1;
H1: X- (0. F1) = rpoly (1,(0. F1)) by FIELD_9:def 2
.= rpoly (1,(0. E1)) by I1, FIELD_4:21
.= X- (0. E1) by FIELD_9:def 2 ;
F2 is Subfield of E2 by FIELD_4:7;
then I2: 0. E2 = 0. F2 by EC_PF_1:def 1;
H2: X- (0. F2) = rpoly (1,(0. F2)) by FIELD_9:def 2
.= rpoly (1,(0. E2)) by I2, FIELD_4:21
.= X- (0. E2) by FIELD_9:def 2 ;
A: (PolyHom h) . (X- (0. F1)) = X- (h . (0. F1)) by lemNor3d
.= X- (0. F2) by RING_2:6 ;
B: Ext_eval ((X- (0. F1)),a) = eval ((X- (0. E1)),a) by H1, FIELD_4:26
.= eval ((rpoly (1,(0. E1))),a) by FIELD_9:def 2
.= a - (0. E1) by HURWITZ:29 ;
(Psi (a,b,h,p)) . (Ext_eval ((X- (0. F1)),a)) = Ext_eval ((X- (0. F2)),b) by A, AS, FIELD_8:def 10
.= eval ((X- (0. E2)),b) by H2, FIELD_4:26
.= eval ((rpoly (1,(0. E2))),b) by FIELD_9:def 2
.= b - (0. E2) by HURWITZ:29 ;
hence (Psi (a,b,h,p)) . a = b by B; :: thesis: verum