let K, L be Field; :: thesis: for z being Element of L st K is Subring of L & z is_integral_over K holds
ex f being Element of (Polynom-Ring K) st
( f <> 0_. K & {f} -Ideal = Ann_Poly (z,K) & f = NormPolynomial f )
let z be Element of L; :: thesis: ( K is Subring of L & z is_integral_over K implies ex f being Element of (Polynom-Ring K) st
( f <> 0_. K & {f} -Ideal = Ann_Poly (z,K) & f = NormPolynomial f ) )
assume that
A0: K is Subring of L and
A1: z is_integral_over K ; :: thesis: ex f being Element of (Polynom-Ring K) st
( f <> 0_. K & {f} -Ideal = Ann_Poly (z,K) & f = NormPolynomial f )
consider f being Element of (Polynom-Ring K) such that
A2: {f} -Ideal = Ann_Poly (z,K) by A0, Th34;
A3: f <> 0. (Polynom-Ring K) by A1, A2, Th35, IDEAL_1:47;
reconsider f = f as Element of (Polynom-Ring K) ;
A4: f <> 0_. K by A3, POLYNOM3:def 10;
set g = NormPolynomial f;
A7: {(NormPolynomial f)} -Ideal = Ann_Poly (z,K) by A2, RING_4:27, RING_2:21;
NormPolynomial f <> 0. (Polynom-Ring K) by A1, A7, Th35, IDEAL_1:47;
then A8: NormPolynomial f <> 0_. K by POLYNOM3:def 10;
then A9: NormPolynomial f is non zero Element of the carrier of (Polynom-Ring K) by Lm37;
A10: f is non zero Element of the carrier of (Polynom-Ring K) by A4, Lm37;
NormPolynomial f = NormPolynomial (NormPolynomial f) by A9, A10, RING_4:24;
hence ex f being Element of (Polynom-Ring K) st
( f <> 0_. K & {f} -Ideal = Ann_Poly (z,K) & f = NormPolynomial f ) by A7, A8; :: thesis: verum