set C1 = the carrier of (FAdj (F1,{a}));
set C2 = the carrier of (FAdj (F2,{b}));
reconsider a = a as F1 -algebraic Element of E1 by AS, FIELD_6:43;
H1: FAdj (F1,{a}) = RAdj (F1,{a}) by FIELD_6:56;
H2: the carrier of (RAdj (F1,{a})) = { (Ext_eval (p,a)) where p is Polynomial of F1 : verum } by FIELD_6:45;
reconsider b = b as F2 -algebraic Element of E2 by AS, FIELD_6:43;
H4: FAdj (F2,{b}) = RAdj (F2,{b}) by FIELD_6:56;
H5: the carrier of (RAdj (F2,{b})) = { (Ext_eval (p,b)) where p is Polynomial of F2 : verum } by FIELD_6:45;
defpred S1[ object , object ] means for r being Element of the carrier of (Polynom-Ring F1) st $1 = Ext_eval (r,a) holds
$2 = Ext_eval (((PolyHom h) . r),b);
H6: now :: thesis: for r being Element of the carrier of (Polynom-Ring F1) st Ext_eval (r,a) = 0. E1 holds
Ext_eval (((PolyHom h) . r),b) = 0. E2
let r be Element of the carrier of (Polynom-Ring F1); :: thesis: ( Ext_eval (r,a) = 0. E1 implies Ext_eval (((PolyHom h) . r),b) = 0. E2 )
X: (PolyHom h) . (MinPoly (a,F1)) = MinPoly (b,F2) by AS, x1000;
assume Ext_eval (r,a) = 0. E1 ; :: thesis: Ext_eval (((PolyHom h) . r),b) = 0. E2
then MinPoly (b,F2) divides (PolyHom h) . r by X, uu0, FIELD_6:53;
hence Ext_eval (((PolyHom h) . r),b) = 0. E2 by FIELD_6:53; :: thesis: verum
end;
H7: now :: thesis: for r1, r2 being Element of the carrier of (Polynom-Ring F1) st Ext_eval (r1,a) = Ext_eval (r2,a) holds
Ext_eval (((PolyHom h) . r1),b) = Ext_eval (((PolyHom h) . r2),b)
let r1, r2 be Element of the carrier of (Polynom-Ring F1); :: thesis: ( Ext_eval (r1,a) = Ext_eval (r2,a) implies Ext_eval (((PolyHom h) . r1),b) = Ext_eval (((PolyHom h) . r2),b) )
reconsider r1p = r1, r2p = r2 as Polynomial of F1 ;
reconsider r = r1 - r2 as Element of the carrier of (Polynom-Ring F1) ;
reconsider rp = r as Polynomial of F1 ;
X: (PolyHom h) . (r1 - r2) = ((PolyHom h) . r1) - ((PolyHom h) . r2) by RING_2:8;
reconsider q = (PolyHom h) . r, q1 = (PolyHom h) . r1, q2 = (PolyHom h) . r2 as Polynomial of F2 ;
H9: - q2 = - ((PolyHom h) . r2) by DZIW;
H8: q1 - q2 = q by X, H9, POLYNOM3:def 10;
- r2p = - r2 by DZIW;
then H10: r1 - r2 = r1p - r2p by POLYNOM3:def 10;
assume Ext_eval (r1,a) = Ext_eval (r2,a) ; :: thesis: Ext_eval (((PolyHom h) . r1),b) = Ext_eval (((PolyHom h) . r2),b)
then 0. E1 = (Ext_eval (r1p,a)) - (Ext_eval (r2p,a)) by RLVECT_1:15
.= Ext_eval (r,a) by H10, FIELD_6:27 ;
then 0. E2 = Ext_eval (((PolyHom h) . r),b) by H6
.= (Ext_eval (((PolyHom h) . r1),b)) - (Ext_eval (((PolyHom h) . r2),b)) by H8, FIELD_6:27 ;
hence Ext_eval (((PolyHom h) . r1),b) = Ext_eval (((PolyHom h) . r2),b) by RLVECT_1:21; :: thesis: verum
end;
A1: now :: thesis: for x being object st x in the carrier of (FAdj (F1,{a})) holds
ex y being object st
( y in the carrier of (FAdj (F2,{b})) & S1[x,y] )
let x be object ; :: thesis: ( x in the carrier of (FAdj (F1,{a})) implies ex y being object st
( y in the carrier of (FAdj (F2,{b})) & S1[x,y] ) )
assume x in the carrier of (FAdj (F1,{a})) ; :: thesis: ex y being object st
( y in the carrier of (FAdj (F2,{b})) & S1[x,y] )
then consider r being Polynomial of F1 such that
H8: x = Ext_eval (r,a) by H1, H2;
reconsider r = r as Element of the carrier of (Polynom-Ring F1) by POLYNOM3:def 10;
thus ex y being object st
( y in the carrier of (FAdj (F2,{b})) & S1[x,y] ) :: thesis: verum
proof
take y = Ext_eval (((PolyHom h) . r),b); :: thesis: ( y in the carrier of (FAdj (F2,{b})) & S1[x,y] )
thus y in the carrier of (FAdj (F2,{b})) by H4, H5; :: thesis: S1[x,y]
thus S1[x,y] by H7, H8; :: thesis: verum
end;
end;
consider f being Function of the carrier of (FAdj (F1,{a})), the carrier of (FAdj (F2,{b})) such that
A: for x being object st x in the carrier of (FAdj (F1,{a})) holds
S1[x,f . x] from FUNCT_2:sch 1(A1);
now :: thesis: for r being Element of the carrier of (Polynom-Ring F1) holds f . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b)
let r be Element of the carrier of (Polynom-Ring F1); :: thesis: f . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b)
Ext_eval (r,a) in the carrier of (FAdj (F1,{a})) by H1, H2;
hence f . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b) by A; :: thesis: verum
end;
hence ex b1 being Function of (FAdj (F1,{a})),(FAdj (F2,{b})) st
for r being Element of the carrier of (Polynom-Ring F1) holds b1 . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b) ; :: thesis: verum