let R be Ring; :: thesis: for S being R -homomorphic R -monomorphic Ring
for h being Monomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R) holds Roots p = { a where a is Element of R : h . a in Roots ((PolyHom h) . p) }
let S be R -homomorphic R -monomorphic Ring; :: thesis: for h being Monomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R) holds Roots p = { a where a is Element of R : h . a in Roots ((PolyHom h) . p) }
let h be Monomorphism of R,S; :: thesis: for p being Element of the carrier of (Polynom-Ring R) holds Roots p = { a where a is Element of R : h . a in Roots ((PolyHom h) . p) }
let p be Element of the carrier of (Polynom-Ring R); :: thesis: Roots p = { a where a is Element of R : h . a in Roots ((PolyHom h) . p) }
A1: Roots p c= { a where a is Element of R : h . a in Roots ((PolyHom h) . p) } by Th37;
now :: thesis: for o being object st o in { a where a is Element of R : h . a in Roots ((PolyHom h) . p) } holds
o in Roots p
let o be object ; :: thesis: ( o in { a where a is Element of R : h . a in Roots ((PolyHom h) . p) } implies o in Roots p )
assume o in { a where a is Element of R : h . a in Roots ((PolyHom h) . p) } ; :: thesis: o in Roots p
then consider a being Element of R such that
A2: ( o = a & h . a in Roots ((PolyHom h) . p) ) ;
h . a is_a_root_of (PolyHom h) . p by A2, POLYNOM5:def 10;
then a is_a_root_of p by Th35;
hence o in Roots p by A2, POLYNOM5:def 10; :: thesis: verum
end;
hence Roots p = { a where a is Element of R : h . a in Roots ((PolyHom h) . p) } by TARSKI:2, A1; :: thesis: verum