let R be Ring; :: thesis: for I being Ideal of R holds
( I is quasi-prime iff R / I is domRing-like )
let I be Ideal of R; :: thesis: ( I is quasi-prime iff R / I is domRing-like )
set E = EqRel R,I;
A1:
Class (EqRel R,I),(0. R) = 0. (R / I)
by Def6;
thus
( I is quasi-prime implies R / I is domRing-like )
:: thesis: ( R / I is domRing-like implies I is quasi-prime )proof
assume A2:
I is
quasi-prime
;
:: thesis: R / I is domRing-like
let x,
y be
Element of
(R / I);
:: according to VECTSP_2:def 5 :: thesis: ( not x * y = 0. (R / I) or x = 0. (R / I) or y = 0. (R / I) )
assume A3:
x * y = 0. (R / I)
;
:: thesis: ( x = 0. (R / I) or y = 0. (R / I) )
consider a being
Element of
R such that A4:
x = Class (EqRel R,I),
a
by Th11;
consider b being
Element of
R such that A5:
y = Class (EqRel R,I),
b
by Th11;
A6:
(a * b) - (0. R) = a * b
by RLVECT_1:26;
A7:
(
a - (0. R) = a &
b - (0. R) = b )
by RLVECT_1:26;
x * y = Class (EqRel R,I),
(a * b)
by A4, A5, Th14;
then
(a * b) - (0. R) in I
by A1, A3, Th6;
then
(
a in I or
b in I )
by A2, A6, Def1;
hence
(
x = 0. (R / I) or
y = 0. (R / I) )
by A1, A4, A5, A7, Th6;
:: thesis: verum
end;
assume A8:
R / I is domRing-like
; :: thesis: I is quasi-prime
let a, b be Element of R; :: according to RING_1:def 1 :: thesis: ( not a * b in I or a in I or b in I )
reconsider x = Class (EqRel R,I),a, y = Class (EqRel R,I),b as Element of (R / I) by Th12;
assume A9:
a * b in I
; :: thesis: ( a in I or b in I )
(a * b) - (0. R) = a * b
by RLVECT_1:26;
then A10:
Class (EqRel R,I),(a * b) = Class (EqRel R,I),(0. R)
by A9, Th6;
Class (EqRel R,I),(a * b) = x * y
by Th14;
then
( x = 0. (R / I) or y = 0. (R / I) )
by A1, A8, A10, VECTSP_2:def 5;
then
( a - (0. R) in I or b - (0. R) in I )
by A1, Th6;
hence
( a in I or b in I )
by RLVECT_1:26; :: thesis: verum