:: by Artur Korni{\l}owicz and Christoph Schwarzweller

::

:: Received November 29, 2014

:: Copyright (c) 2014-2018 Association of Mizar Users

definition

let R be non empty set ;

let f be non empty FinSequence of R;

let x be Element of dom f;

:: original: .

redefine func f . x -> Element of R;

coherence

f . x is Element of R

end;
let f be non empty FinSequence of R;

let x be Element of dom f;

:: original: .

redefine func f . x -> Element of R;

coherence

f . x is Element of R

proof end;

registration
end;

theorem prod4: :: RING_2:1

for R being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr

for F being FinSequence of R st ex i being Nat st

( i in dom F & F . i = 0. R ) holds

Product F = 0. R

for F being FinSequence of R st ex i being Nat st

( i in dom F & F . i = 0. R ) holds

Product F = 0. R

proof end;

theorem prod5: :: RING_2:2

for R being non degenerated right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr

for F being FinSequence of R holds

( Product F = 0. R iff ex i being Nat st

( i in dom F & F . i = 0. R ) )

for F being FinSequence of R holds

( Product F = 0. R iff ex i being Nat st

( i in dom F & F . i = 0. R ) )

proof end;

definition

let X be non empty set ;

let C be Chain of X;

end;
let C be Chain of X;

attr C is stagnating means :: RING_2:def 2

ex i being Nat st

for j being Nat st j >= i holds

C . j = C . i;

ex i being Nat st

for j being Nat st j >= i holds

C . j = C . i;

:: deftheorem asc defines ascending RING_2:def 1 :

for X being non empty set

for C being Chain of X holds

( C is ascending iff for i being Nat holds C . i c= C . (i + 1) );

for X being non empty set

for C being Chain of X holds

( C is ascending iff for i being Nat holds C . i c= C . (i + 1) );

:: deftheorem defines stagnating RING_2:def 2 :

for X being non empty set

for C being Chain of X holds

( C is stagnating iff ex i being Nat st

for j being Nat st j >= i holds

C . j = C . i );

for X being non empty set

for C being Chain of X holds

( C is stagnating iff ex i being Nat st

for j being Nat st j >= i holds

C . j = C . i );

registration

let X be non empty set ;

let x be Element of X;

coherence

for b_{1} being Chain of X st b_{1} = NAT --> x holds

( b_{1} is ascending & b_{1} is stagnating )

end;
let x be Element of X;

coherence

for b

