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 )

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;

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 ; :: thesis: ( 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; :: thesis: verum

( 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 A7:
R / I is domRing-like
; :: thesis: I is quasi-prime
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 1 :: 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;

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; :: thesis: verum

end;let x, y be Element of (R / I); :: according to VECTSP_2:def 1 :: 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;

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; :: thesis: verum

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;

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 ; :: thesis: ( 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; :: thesis: verum