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