:: by Artur Korni{\l}owicz

::

:: Received December 7, 2005

:: Copyright (c) 2005-2017 Association of Mizar Users

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

for a, b being Element of L holds (a - b) + b = a

proof 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)

for b, c being Element of L holds c = b - (b - c)

proof 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

for a, b, c being Element of L holds (a - b) - (c - b) = a - c

proof end;

definition

let K be non empty multMagma ;

let S be Subset of K;

end;
let S be Subset of K;

attr S is quasi-prime means :: 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 );

for a, b being Element of K holds

( not a * b in S or a in S or b in S );

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

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

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

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;

end;
let I be Subset of R;

attr I is quasi-maximal means :: RING_1:def 3

for J being Ideal of R holds

( not I c= J or J = I or not J is proper );

for J being Ideal of R holds

( not I c= J or J = I or not J is proper );

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

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

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

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 ;

coherence

for b_{1} being Subset of K st b_{1} is prime holds

( b_{1} is proper & b_{1} is quasi-prime )
;

coherence

for b_{1} being Subset of K st b_{1} is proper & b_{1} is quasi-prime holds

b_{1} is prime
;

end;
coherence

for b

( b

coherence

for b

b

registration

let R be non empty doubleLoopStr ;

coherence

for b_{1} being Subset of R st b_{1} is maximal holds

( b_{1} is proper & b_{1} is quasi-maximal )
;

coherence

for b_{1} being Subset of R st b_{1} is proper & b_{1} is quasi-maximal holds

b_{1} is maximal
;

end;
coherence

for b

( b

coherence

for b

b

registration
end;

registration
end;

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

definition

let R be Ring;

let I be Ideal of R;

ex b_{1} being Relation of R st

for a, b being Element of R holds

( [a,b] in b_{1} iff a - b in I )

for b_{1}, b_{2} being Relation of R st ( for a, b being Element of R holds

( [a,b] in b_{1} iff a - b in I ) ) & ( for a, b being Element of R holds

( [a,b] in b_{2} iff a - b in I ) ) holds

b_{1} = b_{2}

end;
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 for a, b being Element of R holds

( [a,b] in it iff a - b in I );

ex b

for a, b being Element of R holds

( [a,b] in b

proof end;

uniqueness for b

( [a,b] in b

( [a,b] in b

b

proof end;

:: deftheorem Def5 defines EqRel RING_1:def 5 :

for R being Ring

for I being Ideal of R

for b_{3} being Relation of R holds

( b_{3} = EqRel (R,I) iff for a, b being Element of R holds

( [a,b] in b_{3} iff a - b in I ) );

for R being Ring

for I being Ideal of R

for b

( b

( [a,b] in b

registration

let R be Ring;

let I be Ideal of R;

coherence

( not EqRel (R,I) is empty & EqRel (R,I) is total & EqRel (R,I) is symmetric & EqRel (R,I) is transitive )

end;
let I be Ideal of R;

coherence

( not EqRel (R,I) is empty & EqRel (R,I) is total & EqRel (R,I) is symmetric & EqRel (R,I) is transitive )

proof 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 )

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

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

definition

let R be Ring;

let I be Ideal of R;

ex b_{1} being strict doubleLoopStr st

( the carrier of b_{1} = Class (EqRel (R,I)) & 1. b_{1} = Class ((EqRel (R,I)),(1. R)) & 0. b_{1} = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of b_{1} ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of b_{1} . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of b_{1} ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of b_{1} . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) )

for b_{1}, b_{2} being strict doubleLoopStr st the carrier of b_{1} = Class (EqRel (R,I)) & 1. b_{1} = Class ((EqRel (R,I)),(1. R)) & 0. b_{1} = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of b_{1} ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of b_{1} . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of b_{1} ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of b_{1} . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) & the carrier of b_{2} = Class (EqRel (R,I)) & 1. b_{2} = Class ((EqRel (R,I)),(1. R)) & 0. b_{2} = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of b_{2} ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of b_{2} . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of b_{2} ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of b_{2} . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) holds

b_{1} = b_{2}

end;
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 ( 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)) ) ) );

ex b

( the carrier of b

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of b

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of b

proof end;

uniqueness for b

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of b

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of b

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of b

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of b

b

proof end;

:: deftheorem Def6 defines QuotientRing RING_1:def 6 :

for R being Ring

for I being Ideal of R

for b_{3} being strict doubleLoopStr holds

( b_{3} = QuotientRing (R,I) iff ( the carrier of b_{3} = Class (EqRel (R,I)) & 1. b_{3} = Class ((EqRel (R,I)),(1. R)) & 0. b_{3} = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of b_{3} ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of b_{3} . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of b_{3} ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of b_{3} . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) ) );

for R being Ring

for I being Ideal of R

for b

( b

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of b

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of b

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)

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

for I being Ideal of R

for a being Element of R holds Class ((EqRel (R,I)),a) is Element of (R / I)

proof 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))

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

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

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 ;

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 ;

thus e * h = Class ((EqRel (R,I)),(a * b)) by A2, A3, Th14

.= h by A3, A5, A8, Th6 ; :: thesis: verum

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

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 ;

thus e * h = Class ((EqRel (R,I)),(a * b)) by A2, A3, Th14

.= h by A3, A5, A8, Th6 ; :: thesis: verum

theorem :: RING_1:15

registration

let R be Ring;

let I be Ideal of R;

( 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 )

end;
let I be Ideal of R;

cluster QuotientRing (R,I) -> right_complementable strict well-unital distributive Abelian add-associative right_zeroed associative ;

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

registration
end;

theorem :: RING_1:18

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

for I being Ideal of R st R is commutative & I is quasi-maximal holds

R / I is almost_left_invertible

proof 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 ) by Th16, Th19, Th20;

for I being Ideal of R holds

( I is maximal iff R / I is Skew-Field ) by Th16, Th19, Th20;

registration

let R be non degenerated commutative Ring;

for b_{1} being Ideal of R st b_{1} is maximal holds

b_{1} is prime

end;
cluster non empty add-closed left-ideal right-ideal maximal -> prime for Element of K34( the carrier of R);

coherence for b

b

proof end;

:: Krull's theorem

registration
end;

registration

let R be non degenerated commutative Ring;

existence

ex b_{1} being Ideal of R st b_{1} is maximal

end;
existence

ex b

proof end;

registration

let R be non degenerated commutative Ring;

let I be quasi-prime Ideal of R;

coherence

R / I is domRing-like by Th17;

end;
let I be quasi-prime Ideal of R;

coherence

R / I is domRing-like by Th17;

registration

let R be non degenerated commutative Ring;

let I be quasi-maximal Ideal of R;

coherence

R / I is almost_left_invertible by Th19;

end;
let I be quasi-maximal Ideal of R;

coherence

R / I is almost_left_invertible by Th19;