let R be Ring; 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; 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; 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; ( r = s & s is_integral_over S implies r is_integral_over R )
assume A1:
r = s
; ( 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
; ALGNUM_1:def 2 r is_integral_over R
reconsider f1 = f as Polynomial of R by Th8;
take
f1
; ALGNUM_1:def 2 ( 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; 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; verum