:: RING_1 semantic presentation

begin

theorem Th1: :: RING_1:1
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for a, b being Element of L holds (a - b) + b = a
proof
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for a, b being Element of L holds (a - b) + b = a
let a, b be Element of L; ::_thesis: (a - b) + b = a
thus (a - b) + b = a + ((- b) + b) by RLVECT_1:def_3
.= a + (0. L) by RLVECT_1:5
.= a by RLVECT_1:def_4 ; ::_thesis: verum
end;

theorem Th2: :: RING_1:2
for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for b, c being Element of L holds c = b - (b - c)
proof
let L be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for b, c being Element of L holds c = b - (b - c)
let b, c be Element of L; ::_thesis: c = b - (b - c)
set a = b - c;
((b - c) + c) - (b - c) = (c - (b - c)) + (b - c) by RLVECT_1:28
.= c by Th1 ;
hence  c = b - (b - c) by Th1; ::_thesis: verum
end;

theorem Th3: :: RING_1:3
for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for a, b, c being Element of L holds (a - b) - (c - b) = a - c
proof
let L be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for a, b, c being Element of L holds (a - b) - (c - b) = a - c
let a, b, c be Element of L; ::_thesis: (a - b) - (c - b) = a - c
thus (a - b) - (c - b) = ((a - b) - c) + b by RLVECT_1:29
.= ((a - b) + b) - c by RLVECT_1:28
.= (a - (b - b)) - c by RLVECT_1:29
.= (a - (0. L)) - c by RLVECT_1:15
.= a - c by RLVECT_1:13 ; ::_thesis: verum
end;

begin

definition
let K be non empty multMagma ;
let S be Subset of K;
attrS is quasi-prime  means :Def1: :: RING_1:def 1
 for a, b being Element of K holds
( not a * b in S or a in S or b in S );
end;

:: deftheorem Def1 defines quasi-prime RING_1:def_1_:_
 for K being non empty multMagma
for S being Subset of K holds
( S is quasi-prime iff for a, b being Element of K holds
( not a * b in S or a in S or b in S ) );

definition
let K be non empty multLoopStr ;
let S be Subset of K;
attrS is prime  means :Def2: :: RING_1:def 2
( S is proper & S is quasi-prime );
end;

:: deftheorem Def2 defines prime RING_1:def_2_:_
 for K being non empty multLoopStr
for S being Subset of K holds
( S is prime iff ( S is proper & S is quasi-prime ) );

definition
let R be non empty doubleLoopStr ;
let I be Subset of R;
attrI is quasi-maximal  means :Def3: :: RING_1:def 3
 for J being Ideal of R holds
( not I c= J or J = I or not J is proper );
end;

:: deftheorem Def3 defines quasi-maximal RING_1:def_3_:_
 for R being non empty doubleLoopStr
for I being Subset of R holds
( I is quasi-maximal iff for J being Ideal of R holds
( not I c= J or J = I or not J is proper ) );

definition
let R be non empty doubleLoopStr ;
let I be Subset of R;
attrI is maximal  means :Def4: :: RING_1:def 4
( I is proper & I is quasi-maximal );
end;

:: deftheorem Def4 defines maximal RING_1:def_4_:_
 for R being non empty doubleLoopStr
for I being Subset of R holds
( I is maximal iff ( I is proper & I is quasi-maximal ) );

registration
let K be non empty multLoopStr ;
cluster prime  ->  proper quasi-prime for Element of K32( the carrier of K);
coherence
 for b1 being Subset of K st b1 is prime holds
( b1 is proper & b1 is quasi-prime ) by Def2;
cluster proper quasi-prime  ->  prime for Element of K32( the carrier of K);
coherence
 for b1 being Subset of K st b1 is proper & b1 is quasi-prime holds
b1 is prime by Def2;
end;

registration
let R be non empty doubleLoopStr ;
cluster maximal  ->  proper quasi-maximal for Element of K32( the carrier of R);
coherence
 for b1 being Subset of R st b1 is maximal holds
( b1 is proper & b1 is quasi-maximal ) by Def4;
cluster proper quasi-maximal  ->  maximal for Element of K32( the carrier of R);
coherence
 for b1 being Subset of R st b1 is proper & b1 is quasi-maximal holds
b1 is maximal by Def4;
end;

