let R be non empty right_complementable distributive left_unital Abelian add-associative right_zeroed doubleLoopStr ; :: 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 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;

assume A7: 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;
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