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

A5: 0. R in I by IDEAL_1:2;

A6: M is left-ideal

.= 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

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

then reconsider M = { ((a * r) + s) where r, s is Element of R : s in I } as Subset of R ;
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;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

A5: 0. R in I by IDEAL_1:2;

A6: M is left-ideal

proof

A10:
I c= M
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;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

proof

A11:
M is right-ideal
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;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

proof

A15:
M is add-closed
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;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

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;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

A21: now :: thesis: not a in I

(a * (1. R)) + (0. R) =
a + (0. R)
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;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

.= 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