let A be non degenerated commutative Ring; for f being Element of A
for J being proper Ideal of A st not f in sqrt J holds
ex m being prime Ideal of A st
( not f in m & J c= m )
let f be Element of A; for J being proper Ideal of A st not f in sqrt J holds
ex m being prime Ideal of A st
( not f in m & J c= m )
let J be proper Ideal of A; ( not f in sqrt J implies ex m being prime Ideal of A st
( not f in m & J c= m ) )
assume A1:
not f in sqrt J
; ex m being prime Ideal of A st
( not f in m & J c= m )
set S = Ideals (A,J,f);
set P = RelIncl (Ideals (A,J,f));
A2:
field (RelIncl (Ideals (A,J,f))) = Ideals (A,J,f)
by WELLORD2:def 1;
RelIncl (Ideals (A,J,f)) partially_orders Ideals (A,J,f)
by WELLORD2:19, WELLORD2:21, WELLORD2:20;
then consider I being set such that
A3:
I is_maximal_in RelIncl (Ideals (A,J,f))
by A1, A2, Th8, ORDERS_1:63;
I in Ideals (A,J,f)
by WELLORD2:def 1, A3;
then consider p being Subset of A such that
A4:
p = I
and
A6:
p is proper Ideal of A
and
A7:
J c= p
and
A8:
p /\ (multClSet (J,f)) = {}
;
f |^ 1 = f
by BINOM:8;
then
f in multClSet (J,f)
;
then A11:
not f in p
by A8, XBOOLE_0:def 4;
p is quasi-prime Ideal of A
proof
for
x,
y being
Element of
A st not
x in p & not
y in p holds
not
x * y in p
proof
let x,
y be
Element of
A;
( not x in p & not y in p implies not x * y in p )
assume that A12:
not
x in p
and A13:
not
y in p
;
not x * y in p
assume A14:
x * y in p
;
contradiction
A15:
p c< p + ({x} -Ideal)
A17:
p c< p + ({y} -Ideal)
set J2 =
p + ({x} -Ideal);
A19:
not
p + ({x} -Ideal) in Ideals (
A,
J,
f)
proof
assume A20:
p + ({x} -Ideal) in Ideals (
A,
J,
f)
;
contradiction
then A21:
p + ({x} -Ideal) in field (RelIncl (Ideals (A,J,f)))
by WELLORD2:def 1;
(
p + ({x} -Ideal) <> I &
[I,(p + ({x} -Ideal))] in RelIncl (Ideals (A,J,f)) )
by A2, A3, A4, A15, A20, WELLORD2:def 1;
hence
contradiction
by A3, A21;
verum
end;
A22:
not
p + ({y} -Ideal) in Ideals (
A,
J,
f)
proof
assume A23:
p + ({y} -Ideal) in Ideals (
A,
J,
f)
;
contradiction
set J2 =
p + ({y} -Ideal);
A24:
p + ({y} -Ideal) in field (RelIncl (Ideals (A,J,f)))
by WELLORD2:def 1, A23;
(
p + ({y} -Ideal) <> I &
[I,(p + ({y} -Ideal))] in RelIncl (Ideals (A,J,f)) )
by A2, A3, A4, A17, A23, WELLORD2:def 1;
hence
contradiction
by A3, A24;
verum
end;
reconsider q =
p + ({x} -Ideal) as
Subset of
A ;
A26:
p c= p + ({x} -Ideal)
by A6, IDEAL_1:73;
A27:
( not
q is
proper Ideal of
A or not
J c= q or not
q /\ (multClSet (J,f)) = {} )
by A19;
A28:
ex
n being
Nat st
f |^ n in p + ({x} -Ideal)
reconsider q =
p + ({y} -Ideal) as
Subset of
A ;
p c= p + ({y} -Ideal)
by A6, IDEAL_1:73;
then A36:
J c= q
by A7;
A37:
ex
m being
Nat st
f |^ m in p + ({y} -Ideal)
reconsider p =
p as
Ideal of
A by A6;
consider n being
Nat such that A43:
f |^ n in p + ({x} -Ideal)
by A28;
consider m being
Nat such that A44:
f |^ m in p + ({y} -Ideal)
by A37;
f |^ n in { (a + b) where a, b is Element of A : ( a in p & b in {x} -Ideal ) }
by A43, IDEAL_1:def 19;
then consider p1,
x1 being
Element of
A such that A45:
f |^ n = p1 + x1
and A46:
p1 in p
and A47:
x1 in {x} -Ideal
;
f |^ m in { (a + b) where a, b is Element of A : ( a in p & b in {y} -Ideal ) }
by A44, IDEAL_1:def 19;
then consider p2,
y2 being
Element of
A such that A48:
f |^ m = p2 + y2
and A49:
p2 in p
and A50:
y2 in {y} -Ideal
;
x1 in { (x * a) where a is Element of A : verum }
by A47, IDEAL_1:64;
then consider a being
Element of
A such that A51:
x1 = x * a
;
y2 in { (y * a) where a is Element of A : verum }
by A50, IDEAL_1:64;
then consider b being
Element of
A such that A52:
y2 = y * b
;
A53:
((p1 + x1) * p2) + (p1 * y2) in p
A56a:
x1 * y2 in {(x * y)} -Ideal
A59:
f |^ (n + m) =
(f |^ n) * (f |^ m)
by BINOM:10
.=
((p1 + x1) * p2) + ((p1 + x1) * y2)
by VECTSP_1:def 7, A45, A48
.=
((p1 + x1) * p2) + ((p1 * y2) + (x1 * y2))
by VECTSP_1:def 7
.=
(((p1 + x1) * p2) + (p1 * y2)) + (x1 * y2)
by RLVECT_1:def 3
;
reconsider s =
((p1 + x1) * p2) + (p1 * y2),
t =
x1 * y2 as
Element of
A ;
s + t in { (u + v) where u, v is Element of A : ( u in p & v in {(x * y)} -Ideal ) }
by A53, A56a;
then A61:
f |^ (n + m) in p + ({(x * y)} -Ideal)
by A59, IDEAL_1:def 19;
reconsider n1 =
n + m as
Nat ;
A63:
f |^ (n + m) in multClSet (
J,
f)
;
A64:
not
p + ({(x * y)} -Ideal) in Ideals (
A,
J,
f)
p -Ideal = p
by IDEAL_1:44;
then
{(x * y)} -Ideal c= p
by IDEAL_1:67, A14;
then
p = p + ({(x * y)} -Ideal)
by IDEAL_1:74, IDEAL_1:75;
hence
contradiction
by A3, A4, A64, WELLORD2:def 1;
verum
end;
then
for
a,
b being
Element of
A holds
( not
a * b in p or
a in p or
b in p )
;
hence
p is
quasi-prime Ideal of
A
by A6, RING_1:def 1;
verum
end;
hence
ex m being prime Ideal of A st
( not f in m & J c= m )
by A6, A7, A11; verum