let R be Ring; :: thesis: for S being R -homomorphic R -isomorphic Ring
for h being Isomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for b being Element of S holds
( b is_a_root_of (PolyHom h) . p iff ex a being Element of R st
( a is_a_root_of p & h . a = b ) )
let S be R -homomorphic R -isomorphic Ring; :: thesis: for h being Isomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for b being Element of S holds
( b is_a_root_of (PolyHom h) . p iff ex a being Element of R st
( a is_a_root_of p & h . a = b ) )
let h be Isomorphism of R,S; :: thesis: for p being Element of the carrier of (Polynom-Ring R)
for b being Element of S holds
( b is_a_root_of (PolyHom h) . p iff ex a being Element of R st
( a is_a_root_of p & h . a = b ) )
let p be Element of the carrier of (Polynom-Ring R); :: thesis: for b being Element of S holds
( b is_a_root_of (PolyHom h) . p iff ex a being Element of R st
( a is_a_root_of p & h . a = b ) )
let b be Element of S; :: thesis: ( b is_a_root_of (PolyHom h) . p iff ex a being Element of R st
( a is_a_root_of p & h . a = b ) )
A1: now :: thesis: ( b is_a_root_of (PolyHom h) . p implies ex a being Element of R st
( h . a = b & a is_a_root_of p ) )
assume A2: b is_a_root_of (PolyHom h) . p ; :: thesis: ex a being Element of R st
( h . a = b & a is_a_root_of p )
set a = (h ") . b;
A3: dom (h ") = the carrier of S by FUNCT_2:def 1;
A4: h . ((h ") . b) = ((h ") ") . ((h ") . b)
.= b by A3, FUNCT_1:34 ;
h . (eval (p,((h ") . b))) = eval (((PolyHom h) . p),(h . ((h ") . b))) by Th28
.= 0. S by A4, A2, POLYNOM5:def 7
.= h . (0. R) by RING_2:6 ;
then eval (p,((h ") . b)) = 0. R by FUNCT_2:19;
hence ex a being Element of R st
( h . a = b & a is_a_root_of p ) by A4, POLYNOM5:def 7; :: thesis: verum
end;
now :: thesis: ( ex a being Element of R st
( h . a = b & a is_a_root_of p ) implies b is_a_root_of (PolyHom h) . p )
assume ex a being Element of R st
( h . a = b & a is_a_root_of p ) ; :: thesis: b is_a_root_of (PolyHom h) . p
then consider a being Element of R such that
A5: ( h . a = b & a is_a_root_of p ) ;
eval (((PolyHom h) . p),b) = h . (eval (p,a)) by A5, Th28
.= h . (0. R) by A5, POLYNOM5:def 7
.= 0. S by RING_2:6 ;
hence b is_a_root_of (PolyHom h) . p by POLYNOM5:def 7; :: thesis: verum
end;
hence ( b is_a_root_of (PolyHom h) . p iff ex a being Element of R st
( a is_a_root_of p & h . a = b ) ) by A1; :: thesis: verum