let R be Ring; for I being Ideal of R holds
( I is quasi-prime iff R / I is domRing-like )
let I be Ideal of R; ( 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 )
( R / I is domRing-like implies I is quasi-prime )proof
assume A2:
I is
quasi-prime
;
R / I is domRing-like
let x,
y be
Element of
(R / I);
VECTSP_2:def 1 ( not x * y = 0. (R / I) or x = 0. (R / I) or y = 0. (R / I) )
assume A3:
x * y = 0. (R / I)
;
( 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;
x * y = Class (
(EqRel (R,I)),
(a * b))
by A4, A5, Th14;
then
(
(a * b) - (0. R) = a * b &
(a * b) - (0. R) in I )
by A1, A3, Th6, RLVECT_1:13;
then A6:
(
a in I or
b in I )
by A2;
(
a - (0. R) = a &
b - (0. R) = b )
by RLVECT_1:13;
hence
(
x = 0. (R / I) or
y = 0. (R / I) )
by A1, A4, A5, A6, Th6;
verum
end;
assume A7:
R / I is domRing-like
; I is quasi-prime
let a, b be Element of R; RING_1:def 1 ( 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;
A8:
(a * b) - (0. R) = a * b
by RLVECT_1:13;
A9:
Class ((EqRel (R,I)),(a * b)) = x * y
by Th14;
assume
a * b in I
; ( a in I or b in I )
then
Class ((EqRel (R,I)),(a * b)) = Class ((EqRel (R,I)),(0. R))
by A8, Th6;
then
( x = 0. (R / I) or y = 0. (R / I) )
by A1, A7, A9;
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:13; verum