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 39 :: 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 set ; :: 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: (a * (1. R)) + (0. R) = a + (0. R) by VECTSP_1:def 13
.= a by RLVECT_1:def 7 ;
0. R in I by IDEAL_1:2;
then A6: a in M by A5;
A7: 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
A8: c = (a * rc) + sc and
A9: sc in I ;
assume d in M ; :: thesis: c + d in M
then consider rd, sd being Element of R such that
A10: d = (a * rd) + sd and
A11: sd in I ;
A12: sc + sd in I by A9, A11, IDEAL_1:def 1;
(a * (rc + rd)) + (sc + sd) = ((a * rc) + (a * rd)) + (sc + sd) by VECTSP_1:def 11
.= (((a * rc) + (a * rd)) + sc) + sd by RLVECT_1:def 6
.= (((a * rc) + sc) + (a * rd)) + sd by RLVECT_1:def 6
.= c + d by A8, A10, RLVECT_1:def 6 ;
hence c + d in M by A12; :: thesis: verum

end;

A13: 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
A14: x = (a * r) + s and
A15: s in I ;
A16: p * s in I by A15, IDEAL_1:def 2;
(a * (r * p)) + (p * s) = ((a * r) * p) + (p * s) by GROUP_1:def 4
.= ((a * r) * p) + (s * p) by A1, GROUP_1:def 16
.= x * p by A14, VECTSP_1:def 12
.= p * x by A1, GROUP_1:def 16 ;
hence p * x in M by A16; :: thesis: verum

end;

A17: 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
A18: x = (a * r) + s and
A19: s in I ;
A20: p * s in I by A19, IDEAL_1:def 2;
(a * (r * p)) + (p * s) = ((a * r) * p) + (p * s) by GROUP_1:def 4
.= ((a * r) * p) + (s * p) by A1, GROUP_1:def 16
.= x * p by A18, VECTSP_1:def 12 ;
hence x * p in M by A20; :: thesis: verum

end;

A21: now

assume A22: a in I ; :: thesis: contradiction
a - (0. R) = a by RLVECT_1:26;
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;

I c= M

proof

let i be set ; :: 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 by VECTSP_1:36
.= i by RLVECT_1:def 7 ;
hence i in M ; :: thesis: verum

end;

then not M is proper by A2, A6, A7, A13, A17, A21, Def3;
then M = the carrier of R by SUBSET_1:def 7;
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 ;
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)
A25: m = (1. R) - (a * b) by A23, VECTSP_2:22;
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, GROUP_1:def 16
.= 1. (R / I) by A24, A25, A26, Th6 ; :: thesis: verum