let R be Ring; :: thesis: for I being Ideal of R st R / I is almost_left_invertible holds

I is quasi-maximal

let I be Ideal of R; :: thesis: ( R / I is almost_left_invertible implies I is quasi-maximal )

set E = EqRel (R,I);

assume A1: R / I is almost_left_invertible ; :: thesis: I is quasi-maximal

given J being Ideal of R such that A2: I c= J and

A3: J <> I and

A4: J is proper ; :: according to RING_1:def 3 :: thesis: contradiction

not J c= I by A2, A3;

then consider a being object such that

A5: a in J and

A6: not a in I ;

reconsider a = a as Element of R by A5;

reconsider x = Class ((EqRel (R,I)),a) as Element of (R / I) by Th12;

A7: Class ((EqRel (R,I)),(0. R)) = 0. (R / I) by Def6;

A8: y * x = 1. (R / I) by A1;

consider b being Element of R such that

A9: y = Class ((EqRel (R,I)),b) by Th11;

A10: Class ((EqRel (R,I)),(1. R)) = 1. (R / I) by Def6;

y * x = Class ((EqRel (R,I)),(b * a)) by A9, Th14;

then A11: (b * a) - (1. R) in I by A10, A8, Th6;

A12: 1. R = (b * a) - ((b * a) - (1. R)) by Th2;

b * a in J by A5, IDEAL_1:def 2;

then 1. R in J by A2, A11, A12, IDEAL_1:15;

hence contradiction by A4, IDEAL_1:19; :: thesis: verum

I is quasi-maximal

let I be Ideal of R; :: thesis: ( R / I is almost_left_invertible implies I is quasi-maximal )

set E = EqRel (R,I);

assume A1: R / I is almost_left_invertible ; :: thesis: I is quasi-maximal

given J being Ideal of R such that A2: I c= J and

A3: J <> I and

A4: J is proper ; :: according to RING_1:def 3 :: thesis: contradiction

not J c= I by A2, A3;

then consider a being object such that

A5: a in J and

A6: not a in I ;

reconsider a = a as Element of R by A5;

reconsider x = Class ((EqRel (R,I)),a) as Element of (R / I) by Th12;

A7: Class ((EqRel (R,I)),(0. R)) = 0. (R / I) by Def6;

now :: thesis: not x = 0. (R / I)

then consider y being Element of (R / I) such that assume
x = 0. (R / I)
; :: thesis: contradiction

then a - (0. R) in I by A7, Th6;

hence contradiction by A6, RLVECT_1:13; :: thesis: verum

end;then a - (0. R) in I by A7, Th6;

hence contradiction by A6, RLVECT_1:13; :: thesis: verum

A8: y * x = 1. (R / I) by A1;

consider b being Element of R such that

A9: y = Class ((EqRel (R,I)),b) by Th11;

A10: Class ((EqRel (R,I)),(1. R)) = 1. (R / I) by Def6;

y * x = Class ((EqRel (R,I)),(b * a)) by A9, Th14;

then A11: (b * a) - (1. R) in I by A10, A8, Th6;

A12: 1. R = (b * a) - ((b * a) - (1. R)) by Th2;

b * a in J by A5, IDEAL_1:def 2;

then 1. R in J by A2, A11, A12, IDEAL_1:15;

hence contradiction by A4, IDEAL_1:19; :: thesis: verum