let A be non degenerated commutative Ring; for I being Ideal of A holds
( I <> [#] A & ( for x, y being Element of A st x * y in I & not x in I holds
y in sqrt I ) iff ( not A / I is degenerated & ( for z being Element of (A / I) st z is zero_divisible holds
z is nilpotent ) ) )
let I be Ideal of A; ( I <> [#] A & ( for x, y being Element of A st x * y in I & not x in I holds
y in sqrt I ) iff ( not A / I is degenerated & ( for z being Element of (A / I) st z is zero_divisible holds
z is nilpotent ) ) )
A1:
( I <> [#] A & ( for x, y being Element of A st x * y in I & not x in I holds
y in sqrt I ) implies ( not A / I is degenerated & ( for z being Element of (A / I) st z is zero_divisible holds
z is nilpotent ) ) )
proof
assume A2:
(
I <> [#] A & ( for
x,
y being
Element of
A st
x * y in I & not
x in I holds
y in sqrt I ) )
;
( not A / I is degenerated & ( for z being Element of (A / I) st z is zero_divisible holds
z is nilpotent ) )
A3:
I is
proper
by A2;
for
z being
Element of
(A / I) st
z is
zero_divisible holds
z is
nilpotent
proof
let z be
Element of
(A / I);
( z is zero_divisible implies z is nilpotent )
assume
z is
zero_divisible
;
z is nilpotent
then consider y being
Element of
(A / I) such that A5:
(
y <> 0. (A / I) &
y * z = 0. (A / I) )
;
consider z0 being
Element of
A such that A6:
z = Class (
(EqRel (A,I)),
z0)
by RING_1:11;
consider y0 being
Element of
A such that A7:
y = Class (
(EqRel (A,I)),
y0)
by RING_1:11;
A8:
not
y0 in I
Class (
(EqRel (A,I)),
(0. A)) =
0. (A / I)
by RING_1:def 6
.=
Class (
(EqRel (A,I)),
(y0 * z0))
by A5, A6, A7, RING_1:14
;
then
(y0 * z0) - (0. A) in I
by RING_1:6;
then A12:
z0 in sqrt I
by A8, A2;
z0 in { a where a is Element of A : ex n being Element of NAT st a |^ n in I }
by A12, IDEAL_1:def 24;
then consider z1 being
Element of
A such that A13:
z1 = z0
and A14:
ex
n being
Element of
NAT st
z1 |^ n in I
;
consider n1 being
Element of
NAT such that A15:
z1 |^ n1 in I
by A14;
(z0 |^ n1) - (0. A) in I
by A15, A13;
then A16:
Class (
(EqRel (A,I)),
(z0 |^ n1)) =
Class (
(EqRel (A,I)),
(0. A))
by RING_1:6
.=
0. (A / I)
by RING_1:def 6
;
n1 <> 0
then reconsider n1 =
n1 as non
zero Nat ;
z |^ n1 = 0. (A / I)
by A16, A6, FIELD_1:2;
hence
z is
nilpotent
;
verum
end;
hence
( not
A / I is
degenerated & ( for
z being
Element of
(A / I) st
z is
zero_divisible holds
z is
nilpotent ) )
by A3;
verum
end;
( not A / I is degenerated & ( for z being Element of (A / I) st z is zero_divisible holds
z is nilpotent ) implies ( I <> [#] A & ( for x1, y1 being Element of A st x1 * y1 in I & not x1 in I holds
y1 in sqrt I ) ) )
proof
assume A19:
( not
A / I is
degenerated & ( for
z being
Element of
(A / I) st
z is
zero_divisible holds
z is
nilpotent ) )
;
( I <> [#] A & ( for x1, y1 being Element of A st x1 * y1 in I & not x1 in I holds
y1 in sqrt I ) )
for
x1,
y1 being
Element of
A st
x1 * y1 in I & not
x1 in I holds
y1 in sqrt I
proof
let x1,
y1 be
Element of
A;
( x1 * y1 in I & not x1 in I implies y1 in sqrt I )
assume A20:
(
x1 * y1 in I & not
x1 in I )
;
y1 in sqrt I
then A21:
(y1 * x1) - (0. A) in I
;
reconsider z =
Class (
(EqRel (A,I)),
x1) as
Element of
(A / I) by RING_1:12;
reconsider y =
Class (
(EqRel (A,I)),
y1) as
Element of
(A / I) by RING_1:12;
A22:
z <> 0. (A / I)
y * z =
Class (
(EqRel (A,I)),
(y1 * x1))
by RING_1:14
.=
Class (
(EqRel (A,I)),
(0. A))
by A21, RING_1:6
.=
0. (A / I)
by RING_1:def 6
;
then
y is
zero_divisible
by A22;
then
y is
nilpotent
by A19;
then consider n being non
zero Nat such that A25:
y |^ n = 0. (A / I)
;
Class (
(EqRel (A,I)),
(y1 |^ n)) =
0. (A / I)
by A25, FIELD_1:2
.=
Class (
(EqRel (A,I)),
(0. A))
by RING_1:def 6
;
then A26:
(y1 |^ n) - (0. A) in I
by RING_1:6;
reconsider n1 =
n as
Element of
NAT by ORDINAL1:def 12;
reconsider I =
I as
Subset of
A ;
y1 |^ n1 in I
by A26;
then
y1 in { a where a is Element of A : ex n being Element of NAT st a |^ n in I }
;
hence
y1 in sqrt I
by IDEAL_1:def 24;
verum
end;
hence
(
I <> [#] A & ( for
x1,
y1 being
Element of
A st
x1 * y1 in I & not
x1 in I holds
y1 in sqrt I ) )
by A19;
verum
end;
hence
( I <> [#] A & ( for x, y being Element of A st x * y in I & not x in I holds
y in sqrt I ) iff ( not A / I is degenerated & ( for z being Element of (A / I) st z is zero_divisible holds
z is nilpotent ) ) )
by A1; verum