let A be non degenerated commutative Ring; :: thesis: for p being Element of Spectrum A holds
( A ~ p is local & Loc-Ideal p is maximal Ideal of (A ~ p) )
let p be Element of Spectrum A; :: thesis: ( A ~ p is local & Loc-Ideal p is maximal Ideal of (A ~ p) )
reconsider J = Loc-Ideal p as proper Ideal of (A ~ p) by Th53;
A1: A ~ p is local
proof
( ( for x being object st x in ([#] (A ~ p)) \ J holds
x is Unit of (A ~ p) ) implies A ~ p is local ) by TOPZARI1:13;
hence A ~ p is local by Th54; :: thesis: verum
end;
J is maximal Ideal of (A ~ p)
proof
consider m being maximal Ideal of (A ~ p) such that
A3: J c= m by TOPZARI1:8;
for o being object st o in m holds
o in J
proof
let o be object ; :: thesis: ( o in m implies o in J )
assume A4: o in m ; :: thesis: o in J
then A5: o is NonUnit of (A ~ p) by TOPZARI1:11;
per cases ( o in m \ J or not o in m \ J ) ;
suppose o in m \ J ; :: thesis: o in J
then A7: ( o in m & not o in J ) by XBOOLE_0:def 5;
o in ([#] (A ~ p)) \ J by A7, XBOOLE_0:def 5;
hence o in J by A5, Th54; :: thesis: verum
end;
end;
end;
then m c= J ;
hence J is maximal Ideal of (A ~ p) by A3, XBOOLE_0:def 10; :: thesis: verum
end;
hence ( A ~ p is local & Loc-Ideal p is maximal Ideal of (A ~ p) ) by A1; :: thesis: verum