let R be Ring; :: thesis: for S being Subring of R
for r being Element of R
for s being Element of S st r = s & s is_integral_over S holds
r is_integral_over R
let S be Subring of R; :: thesis: for r being Element of R
for s being Element of S st r = s & s is_integral_over S holds
r is_integral_over R
let r be Element of R; :: thesis: for s being Element of S st r = s & s is_integral_over S holds
r is_integral_over R
let s be Element of S; :: thesis: ( r = s & s is_integral_over S implies r is_integral_over R )
assume A1: r = s ; :: thesis: ( not s is_integral_over S or r is_integral_over R )
given f being Polynomial of S such that A2: LC f = 1. S and
A3: Ext_eval (f,s) = 0. S ; :: according to ALGNUM_1:def 2 :: thesis: r is_integral_over R
reconsider f1 = f as Polynomial of R by Th8;
take f1 ; :: according to ALGNUM_1:def 2 :: thesis: ( Leading-Coefficient f1 = 1. R & Ext_eval (f1,r) = 0. R )
LC f = LC f1 by Th9;
hence LC f1 = 1. R by A2, C0SP1:def 3; :: thesis: Ext_eval (f1,r) = 0. R
r = In (r,R) ;
then Ext_eval (f1,r) = Ext_eval (f,r) by Th15
.= Ext_eval (f,s) by A1, Th16 ;
hence Ext_eval (f1,r) = 0. R by A3, C0SP1:def 3; :: thesis: verum