let A be non degenerated commutative Ring; :: thesis: for p being Element of Spectrum A
for x being object st x in ([#] (A ~ p)) \ (Loc-Ideal p) holds
x is Unit of (A ~ p)
let p be Element of Spectrum A; :: thesis: for x being object st x in ([#] (A ~ p)) \ (Loc-Ideal p) holds
x is Unit of (A ~ p)
let x be object ; :: thesis: ( x in ([#] (A ~ p)) \ (Loc-Ideal p) implies x is Unit of (A ~ p) )
assume A1: x in ([#] (A ~ p)) \ (Loc-Ideal p) ; :: thesis: x is Unit of (A ~ p)
then consider a being Element of Frac (Loc (A,p)) such that
A2: x = Class ((EqRel (Loc (A,p))),a) by Th32;
a in Frac (Loc (A,p)) ;
then a in [:([#] A),(Loc (A,p)):] by Th15;
then A3: ( a `1 in [#] A & a `2 in Loc (A,p) ) by MCART_1:10;
per cases ( a `1 in ([#] A) \ p or not a `1 in ([#] A) \ p ) ;
suppose A4: a `1 in ([#] A) \ p ; :: thesis: x is Unit of (A ~ p)
reconsider b = [(a `1),(a `2)] as Element of Frac (Loc (A,p)) ;
thus x is Unit of (A ~ p) by A4, A2, Lm45; :: thesis: verum
end;
suppose not a `1 in ([#] A) \ p ; :: thesis: x is Unit of (A ~ p)
then A7: a `1 in p by XBOOLE_0:def 5;
reconsider b = [(a `1),(a `2)] as Element of Frac (Loc (A,p)) ;
reconsider y = x as Element of (A ~ p) by A1;
A8: b in [:p,(Loc (A,p)):] by A3, A7, ZFMISC_1:87;
y = Class ((EqRel (Loc (A,p))),b) by A2;
then x in Loc-Ideal p by A8;
hence x is Unit of (A ~ p) by A1, XBOOLE_0:def 5; :: thesis: verum
end;
end;