let A be non degenerated commutative Ring; for p being Element of Spectrum A holds Loc-Ideal p is proper Ideal of (A ~ p)
let p be Element of Spectrum A; Loc-Ideal p is proper Ideal of (A ~ p)
reconsider M = Loc-Ideal p as Subset of (A ~ p) ;
A1:
for m, n being Element of (A ~ p) st m in M & n in M holds
m + n in M
proof
let m,
n be
Element of
(A ~ p);
( m in M & n in M implies m + n in M )
assume that A2:
m in M
and A3:
n in M
;
m + n in M
consider y1 being
Element of
(A ~ p) such that A4:
y1 = m
and A5:
ex
a being
Element of
Frac (Loc (A,p)) st
(
a in [:p,(Loc (A,p)):] &
y1 = Class (
(EqRel (Loc (A,p))),
a) )
by A2;
consider y2 being
Element of
(A ~ p) such that A6:
y2 = n
and A7:
ex
a being
Element of
Frac (Loc (A,p)) st
(
a in [:p,(Loc (A,p)):] &
y2 = Class (
(EqRel (Loc (A,p))),
a) )
by A3;
consider a1 being
Element of
Frac (Loc (A,p)) such that A8:
a1 in [:p,(Loc (A,p)):]
and A9:
y1 = Class (
(EqRel (Loc (A,p))),
a1)
by A5;
consider a2 being
Element of
Frac (Loc (A,p)) such that A10:
a2 in [:p,(Loc (A,p)):]
and A11:
y2 = Class (
(EqRel (Loc (A,p))),
a2)
by A7;
A12:
(
a1 `1 in p &
a2 `1 in p )
by A8, A10, MCART_1:10;
(
a1 `2 in Loc (
A,
p) &
a2 `2 in Loc (
A,
p) )
by A8, A10, MCART_1:10;
then A17:
(a1 `2) * (a2 `2) in Loc (
A,
p)
by C0SP1:def 4;
A14:
p is
prime Ideal of
A
by Lm5;
then A15:
(a1 `1) * (a2 `2) in p
by A12, IDEAL_1:def 3;
(a2 `1) * (a1 `2) in p
by A12, A14, IDEAL_1:def 2;
then A16:
((a1 `1) * (a2 `2)) + ((a2 `1) * (a1 `2)) in p
by A14, A15, IDEAL_1:def 1;
reconsider a3 =
a1 + a2 as
Element of
Frac (Loc (A,p)) ;
A18:
a3 in [:p,(Loc (A,p)):]
by A16, A17, ZFMISC_1:87;
reconsider y3 =
y1 + y2 as
Element of
(A ~ p) ;
y3 = Class (
(EqRel (Loc (A,p))),
a3)
by A9, A11, Th35;
hence
m + n in M
by A4, A6, A18;
verum
end;
for x, m being Element of (A ~ p) st m in M holds
x * m in M
proof
let x,
m be
Element of
(A ~ p);
( m in M implies x * m in M )
assume
m in M
;
x * m in M
then consider y1 being
Element of
(A ~ p) such that A20:
y1 = m
and A21:
ex
a being
Element of
Frac (Loc (A,p)) st
(
a in [:p,(Loc (A,p)):] &
y1 = Class (
(EqRel (Loc (A,p))),
a) )
;
consider a1 being
Element of
Frac (Loc (A,p)) such that A22:
a1 in [:p,(Loc (A,p)):]
and A23:
y1 = Class (
(EqRel (Loc (A,p))),
a1)
by A21;
consider b being
Element of
Frac (Loc (A,p)) such that A24:
x = Class (
(EqRel (Loc (A,p))),
b)
by Th32;
A25:
(
a1 `1 in p &
a1 `2 in Loc (
A,
p) )
by A22, MCART_1:10;
b in Frac (Loc (A,p))
;
then
b in [:([#] A),(Loc (A,p)):]
by Th15;
then
(
b `1 in [#] A &
b `2 in Loc (
A,
p) )
by MCART_1:10;
then A28:
(b `2) * (a1 `2) in Loc (
A,
p)
by A25, C0SP1:def 4;
reconsider ba1 =
b * a1 as
Element of
Frac (Loc (A,p)) ;
p is
prime Ideal of
A
by Lm5;
then
(b `1) * (a1 `1) in p
by A22, MCART_1:10, IDEAL_1:def 2;
then A29:
ba1 in [:p,(Loc (A,p)):]
by A28, ZFMISC_1:87;
reconsider xy =
x * y1 as
Element of
(A ~ p) ;
xy = Class (
(EqRel (Loc (A,p))),
ba1)
by A23, A24, Th33;
hence
x * m in M
by A20, A29;
verum
end;
then A31:
M is left-ideal
by IDEAL_1:def 2;
M is proper
proof
assume
not
M is
proper
;
contradiction
then
1. (A ~ p) in M
by A31, IDEAL_1:19;
then consider y1 being
Element of
(A ~ p) such that A34:
y1 = 1. (A ~ p)
and A35:
ex
a being
Element of
Frac (Loc (A,p)) st
(
a in [:p,(Loc (A,p)):] &
y1 = Class (
(EqRel (Loc (A,p))),
a) )
;
consider a being
Element of
Frac (Loc (A,p)) such that A36:
a in [:p,(Loc (A,p)):]
and A37:
y1 = Class (
(EqRel (Loc (A,p))),
a)
by A35;
A38:
(frac1 (Loc (A,p))) . (1. A) = [(1. A),(1. A)]
by Def4;
Class (
(EqRel (Loc (A,p))),
a)
= Class (
(EqRel (Loc (A,p))),
((frac1 (Loc (A,p))) . (1. A)))
by A34, A37, Lm43;
then A39:
a,
(frac1 (Loc (A,p))) . (1. A) Fr_Eq Loc (
A,
p)
by Th26;
reconsider y =
(frac1 (Loc (A,p))) . (1. A) as
Element of
Frac (Loc (A,p)) ;
consider s1 being
Element of
A such that A40:
s1 in Loc (
A,
p)
and A41:
(((a `1) * (y `2)) - ((y `1) * (a `2))) * s1 = 0. A
by A39;
0. A = ((a `1) * s1) - ((a `2) * s1)
by A38, A41, VECTSP_1:13;
then A42:
(a `1) * s1 = (a `2) * s1
by VECTSP_1:27;
A43:
(
a `1 in p &
a `2 in Loc (
A,
p) )
by A36, MCART_1:10;
p is
prime Ideal of
A
by Lm5;
then A44:
(a `1) * s1 in p
by A36, MCART_1:10, IDEAL_1:def 2;
(a `2) * s1 in Loc (
A,
p)
by A40, A43, C0SP1:def 4;
hence
contradiction
by A42, A44, XBOOLE_0:def 5;
verum
end;
hence
Loc-Ideal p is proper Ideal of (A ~ p)
by A1, A31, IDEAL_1:def 1; verum