let B be Ring; :: thesis: for A being non degenerated Ring
for a being Element of A st A is Subring of B holds
In (a,B) is_integral_over A
let A be non degenerated Ring; :: thesis: for a being Element of A st A is Subring of B holds
In (a,B) is_integral_over A
let a be Element of A; :: thesis: ( A is Subring of B implies In (a,B) is_integral_over A )
assume A0: A is Subring of B ; :: thesis: In (a,B) is_integral_over A
set p = <%(- a),(1. A)%>;
<%(- a),(1. A)%> . ((len <%(- a),(1. A)%>) -' 1) = <%(- a),(1. A)%> . (2 -' 1) by POLYNOM5:40
.= <%(- a),(1. A)%> . (2 - 1) by XREAL_1:233
.= <%(- a),(1. A)%> . 1 ;
then A2: LC <%(- a),(1. A)%> = 1. A by POLYNOM5:38;
A3: eval (<%(- a),(1. A)%>,a) = (- a) + a by POLYNOM5:47
.= a - a
.= 0. A by RLVECT_1:15 ;
Ext_eval (<%(- a),(1. A)%>,(In (a,B))) = In ((eval (<%(- a),(1. A)%>,a)),B) by A0, Th16
.= 0. B by A0, Lm5, A3 ;
hence In (a,B) is_integral_over A by A2; :: thesis: verum