registration
let R be non empty addLoopStr ;
cluster [#] R ->  add-closed ;
coherence
 [#] R is add-closed
proof
let x, y be Element of R; :: according to IDEAL_1:def_1 ::_thesis: ( not x in [#] R or not y in [#] R or x + y in [#] R )
thus  ( not x in [#] R or not y in [#] R or x + y in [#] R ) ; ::_thesis: verum
end;
end;

registration
let R be non empty multMagma ;
cluster [#] R ->  left-ideal right-ideal ;
coherence
 ( [#] R is left-ideal & [#] R is right-ideal )
proof
thus  [#] R is left-ideal ::_thesis: [#] R is right-ideal
proof
let x, y be Element of R; :: according to IDEAL_1:def_2 ::_thesis: ( not y in [#] R or x * y in [#] R )
thus  ( not y in [#] R or x * y in [#] R ) ; ::_thesis: verum
end;
let x, y be Element of R; :: according to IDEAL_1:def_3 ::_thesis: ( not y in [#] R or y * x in [#] R )
thus  ( not y in [#] R or y * x in [#] R ) ; ::_thesis: verum
end;
end;

theorem :: RING_1:4
for R being domRing holds {(0. R)} is prime
proof
let R be domRing; ::_thesis: {(0. R)} is prime
 not 1_ R in {(0. R)} by TARSKI:def_1;
hence  {(0. R)} is proper by IDEAL_1:19; :: according to RING_1:def_2 ::_thesis: {(0. R)} is quasi-prime
let a, b be Element of R; :: according to RING_1:def_1 ::_thesis: ( not a * b in {(0. R)} or a in {(0. R)} or b in {(0. R)} )
assume  a * b in {(0. R)} ; ::_thesis: ( a in {(0. R)} or b in {(0. R)} )
then  a * b = 0. R by TARSKI:def_1;
then  ( a = 0. R or b = 0. R ) by VECTSP_2:def_1;
hence  ( a in {(0. R)} or b in {(0. R)} ) by TARSKI:def_1; ::_thesis: verum
end;

begin

    Lm1:  for R being Ring
for I being Ideal of R ex E being Equivalence_Relation of the carrier of R st
for x, y being set holds
( [x,y] in E iff ( x in the carrier of R & y in the carrier of R & ex P, Q being Element of R st
( P = x & Q = y & P - Q in I ) ) )
proof
let R be Ring; ::_thesis: for I being Ideal of R ex E being Equivalence_Relation of the carrier of R st
for x, y being set holds
( [x,y] in E iff ( x in the carrier of R & y in the carrier of R & ex P, Q being Element of R st
( P = x & Q = y & P - Q in I ) ) )
let I be Ideal of R; ::_thesis: ex E being Equivalence_Relation of the carrier of R st
for x, y being set holds
( [x,y] in E iff ( x in the carrier of R & y in the carrier of R & ex P, Q being Element of R st
( P = x & Q = y & P - Q in I ) ) )
defpred S1[ set , set ] means  ex P, Q being Element of R st
( P = $1 & Q = $2 & P - Q in I );
A1: for x, y being set st S1[x,y] holds
S1[y,x]
proof
let x, y be set ; ::_thesis: ( S1[x,y] implies S1[y,x] )
given P, Q being Element of R such that A2: ( P = x & Q = y & P - Q in I ) ; ::_thesis: S1[y,x]
take  Q ; ::_thesis: ex Q being Element of R st
( Q = y & Q = x & Q - Q in I )
take  P ; ::_thesis: ( Q = y & P = x & Q - P in I )
 - (P - Q) = Q - P by RLVECT_1:33;
hence  ( Q = y & P = x & Q - P in I ) by A2, IDEAL_1:13; ::_thesis: verum
end;
A3: for x, y, z being set st S1[x,y] & S1[y,z] holds
S1[x,z]
proof
let x, y, z be set ; ::_thesis: ( S1[x,y] & S1[y,z] implies S1[x,z] )
assume  S1[x,y] ; ::_thesis: ( not S1[y,z] or S1[x,z] )
then consider P, Q being Element of R such that
A4: ( P = x & Q = y & P - Q in I ) ;
assume  S1[y,z] ; ::_thesis: S1[x,z]
then consider W, S being Element of R such that
A5: ( W = y & S = z & W - S in I ) ;
take  P ; ::_thesis: ex Q being Element of R st
( P = x & Q = z & P - Q in I )
take  S ; ::_thesis: ( P = x & S = z & P - S in I )
(P - Q) + (Q - S) = ((P - Q) + Q) - S by RLVECT_1:28
.= P - S by Th1 ;
hence  ( P = x & S = z & P - S in I ) by A4, A5, IDEAL_1:def_1; ::_thesis: verum
end;
A6: for x being set st x in the carrier of R holds
S1[x,x]
proof
let x be set ; ::_thesis: ( x in the carrier of R implies S1[x,x] )
assume  x in the carrier of R ; ::_thesis: S1[x,x]
then reconsider x = x as Element of R ;
 x - x = 0. R by RLVECT_1:15;
hence  S1[x,x] by IDEAL_1:2; ::_thesis: verum
end;
thus  ex EqR being Equivalence_Relation of the carrier of R st
for x, y being set holds
( [x,y] in EqR iff ( x in the carrier of R & y in the carrier of R & S1[x,y] ) ) from EQREL_1:sch_1(A6, A1, A3); ::_thesis: verum
end;

definition
let R be Ring;
let I be Ideal of R;
func EqRel (R,I) ->  Relation of R means :Def5: :: RING_1:def 5
 for a, b being Element of R holds
( [a,b] in it iff a - b in I );
existence
 ex b1 being Relation of R st
for a, b being Element of R holds
( [a,b] in b1 iff a - b in I )
proof
consider E being Equivalence_Relation of the carrier of R such that
A1: for x, y being set holds
( [x,y] in E iff ( x in the carrier of R & y in the carrier of R & ex P, Q being Element of R st
( P = x & Q = y & P - Q in I ) ) ) by Lm1;
take  E ; ::_thesis: for a, b being Element of R holds
( [a,b] in E iff a - b in I )
let a, b be Element of R; ::_thesis: ( [a,b] in E iff a - b in I )
thus  ( [a,b] in E implies a - b in I ) ::_thesis: ( a - b in I implies [a,b] in E )
proof
assume  [a,b] in E ; ::_thesis: a - b in I
then  ex P, Q being Element of R st
( P = a & Q = b & P - Q in I ) by A1;
hence  a - b in I ; ::_thesis: verum
end;
thus  ( a - b in I implies [a,b] in E ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation of R st ( for a, b being Element of R holds
( [a,b] in b1 iff a - b in I ) ) & ( for a, b being Element of R holds
( [a,b] in b2 iff a - b in I ) ) holds
b1 = b2
proof
let A, B be Relation of R; ::_thesis: ( ( for a, b being Element of R holds
( [a,b] in A iff a - b in I ) ) & ( for a, b being Element of R holds
( [a,b] in B iff a - b in I ) ) implies A = B )
assume that
A2: for a, b being Element of R holds
( [a,b] in A iff a - b in I ) and
A3: for a, b being Element of R holds
( [a,b] in B iff a - b in I ) ; ::_thesis: A = B
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in A or [x,y] in B ) & ( not [x,y] in B or [x,y] in A ) )
thus  ( [x,y] in A implies [x,y] in B ) ::_thesis: ( not [x,y] in B or [x,y] in A )
proof
assume A4: [x,y] in A ; ::_thesis: [x,y] in B
then reconsider x = x, y = y as Element of R by ZFMISC_1:87;
 x - y in I by A2, A4;
hence  [x,y] in B by A3; ::_thesis: verum
end;
assume A5: [x,y] in B ; ::_thesis: [x,y] in A
then reconsider x = x, y = y as Element of R by ZFMISC_1:87;
 x - y in I by A3, A5;
hence  [x,y] in A by A2; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines EqRel RING_1:def_5_:_
 for R being Ring
for I being Ideal of R
for b3 being Relation of R holds
( b3 = EqRel (R,I) iff for a, b being Element of R holds
( [a,b] in b3 iff a - b in I ) );

registration
let R be Ring;
let I be Ideal of R;
cluster EqRel (R,I) ->  non empty total symmetric transitive ;
coherence
 ( not EqRel (R,I) is empty & EqRel (R,I) is total & EqRel (R,I) is symmetric & EqRel (R,I) is transitive )
proof
set A = EqRel (R,I);
consider B being Equivalence_Relation of the carrier of R such that
A1: for x, y being set holds
( [x,y] in B iff ( x in the carrier of R & y in the carrier of R & ex P, Q being Element of R st
( P = x & Q = y & P - Q in I ) ) ) by Lm1;
 EqRel (R,I) = B
proof
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in EqRel (R,I) or [x,y] in B ) & ( not [x,y] in B or [x,y] in EqRel (R,I) ) )
thus  ( [x,y] in EqRel (R,I) implies [x,y] in B ) ::_thesis: ( not [x,y] in B or [x,y] in EqRel (R,I) )
proof
assume A2: [x,y] in EqRel (R,I) ; ::_thesis: [x,y] in B
then reconsider x = x, y = y as Element of R by ZFMISC_1:87;
 x - y in I by A2, Def5;
hence  [x,y] in B by A1; ::_thesis: verum
end;
assume  [x,y] in B ; ::_thesis: [x,y] in EqRel (R,I)
then  ex P, Q being Element of R st
( P = x & Q = y & P - Q in I ) by A1;
hence  [x,y] in EqRel (R,I) by Def5; ::_thesis: verum
end;
hence  ( not EqRel (R,I) is empty & EqRel (R,I) is total & EqRel (R,I) is symmetric & EqRel (R,I) is transitive ) by EQREL_1:9, RELAT_1:40; ::_thesis: verum
end;
end;

theorem Th5: :: RING_1:5
for R being Ring
for I being Ideal of R
for a, b being Element of R holds
( a in Class ((EqRel (R,I)),b) iff a - b in I )
proof
let R be Ring; ::_thesis: for I being Ideal of R
for a, b being Element of R holds
( a in Class ((EqRel (R,I)),b) iff a - b in I )
let I be Ideal of R; ::_thesis: for a, b being Element of R holds
( a in Class ((EqRel (R,I)),b) iff a - b in I )
let a, b be Element of R; ::_thesis: ( a in Class ((EqRel (R,I)),b) iff a - b in I )
set E = EqRel (R,I);
hereby  ::_thesis: ( a - b in I implies a in Class ((EqRel (R,I)),b) )
assume  a in Class ((EqRel (R,I)),b) ; ::_thesis: a - b in I
then  [a,b] in EqRel (R,I) by EQREL_1:19;
hence  a - b in I by Def5; ::_thesis: verum
end;
assume  a - b in I ; ::_thesis: a in Class ((EqRel (R,I)),b)
then  [a,b] in EqRel (R,I) by Def5;
hence  a in Class ((EqRel (R,I)),b) by EQREL_1:19; ::_thesis: verum
end;

theorem Th6: :: RING_1:6
for R being Ring
for I being Ideal of R
for a, b being Element of R holds
( Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b) iff a - b in I )
proof
let R be Ring; ::_thesis: for I being Ideal of R
for a, b being Element of R holds
( Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b) iff a - b in I )
let I be Ideal of R; ::_thesis: for a, b being Element of R holds
( Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b) iff a - b in I )
let a, b be Element of R; ::_thesis: ( Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b) iff a - b in I )
set E = EqRel (R,I);
thus  ( Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b) implies a - b in I ) ::_thesis: ( a - b in I implies Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b) )
proof
assume  Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b) ; ::_thesis: a - b in I
then  a in Class ((EqRel (R,I)),b) by EQREL_1:23;
hence  a - b in I by Th5; ::_thesis: verum
end;
assume  a - b in I ; ::_thesis: Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b)
then  a in Class ((EqRel (R,I)),b) by Th5;
hence  Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b) by EQREL_1:23; ::_thesis: verum
end;

theorem Th7: :: RING_1:7
for R being Ring
for a being Element of R holds Class ((EqRel (R,([#] R))),a) = the carrier of R
proof
let R be Ring; ::_thesis: for a being Element of R holds Class ((EqRel (R,([#] R))),a) = the carrier of R
let a be Element of R; ::_thesis: Class ((EqRel (R,([#] R))),a) = the carrier of R
set E = EqRel (R,([#] R));
thus  Class ((EqRel (R,([#] R))),a) c= the carrier of R ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of R c= Class ((EqRel (R,([#] R))),a)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of R or x in Class ((EqRel (R,([#] R))),a) )
assume  x in the carrier of R ; ::_thesis: x in Class ((EqRel (R,([#] R))),a)
then reconsider x = x as Element of R ;
 x - a in [#] R ;
then  [x,a] in EqRel (R,([#] R)) by Def5;
hence  x in Class ((EqRel (R,([#] R))),a) by EQREL_1:19; ::_thesis: verum
end;

theorem :: RING_1:8
for R being Ring holds Class (EqRel (R,([#] R))) = { the carrier of R}
proof
let R be Ring; ::_thesis: Class (EqRel (R,([#] R))) = { the carrier of R}
set E = EqRel (R,([#] R));
thus  Class (EqRel (R,([#] R))) c= { the carrier of R} :: according to XBOOLE_0:def_10 ::_thesis: { the carrier of R} c= Class (EqRel (R,([#] R)))
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in Class (EqRel (R,([#] R))) or A in { the carrier of R} )
assume  A in Class (EqRel (R,([#] R))) ; ::_thesis: A in { the carrier of R}
then consider x being set  such that
A1: x in the carrier of R and
A2: A = Class ((EqRel (R,([#] R))),x) by EQREL_1:def_3;
reconsider x = x as Element of R by A1;
 Class ((EqRel (R,([#] R))),x) = the carrier of R
proof
thus  Class ((EqRel (R,([#] R))),x) c= the carrier of R ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of R c= Class ((EqRel (R,([#] R))),x)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of R or a in Class ((EqRel (R,([#] R))),x) )
assume  a in the carrier of R ; ::_thesis: a in Class ((EqRel (R,([#] R))),x)
then reconsider a = a as Element of R ;
 a - x in [#] R ;
then  [a,x] in EqRel (R,([#] R)) by Def5;
hence  a in Class ((EqRel (R,([#] R))),x) by EQREL_1:19; ::_thesis: verum
end;
hence  A in { the carrier of R} by A2, TARSKI:def_1; ::_thesis: verum
end;
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in { the carrier of R} or A in Class (EqRel (R,([#] R))) )
assume  A in { the carrier of R} ; ::_thesis: A in Class (EqRel (R,([#] R)))
then A = the carrier of R by TARSKI:def_1
.= Class ((EqRel (R,([#] R))),(0. R)) by Th7 ;
hence  A in Class (EqRel (R,([#] R))) by EQREL_1:def_3; ::_thesis: verum
end;

theorem Th9: :: RING_1:9
for R being Ring
for a being Element of R holds Class ((EqRel (R,{(0. R)})),a) = {a}
proof
let R be Ring; ::_thesis: for a being Element of R holds Class ((EqRel (R,{(0. R)})),a) = {a}
let a be Element of R; ::_thesis: Class ((EqRel (R,{(0. R)})),a) = {a}
set E = EqRel (R,{(0. R)});
thus  Class ((EqRel (R,{(0. R)})),a) c= {a} :: according to XBOOLE_0:def_10 ::_thesis: {a} c= Class ((EqRel (R,{(0. R)})),a)
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in Class ((EqRel (R,{(0. R)})),a) or A in {a} )
assume A1: A in Class ((EqRel (R,{(0. R)})),a) ; ::_thesis: A in {a}
then reconsider A = A as Element of R ;
 [A,a] in EqRel (R,{(0. R)}) by A1, EQREL_1:19;
then  A - a in {(0. R)} by Def5;
then  A - a = 0. R by TARSKI:def_1;
then  A = a by RLVECT_1:21;
hence  A in {a} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a} or x in Class ((EqRel (R,{(0. R)})),a) )
assume  x in {a} ; ::_thesis: x in Class ((EqRel (R,{(0. R)})),a)
then A2: x = a by TARSKI:def_1;
 ( a - a = 0. R & 0. R in {(0. R)} ) by RLVECT_1:15, TARSKI:def_1;
then  [x,a] in EqRel (R,{(0. R)}) by A2, Def5;
hence  x in Class ((EqRel (R,{(0. R)})),a) by EQREL_1:19; ::_thesis: verum
end;

theorem :: RING_1:10
for R being Ring holds Class (EqRel (R,{(0. R)})) = rng (singleton the carrier of R)
proof
let R be Ring; ::_thesis: Class (EqRel (R,{(0. R)})) = rng (singleton the carrier of R)
set E = EqRel (R,{(0. R)});
set f = singleton the carrier of R;
A1: dom (singleton the carrier of R) = the carrier of R by FUNCT_2:def_1;
thus  Class (EqRel (R,{(0. R)})) c= rng (singleton the carrier of R) :: according to XBOOLE_0:def_10 ::_thesis: rng (singleton the carrier of R) c= Class (EqRel (R,{(0. R)}))
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in Class (EqRel (R,{(0. R)})) or A in rng (singleton the carrier of R) )
assume  A in Class (EqRel (R,{(0. R)})) ; ::_thesis: A in rng (singleton the carrier of R)
then consider x being set  such that
A2: x in the carrier of R and
A3: A = Class ((EqRel (R,{(0. R)})),x) by EQREL_1:def_3;
reconsider x = x as Element of R by A2;
A4: Class ((EqRel (R,{(0. R)})),x) = {x}
proof
thus  Class ((EqRel (R,{(0. R)})),x) c= {x} :: according to XBOOLE_0:def_10 ::_thesis: {x} c= Class ((EqRel (R,{(0. R)})),x)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Class ((EqRel (R,{(0. R)})),x) or a in {x} )
assume A5: a in Class ((EqRel (R,{(0. R)})),x) ; ::_thesis: a in {x}
then reconsider a = a as Element of R ;
 [a,x] in EqRel (R,{(0. R)}) by A5, EQREL_1:19;
then  a - x in {(0. R)} by Def5;
then  a - x = 0. R by TARSKI:def_1;
then  a = x by RLVECT_1:21;
hence  a in {x} by TARSKI:def_1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x} or a in Class ((EqRel (R,{(0. R)})),x) )
 x - x = 0. R by RLVECT_1:15;
then A6: x - x in {(0. R)} by TARSKI:def_1;
assume  a in {x} ; ::_thesis: a in Class ((EqRel (R,{(0. R)})),x)
then  a = x by TARSKI:def_1;
then  [a,x] in EqRel (R,{(0. R)}) by A6, Def5;
hence  a in Class ((EqRel (R,{(0. R)})),x) by EQREL_1:19; ::_thesis: verum
end;
 (singleton the carrier of R) . x = {x} by SETWISEO:def_6;
hence  A in rng (singleton the carrier of R) by A1, A3, A4, FUNCT_1:def_3; ::_thesis: verum
end;
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in rng (singleton the carrier of R) or A in Class (EqRel (R,{(0. R)})) )
assume  A in rng (singleton the carrier of R) ; ::_thesis: A in Class (EqRel (R,{(0. R)}))
then consider w being set  such that
A7: w in dom (singleton the carrier of R) and
A8: (singleton the carrier of R) . w = A by FUNCT_1:def_3;
(singleton the carrier of R) . w = {w} by A7, SETWISEO:def_6
.= Class ((EqRel (R,{(0. R)})),w) by A7, Th9 ;
hence  A in Class (EqRel (R,{(0. R)})) by A7, A8, EQREL_1:def_3; ::_thesis: verum
end;

begin

definition
let R be Ring;
let I be Ideal of R;
func QuotientRing (R,I) ->  strict doubleLoopStr  means :Def6: :: RING_1:def 6
( the carrier of it = Class (EqRel (R,I)) & 1. it = Class ((EqRel (R,I)),(1. R)) & 0. it = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of it ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of it . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of it ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of it . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) );
existence
 ex b1 being strict doubleLoopStr st
( the carrier of b1 = Class (EqRel (R,I)) & 1. b1 = Class ((EqRel (R,I)),(1. R)) & 0. b1 = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of b1 ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of b1 . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of b1 ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of b1 . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) )
proof
set E = EqRel (R,I);
set A = Class (EqRel (R,I));
defpred S1[ set , set , set ] means  ex P, Q being Element of R st
( $1 = Class ((EqRel (R,I)),P) & $2 = Class ((EqRel (R,I)),Q) & $3 = Class ((EqRel (R,I)),(P + Q)) );
defpred S2[ set , set , set ] means  ex P, Q being Element of R st
( $1 = Class ((EqRel (R,I)),P) & $2 = Class ((EqRel (R,I)),Q) & $3 = Class ((EqRel (R,I)),(P * Q)) );
reconsider u = Class ((EqRel (R,I)),(1_ R)) as Element of Class (EqRel (R,I)) by EQREL_1:def_3;
reconsider z = Class ((EqRel (R,I)),(0. R)) as Element of Class (EqRel (R,I)) by EQREL_1:def_3;
A1: for x, y being Element of Class (EqRel (R,I)) ex z being Element of Class (EqRel (R,I)) st S1[x,y,z]
proof
let x, y be Element of Class (EqRel (R,I)); ::_thesis: ex z being Element of Class (EqRel (R,I)) st S1[x,y,z]
consider P being set  such that
A2: P in the carrier of R and
A3: x = Class ((EqRel (R,I)),P) by EQREL_1:def_3;
consider Q being set  such that
A4: Q in the carrier of R and
A5: y = Class ((EqRel (R,I)),Q) by EQREL_1:def_3;
reconsider P = P, Q = Q as Element of R by A2, A4;
 Class ((EqRel (R,I)),(P + Q)) is Element of Class (EqRel (R,I)) by EQREL_1:def_3;
hence  ex z being Element of Class (EqRel (R,I)) st S1[x,y,z] by A3, A5; ::_thesis: verum
end;
consider g being BinOp of (Class (EqRel (R,I))) such that
A6: for a, b being Element of Class (EqRel (R,I)) holds S1[a,b,g . (a,b)] from BINOP_1:sch_3(A1);
A7: for x, y being Element of Class (EqRel (R,I)) ex z being Element of Class (EqRel (R,I)) st S2[x,y,z]
proof
let x, y be Element of Class (EqRel (R,I)); ::_thesis: ex z being Element of Class (EqRel (R,I)) st S2[x,y,z]
consider P being set  such that
A8: P in the carrier of R and
A9: x = Class ((EqRel (R,I)),P) by EQREL_1:def_3;
consider Q being set  such that
A10: Q in the carrier of R and
A11: y = Class ((EqRel (R,I)),Q) by EQREL_1:def_3;
reconsider P = P, Q = Q as Element of R by A8, A10;
 Class ((EqRel (R,I)),(P * Q)) is Element of Class (EqRel (R,I)) by EQREL_1:def_3;
hence  ex z being Element of Class (EqRel (R,I)) st S2[x,y,z] by A9, A11; ::_thesis: verum
end;
consider h being BinOp of (Class (EqRel (R,I))) such that
A12: for a, b being Element of Class (EqRel (R,I)) holds S2[a,b,h . (a,b)] from BINOP_1:sch_3(A7);
take  doubleLoopStr(# (Class (EqRel (R,I))),g,h,u,z #) ; ::_thesis: ( the carrier of doubleLoopStr(# (Class (EqRel (R,I))),g,h,u,z #) = Class (EqRel (R,I)) & 1. doubleLoopStr(# (Class (EqRel (R,I))),g,h,u,z #) = Class ((EqRel (R,I)),(1. R)) & 0. doubleLoopStr(# (Class (EqRel (R,I))),g,h,u,z #) = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of doubleLoopStr(# (Class (EqRel (R,I))),g,h,u,z #) ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of doubleLoopStr(# (Class (EqRel (R,I))),g,h,u,z #) . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of doubleLoopStr(# (Class (EqRel (R,I))),g,h,u,z #) ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of doubleLoopStr(# (Class (EqRel (R,I))),g,h,u,z #) . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) )
thus  ( the carrier of doubleLoopStr(# (Class (EqRel (R,I))),g,h,u,z #) = Class (EqRel (R,I)) & 1. doubleLoopStr(# (Class (EqRel (R,I))),g,h,u,z #) = Class ((EqRel (R,I)),(1. R)) & 0. doubleLoopStr(# (Class (EqRel (R,I))),g,h,u,z #) = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of doubleLoopStr(# (Class (EqRel (R,I))),g,h,u,z #) ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of doubleLoopStr(# (Class (EqRel (R,I))),g,h,u,z #) . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of doubleLoopStr(# (Class (EqRel (R,I))),g,h,u,z #) ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of doubleLoopStr(# (Class (EqRel (R,I))),g,h,u,z #) . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) ) by A6, A12; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict doubleLoopStr st the carrier of b1 = Class (EqRel (R,I)) & 1. b1 = Class ((EqRel (R,I)),(1. R)) & 0. b1 = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of b1 ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of b1 . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of b1 ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of b1 . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) & the carrier of b2 = Class (EqRel (R,I)) & 1. b2 = Class ((EqRel (R,I)),(1. R)) & 0. b2 = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of b2 ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of b2 . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of b2 ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of b2 . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) holds
b1 = b2
proof
set E = EqRel (R,I);
let X, Y be strict doubleLoopStr ; ::_thesis: ( the carrier of X = Class (EqRel (R,I)) & 1. X = Class ((EqRel (R,I)),(1. R)) & 0. X = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of X ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of X . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of X ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of X . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) & the carrier of Y = Class (EqRel (R,I)) & 1. Y = Class ((EqRel (R,I)),(1. R)) & 0. Y = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of Y ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of Y . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of Y ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of Y . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) implies X = Y )
assume that
A13: the carrier of X = Class (EqRel (R,I)) and
A14: ( 1. X = Class ((EqRel (R,I)),(1. R)) & 0. X = Class ((EqRel (R,I)),(0. R)) ) and
A15: for x, y being Element of X ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of X . (x,y) = Class ((EqRel (R,I)),(a + b)) ) and
A16: for x, y being Element of X ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of X . (x,y) = Class ((EqRel (R,I)),(a * b)) ) and
A17: the carrier of Y = Class (EqRel (R,I)) and
A18: ( 1. Y = Class ((EqRel (R,I)),(1. R)) & 0. Y = Class ((EqRel (R,I)),(0. R)) ) and
A19: for x, y being Element of Y ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of Y . (x,y) = Class ((EqRel (R,I)),(a + b)) ) and
A20: for x, y being Element of Y ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of Y . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ; ::_thesis: X = Y
A21: for x, y being Element of X holds the multF of X . (x,y) = the multF of Y . (x,y)
proof
let x, y be Element of X; ::_thesis: the multF of X . (x,y) = the multF of Y . (x,y)
consider a, b being Element of R such that
A22: x = Class ((EqRel (R,I)),a) and
A23: y = Class ((EqRel (R,I)),b) and
A24: the multF of X . (x,y) = Class ((EqRel (R,I)),(a * b)) by A16;
consider a1, b1 being Element of R such that
A25: x = Class ((EqRel (R,I)),a1) and
A26: y = Class ((EqRel (R,I)),b1) and
A27: the multF of Y . (x,y) = Class ((EqRel (R,I)),(a1 * b1)) by A13, A17, A20;
 b - b1 in I by A23, A26, Th6;
then A28: a1 * (b - b1) in I by IDEAL_1:def_2;
A29: ((a - a1) * b) + (a1 * (b - b1)) = ((a * b) - (a1 * b)) + (a1 * (b - b1)) by VECTSP_1:13
.= ((a * b) - (a1 * b)) + ((a1 * b) - (a1 * b1)) by VECTSP_1:11
.= (((a * b) - (a1 * b)) + (a1 * b)) - (a1 * b1) by RLVECT_1:28
.= (a * b) - (a1 * b1) by Th1 ;
 a - a1 in I by A22, A25, Th6;
then  (a - a1) * b in I by IDEAL_1:def_3;
then  ((a - a1) * b) + (a1 * (b - b1)) in I by A28, IDEAL_1:def_1;
hence  the multF of X . (x,y) = the multF of Y . (x,y) by A24, A27, A29, Th6; ::_thesis: verum
end;
 for x, y being Element of X holds the addF of X . (x,y) = the addF of Y . (x,y)
proof
let x, y be Element of X; ::_thesis: the addF of X . (x,y) = the addF of Y . (x,y)
consider a, b being Element of R such that
A30: ( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) ) and
A31: the addF of X . (x,y) = Class ((EqRel (R,I)),(a + b)) by A15;
consider a1, b1 being Element of R such that
A32: ( x = Class ((EqRel (R,I)),a1) & y = Class ((EqRel (R,I)),b1) ) and
A33: the addF of Y . (x,y) = Class ((EqRel (R,I)),(a1 + b1)) by A13, A17, A19;
 ( a - a1 in I & b - b1 in I ) by A30, A32, Th6;
then A34: (a - a1) + (b - b1) in I by IDEAL_1:def_1;
(a + b) - (a1 + b1) = ((a + b) - a1) - b1 by RLVECT_1:27
.= ((a - a1) + b) - b1 by RLVECT_1:28
.= (a - a1) + (b - b1) by RLVECT_1:28 ;
hence  the addF of X . (x,y) = the addF of Y . (x,y) by A31, A33, A34, Th6; ::_thesis: verum
end;
then  the addF of X = the addF of Y by A13, A17, BINOP_1:2;
hence  X = Y by A13, A14, A17, A18, A21, BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines QuotientRing RING_1:def_6_:_
 for R being Ring
for I being Ideal of R
for b3 being strict doubleLoopStr holds
( b3 = QuotientRing (R,I) iff ( the carrier of b3 = Class (EqRel (R,I)) & 1. b3 = Class ((EqRel (R,I)),(1. R)) & 0. b3 = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of b3 ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of b3 . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of b3 ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of b3 . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) ) );

notation
let R be Ring;
let I be Ideal of R;
synonym R / I for  QuotientRing (R,I);
end;

registration
let R be Ring;
let I be Ideal of R;
cluster QuotientRing (R,I) ->  non empty strict ;
coherence
 not R / I is empty
proof
 the carrier of (R / I) = Class (EqRel (R,I)) by Def6;
hence  not the carrier of (R / I) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;


theorem Th11: :: RING_1:11
for R being Ring
for I being Ideal of R
for x being Element of (R / I) ex a being Element of R st x = Class ((EqRel (R,I)),a)
proof
let R be Ring; ::_thesis: for I being Ideal of R
for x being Element of (R / I) ex a being Element of R st x = Class ((EqRel (R,I)),a)
let I be Ideal of R; ::_thesis: for x being Element of (R / I) ex a being Element of R st x = Class ((EqRel (R,I)),a)
let x be Element of (R / I); ::_thesis: ex a being Element of R st x = Class ((EqRel (R,I)),a)
 the carrier of (R / I) = Class (EqRel (R,I)) by Def6;
then  x in Class (EqRel (R,I)) ;
then  ex a being set st
( a in the carrier of R & x = Class ((EqRel (R,I)),a) ) by EQREL_1:def_3;
hence  ex a being Element of R st x = Class ((EqRel (R,I)),a) ; ::_thesis: verum
end;

theorem Th12: :: RING_1:12
for R being Ring
for I being Ideal of R
for a being Element of R holds Class ((EqRel (R,I)),a) is Element of (R / I)
proof
let R be Ring; ::_thesis: for I being Ideal of R
for a being Element of R holds Class ((EqRel (R,I)),a) is Element of (R / I)
let I be Ideal of R; ::_thesis: for a being Element of R holds Class ((EqRel (R,I)),a) is Element of (R / I)
let a be Element of R; ::_thesis: Class ((EqRel (R,I)),a) is Element of (R / I)
 the carrier of (R / I) = Class (EqRel (R,I)) by Def6;
hence  Class ((EqRel (R,I)),a) is Element of (R / I) by EQREL_1:def_3; ::_thesis: verum
end;

theorem Th13: :: RING_1:13
for R being Ring
for I being Ideal of R
for a, b being Element of R
for x, y being Element of (R / I) st x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) holds
x + y = Class ((EqRel (R,I)),(a + b))
proof
let R be Ring; ::_thesis: for I being Ideal of R
for a, b being Element of R
for x, y being Element of (R / I) st x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) holds
x + y = Class ((EqRel (R,I)),(a + b))
let I be Ideal of R; ::_thesis: for a, b being Element of R
for x, y being Element of (R / I) st x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) holds
x + y = Class ((EqRel (R,I)),(a + b))
let a, b be Element of R; ::_thesis: for x, y being Element of (R / I) st x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) holds
x + y = Class ((EqRel (R,I)),(a + b))
let x, y be Element of (R / I); ::_thesis: ( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) implies x + y = Class ((EqRel (R,I)),(a + b)) )
consider a1, b1 being Element of R such that
A1: ( x = Class ((EqRel (R,I)),a1) & y = Class ((EqRel (R,I)),b1) ) and
A2: the addF of (R / I) . (x,y) = Class ((EqRel (R,I)),(a1 + b1)) by Def6;
A3: (a1 - a) + (b1 - b) = ((a1 - a) + b1) - b by RLVECT_1:28
.= ((a1 + b1) - a) - b by RLVECT_1:28
.= (a1 + b1) - (a + b) by RLVECT_1:27 ;
assume  ( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) ) ; ::_thesis: x + y = Class ((EqRel (R,I)),(a + b))
then  ( a1 - a in I & b1 - b in I ) by A1, Th6;
then  (a1 + b1) - (a + b) in I by A3, IDEAL_1:def_1;
hence  x + y = Class ((EqRel (R,I)),(a + b)) by A2, Th6; ::_thesis: verum
end;

theorem Th14: :: RING_1:14
for R being Ring
for I being Ideal of R
for a, b being Element of R
for x, y being Element of (R / I) st x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) holds
x * y = Class ((EqRel (R,I)),(a * b))
proof
let R be Ring; ::_thesis: for I being Ideal of R
for a, b being Element of R
for x, y being Element of (R / I) st x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) holds
x * y = Class ((EqRel (R,I)),(a * b))
let I be Ideal of R; ::_thesis: for a, b being Element of R
for x, y being Element of (R / I) st x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) holds
x * y = Class ((EqRel (R,I)),(a * b))
let a, b be Element of R; ::_thesis: for x, y being Element of (R / I) st x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) holds
x * y = Class ((EqRel (R,I)),(a * b))
let x, y be Element of (R / I); ::_thesis: ( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) implies x * y = Class ((EqRel (R,I)),(a * b)) )
assume that
A1: x = Class ((EqRel (R,I)),a) and
A2: y = Class ((EqRel (R,I)),b) ; ::_thesis: x * y = Class ((EqRel (R,I)),(a * b))
consider a1, b1 being Element of R such that
A3: x = Class ((EqRel (R,I)),a1) and
A4: y = Class ((EqRel (R,I)),b1) and
A5: the multF of (R / I) . (x,y) = Class ((EqRel (R,I)),(a1 * b1)) by Def6;
 b1 - b in I by A2, A4, Th6;
then A6: a1 * (b1 - b) in I by IDEAL_1:def_2;
 ( (a1 - a) * b = (a1 * b) - (a * b) & a1 * (b1 - b) = (a1 * b1) - (a1 * b) ) by VECTSP_1:11, VECTSP_1:13;
then A7: (a1 * (b1 - b)) + ((a1 - a) * b) = (((a1 * b1) - (a1 * b)) + (a1 * b)) - (a * b) by RLVECT_1:28
.= (a1 * b1) - (a * b) by Th1 ;
 a1 - a in I by A1, A3, Th6;
then  (a1 - a) * b in I by IDEAL_1:def_3;
then  ((a1 - a) * b) + (a1 * (b1 - b)) in I by A6, IDEAL_1:def_1;
hence  x * y = Class ((EqRel (R,I)),(a * b)) by A5, A7, Th6; ::_thesis: verum
end;

Lm2: now__::_thesis:_for_R_being_Ring
for_I_being_Ideal_of_R
for_e_being_Element_of_(R_/_I)_st_e_=_Class_((EqRel_(R,I)),(1__R))_holds_
for_h_being_Element_of_(R_/_I)_holds_
(_h_*_e_=_h_&_e_*_h_=_h_)
let R be Ring; ::_thesis: for I being Ideal of R
for e being Element of (R / I) st e = Class ((EqRel (R,I)),(1_ R)) holds
for h being Element of (R / I) holds
( h * e = h & e * h = h )
let I be Ideal of R; ::_thesis: for e being Element of (R / I) st e = Class ((EqRel (R,I)),(1_ R)) holds
for h being Element of (R / I) holds
( h * e = h & e * h = h )
set E = EqRel (R,I);
let e be Element of (R / I); ::_thesis: ( e = Class ((EqRel (R,I)),(1_ R)) implies for h being Element of (R / I) holds
( h * e = h & e * h = h ) )
assume A1: e = Class ((EqRel (R,I)),(1_ R)) ; ::_thesis: for h being Element of (R / I) holds
( h * e = h & e * h = h )
let h be Element of (R / I); ::_thesis: ( h * e = h & e * h = h )
consider a being Element of R such that
A2: e = Class ((EqRel (R,I)),a) by Th11;
consider b being Element of R such that
A3: h = Class ((EqRel (R,I)),b) by Th11;
A4: a - (1_ R) in I by A1, A2, Th6;
then A5: (a - (1_ R)) * b in I by IDEAL_1:def_3;
A6: b * (a - (1_ R)) = (b * a) - (b * (1_ R)) by VECTSP_1:11
.= (b * a) - b by VECTSP_1:def_4 ;
A7: b * (a - (1_ R)) in I by A4, IDEAL_1:def_2;
thus h * e = Class ((EqRel (R,I)),(b * a)) by A2, A3, Th14
.= h by A3, A7, A6, Th6 ; ::_thesis: e * h = h
A8: (a - (1_ R)) * b = (a * b) - ((1_ R) * b) by VECTSP_1:13
.= (a * b) - b by VECTSP_1:def_8 ;
thus e * h = Class ((EqRel (R,I)),(a * b)) by A2, A3, Th14
.= h by A3, A5, A8, Th6 ; ::_thesis: verum
end;

theorem :: RING_1:15
for R being Ring
for I being Ideal of R holds Class ((EqRel (R,I)),(1. R)) = 1. (R / I) by Def6;

registration
let R be Ring;
let I be Ideal of R;
cluster QuotientRing (R,I) ->  right_complementable strict associative well-unital distributive Abelian add-associative right_zeroed ;
coherence
 ( R / I is Abelian & R / I is add-associative & R / I is right_zeroed & R / I is right_complementable & R / I is associative & R / I is well-unital & R / I is distributive )
proof
set g = the addF of (R / I);
set E = EqRel (R,I);
hereby  :: according to RLVECT_1:def_2 ::_thesis: ( R / I is add-associative & R / I is right_zeroed & R / I is right_complementable & R / I is associative & R / I is well-unital & R / I is distributive )
let x, y be Element of (R / I); ::_thesis: x + y = y + x
consider a being Element of R such that
A1: x = Class ((EqRel (R,I)),a) by Th11;
consider b being Element of R such that
A2: y = Class ((EqRel (R,I)),b) by Th11;
thus x + y = Class ((EqRel (R,I)),(a + b)) by A1, A2, Th13
.= y + x by A1, A2, Th13 ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_3 ::_thesis: ( R / I is right_zeroed & R / I is right_complementable & R / I is associative & R / I is well-unital & R / I is distributive )
let x, y, z be Element of (R / I); ::_thesis: (x + y) + z = x + (y + z)
consider a being Element of R such that
A3: x = Class ((EqRel (R,I)),a) by Th11;
consider b being Element of R such that
A4: y = Class ((EqRel (R,I)),b) by Th11;
consider bc being Element of R such that
A5: y + z = Class ((EqRel (R,I)),bc) by Th11;
consider c being Element of R such that
A6: z = Class ((EqRel (R,I)),c) by Th11;
 y + z = Class ((EqRel (R,I)),(b + c)) by A4, A6, Th13;
then A7: bc - (b + c) in I by A5, Th6;
consider ab being Element of R such that
A8: x + y = Class ((EqRel (R,I)),ab) by Th11;
 x + y = Class ((EqRel (R,I)),(a + b)) by A3, A4, Th13;
then  ab - (a + b) in I by A8, Th6;
then A9: (ab - (a + b)) - (bc - (b + c)) in I by A7, IDEAL_1:15;
A10: (ab - (a + b)) - (bc - (b + c)) = ((ab - (a + b)) - bc) + (b + c) by RLVECT_1:29
.= ((ab - (a + b)) + (b + c)) - bc by RLVECT_1:28
.= (((ab - a) - b) + (b + c)) - bc by RLVECT_1:27
.= ((((ab - a) - b) + b) + c) - bc by RLVECT_1:def_3
.= ((ab - a) + c) - bc by Th1
.= ((ab + c) - a) - bc by RLVECT_1:28
.= (ab + c) - (a + bc) by RLVECT_1:27 ;
thus (x + y) + z = Class ((EqRel (R,I)),(ab + c)) by A6, A8, Th13
.= Class ((EqRel (R,I)),(a + bc)) by A9, A10, Th6
.= x + (y + z) by A3, A5, Th13 ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_4 ::_thesis: ( R / I is right_complementable & R / I is associative & R / I is well-unital & R / I is distributive )
let v be Element of (R / I); ::_thesis: v + (0. (R / I)) = v
consider a, b being Element of R such that
A11: v = Class ((EqRel (R,I)),a) and
A12: 0. (R / I) = Class ((EqRel (R,I)),b) and
A13: the addF of (R / I) . (v,(0. (R / I))) = Class ((EqRel (R,I)),(a + b)) by Def6;
A14: b - (0. R) = b by RLVECT_1:13;
A15: (a + b) - a = (a - a) + b by RLVECT_1:28
.= (0. R) + b by RLVECT_1:15
.= b by RLVECT_1:def_4 ;
 0. (R / I) = Class ((EqRel (R,I)),(0. R)) by Def6;
then  b - (0. R) in I by A12, Th6;
hence  v + (0. (R / I)) = v by A11, A13, A14, A15, Th6; ::_thesis: verum
end;
thus  R / I is right_complementable ::_thesis: ( R / I is associative & R / I is well-unital & R / I is distributive )
proof
let v be Element of (R / I); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
consider a, b being Element of R such that
A16: v = Class ((EqRel (R,I)),a) and
 0. (R / I) = Class ((EqRel (R,I)),b) and
 the addF of (R / I) . (v,(0. (R / I))) = Class ((EqRel (R,I)),(a + b)) by Def6;
reconsider w = Class ((EqRel (R,I)),(- a)) as Element of (R / I) by Th12;
take  w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. (R / I)
A17: 0. (R / I) = Class ((EqRel (R,I)),(0. R)) by Def6;
thus v + w = Class ((EqRel (R,I)),(a + (- a))) by A16, Th13
.= 0. (R / I) by A17, RLVECT_1:def_10 ; ::_thesis: verum
end;
hereby  :: according to GROUP_1:def_3 ::_thesis: ( R / I is well-unital & R / I is distributive )
let x, y, z be Element of (R / I); ::_thesis: (x * y) * z = x * (y * z)
consider a being Element of R such that
A18: x = Class ((EqRel (R,I)),a) by Th11;
consider ab being Element of R such that
A19: x * y = Class ((EqRel (R,I)),ab) by Th11;
consider c being Element of R such that
A20: z = Class ((EqRel (R,I)),c) by Th11;
consider b being Element of R such that
A21: y = Class ((EqRel (R,I)),b) by Th11;
 x * y = Class ((EqRel (R,I)),(a * b)) by A18, A21, Th14;
then  ab - (a * b) in I by A19, Th6;
then A22: (ab - (a * b)) * c in I by IDEAL_1:def_3;
consider bc being Element of R such that
A23: y * z = Class ((EqRel (R,I)),bc) by Th11;
 y * z = Class ((EqRel (R,I)),(b * c)) by A21, A20, Th14;
then  bc - (b * c) in I by A23, Th6;
then A24: a * (bc - (b * c)) in I by IDEAL_1:def_2;
A25: ( (ab - (a * b)) * c = (ab * c) - ((a * b) * c) & a * (bc - (b * c)) = (a * bc) - (a * (b * c)) ) by VECTSP_1:11, VECTSP_1:13;
 ( a * (b * c) = (a * b) * c & ((ab * c) - ((a * b) * c)) - ((a * bc) - ((a * b) * c)) = (ab * c) - (a * bc) ) by Th3, GROUP_1:def_3;
then A26: (ab * c) - (a * bc) in I by A22, A24, A25, IDEAL_1:15;
thus (x * y) * z = Class ((EqRel (R,I)),(ab * c)) by A20, A19, Th14
.= Class ((EqRel (R,I)),(a * bc)) by A26, Th6
.= x * (y * z) by A18, A23, Th14 ; ::_thesis: verum
end;
 ( 1. R = 1_ R & Class ((EqRel (R,I)),(1. R)) = 1. (R / I) ) by Def6;
hence  for x being Element of (R / I) holds
( x * (1. (R / I)) = x & (1. (R / I)) * x = x ) by Lm2; :: according to VECTSP_1:def_6 ::_thesis: R / I is distributive
let x, y, z be Element of (R / I); :: according to VECTSP_1:def_7 ::_thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
consider a being Element of R such that
A27: x = Class ((EqRel (R,I)),a) by Th11;
consider ab being Element of R such that
A28: x * y = Class ((EqRel (R,I)),ab) by Th11;
consider ca being Element of R such that
A29: z * x = Class ((EqRel (R,I)),ca) by Th11;
consider c being Element of R such that
A30: z = Class ((EqRel (R,I)),c) by Th11;
 z * x = Class ((EqRel (R,I)),(c * a)) by A27, A30, Th14;
then A31: (c * a) - ca in I by A29, Th6;
consider b being Element of R such that
A32: y = Class ((EqRel (R,I)),b) by Th11;
 x * y = Class ((EqRel (R,I)),(a * b)) by A27, A32, Th14;
then A33: ab - (a * b) in I by A28, Th6;
consider ac being Element of R such that
A34: x * z = Class ((EqRel (R,I)),ac) by Th11;
 x * z = Class ((EqRel (R,I)),(a * c)) by A27, A30, Th14;
then A35: ac - (a * c) in I by A34, Th6;
consider bc being Element of R such that
A36: y + z = Class ((EqRel (R,I)),bc) by Th11;
 y + z = Class ((EqRel (R,I)),(b + c)) by A32, A30, Th13;
then A37: bc - (b + c) in I by A36, Th6;
then A38: (bc - (b + c)) * a in I by IDEAL_1:def_3;
 a * (bc - (b + c)) in I by A37, IDEAL_1:def_2;
then  (a * (bc - (b + c))) - (ab - (a * b)) in I by A33, IDEAL_1:15;
then A39: ((a * (bc - (b + c))) - (ab - (a * b))) - (ac - (a * c)) in I by A35, IDEAL_1:15;
A40: ((a * (bc - (b + c))) - (ab - (a * b))) - (ac - (a * c)) = (((a * bc) - (a * (b + c))) - (ab - (a * b))) - (ac - (a * c)) by VECTSP_1:11
.= (((a * bc) - ((a * b) + (a * c))) - (ab - (a * b))) - (ac - (a * c)) by VECTSP_1:def_2
.= ((((a * bc) - (a * b)) - (a * c)) - (ab - (a * b))) - (ac - (a * c)) by RLVECT_1:27
.= (((((a * bc) - (a * b)) - (a * c)) - ab) + (a * b)) - (ac - (a * c)) by RLVECT_1:29
.= ((((((a * bc) - (a * b)) - (a * c)) - ab) + (a * b)) - ac) + (a * c) by RLVECT_1:29
.= ((((((a * bc) - (a * b)) - (a * c)) + (a * b)) - ab) - ac) + (a * c) by RLVECT_1:28
.= ((((((a * bc) - (a * b)) + (a * b)) - (a * c)) - ab) - ac) + (a * c) by RLVECT_1:28
.= ((((a * bc) - (a * c)) - ab) - ac) + (a * c) by Th1
.= ((((a * bc) - (a * c)) - ab) + (a * c)) - ac by RLVECT_1:28
.= ((((a * bc) - (a * c)) + (a * c)) - ab) - ac by RLVECT_1:28
.= ((a * bc) - ab) - ac by Th1
.= (a * bc) - (ab + ac) by RLVECT_1:27 ;
thus x * (y + z) = Class ((EqRel (R,I)),(a * bc)) by A27, A36, Th14
.= Class ((EqRel (R,I)),(ab + ac)) by A39, A40, Th6
.= (x * y) + (x * z) by A28, A34, Th13 ; ::_thesis: (y + z) * x = (y * x) + (z * x)
consider ba being Element of R such that
A41: y * x = Class ((EqRel (R,I)),ba) by Th11;
 y * x = Class ((EqRel (R,I)),(b * a)) by A27, A32, Th14;
then  (b * a) - ba in I by A41, Th6;
then  ((bc - (b + c)) * a) + ((b * a) - ba) in I by A38, IDEAL_1:def_1;
then A42: (((bc - (b + c)) * a) + ((b * a) - ba)) + ((c * a) - ca) in I by A31, IDEAL_1:def_1;
A43: (((bc - (b + c)) * a) + ((b * a) - ba)) + ((c * a) - ca) = (((bc * a) - ((b + c) * a)) + ((b * a) - ba)) + ((c * a) - ca) by VECTSP_1:13
.= (((bc * a) - ((b * a) + (c * a))) + ((b * a) - ba)) + ((c * a) - ca) by VECTSP_1:def_3
.= ((((bc * a) - (b * a)) - (c * a)) + ((b * a) - ba)) + ((c * a) - ca) by RLVECT_1:27
.= (((((bc * a) - (b * a)) - (c * a)) + (b * a)) - ba) + ((c * a) - ca) by RLVECT_1:28
.= ((((((bc * a) - (b * a)) - (c * a)) + (b * a)) - ba) + (c * a)) - ca by RLVECT_1:28
.= ((((((bc * a) - (b * a)) + (b * a)) - (c * a)) - ba) + (c * a)) - ca by RLVECT_1:28
.= ((((bc * a) - (c * a)) - ba) + (c * a)) - ca by Th1
.= ((((bc * a) - (c * a)) + (c * a)) - ba) - ca by RLVECT_1:28
.= ((bc * a) - ba) - ca by Th1
.= (bc * a) - (ba + ca) by RLVECT_1:27 ;
thus (y + z) * x = Class ((EqRel (R,I)),(bc * a)) by A27, A36, Th14
.= Class ((EqRel (R,I)),(ba + ca)) by A42, A43, Th6
.= (y * x) + (z * x) by A41, A29, Th13 ; ::_thesis: verum
end;
end;

registration
let R be commutative Ring;
let I be Ideal of R;
cluster QuotientRing (R,I) ->  strict commutative ;
coherence
 R / I is commutative
proof
set E = EqRel (R,I);
let x, y be Element of (R / I); :: according to GROUP_1:def_12 ::_thesis: x * y = y * x
consider a being Element of R such that
A1: x = Class ((EqRel (R,I)),a) by Th11;
consider b being Element of R such that
A2: y = Class ((EqRel (R,I)),b) by Th11;
thus x * y = Class ((EqRel (R,I)),(a * b)) by A1, A2, Th14
.= y * x by A1, A2, Th14 ; ::_thesis: verum
end;
end;

theorem Th16: :: RING_1:16
for R being Ring
for I being Ideal of R holds
( I is proper iff not R / I is degenerated )
proof
let R be Ring; ::_thesis: for I being Ideal of R holds
( I is proper iff not R / I is degenerated )
let I be Ideal of R; ::_thesis: ( I is proper iff not R / I is degenerated )
set E = EqRel (R,I);
A1: (1. R) - (0. R) = 1. R by RLVECT_1:13;
A2: ( 0. (R / I) = Class ((EqRel (R,I)),(0. R)) & 1. (R / I) = Class ((EqRel (R,I)),(1. R)) ) by Def6;
thus  ( I is proper implies not R / I is degenerated ) ::_thesis: ( not R / I is degenerated implies I is proper )
proof
assume that
A3: I is proper and
A4: 0. (R / I) = 1. (R / I) ; :: according to STRUCT_0:def_8 ::_thesis: contradiction
 (1. R) - (0. R) in I by A2, A4, Th6;
hence  contradiction by A1, A3, IDEAL_1:19; ::_thesis: verum
end;
assume A5: not R / I is degenerated ; ::_thesis: I is proper
assume  not I is proper ; ::_thesis: contradiction
then  1. R in I by IDEAL_1:19;
hence  contradiction by A2, A1, A5, Th6; ::_thesis: verum
end;

theorem Th17: :: RING_1:17
for R being Ring
for I being Ideal of R holds
( I is quasi-prime iff R / I is domRing-like )
proof
let R be Ring; ::_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, Def1;
 ( 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, VECTSP_2:def_1;
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
end;

theorem :: RING_1:18
for R being commutative Ring
for I being Ideal of R holds
( I is prime iff R / I is domRing )
proof
let R be commutative Ring; ::_thesis: for I being Ideal of R holds
( I is prime iff R / I is domRing )
let I be Ideal of R; ::_thesis: ( I is prime iff R / I is domRing )
thus  ( I is prime implies R / I is domRing ) by Th16, Th17; ::_thesis: ( R / I is domRing implies I is prime )
assume  R / I is domRing ; ::_thesis: I is prime
hence  ( I is proper & I is quasi-prime ) by Th16, Th17; :: according to RING_1:def_2 ::_thesis: verum
end;

theorem Th19: :: RING_1:19
for R being Ring
for I being Ideal of R st R is commutative & I is quasi-maximal holds
R / I is almost_left_invertible
proof
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: 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, GROUP_1:def_12
.= x * p by A7, VECTSP_1:def_3
.= p * x by A1, GROUP_1:def_12 ;
hence  p * x in M by A9; ::_thesis: verum
end;
A10: 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:6
.= 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, GROUP_1:def_12
.= 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) by VECTSP_1:def_4
.= a by RLVECT_1:def_4 ;
then  a in M by A5;
then  not M is proper by A2, A15, A6, A11, A21, A10, Def3;
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, GROUP_1:def_12
.= 1. (R / I) by A24, A25, A26, Th6 ; ::_thesis: verum
end;

theorem Th20: :: RING_1:20
for R being Ring
for I being Ideal of R st R / I is almost_left_invertible holds
I is quasi-maximal
proof
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, XBOOLE_0:def_10;
then consider a being set  such that
A5: a in J and
A6: not a in I by TARSKI:def_3;
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)
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 consider y being Element of (R / I) such that
A8: y * x = 1. (R / I) by A1, VECTSP_1:def_9;
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
end;

theorem :: RING_1:21
for R being commutative Ring
for I being Ideal of R holds
( I is maximal iff R / I is Skew-Field )
proof
let R be commutative Ring; ::_thesis: for I being Ideal of R holds
( I is maximal iff R / I is Skew-Field )
let I be Ideal of R; ::_thesis: ( I is maximal iff R / I is Skew-Field )
thus  ( I is maximal implies R / I is Skew-Field ) by Th16, Th19; ::_thesis: ( R / I is Skew-Field implies I is maximal )
assume  R / I is Skew-Field ; ::_thesis: I is maximal
hence  ( I is proper & I is quasi-maximal ) by Th16, Th20; :: according to RING_1:def_4 ::_thesis: verum
end;

registration
let R be non degenerated commutative Ring;
cluster non empty add-closed left-ideal right-ideal maximal  ->  prime for Element of K32( the carrier of R);
coherence
 for b1 being Ideal of R st b1 is maximal holds
b1 is prime
proof
let I be Ideal of R; ::_thesis: ( I is maximal implies I is prime )
assume A1: ( I is proper & I is quasi-maximal ) ; :: according to RING_1:def_4 ::_thesis: I is prime
then  ( R / I is almost_left_invertible & not R / I is degenerated ) by Th16, Th19;
hence  ( I is proper & I is quasi-prime ) by A1, Th17; :: according to RING_1:def_2 ::_thesis: verum
end;
end;

registration
let R be non degenerated Ring;
cluster non empty add-closed left-ideal right-ideal maximal for Element of K32( the carrier of R);
existence
 ex b1 being Ideal of R st b1 is maximal
proof
set S =  {  A where A is Ideal of R : A is proper  }  ;
set P = RelIncl  {  A where A is Ideal of R : A is proper  }  ;
A1: RelIncl  {  A where A is Ideal of R : A is proper  }  is_antisymmetric_in  {  A where A is Ideal of R : A is proper  }  by WELLORD2:21;
A2: field (RelIncl  {  A where A is Ideal of R : A is proper  }  ) =  {  A where A is Ideal of R : A is proper  }  by WELLORD2:def_1;
A3:  {  A where A is Ideal of R : A is proper  }  has_upper_Zorn_property_wrt RelIncl  {  A where A is Ideal of R : A is proper  }
proof
let Y be set ; :: according to ORDERS_1:def_9 ::_thesis: ( not Y c=  {  A where A is Ideal of R : A is proper  }  or not (RelIncl  {  A where A is Ideal of R : A is proper  }  ) |_2 Y is being_linear-order or ex b1 being set st
( b1 in  {  A where A is Ideal of R : A is proper  }  & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl  {  A where A is Ideal of R : A is proper  }  ) ) ) )
assume that
A4: Y c=  {  A where A is Ideal of R : A is proper  }  and
A5: (RelIncl  {  A where A is Ideal of R : A is proper  }  ) |_2 Y is being_linear-order ; ::_thesis: ex b1 being set st
( b1 in  {  A where A is Ideal of R : A is proper  }  & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl  {  A where A is Ideal of R : A is proper  }  ) ) )
percases ( Y is empty or not Y is empty ) ;
supposeA6: Y is empty ; ::_thesis: ex b1 being set st
( b1 in  {  A where A is Ideal of R : A is proper  }  & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl  {  A where A is Ideal of R : A is proper  }  ) ) )
take x = {(0. R)} -Ideal ; ::_thesis: ( x in  {  A where A is Ideal of R : A is proper  }  & ( for b1 being set holds
( not b1 in Y or [b1,x] in RelIncl  {  A where A is Ideal of R : A is proper  }  ) ) )
now__::_thesis:_x_is_proper
assume  not x is proper ; ::_thesis: contradiction
then A7: x = the carrier of R by SUBSET_1:def_6;
 x = {(0. R)} by IDEAL_1:47;
then  1. R = 0. R by A7, TARSKI:def_1;
hence  contradiction ; ::_thesis: verum
end;
hence  x in  {  A where A is Ideal of R : A is proper  }  ; ::_thesis: for b1 being set holds
( not b1 in Y or [b1,x] in RelIncl  {  A where A is Ideal of R : A is proper  }  )
thus  for b1 being set holds
( not b1 in Y or [b1,x] in RelIncl  {  A where A is Ideal of R : A is proper  }  ) by A6; ::_thesis: verum
end;
suppose not Y is empty ; ::_thesis: ex b1 being set st
( b1 in  {  A where A is Ideal of R : A is proper  }  & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl  {  A where A is Ideal of R : A is proper  }  ) ) )
then consider e being set  such that
A8: e in Y by XBOOLE_0:def_1;
take x = union Y; ::_thesis: ( x in  {  A where A is Ideal of R : A is proper  }  & ( for b1 being set holds
( not b1 in Y or [b1,x] in RelIncl  {  A where A is Ideal of R : A is proper  }  ) ) )
 x c= the carrier of R
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in x or a in the carrier of R )
assume  a in x ; ::_thesis: a in the carrier of R
then consider Z being set  such that
A9: a in Z and
A10: Z in Y by TARSKI:def_4;
 Z in  {  A where A is Ideal of R : A is proper  }  by A4, A10;
then  ex A being Ideal of R st
( Z = A & A is proper ) ;
hence  a in the carrier of R by A9; ::_thesis: verum
end;
then reconsider B = x as Subset of R ;
A11: B is right-ideal
proof
let p, a be Element of R; :: according to IDEAL_1:def_3 ::_thesis: ( not a in B or a * p in B )
assume  a in B ; ::_thesis: a * p in B
then consider Aa being set  such that
A12: a in Aa and
A13: Aa in Y by TARSKI:def_4;
 Aa in  {  A where A is Ideal of R : A is proper  }  by A4, A13;
then consider Ia being Ideal of R such that
A14: Aa = Ia and
 Ia is proper ;
 ( a * p in Ia & Ia c= B ) by A12, A13, A14, IDEAL_1:def_3, ZFMISC_1:74;
hence  a * p in B ; ::_thesis: verum
end;
A15: B is left-ideal
proof
let p, a be Element of R; :: according to IDEAL_1:def_2 ::_thesis: ( not a in B or p * a in B )
assume  a in B ; ::_thesis: p * a in B
then consider Aa being set  such that
A16: a in Aa and
A17: Aa in Y by TARSKI:def_4;
 Aa in  {  A where A is Ideal of R : A is proper  }  by A4, A17;
then consider Ia being Ideal of R such that
A18: Aa = Ia and
 Ia is proper ;
 ( p * a in Ia & Ia c= B ) by A16, A17, A18, IDEAL_1:def_2, ZFMISC_1:74;
hence  p * a in B ; ::_thesis: verum
end;
A19: now__::_thesis:_B_is_proper
assume  not B is proper ; ::_thesis: contradiction
then  1. R in B by A15, IDEAL_1:19;
then consider Aa being set  such that
A20: 1. R in Aa and
A21: Aa in Y by TARSKI:def_4;
 Aa in  {  A where A is Ideal of R : A is proper  }  by A4, A21;
then  ex Ia being Ideal of R st
( Aa = Ia & Ia is proper ) ;
hence  contradiction by A20, IDEAL_1:19; ::_thesis: verum
end;
A22: B is add-closed
proof
 RelIncl  {  A where A is Ideal of R : A is proper  }  is_reflexive_in field (RelIncl  {  A where A is Ideal of R : A is proper  }  ) by A2, WELLORD2:19;
then  RelIncl  {  A where A is Ideal of R : A is proper  }  is reflexive by RELAT_2:def_9;
then A23: field ((RelIncl  {  A where A is Ideal of R : A is proper  }  ) |_2 Y) = Y by A2, A4, ORDERS_1:71;
let a, b be Element of R; :: according to IDEAL_1:def_1 ::_thesis: ( not a in B or not b in B or a + b in B )
A24: now__::_thesis:_for_A_being_Ideal_of_R_st_a_in_A_&_b_in_A_&_A_in_Y_holds_
a_+_b_in_B
let A be Ideal of R; ::_thesis: ( a in A & b in A & A in Y implies a + b in B )
assume  ( a in A & b in A ) ; ::_thesis: ( A in Y implies a + b in B )
then A25: a + b in A by IDEAL_1:def_1;
assume  A in Y ; ::_thesis: a + b in B
hence  a + b in B by A25, TARSKI:def_4; ::_thesis: verum
end;
assume  a in B ; ::_thesis: ( not b in B or a + b in B )
then consider Aa being set  such that
A26: a in Aa and
A27: Aa in Y by TARSKI:def_4;
 Aa in  {  A where A is Ideal of R : A is proper  }  by A4, A27;
then A28: ex Ia being Ideal of R st
( Aa = Ia & Ia is proper ) ;
assume  b in B ; ::_thesis: a + b in B
then consider Ab being set  such that
A29: b in Ab and
A30: Ab in Y by TARSKI:def_4;
 (RelIncl  {  A where A is Ideal of R : A is proper  }  ) |_2 Y is connected by A5, ORDERS_1:def_5;
then  (RelIncl  {  A where A is Ideal of R : A is proper  }  ) |_2 Y is_connected_in field ((RelIncl  {  A where A is Ideal of R : A is proper  }  ) |_2 Y) by RELAT_2:def_14;
then  ( [Aa,Ab] in (RelIncl  {  A where A is Ideal of R : A is proper  }  ) |_2 Y or [Ab,Aa] in (RelIncl  {  A where A is Ideal of R : A is proper  }  ) |_2 Y or Aa = Ab ) by A27, A30, A23, RELAT_2:def_6;
then  ( [Aa,Ab] in RelIncl  {  A where A is Ideal of R : A is proper  }  or [Ab,Aa] in RelIncl  {  A where A is Ideal of R : A is proper  }  or Aa = Ab ) by XBOOLE_0:def_4;
then A31: ( Aa c= Ab or Ab c= Aa ) by A4, A27, A30, WELLORD2:def_1;
 Ab in  {  A where A is Ideal of R : A is proper  }  by A4, A30;
then  ex Ib being Ideal of R st
( Ab = Ib & Ib is proper ) ;
hence  a + b in B by A26, A27, A29, A30, A24, A28, A31; ::_thesis: verum
end;
 e in  {  A where A is Ideal of R : A is proper  }  by A4, A8;
then consider A being Ideal of R such that
A32: e = A and
 A is proper ;
 ex q being set st q in A by XBOOLE_0:def_1;
then  not B is empty by A8, A32, TARSKI:def_4;
hence A33: x in  {  A where A is Ideal of R : A is proper  }  by A22, A15, A11, A19; ::_thesis: for b1 being set holds
( not b1 in Y or [b1,x] in RelIncl  {  A where A is Ideal of R : A is proper  }  )
let y be set ; ::_thesis: ( not y in Y or [y,x] in RelIncl  {  A where A is Ideal of R : A is proper  }  )
assume A34: y in Y ; ::_thesis: [y,x] in RelIncl  {  A where A is Ideal of R : A is proper  }
then  y c= x by ZFMISC_1:74;
hence  [y,x] in RelIncl  {  A where A is Ideal of R : A is proper  }  by A4, A33, A34, WELLORD2:def_1; ::_thesis: verum
end;
end;
end;
 ( RelIncl  {  A where A is Ideal of R : A is proper  }  is_reflexive_in  {  A where A is Ideal of R : A is proper  }  & RelIncl  {  A where A is Ideal of R : A is proper  }  is_transitive_in  {  A where A is Ideal of R : A is proper  }  ) by WELLORD2:19, WELLORD2:20;
then  RelIncl  {  A where A is Ideal of R : A is proper  }  partially_orders  {  A where A is Ideal of R : A is proper  }  by A1, ORDERS_1:def_7;
then consider x being set  such that
A35: x is_maximal_in RelIncl  {  A where A is Ideal of R : A is proper  }  by A2, A3, ORDERS_1:63;
A36: x in field (RelIncl  {  A where A is Ideal of R : A is proper  }  ) by A35, ORDERS_1:def_11;
then consider I being Ideal of R such that
A37: x = I and
A38: I is proper by A2;
take  I ; ::_thesis: I is maximal
thus  I is proper by A38; :: according to RING_1:def_4 ::_thesis: I is quasi-maximal
let J be Ideal of R; :: according to RING_1:def_3 ::_thesis: ( not I c= J or J = I or not J is proper )
assume A39: I c= J ; ::_thesis: ( J = I or not J is proper )
now__::_thesis:_(_J_is_proper_implies_I_=_J_)
assume  J is proper ; ::_thesis: I = J
then A40: J in  {  A where A is Ideal of R : A is proper  }  ;
then  [I,J] in RelIncl  {  A where A is Ideal of R : A is proper  }  by A2, A36, A37, A39, WELLORD2:def_1;
hence  I = J by A2, A35, A37, A40, ORDERS_1:def_11; ::_thesis: verum
end;
hence  ( J = I or not J is proper ) ; ::_thesis: verum
end;
end;

registration
let R be non degenerated commutative Ring;
cluster non empty add-closed left-ideal right-ideal maximal for Element of K32( the carrier of R);
existence
 ex b1 being Ideal of R st b1 is maximal
proof
set I = the maximal Ideal of R;
take  the maximal Ideal of R ; ::_thesis: the maximal Ideal of R is maximal
thus  the maximal Ideal of R is maximal ; ::_thesis: verum
end;
end;

registration
let R be non degenerated commutative Ring;
let I be quasi-prime Ideal of R;
cluster QuotientRing (R,I) ->  strict domRing-like ;
coherence
 R / I is domRing-like by Th17;
end;

registration
let R be non degenerated commutative Ring;
let I be quasi-maximal Ideal of R;
cluster QuotientRing (R,I) ->  almost_left_invertible strict ;
coherence
 R / I is almost_left_invertible by Th19;
end;