( b

proof end;

registration

let X be non empty set ;

ex b_{1} being Chain of X st

( b_{1} is ascending & b_{1} is stagnating )

end;
cluster Relation-like NAT -defined X -valued Function-like non empty total quasi_total ascending stagnating for Chain of ;

existence ex b

( b

proof end;

ch1: for X being non empty set

for C being ascending Chain of X

for x being object

for i, j being Nat st i <= j & x in C . i holds

x in C . j

proof end;

theorem :: RING_2:3

definition

let R be Ring;

{ I where I is Ideal of R : verum } is Subset-Family of the carrier of R

end;
func Ideals R -> Subset-Family of the carrier of R equals :: RING_2:def 3

{ I where I is Ideal of R : verum } ;

coherence { I where I is Ideal of R : verum } ;

{ I where I is Ideal of R : verum } is Subset-Family of the carrier of R

proof end;

:: deftheorem defines Ideals RING_2:def 3 :

for R being Ring holds Ideals R = { I where I is Ideal of R : verum } ;

for R being Ring holds Ideals R = { I where I is Ideal of R : verum } ;

registration
end;

theorem id1: :: RING_2:5

for R being Ring

for C being ascending Chain of (Ideals R) holds union { (C . i) where i is Nat : verum } is Ideal of R

for C being ascending Chain of (Ideals R) holds union { (C . i) where i is Nat : verum } is Ideal of R

proof end;

registration

let R be non empty doubleLoopStr ;

let S be non empty right_zeroed doubleLoopStr ;

coherence

R --> (0. S) is additive

end;
let S be non empty right_zeroed doubleLoopStr ;

coherence

R --> (0. S) is additive

proof end;

registration

let R be non empty doubleLoopStr ;

let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;

coherence

R --> (0. S) is multiplicative

end;
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;

coherence

R --> (0. S) is multiplicative

proof end;

registration

let R be non empty well-unital doubleLoopStr ;

let S be non degenerated well-unital doubleLoopStr ;

coherence

not R --> (0. S) is unity-preserving by FUNCOP_1:7;

end;
let S be non degenerated well-unital doubleLoopStr ;

coherence

not R --> (0. S) is unity-preserving by FUNCOP_1:7;

registration

let R be non empty doubleLoopStr ;

coherence

( id R is additive & id R is multiplicative & id R is unity-preserving ) ;

end;
coherence

( id R is additive & id R is multiplicative & id R is unity-preserving ) ;

registration

let R be non empty doubleLoopStr ;

coherence

( id R is RingMonomorphism & id R is RingEpimorphism ) ;

end;
coherence

( id R is RingMonomorphism & id R is RingEpimorphism ) ;

registration

let R be non empty doubleLoopStr ;

let S be non empty right_zeroed doubleLoopStr ;

ex b_{1} being Function of R,S st b_{1} is additive

end;
let S be non empty right_zeroed doubleLoopStr ;

cluster Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty total quasi_total additive for Function of ,;

existence ex b

proof end;

registration

let R be non empty doubleLoopStr ;

let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;

ex b_{1} being Function of R,S st b_{1} is multiplicative

end;
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;

cluster Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty total quasi_total multiplicative for Function of ,;

existence ex b

proof end;

registration

let R, S be non empty well-unital doubleLoopStr ;

ex b_{1} being Function of R,S st b_{1} is unity-preserving

end;
cluster Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty total quasi_total unity-preserving for Function of ,;

existence ex b

proof end;

registration

let R be non empty doubleLoopStr ;

let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;

ex b_{1} being Function of R,S st

( b_{1} is additive & b_{1} is multiplicative )

end;
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;

cluster Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty total quasi_total additive multiplicative for Function of ,;

existence ex b

( b

proof end;

definition

let R, S be Ring;

end;
attr S is R -homomorphic means :defhom: :: RING_2:def 4

ex f being Function of R,S st f is RingHomomorphism ;

ex f being Function of R,S st f is RingHomomorphism ;

:: deftheorem defhom defines -homomorphic RING_2:def 4 :

for R, S being Ring holds

( S is R -homomorphic iff ex f being Function of R,S st f is RingHomomorphism );

for R, S being Ring holds

( S is R -homomorphic iff ex f being Function of R,S st f is RingHomomorphism );

registration

let R be Ring;

ex b_{1} being Ring st b_{1} is R -homomorphic

end;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V115() unital associative V124() V125() V126() V127() R -homomorphic for Ring;

existence ex b

proof end;

registration

let R be comRing;

ex b_{1} being comRing st b_{1} is R -homomorphic

ex b_{1} being Ring st b_{1} is R -homomorphic

end;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V115() unital associative commutative V124() V125() V126() V127() R -homomorphic for comRing;

existence ex b

proof end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V115() unital associative V124() V125() V126() V127() R -homomorphic for Ring;

existence ex b

proof end;

registration

let R be Field;

ex b_{1} being Field st b_{1} is R -homomorphic

ex b_{1} being comRing st b_{1} is R -homomorphic

ex b_{1} being Ring st b_{1} is R -homomorphic

end;
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V115() unital associative commutative V124() V125() V126() V127() domRing-like gcd-like Euclidian R -homomorphic for Field;

existence ex b

proof end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V115() unital associative commutative V124() V125() V126() V127() R -homomorphic for comRing;

existence ex b

proof end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V115() unital associative V124() V125() V126() V127() R -homomorphic for Ring;

existence ex b

proof end;

registration

let R be Ring;

let S be R -homomorphic Ring;

ex b_{1} being Function of R,S st

( b_{1} is additive & b_{1} is multiplicative & b_{1} is unity-preserving )

end;
let S be R -homomorphic Ring;

cluster Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty total quasi_total additive unity-preserving multiplicative for Function of ,;

existence ex b

( b

proof end;

definition

let R be Ring;

let S be R -homomorphic Ring;

mode Homomorphism of R,S is additive unity-preserving multiplicative Function of R,S;

end;
let S be R -homomorphic Ring;

mode Homomorphism of R,S is additive unity-preserving multiplicative Function of R,S;

registration

let R, S, T be Ring;

let f be unity-preserving Function of R,S;

let g be unity-preserving Function of S,T;

coherence

for b_{1} being Function of R,T st b_{1} = g * f holds

b_{1} is unity-preserving

end;
let f be unity-preserving Function of R,S;

let g be unity-preserving Function of S,T;

coherence

for b

b

proof end;

registration

let R be Ring;

let S be R -homomorphic Ring;

for b_{1} being S -homomorphic Ring holds b_{1} is R -homomorphic

end;
let S be R -homomorphic Ring;

cluster non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative S -homomorphic -> R -homomorphic S -homomorphic for Ring;

coherence for b

proof end;

notation
end;

theorem hom1: :: RING_2:6

for R being non empty right_complementable add-associative right_zeroed doubleLoopStr

for S being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr

for f being additive Function of R,S holds f . (0. R) = 0. S

for S being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr

for f being additive Function of R,S holds f . (0. R) = 0. S

proof end;

theorem hom4a: :: RING_2:7

for R being non empty right_complementable add-associative right_zeroed doubleLoopStr

for S being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr

for f being additive Function of R,S

for x being Element of R holds f . (- x) = - (f . x)

for S being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr

for f being additive Function of R,S

for x being Element of R holds f . (- x) = - (f . x)

proof end;

theorem hom4: :: RING_2:8

for R being non empty right_complementable add-associative right_zeroed doubleLoopStr

for S being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr

for f being additive Function of R,S

for x, y being Element of R holds f . (x - y) = (f . x) - (f . y)

for S being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr

for f being additive Function of R,S

for x, y being Element of R holds f . (x - y) = (f . x) - (f . y)

proof end;

theorem hom2: :: RING_2:9

for R being non empty right_unital doubleLoopStr

for S being non empty right_complementable right-distributive right_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr

for f being multiplicative Function of R,S holds

( f . (1. R) = 0. S or f . (1. R) = 1. S )

for S being non empty right_complementable right-distributive right_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr

for f being multiplicative Function of R,S holds

( f . (1. R) = 0. S or f . (1. R) = 1. S )

proof end;

hom3: for E, F being Field

for f being additive multiplicative Function of E,F holds

( ( f . (1. E) = 0. F & f = E --> (0. F) ) or ( f . (1. E) = 1. F & f is monomorphism ) )

proof end;

theorem :: RING_2:10

for E, F being Field

for f being additive multiplicative Function of E,F holds

( f . (1. E) = 0. F iff f = E --> (0. F) )

for f being additive multiplicative Function of E,F holds

( f . (1. E) = 0. F iff f = E --> (0. F) )

proof end;

theorem hom3a: :: RING_2:11

for E, F being Field

for f being additive multiplicative Function of E,F holds

( f . (1. E) = 1. F iff f is monomorphism )

for f being additive multiplicative Function of E,F holds

( f . (1. E) = 1. F iff f is monomorphism )

proof end;

registration

let E, F be Field;

for b_{1} being Function of E,F st b_{1} is additive & b_{1} is multiplicative & b_{1} is unity-preserving holds

b_{1} is monomorphism
by hom3a;

end;
cluster Function-like quasi_total additive unity-preserving multiplicative -> monomorphism for Function of ,;

coherence for b

b

definition

let R be Ring;

let I be Ideal of R;

ex b_{1} being Function of R,(R / I) st

for a being Element of R holds b_{1} . a = Class ((EqRel (R,I)),a)

for b_{1}, b_{2} being Function of R,(R / I) st ( for a being Element of R holds b_{1} . a = Class ((EqRel (R,I)),a) ) & ( for a being Element of R holds b_{2} . a = Class ((EqRel (R,I)),a) ) holds

b_{1} = b_{2}

end;
let I be Ideal of R;

func canHom I -> Function of R,(R / I) means :defhomI: :: RING_2:def 5

for a being Element of R holds it . a = Class ((EqRel (R,I)),a);

existence for a being Element of R holds it . a = Class ((EqRel (R,I)),a);

ex b

for a being Element of R holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defhomI defines canHom RING_2:def 5 :

for R being Ring

for I being Ideal of R

for b_{3} being Function of R,(R / I) holds

( b_{3} = canHom I iff for a being Element of R holds b_{3} . a = Class ((EqRel (R,I)),a) );

for R being Ring

for I being Ideal of R

for b

( b

registration

let R be Ring;

let I be Ideal of R;

coherence

( canHom I is additive & canHom I is multiplicative & canHom I is unity-preserving )

end;
let I be Ideal of R;

coherence

( canHom I is additive & canHom I is multiplicative & canHom I is unity-preserving )

proof end;

registration
end;

registration

let R be non empty right_complementable add-associative right_zeroed doubleLoopStr ;

let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;

let f be additive Function of R,S;

coherence

not ker f is empty

end;
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;

let f be additive Function of R,S;

coherence

not ker f is empty

proof end;

ker1: for R, S being non empty doubleLoopStr

for f being Function of R,S

for x being Element of R st x in ker f holds

f . x = 0. S

proof end;

registration

let R be non empty doubleLoopStr ;

let S be non empty right_complementable add-associative right_zeroed doubleLoopStr ;

let f be additive Function of R,S;

coherence

ker f is add-closed

end;
let S be non empty right_complementable add-associative right_zeroed doubleLoopStr ;

let f be additive Function of R,S;

coherence

ker f is add-closed

proof end;

registration

let R be non empty doubleLoopStr ;

let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;

let f be multiplicative Function of R,S;

coherence

ker f is left-ideal

end;
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;

let f be multiplicative Function of R,S;

coherence

ker f is left-ideal

proof end;

registration

let R be non empty doubleLoopStr ;

let S be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;

let f be multiplicative Function of R,S;

coherence

ker f is right-ideal

end;
let S be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;

let f be multiplicative Function of R,S;

coherence

ker f is right-ideal

proof end;

registration

let R be non empty well-unital doubleLoopStr ;

let S be non degenerated well-unital doubleLoopStr ;

let f be unity-preserving Function of R,S;

coherence

ker f is proper

end;
let S be non degenerated well-unital doubleLoopStr ;

let f be unity-preserving Function of R,S;

coherence

ker f is proper

proof end;

theorem ker0: :: RING_2:12

for R being Ring

for S being b_{1} -homomorphic Ring

for f being Homomorphism of R,S holds

( f is monomorphism iff ker f = {(0. R)} )

for S being b

for f being Homomorphism of R,S holds

( f is monomorphism iff ker f = {(0. R)} )

proof end;

theorem :: RING_2:14

for R being Ring

for I being Subset of R holds

( I is Ideal of R iff ex S being b_{1} -homomorphic Ring ex f being Homomorphism of R,S st ker f = I )

for I being Subset of R holds

( I is Ideal of R iff ex S being b

proof end;

T0: for R being Ring

for S being b

for f being Homomorphism of R,S holds 0. S in rng f

proof end;

T1: for R being Ring

for S being b

for f being Homomorphism of R,S holds 1. S in rng f

proof end;

T3: for R being Ring

for S being b

for f being Homomorphism of R,S holds rng f is Preserv of the addF of S

proof end;

T4: for R being Ring

for S being b

for f being Homomorphism of R,S holds rng f is Preserv of the multF of S

proof end;

definition

let R be Ring;

let S be R -homomorphic Ring;

let f be Homomorphism of R,S;

ex b_{1} being strict doubleLoopStr st

( the carrier of b_{1} = rng f & the addF of b_{1} = the addF of S || (rng f) & the multF of b_{1} = the multF of S || (rng f) & the OneF of b_{1} = 1. S & the ZeroF of b_{1} = 0. S )

for b_{1}, b_{2} being strict doubleLoopStr st the carrier of b_{1} = rng f & the addF of b_{1} = the addF of S || (rng f) & the multF of b_{1} = the multF of S || (rng f) & the OneF of b_{1} = 1. S & the ZeroF of b_{1} = 0. S & the carrier of b_{2} = rng f & the addF of b_{2} = the addF of S || (rng f) & the multF of b_{2} = the multF of S || (rng f) & the OneF of b_{2} = 1. S & the ZeroF of b_{2} = 0. S holds

b_{1} = b_{2}
;

end;
let S be R -homomorphic Ring;

let f be Homomorphism of R,S;

func Image f -> strict doubleLoopStr means :defim: :: RING_2:def 6

( the carrier of it = rng f & the addF of it = the addF of S || (rng f) & the multF of it = the multF of S || (rng f) & the OneF of it = 1. S & the ZeroF of it = 0. S );

existence ( the carrier of it = rng f & the addF of it = the addF of S || (rng f) & the multF of it = the multF of S || (rng f) & the OneF of it = 1. S & the ZeroF of it = 0. S );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem defim defines Image RING_2:def 6 :

for R being Ring

for S being b_{1} -homomorphic Ring

for f being Homomorphism of R,S

for b_{4} being strict doubleLoopStr holds

( b_{4} = Image f iff ( the carrier of b_{4} = rng f & the addF of b_{4} = the addF of S || (rng f) & the multF of b_{4} = the multF of S || (rng f) & the OneF of b_{4} = 1. S & the ZeroF of b_{4} = 0. S ) );

for R being Ring

for S being b

for f being Homomorphism of R,S

for b

( b

T5: for R being Ring

for S being b

for f being Homomorphism of R,S

for a, b being Element of (Image f)

for x, y being Element of S st a = x & b = y holds

( a + b = x + y & a * b = x * y )

proof end;

T6: for R being Ring

for S being b

for f being Homomorphism of R,S

for a being Element of (Image f) ex x being Element of R st f . x = a

proof end;

registration

let R be Ring;

let S be R -homomorphic Ring;

let f be Homomorphism of R,S;

coherence

not Image f is empty

end;
let S be R -homomorphic Ring;

let f be Homomorphism of R,S;

coherence

not Image f is empty

proof end;

registration

let R be Ring;

let S be R -homomorphic Ring;

let f be Homomorphism of R,S;

coherence

( Image f is Abelian & Image f is add-associative & Image f is right_zeroed & Image f is right_complementable )

end;
let S be R -homomorphic Ring;

let f be Homomorphism of R,S;

coherence

( Image f is Abelian & Image f is add-associative & Image f is right_zeroed & Image f is right_complementable )

proof end;

registration

let R be Ring;

let S be R -homomorphic Ring;

let f be Homomorphism of R,S;

coherence

( Image f is associative & Image f is well-unital & Image f is distributive )

end;
let S be R -homomorphic Ring;

let f be Homomorphism of R,S;

coherence

( Image f is associative & Image f is well-unital & Image f is distributive )

proof end;

registration

let R be comRing;

let S be R -homomorphic comRing;

let f be Homomorphism of R,S;

coherence

Image f is commutative

end;
let S be R -homomorphic comRing;

let f be Homomorphism of R,S;

coherence

Image f is commutative

proof end;

definition

let R be Ring;

let S be R -homomorphic Ring;

let f be Homomorphism of R,S;

:: original: Image

redefine func Image f -> strict Subring of S;

coherence

Image f is strict Subring of S

end;
let S be R -homomorphic Ring;

let f be Homomorphism of R,S;

:: original: Image

redefine func Image f -> strict Subring of S;

coherence

Image f is strict Subring of S

proof end;

definition

let R be Ring;

let S be R -homomorphic Ring;

let f be Homomorphism of R,S;

ex b_{1} being Function of (R / (ker f)),(Image f) st

for a being Element of R holds b_{1} . (Class ((EqRel (R,(ker f))),a)) = f . a

for b_{1}, b_{2} being Function of (R / (ker f)),(Image f) st ( for a being Element of R holds b_{1} . (Class ((EqRel (R,(ker f))),a)) = f . a ) & ( for a being Element of R holds b_{2} . (Class ((EqRel (R,(ker f))),a)) = f . a ) holds

b_{1} = b_{2}

end;
let S be R -homomorphic Ring;

let f be Homomorphism of R,S;

func canHom f -> Function of (R / (ker f)),(Image f) means :ch: :: RING_2:def 7

for a being Element of R holds it . (Class ((EqRel (R,(ker f))),a)) = f . a;

existence for a being Element of R holds it . (Class ((EqRel (R,(ker f))),a)) = f . a;

ex b

for a being Element of R holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem ch defines canHom RING_2:def 7 :

for R being Ring

for S being b_{1} -homomorphic Ring

for f being Homomorphism of R,S

for b_{4} being Function of (R / (ker f)),(Image f) holds

( b_{4} = canHom f iff for a being Element of R holds b_{4} . (Class ((EqRel (R,(ker f))),a)) = f . a );

for R being Ring

for S being b

for f being Homomorphism of R,S

for b

( b

registration

let R be Ring;

let S be R -homomorphic Ring;

let f be Homomorphism of R,S;

coherence

( canHom f is additive & canHom f is multiplicative & canHom f is unity-preserving )

end;
let S be R -homomorphic Ring;

let f be Homomorphism of R,S;

coherence

( canHom f is additive & canHom f is multiplicative & canHom f is unity-preserving )

proof end;

registration

let R be Ring;

let S be R -homomorphic Ring;

let f be Homomorphism of R,S;

coherence

( canHom f is RingMonomorphism & canHom f is RingEpimorphism )

end;
let S be R -homomorphic Ring;

let f be Homomorphism of R,S;

coherence

( canHom f is RingMonomorphism & canHom f is RingEpimorphism )

proof end;

theorem :: RING_2:15

for R being Ring

for S being b_{1} -homomorphic Ring

for f being Homomorphism of R,S holds R / (ker f), Image f are_isomorphic

for S being b

for f being Homomorphism of R,S holds R / (ker f), Image f are_isomorphic

proof end;

theorem :: RING_2:16

for R being Ring

for S being b_{1} -homomorphic Ring

for f being Homomorphism of R,S st f is onto holds

R / (ker f),S are_isomorphic

for S being b

for f being Homomorphism of R,S st f is onto holds

R / (ker f),S are_isomorphic

proof end;

registration
end;

registration

let L be non empty right_unital multLoopStr ;

existence

ex b_{1} being Element of L st b_{1} is unital

end;
existence

ex b

proof end;

registration

let L be non degenerated right_complementable left-distributive add-associative right_zeroed doubleLoopStr ;

not for b_{1} being Element of L holds b_{1} is unital

end;
cluster left_add-cancelable right_add-cancelable add-cancelable right_complementable non unital for Element of L;

existence not for b

proof end;

definition

let L be non degenerated right_complementable left-distributive add-associative right_zeroed doubleLoopStr ;

mode NonUnit of L is non unital Element of L;

end;
mode NonUnit of L is non unital Element of L;

registration

let L be non degenerated right_complementable left-distributive add-associative right_zeroed doubleLoopStr ;

coherence

not 0. L is unital

end;
coherence

not 0. L is unital

proof end;

registration

let L be non degenerated right_complementable left-distributive right_unital add-associative right_zeroed doubleLoopStr ;

coherence

for b_{1} being Unit of L holds not b_{1} is zero
;

end;
coherence

for b

registration
end;

registration
end;

definition

let R be non empty right_unital doubleLoopStr ;

let x be Element of R;

end;
let x be Element of R;

attr x is prime means :defprim: :: RING_2:def 8

( x <> 0. R & x is not Unit of R & ( for a, b being Element of R holds

( not x divides a * b or x divides a or x divides b ) ) );

( x <> 0. R & x is not Unit of R & ( for a, b being Element of R holds

( not x divides a * b or x divides a or x divides b ) ) );

attr x is irreducible means :: RING_2:def 9

( x <> 0. R & x is not Unit of R & ( for a being Element of R holds

( not a divides x or a is Unit of R or a is_associated_to x ) ) );

( x <> 0. R & x is not Unit of R & ( for a being Element of R holds

( not a divides x or a is Unit of R or a is_associated_to x ) ) );

:: deftheorem defprim defines prime RING_2:def 8 :

for R being non empty right_unital doubleLoopStr

for x being Element of R holds

( x is prime iff ( x <> 0. R & x is not Unit of R & ( for a, b being Element of R holds

( not x divides a * b or x divides a or x divides b ) ) ) );

for R being non empty right_unital doubleLoopStr

for x being Element of R holds

( x is prime iff ( x <> 0. R & x is not Unit of R & ( for a, b being Element of R holds

( not x divides a * b or x divides a or x divides b ) ) ) );

:: deftheorem defines irreducible RING_2:def 9 :

for R being non empty right_unital doubleLoopStr

for x being Element of R holds

( x is irreducible iff ( x <> 0. R & x is not Unit of R & ( for a being Element of R holds

( not a divides x or a is Unit of R or a is_associated_to x ) ) ) );

for R being non empty right_unital doubleLoopStr

for x being Element of R holds

( x is irreducible iff ( x <> 0. R & x is not Unit of R & ( for a being Element of R holds

( not a divides x or a is Unit of R or a is_associated_to x ) ) ) );

notation

let R be non empty right_unital doubleLoopStr ;

let x be Element of R;

antonym reducible x for irreducible ;

end;
let x be Element of R;

antonym reducible x for irreducible ;

registration

let R be non empty right_unital doubleLoopStr ;

existence

not for b_{1} being Element of R holds b_{1} is prime

end;
existence

not for b

proof end;

lemintr: for x, y being Integer

for a, b being Element of INT.Ring st x <> 0 & x = a & y = b holds

( x divides y iff a divides b )

proof end;

registration

ex b_{1} being Element of INT.Ring st b_{1} is prime
end;

cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable V106() integer complex ext-real V192() prime for Element of INT.Ring;

existence ex b

proof end;

registration

let R be non empty right_unital doubleLoopStr ;

coherence

for b_{1} being Element of R st b_{1} is prime holds

( not b_{1} is zero & not b_{1} is unital )
;

coherence

for b_{1} being Element of R st b_{1} is irreducible holds

( not b_{1} is zero & not b_{1} is unital )
;

end;
coherence

for b

( not b

coherence

for b

( not b

registration

let R be domRing;

coherence

for b_{1} being Element of R st b_{1} is prime holds

b_{1} is irreducible

end;
coherence

for b

b

proof end;

definition

let R be non empty right_unital doubleLoopStr ;

{ x where x is Element of R : x is irreducible } is Subset of R

end;
func IRR R -> Subset of R equals :: RING_2:def 10

{ x where x is Element of R : x is irreducible } ;

coherence { x where x is Element of R : x is irreducible } ;

{ x where x is Element of R : x is irreducible } is Subset of R

proof end;

:: deftheorem defines IRR RING_2:def 10 :

for R being non empty right_unital doubleLoopStr holds IRR R = { x where x is Element of R : x is irreducible } ;

for R being non empty right_unital doubleLoopStr holds IRR R = { x where x is Element of R : x is irreducible } ;

theorem ass0: :: RING_2:22

for R being domRing

for c being non zero Element of R

for b, a, d being Element of R st a * b is_associated_to c * d & a is_associated_to c holds

b is_associated_to d

for c being non zero Element of R

for b, a, d being Element of R st a * b is_associated_to c * d & a is_associated_to c holds

b is_associated_to d

proof end;

theorem ass1: :: RING_2:23

for R being domRing

for a, b being Element of R st a is irreducible & b is_associated_to a holds

b is irreducible

for a, b being Element of R st a is irreducible & b is_associated_to a holds

b is irreducible

proof end;

theorem thpr: :: RING_2:24

for R being non degenerated comRing

for a being non zero Element of R holds

( a is prime iff {a} -Ideal is prime )

for a being non zero Element of R holds

( a is prime iff {a} -Ideal is prime )

proof end;

theorem maxirr: :: RING_2:25

for R being non degenerated comRing

for a being non zero Element of R st {a} -Ideal is maximal holds

a is irreducible

for a being non zero Element of R st {a} -Ideal is maximal holds

a is irreducible

proof end;

registration

for b_{1} being Field holds b_{1} is PID
end;

cluster non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative -> PID for Field;

coherence for b

proof end;

theorem maxirr2: :: RING_2:26

for R being PIDomain

for a being non zero Element of R holds

( {a} -Ideal is maximal iff a is irreducible )

for a being non zero Element of R holds

( {a} -Ideal is maximal iff a is irreducible )

proof end;

registration

let R be PIDomain;

coherence

for b_{1} being Element of R st b_{1} is irreducible holds

b_{1} is prime

end;
coherence

for b

b

proof end;

registration

for b_{1} being comRing st b_{1} is Euclidian holds

b_{1} is PID
by IDEAL_1:94;

end;

cluster non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative Euclidian -> PID for comRing;

coherence for b

b

registration

let R be PIDomain;

coherence

for b_{1} being Chain of (Ideals R) st b_{1} is ascending holds

b_{1} is stagnating

end;
coherence

for b

b

proof end;

definition

let R be non empty right_unital doubleLoopStr ;

let x be Element of R;

let F be non empty FinSequence of R;

end;
let x be Element of R;

let F be non empty FinSequence of R;

pred F is_a_factorization_of x means :: RING_2:def 11

( x = Product F & ( for i being Element of dom F holds F . i is irreducible ) );

( x = Product F & ( for i being Element of dom F holds F . i is irreducible ) );

:: deftheorem defines is_a_factorization_of RING_2:def 11 :

for R being non empty right_unital doubleLoopStr

for x being Element of R

for F being non empty FinSequence of R holds

( F is_a_factorization_of x iff ( x = Product F & ( for i being Element of dom F holds F . i is irreducible ) ) );

for R being non empty right_unital doubleLoopStr

for x being Element of R

for F being non empty FinSequence of R holds

( F is_a_factorization_of x iff ( x = Product F & ( for i being Element of dom F holds F . i is irreducible ) ) );

definition

let R be non empty right_unital doubleLoopStr ;

let x be Element of R;

end;
let x be Element of R;

attr x is factorizable means :: RING_2:def 12

ex F being non empty FinSequence of R st F is_a_factorization_of x;

ex F being non empty FinSequence of R st F is_a_factorization_of x;

:: deftheorem defines factorizable RING_2:def 12 :

for R being non empty right_unital doubleLoopStr

for x being Element of R holds

( x is factorizable iff ex F being non empty FinSequence of R st F is_a_factorization_of x );

for R being non empty right_unital doubleLoopStr

for x being Element of R holds

( x is factorizable iff ex F being non empty FinSequence of R st F is_a_factorization_of x );

definition

let R be non empty right_unital doubleLoopStr ;

let x be Element of R;

assume AS: x is factorizable ;

ex b_{1} being non empty FinSequence of R st b_{1} is_a_factorization_of x
by AS;

end;
let x be Element of R;

assume AS: x is factorizable ;

mode Factorization of x -> non empty FinSequence of R means :ddf: :: RING_2:def 13

it is_a_factorization_of x;

existence it is_a_factorization_of x;

ex b

:: deftheorem ddf defines Factorization RING_2:def 13 :

for R being non empty right_unital doubleLoopStr

for x being Element of R st x is factorizable holds

for b_{3} being non empty FinSequence of R holds

( b_{3} is Factorization of x iff b_{3} is_a_factorization_of x );

for R being non empty right_unital doubleLoopStr

for x being Element of R st x is factorizable holds

for b

( b

definition

let R be non empty right_unital doubleLoopStr ;

let x be Element of R;

end;
let x be Element of R;

attr x is uniquely_factorizable means :: RING_2:def 14

( x is factorizable & ( for F, G being Factorization of x ex B being Function of (dom F),(dom G) st

( B is bijective & ( for i being Element of dom F holds G . (B . i) is_associated_to F . i ) ) ) );

( x is factorizable & ( for F, G being Factorization of x ex B being Function of (dom F),(dom G) st

( B is bijective & ( for i being Element of dom F holds G . (B . i) is_associated_to F . i ) ) ) );

:: deftheorem defines uniquely_factorizable RING_2:def 14 :

for R being non empty right_unital doubleLoopStr

for x being Element of R holds

( x is uniquely_factorizable iff ( x is factorizable & ( for F, G being Factorization of x ex B being Function of (dom F),(dom G) st

( B is bijective & ( for i being Element of dom F holds G . (B . i) is_associated_to F . i ) ) ) ) );

for R being non empty right_unital doubleLoopStr

for x being Element of R holds

( x is uniquely_factorizable iff ( x is factorizable & ( for F, G being Factorization of x ex B being Function of (dom F),(dom G) st

( B is bijective & ( for i being Element of dom F holds G . (B . i) is_associated_to F . i ) ) ) ) );

registration

let R be non empty right_unital doubleLoopStr ;

coherence

for b_{1} being Element of R st b_{1} is uniquely_factorizable holds

b_{1} is factorizable
;

end;
coherence

for b

b

registration

let R be domRing;

coherence

for b_{1} being Element of R st b_{1} is factorizable holds

( not b_{1} is zero & not b_{1} is unital )

end;
coherence

for b

( not b

proof end;

fact1: for R being non empty right_unital doubleLoopStr

for a being Element of R holds

( a is irreducible iff <*a*> is_a_factorization_of a )

proof end;

registration

let R be non empty right_unital doubleLoopStr ;

coherence

for b_{1} being Element of R st b_{1} is irreducible holds

b_{1} is factorizable

end;
coherence

for b

b

proof end;

theorem :: RING_2:27

for R being non empty right_unital doubleLoopStr

for a being Element of R holds

( a is irreducible iff <*a*> is_a_factorization_of a ) by fact1;

for a being Element of R holds

( a is irreducible iff <*a*> is_a_factorization_of a ) by fact1;

theorem fact2: :: RING_2:28

for R being non empty well-unital associative doubleLoopStr

for a, b being Element of R

for F, G being non empty FinSequence of R st F is_a_factorization_of a & G is_a_factorization_of b holds

F ^ G is_a_factorization_of a * b

for a, b being Element of R

for F, G being non empty FinSequence of R st F is_a_factorization_of a & G is_a_factorization_of b holds

F ^ G is_a_factorization_of a * b

proof end;

lemfactunique1: for R being domRing

for a, b, x being Element of R

for F being non empty FinSequence of R st x is prime & x divides a & a is_associated_to b & F is_a_factorization_of b holds

ex i being Element of dom F st F . i is_associated_to x

proof end;

lemfactunique: for R being PIDomain

for x, y being Element of R

for F, G being non empty FinSequence of R st F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y holds

ex p being Function of (dom F),(dom G) st

( p is bijective & ( for i being Element of dom F holds G . (p . i) is_associated_to F . i ) )

proof end;

registration

let R be PIDomain;

coherence

for b_{1} being Element of R st b_{1} is factorizable holds

b_{1} is uniquely_factorizable

end;
coherence

for b

b

proof end;

definition

let R be non degenerated Ring;

end;
attr R is factorial means :df: :: RING_2:def 15

for a being non zero Element of R st a is NonUnit of R holds

a is uniquely_factorizable ;

for a being non zero Element of R st a is NonUnit of R holds

a is uniquely_factorizable ;

:: deftheorem df defines factorial RING_2:def 15 :

for R being non degenerated Ring holds

( R is factorial iff for a being non zero Element of R st a is NonUnit of R holds

a is uniquely_factorizable );

for R being non degenerated Ring holds

( R is factorial iff for a being non zero Element of R st a is NonUnit of R holds

a is uniquely_factorizable );

registration

ex b_{1} being non degenerated Ring st b_{1} is factorial
end;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V115() unital associative V124() V125() V126() V127() factorial for Ring;

existence ex b

proof end;

registration

let R be non degenerated factorial Ring;

coherence

for b_{1} being Element of R st not b_{1} is zero & not b_{1} is unital holds

b_{1} is factorizable

end;
coherence

for b

b

proof end;

registration

for b_{1} being domRing st b_{1} is PID holds

b_{1} is factorial
end;

cluster non empty non degenerated right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative PID domRing-like -> factorial for domRing;

coherence for b

b

proof end;

definition

let L be Field;

let p be Polynomial of L;

coherence

( ( p <> 0_. L implies deg p is Nat ) & ( not p <> 0_. L implies 0 is Nat ) )

for b_{1} being Nat holds verum
;

end;
let p be Polynomial of L;

coherence

( ( p <> 0_. L implies deg p is Nat ) & ( not p <> 0_. L implies 0 is Nat ) )

proof end;

consistency for b

:: deftheorem S defines deg* RING_2:def 16 :

for L being Field

for p being Polynomial of L holds

( ( p <> 0_. L implies deg* p = deg p ) & ( not p <> 0_. L implies deg* p = 0 ) );

for L being Field

for p being Polynomial of L holds

( ( p <> 0_. L implies deg* p = deg p ) & ( not p <> 0_. L implies deg* p = 0 ) );

definition

let L be Field;

ex b_{1} being Function of (Polynom-Ring L),NAT st

for p being Polynomial of L holds b_{1} . p = deg* p

for b_{1}, b_{2} being Function of (Polynom-Ring L),NAT st ( for p being Polynomial of L holds b_{1} . p = deg* p ) & ( for p being Polynomial of L holds b_{2} . p = deg* p ) holds

b_{1} = b_{2}

end;
func deg* L -> Function of (Polynom-Ring L),NAT means :T: :: RING_2:def 17

for p being Polynomial of L holds it . p = deg* p;

existence for p being Polynomial of L holds it . p = deg* p;

ex b

for p being Polynomial of L holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem T defines deg* RING_2:def 17 :

for L being Field

for b_{2} being Function of (Polynom-Ring L),NAT holds

( b_{2} = deg* L iff for p being Polynomial of L holds b_{2} . p = deg* p );

for L being Field

for b

( b

theorem degA: :: RING_2:29

for L being Field

for p being Polynomial of L

for q being non zero Polynomial of L holds deg (p mod q) < deg q

for p being Polynomial of L

for q being non zero Polynomial of L holds deg (p mod q) < deg q

proof end;

theorem thEucl1: :: RING_2:30

for L being Field

for p being Element of (Polynom-Ring L)

for q being non zero Element of (Polynom-Ring L) ex u, r being Element of (Polynom-Ring L) st

( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or (deg* L) . r < (deg* L) . q ) )

for p being Element of (Polynom-Ring L)

for q being non zero Element of (Polynom-Ring L) ex u, r being Element of (Polynom-Ring L) st

( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or (deg* L) . r < (deg* L) . q ) )

proof end;

thEucl2: for L being Field ex f being Function of (Polynom-Ring L),NAT st

for p, q being Element of (Polynom-Ring L) st q <> 0. (Polynom-Ring L) holds

ex u, r being Element of (Polynom-Ring L) st

( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or f . r < f . q ) )

proof end;

definition

let L be Field;

:: original: deg*

redefine func deg* L -> DegreeFunction of Polynom-Ring L;

coherence

deg* L is DegreeFunction of Polynom-Ring L

end;
:: original: deg*

redefine func deg* L -> DegreeFunction of Polynom-Ring L;

coherence

deg* L is DegreeFunction of Polynom-Ring L

proof end;