let R be Ring; :: thesis: for I being Ideal of R st R is commutative & I is quasi-maximal holds
R / I is almost_left_invertible
let I be Ideal of R; :: thesis: ( R is commutative & I is quasi-maximal implies R / I is almost_left_invertible )
set E = EqRel (R,I);
assume that
A1: R is commutative and
A2: I is quasi-maximal ; :: thesis: R / I is almost_left_invertible
let x be Element of (R / I); :: according to ALGSTR_0:def 38 :: thesis: ( x = 0. (R / I) or x is left_invertible )
assume A3: x <> 0. (R / I) ; :: thesis: x is left_invertible
consider a being Element of R such that
A4: x = Class ((EqRel (R,I)),a) by Th11;
set M = { ((a * r) + s) where r, s is Element of R : s in I } ;
{ ((a * r) + s) where r, s is Element of R : s in I } c= the carrier of R

proof

let k be object ; :: according to TARSKI:def 3 :: thesis: ( not k in { ((a * r) + s) where r, s is Element of R : s in I } or k in the carrier of R )
assume k in { ((a * r) + s) where r, s is Element of R : s in I } ; :: thesis: k in the carrier of R
then ex r, s being Element of R st
( k = (a * r) + s & s in I ) ;
hence k in the carrier of R ; :: thesis: verum

end;

then reconsider M = { ((a * r) + s) where r, s is Element of R : s in I } as Subset of R ;
A5: 0. R in I by IDEAL_1:2;
A6: M is left-ideal

proof

let p, x be Element of R; :: according to IDEAL_1:def 2 :: thesis: ( not x in M or p * x in M )
assume x in M ; :: thesis: p * x in M
then consider r, s being Element of R such that
A7: x = (a * r) + s and
A8: s in I ;
A9: p * s in I by A8, IDEAL_1:def 2;
(a * (r * p)) + (p * s) = ((a * r) * p) + (p * s) by GROUP_1:def 3
.= ((a * r) * p) + (s * p) by A1
.= x * p by A7, VECTSP_1:def 3
.= p * x by A1 ;
hence p * x in M by A9; :: thesis: verum

end;

A10: I c= M

proof

let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in I or i in M )
assume i in I ; :: thesis: i in M
then reconsider i = i as Element of I ;
(a * (0. R)) + i = (0. R) + i
.= i by RLVECT_1:def 4 ;
hence i in M ; :: thesis: verum

end;

A11: M is right-ideal

proof

let p, x be Element of R; :: according to IDEAL_1:def 3 :: thesis: ( not x in M or x * p in M )
assume x in M ; :: thesis: x * p in M
then consider r, s being Element of R such that
A12: x = (a * r) + s and
A13: s in I ;
A14: p * s in I by A13, IDEAL_1:def 2;
(a * (r * p)) + (p * s) = ((a * r) * p) + (p * s) by GROUP_1:def 3
.= ((a * r) * p) + (s * p) by A1
.= x * p by A12, VECTSP_1:def 3 ;
hence x * p in M by A14; :: thesis: verum

end;

A15: M is add-closed

proof

let c, d be Element of R; :: according to IDEAL_1:def 1 :: thesis: ( not c in M or not d in M or c + d in M )
assume c in M ; :: thesis: ( not d in M or c + d in M )
then consider rc, sc being Element of R such that
A16: c = (a * rc) + sc and
A17: sc in I ;
assume d in M ; :: thesis: c + d in M
then consider rd, sd being Element of R such that
A18: d = (a * rd) + sd and
A19: sd in I ;
A20: (a * (rc + rd)) + (sc + sd) = ((a * rc) + (a * rd)) + (sc + sd) by VECTSP_1:def 2
.= (((a * rc) + (a * rd)) + sc) + sd by RLVECT_1:def 3
.= (((a * rc) + sc) + (a * rd)) + sd by RLVECT_1:def 3
.= c + d by A16, A18, RLVECT_1:def 3 ;
sc + sd in I by A17, A19, IDEAL_1:def 1;
hence c + d in M by A20; :: thesis: verum

end;

A21: now :: thesis: not a in I

A22: a - (0. R) = a by RLVECT_1:13;
assume a in I ; :: thesis: contradiction
then Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),(0. R)) by A22, Th6
.= 0. (R / I) by Def6 ;
hence contradiction by A3, A4; :: thesis: verum

end;

(a * (1. R)) + (0. R) = a + (0. R)
.= a by RLVECT_1:def 4 ;
then a in M by A5;
then not M is proper by A2, A15, A6, A11, A21, A10;
then M = the carrier of R by SUBSET_1:def 6;
then 1. R in M ;
then consider b, m being Element of R such that
A23: 1. R = (a * b) + m and
A24: m in I ;
A25: m = (1. R) - (a * b) by A23, VECTSP_2:2;
reconsider y = Class ((EqRel (R,I)),b) as Element of (R / I) by Th12;
take y ; :: according to ALGSTR_0:def 27 :: thesis: y * x = 1. (R / I)
A26: Class ((EqRel (R,I)),(1. R)) = 1. (R / I) by Def6;
thus y * x = Class ((EqRel (R,I)),(b * a)) by A4, Th14
.= Class ((EqRel (R,I)),(a * b)) by A1
.= 1. (R / I) by A24, A25, A26, Th6 ; :: thesis: verum