let A be non degenerated commutative Ring; for m being maximal Ideal of A st ( for a being Element of A st a in m holds
(1. A) + a is Unit of A ) holds
A is local
let m be maximal Ideal of A; ( ( for a being Element of A st a in m holds
(1. A) + a is Unit of A ) implies A is local )
assume A1:
for a being Element of A st a in m holds
(1. A) + a is Unit of A
; A is local
for x being object st x in ([#] A) \ m holds
x is Unit of A
proof
let x be
object ;
( x in ([#] A) \ m implies x is Unit of A )
assume A2:
x in ([#] A) \ m
;
x is Unit of A
then reconsider a0 =
x as
Element of
A ;
({a0} -Ideal) + m = [#] A
by A2, Th18;
then
1. A in ({a0} -Ideal) + m
;
then
1. A in { (p + q) where p, q is Element of A : ( p in {a0} -Ideal & q in m ) }
by IDEAL_1:def 19;
then consider p,
q being
Element of
A such that A3:
1. A = p + q
and A4:
p in {a0} -Ideal
and A5:
q in m
;
A6:
{a0} -Ideal = { (a0 * s) where s is Element of A : verum }
by IDEAL_1:64;
consider s being
Element of
A such that A7:
p = a0 * s
by A4, A6;
(1. A) + (- q) =
(a0 * s) + ((- q) + q)
by RLVECT_1:def 3, A3, A7
.=
(a0 * s) + (0. A)
by RLVECT_1:5
.=
a0 * s
;
then
a0 * s is
Unit of
A
by A1, A5, IDEAL_1:13;
then
{(a0 * s)} -Ideal = [#] A
by RING_2:20;
then A9:
1. A in {(a0 * s)} -Ideal
;
{(a0 * s)} -Ideal = { ((a0 * s) * t) where t is Element of A : verum }
by IDEAL_1:64;
then consider t1 being
Element of
A such that A11:
1. A = (a0 * s) * t1
by A9;
A12:
a0 * (s * t1) = 1. A
by A11, GROUP_1:def 3;
reconsider t =
s * t1 as
Element of
A ;
1. A in {a0} -Ideal
by A6, A12;
then
not
{a0} -Ideal is
proper
by IDEAL_1:19;
then
{a0} -Ideal = [#] A
;
hence
x is
Unit of
A
by RING_2:20;
verum
end;
hence
A is local
by Th17; verum