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

::

:: Received August 14, 2015

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

theorem Th1: :: RING_3:1

for f being Function

for A being set

for a, b being object st a in A & b in A holds

(f || A) . (a,b) = f . (a,b)

for A being set

for a, b being object st a in A & b in A holds

(f || A) . (a,b) = f . (a,b)

proof end;

theorem Th9: :: RING_3:9

for g, m being Nat

for i being Integer st g divides i & g divides m holds

i / m = (i div g) / (m div g)

for i being Integer st g divides i & g divides m holds

i / m = (i div g) / (m div g)

proof end;

theorem Th15: :: RING_3:15

for m being Nat

for i being Integer st m <> 0 holds

( denominator (i / m) = m div (i gcd m) & numerator (i / m) = i div (i gcd m) )

for i being Integer st m <> 0 holds

( denominator (i / m) = m div (i gcd m) & numerator (i / m) = i div (i gcd m) )

proof end;

theorem :: RING_3:16

for m being Nat

for i being Integer st m <> 0 holds

( denominator (i / m) = m / (i gcd m) & numerator (i / m) = i / (i gcd m) )

for i being Integer st m <> 0 holds

( denominator (i / m) = m / (i gcd m) & numerator (i / m) = i / (i gcd m) )

proof end;

theorem Th17: :: RING_3:17

for m being Nat

for i being Integer st m <> 0 holds

( denominator (- (i / m)) = m div ((- i) gcd m) & numerator (- (i / m)) = (- i) div ((- i) gcd m) )

for i being Integer st m <> 0 holds

( denominator (- (i / m)) = m div ((- i) gcd m) & numerator (- (i / m)) = (- i) div ((- i) gcd m) )

proof end;

theorem :: RING_3:18

for m being Nat

for i being Integer st m <> 0 holds

( denominator (- (i / m)) = m / ((- i) gcd m) & numerator (- (i / m)) = (- i) / ((- i) gcd m) )

for i being Integer st m <> 0 holds

( denominator (- (i / m)) = m / ((- i) gcd m) & numerator (- (i / m)) = (- i) / ((- i) gcd m) )

proof end;

theorem Th19: :: RING_3:19

for m being Nat

for i being Integer st m <> 0 holds

( denominator ((m / i) ") = m div (m gcd i) & numerator ((m / i) ") = i div (m gcd i) )

for i being Integer st m <> 0 holds

( denominator ((m / i) ") = m div (m gcd i) & numerator ((m / i) ") = i div (m gcd i) )

proof end;

theorem :: RING_3:20

for m being Nat

for i being Integer st m <> 0 holds

( denominator ((m / i) ") = m / (m gcd i) & numerator ((m / i) ") = i / (m gcd i) )

for i being Integer st m <> 0 holds

( denominator ((m / i) ") = m / (m gcd i) & numerator ((m / i) ") = i / (m gcd i) )

proof end;

theorem Th21: :: RING_3:21

for m, n being Nat

for i, j being Integer st m <> 0 & n <> 0 holds

( denominator ((i / m) + (j / n)) = (m * n) div (((i * n) + (j * m)) gcd (m * n)) & numerator ((i / m) + (j / n)) = ((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n)) )

for i, j being Integer st m <> 0 & n <> 0 holds

( denominator ((i / m) + (j / n)) = (m * n) div (((i * n) + (j * m)) gcd (m * n)) & numerator ((i / m) + (j / n)) = ((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n)) )

proof end;

theorem :: RING_3:22

for m, n being Nat

for i, j being Integer st m <> 0 & n <> 0 holds

( denominator ((i / m) + (j / n)) = (m * n) / (((i * n) + (j * m)) gcd (m * n)) & numerator ((i / m) + (j / n)) = ((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n)) )

for i, j being Integer st m <> 0 & n <> 0 holds

( denominator ((i / m) + (j / n)) = (m * n) / (((i * n) + (j * m)) gcd (m * n)) & numerator ((i / m) + (j / n)) = ((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n)) )

proof end;

theorem Th23: :: RING_3:23

for m, n being Nat

for i, j being Integer st m <> 0 & n <> 0 holds

( denominator ((i / m) - (j / n)) = (m * n) div (((i * n) - (j * m)) gcd (m * n)) & numerator ((i / m) - (j / n)) = ((i * n) - (j * m)) div (((i * n) - (j * m)) gcd (m * n)) )

for i, j being Integer st m <> 0 & n <> 0 holds

( denominator ((i / m) - (j / n)) = (m * n) div (((i * n) - (j * m)) gcd (m * n)) & numerator ((i / m) - (j / n)) = ((i * n) - (j * m)) div (((i * n) - (j * m)) gcd (m * n)) )

proof end;

theorem :: RING_3:24

for m, n being Nat

for i, j being Integer st m <> 0 & n <> 0 holds

( denominator ((i / m) - (j / n)) = (m * n) / (((i * n) - (j * m)) gcd (m * n)) & numerator ((i / m) - (j / n)) = ((i * n) - (j * m)) / (((i * n) - (j * m)) gcd (m * n)) )

for i, j being Integer st m <> 0 & n <> 0 holds

( denominator ((i / m) - (j / n)) = (m * n) / (((i * n) - (j * m)) gcd (m * n)) & numerator ((i / m) - (j / n)) = ((i * n) - (j * m)) / (((i * n) - (j * m)) gcd (m * n)) )

proof end;

theorem Th25: :: RING_3:25

for m, n being Nat

for i, j being Integer st m <> 0 & n <> 0 holds

( denominator ((i / m) * (j / n)) = (m * n) div ((i * j) gcd (m * n)) & numerator ((i / m) * (j / n)) = (i * j) div ((i * j) gcd (m * n)) )

for i, j being Integer st m <> 0 & n <> 0 holds

( denominator ((i / m) * (j / n)) = (m * n) div ((i * j) gcd (m * n)) & numerator ((i / m) * (j / n)) = (i * j) div ((i * j) gcd (m * n)) )

proof end;

theorem :: RING_3:26

for m, n being Nat

for i, j being Integer st m <> 0 & n <> 0 holds

( denominator ((i / m) * (j / n)) = (m * n) / ((i * j) gcd (m * n)) & numerator ((i / m) * (j / n)) = (i * j) / ((i * j) gcd (m * n)) )

for i, j being Integer st m <> 0 & n <> 0 holds

( denominator ((i / m) * (j / n)) = (m * n) / ((i * j) gcd (m * n)) & numerator ((i / m) * (j / n)) = (i * j) / ((i * j) gcd (m * n)) )

proof end;

theorem Th27: :: RING_3:27

for m, n being Nat

for i, j being Integer st m <> 0 & n <> 0 holds

( denominator ((i / m) / (n / j)) = (m * n) div ((i * j) gcd (m * n)) & numerator ((i / m) / (n / j)) = (i * j) div ((i * j) gcd (m * n)) )

for i, j being Integer st m <> 0 & n <> 0 holds

( denominator ((i / m) / (n / j)) = (m * n) div ((i * j) gcd (m * n)) & numerator ((i / m) / (n / j)) = (i * j) div ((i * j) gcd (m * n)) )

proof end;

theorem :: RING_3:28

for m, n being Nat

for i, j being Integer st m <> 0 & n <> 0 holds

( denominator ((i / m) / (n / j)) = (m * n) / ((i * j) gcd (m * n)) & numerator ((i / m) / (n / j)) = (i * j) / ((i * j) gcd (m * n)) )

for i, j being Integer st m <> 0 & n <> 0 holds

( denominator ((i / m) / (n / j)) = (m * n) / ((i * j) gcd (m * n)) & numerator ((i / m) / (n / j)) = (i * j) / ((i * j) gcd (m * n)) )

proof end;

theorem Th31: :: RING_3:31

for p being Rational

for m being Nat

for i being Integer st m = denominator p & i = numerator p holds

( denominator (- p) = m div ((- i) gcd m) & numerator (- p) = (- i) div ((- i) gcd m) )

for m being Nat

for i being Integer st m = denominator p & i = numerator p holds

( denominator (- p) = m div ((- i) gcd m) & numerator (- p) = (- i) div ((- i) gcd m) )

proof end;

theorem :: RING_3:32

for p being Rational

for m being Nat

for i being Integer st m = denominator p & i = numerator p holds

( denominator (- p) = m / ((- i) gcd m) & numerator (- p) = (- i) / ((- i) gcd m) )

for m being Nat

for i being Integer st m = denominator p & i = numerator p holds

( denominator (- p) = m / ((- i) gcd m) & numerator (- p) = (- i) / ((- i) gcd m) )

proof end;

theorem Th33: :: RING_3:33

for p being Rational

for m, n being Nat st m = denominator p & n = numerator p & n <> 0 holds

( denominator (p ") = n div (n gcd m) & numerator (p ") = m div (n gcd m) )

for m, n being Nat st m = denominator p & n = numerator p & n <> 0 holds

( denominator (p ") = n div (n gcd m) & numerator (p ") = m div (n gcd m) )

proof end;

theorem :: RING_3:34

for p being Rational

for m, n being Nat st m = denominator p & n = numerator p & n <> 0 holds

( denominator (p ") = n / (n gcd m) & numerator (p ") = m / (n gcd m) )

for m, n being Nat st m = denominator p & n = numerator p & n <> 0 holds

( denominator (p ") = n / (n gcd m) & numerator (p ") = m / (n gcd m) )

proof end;

theorem Th35: :: RING_3:35

for p, q being Rational

for m, n being Nat

for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds

( denominator (p + q) = (m * n) div (((i * n) + (j * m)) gcd (m * n)) & numerator (p + q) = ((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n)) )

for m, n being Nat

for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds

( denominator (p + q) = (m * n) div (((i * n) + (j * m)) gcd (m * n)) & numerator (p + q) = ((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n)) )

proof end;

theorem :: RING_3:36

for p, q being Rational

for m, n being Nat

for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds

( denominator (p + q) = (m * n) / (((i * n) + (j * m)) gcd (m * n)) & numerator (p + q) = ((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n)) )

for m, n being Nat

for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds

( denominator (p + q) = (m * n) / (((i * n) + (j * m)) gcd (m * n)) & numerator (p + q) = ((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n)) )

proof end;

theorem Th37: :: RING_3:37

for p, q being Rational

for m, n being Nat

for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds

( denominator (p - q) = (m * n) div (((i * n) - (j * m)) gcd (m * n)) & numerator (p - q) = ((i * n) - (j * m)) div (((i * n) - (j * m)) gcd (m * n)) )

for m, n being Nat

for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds

( denominator (p - q) = (m * n) div (((i * n) - (j * m)) gcd (m * n)) & numerator (p - q) = ((i * n) - (j * m)) div (((i * n) - (j * m)) gcd (m * n)) )

proof end;

theorem :: RING_3:38

for p, q being Rational

for m, n being Nat

for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds

( denominator (p - q) = (m * n) / (((i * n) - (j * m)) gcd (m * n)) & numerator (p - q) = ((i * n) - (j * m)) / (((i * n) - (j * m)) gcd (m * n)) )

for m, n being Nat

for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds

( denominator (p - q) = (m * n) / (((i * n) - (j * m)) gcd (m * n)) & numerator (p - q) = ((i * n) - (j * m)) / (((i * n) - (j * m)) gcd (m * n)) )

proof end;

theorem Th39: :: RING_3:39

for p, q being Rational

for m, n being Nat

for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds

( denominator (p * q) = (m * n) div ((i * j) gcd (m * n)) & numerator (p * q) = (i * j) div ((i * j) gcd (m * n)) )

for m, n being Nat

for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds

( denominator (p * q) = (m * n) div ((i * j) gcd (m * n)) & numerator (p * q) = (i * j) div ((i * j) gcd (m * n)) )

proof end;

theorem :: RING_3:40

for p, q being Rational

for m, n being Nat

for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds

( denominator (p * q) = (m * n) / ((i * j) gcd (m * n)) & numerator (p * q) = (i * j) / ((i * j) gcd (m * n)) )

for m, n being Nat

for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds

( denominator (p * q) = (m * n) / ((i * j) gcd (m * n)) & numerator (p * q) = (i * j) / ((i * j) gcd (m * n)) )

proof end;

theorem Th41: :: RING_3:41

for p, q being Rational

for m1, m2, n1, n2 being Nat st m1 = denominator p & m2 = denominator q & n1 = numerator p & n2 = numerator q & n2 <> 0 holds

( denominator (p / q) = (m1 * n2) div ((n1 * m2) gcd (m1 * n2)) & numerator (p / q) = (n1 * m2) div ((n1 * m2) gcd (m1 * n2)) )

for m1, m2, n1, n2 being Nat st m1 = denominator p & m2 = denominator q & n1 = numerator p & n2 = numerator q & n2 <> 0 holds

( denominator (p / q) = (m1 * n2) div ((n1 * m2) gcd (m1 * n2)) & numerator (p / q) = (n1 * m2) div ((n1 * m2) gcd (m1 * n2)) )

proof end;

theorem :: RING_3:42

for p, q being Rational

for m1, m2, n1, n2 being Nat st m1 = denominator p & m2 = denominator q & n1 = numerator p & n2 = numerator q & n2 <> 0 holds

( denominator (p / q) = (m1 * n2) / ((n1 * m2) gcd (m1 * n2)) & numerator (p / q) = (n1 * m2) / ((n1 * m2) gcd (m1 * n2)) )

for m1, m2, n1, n2 being Nat st m1 = denominator p & m2 = denominator q & n1 = numerator p & n2 = numerator q & n2 <> 0 holds

( denominator (p / q) = (m1 * n2) / ((n1 * m2) gcd (m1 * n2)) & numerator (p / q) = (n1 * m2) / ((n1 * m2) gcd (m1 * n2)) )

proof end;

set I = INT.Ring ;

registration

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

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

cluster V31() integer left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable ext-real positive complex rational g_integer g_rational for Element of INT.Ring;

existence ex b

cluster V31() integer left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable ext-real negative complex rational g_integer g_rational for Element of INT.Ring;

existence ex b

proof end;

registration

let a be non zero Element of F_Rat;

let x be Rational;

compatibility

( a = x implies / a = x " )

end;
let x be Rational;

compatibility

( a = x implies / a = x " )

proof end;

registration

let a be Element of F_Rat;

let b be non zero Element of F_Rat;

let x, y be Rational;

compatibility

( a = x & b = y implies a / b = x / y ) ;

end;
let b be non zero Element of F_Rat;

let x, y be Rational;

compatibility

( a = x & b = y implies a / b = x / y ) ;

registration
end;

definition

let R, S be Ring;

end;
pred R includes_an_isomorphic_copy_of S means :: RING_3:def 1

ex T being strict Subring of R st T,S are_isomorphic ;

ex T being strict Subring of R st T,S are_isomorphic ;

:: deftheorem defines includes_an_isomorphic_copy_of RING_3:def 1 :

for R, S being Ring holds

( R includes_an_isomorphic_copy_of S iff ex T being strict Subring of R st T,S are_isomorphic );

for R, S being Ring holds

( R includes_an_isomorphic_copy_of S iff ex T being strict Subring of R st T,S are_isomorphic );

definition

let R, S be Ring;

:: original: is_ringisomorph_to

redefine pred R,S are_isomorphic ;

reflexivity

for R being Ring holds R24(b_{1},b_{1})

end;
:: original: is_ringisomorph_to

redefine pred R,S are_isomorphic ;

reflexivity

for R being Ring holds R24(b

proof end;

Lm2: ( the carrier of F_Real is Subset of the carrier of F_Complex & the addF of F_Real = the addF of F_Complex || the carrier of F_Real & the multF of F_Real = the multF of F_Complex || the carrier of F_Real & 1. F_Complex = 1. F_Real & 0. F_Complex = 0. F_Real )

by NUMBERS:11, COMPLFLD:def 1, Th2, Th3;

Lm3: for u, v being Integer

for p, q being Element of INT.Ring st u = p & v = q holds

( u divides v iff p divides q )

proof end;

Lm4: ( the carrier of INT.Ring c= the carrier of F_Rat & the addF of INT.Ring = the addF of F_Rat || the carrier of INT.Ring & the multF of INT.Ring = the multF of F_Rat || the carrier of INT.Ring & 1. INT.Ring = 1. F_Rat & 0. INT.Ring = 0. F_Rat )

by NUMBERS:14, Th4, Th5;

registration

let R be domRing;

ex b_{1} being domRing 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 unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like V190() V191() V192() V193() R -homomorphic for domRing;

existence ex b

proof end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital V190() V191() V192() V193() 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 unital associative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital V190() V191() V192() V193() R -homomorphic for Ring;

existence ex b

proof end;

registration

let R be Field;

ex b_{1} being domRing 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 unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like V190() V191() V192() V193() R -homomorphic for domRing;

existence ex b

proof end;

registration

let F be Field;

let R be F -homomorphic Ring;

let f be Homomorphism of F,R;

coherence

Image f is almost_left_invertible

end;
let R be F -homomorphic Ring;

let f be Homomorphism of F,R;

coherence

Image f is almost_left_invertible

proof end;

registration

let F be domRing;

let E be F -homomorphic domRing;

let f be Homomorphism of F,E;

coherence

not Image f is degenerated

end;
let E be F -homomorphic domRing;

let f be Homomorphism of F,E;

coherence

not Image f is degenerated

proof end;

theorem Th48: :: RING_3:49

for R being Ring

for E being b_{1} -homomorphic Ring

for K being Subring of R

for f being Function of R,E

for g being Function of K,E st g = f | the carrier of K & f is additive holds

g is additive

for E being b

for K being Subring of R

for f being Function of R,E

for g being Function of K,E st g = f | the carrier of K & f is additive holds

g is additive

proof end;

theorem Th49: :: RING_3:50

for R being Ring

for E being b_{1} -homomorphic Ring

for K being Subring of R

for f being Function of R,E

for g being Function of K,E st g = f | the carrier of K & f is multiplicative holds

g is multiplicative

for E being b

for K being Subring of R

for f being Function of R,E

for g being Function of K,E st g = f | the carrier of K & f is multiplicative holds

g is multiplicative

proof end;

theorem Th50: :: RING_3:51

for R being Ring

for E being b_{1} -homomorphic Ring

for K being Subring of R

for f being Function of R,E

for g being Function of K,E st g = f | the carrier of K & f is unity-preserving holds

g is unity-preserving

for E being b

for K being Subring of R

for f being Function of R,E

for g being Function of K,E st g = f | the carrier of K & f is unity-preserving holds

g is unity-preserving

proof end;

theorem :: RING_3:52

for R being Ring

for E being b_{1} -homomorphic Ring

for K being Subring of R holds E is K -homomorphic

for E being b

for K being Subring of R holds E is K -homomorphic

proof end;

theorem :: RING_3:53

for R being Ring

for E being b_{1} -homomorphic Ring

for K being Subring of R

for EK being b_{3} -homomorphic Ring

for f being Homomorphism of R,E st E = EK holds

f | K is Homomorphism of K,EK

for E being b

for K being Subring of R

for EK being b

for f being Homomorphism of R,E st E = EK holds

f | K is Homomorphism of K,EK

proof end;

theorem Th53: :: RING_3:54

for F being Field

for E being b_{1} -homomorphic Field

for K being Subfield of F

for f being Function of F,E

for g being Function of K,E st g = f | the carrier of K & f is additive holds

g is additive

for E being b

for K being Subfield of F

for f being Function of F,E

for g being Function of K,E st g = f | the carrier of K & f is additive holds

g is additive

proof end;

theorem Th54: :: RING_3:55

for F being Field

for E being b_{1} -homomorphic Field

for K being Subfield of F

for f being Function of F,E

for g being Function of K,E st g = f | the carrier of K & f is multiplicative holds

g is multiplicative

for E being b

for K being Subfield of F

for f being Function of F,E

for g being Function of K,E st g = f | the carrier of K & f is multiplicative holds

g is multiplicative

proof end;

theorem Th55: :: RING_3:56

for F being Field

for E being b_{1} -homomorphic Field

for K being Subfield of F

for f being Function of F,E

for g being Function of K,E st g = f | the carrier of K & f is unity-preserving holds

g is unity-preserving

for E being b

for K being Subfield of F

for f being Function of F,E

for g being Function of K,E st g = f | the carrier of K & f is unity-preserving holds

g is unity-preserving

proof end;

theorem Th56: :: RING_3:57

for F being Field

for E being b_{1} -homomorphic Field

for K being Subfield of F holds E is K -homomorphic

for E being b

for K being Subfield of F holds E is K -homomorphic

proof end;

theorem Th57: :: RING_3:58

for F being Field

for E being b_{1} -homomorphic Field

for K being Subfield of F

for EK being b_{3} -homomorphic Field

for f being Homomorphism of F,E st E = EK holds

f | K is Homomorphism of K,EK

for E being b

for K being Subfield of F

for EK being b

for f being Homomorphism of F,E st E = EK holds

f | K is Homomorphism of K,EK

proof end;

registration

let n be positive Nat;

coherence

( Z/ n is Abelian & Z/ n is add-associative & Z/ n is right_zeroed & Z/ n is right_complementable )

end;
coherence

( Z/ n is Abelian & Z/ n is add-associative & Z/ n is right_zeroed & Z/ n is right_complementable )

proof end;

registration

let n be positive Nat;

coherence

( Z/ n is associative & Z/ n is well-unital & Z/ n is distributive & Z/ n is commutative )

end;
coherence

( Z/ n is associative & Z/ n is well-unital & Z/ n is distributive & Z/ n is commutative )

proof end;

registration
end;

definition

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

let a be Element of R;

let i be Integer;

ex b_{1} being Element of R ex n being Nat st

( ( i = n & b_{1} = n * a ) or ( i = - n & b_{1} = - (n * a) ) )

for b_{1}, b_{2} being Element of R st ex n being Nat st

( ( i = n & b_{1} = n * a ) or ( i = - n & b_{1} = - (n * a) ) ) & ex n being Nat st

( ( i = n & b_{2} = n * a ) or ( i = - n & b_{2} = - (n * a) ) ) holds

b_{1} = b_{2}

end;
let a be Element of R;

let i be Integer;

func i '*' a -> Element of R means :Def2: :: RING_3:def 2

ex n being Nat st

( ( i = n & it = n * a ) or ( i = - n & it = - (n * a) ) );

existence ex n being Nat st

( ( i = n & it = n * a ) or ( i = - n & it = - (n * a) ) );

ex b

( ( i = n & b

proof end;

uniqueness for b

( ( i = n & b

( ( i = n & b

b

proof end;

:: deftheorem Def2 defines '*' RING_3:def 2 :

for R being non empty right_complementable add-associative right_zeroed doubleLoopStr

for a being Element of R

for i being Integer

for b_{4} being Element of R holds

( b_{4} = i '*' a iff ex n being Nat st

( ( i = n & b_{4} = n * a ) or ( i = - n & b_{4} = - (n * a) ) ) );

for R being non empty right_complementable add-associative right_zeroed doubleLoopStr

for a being Element of R

for i being Integer

for b

( b

( ( i = n & b

theorem Th58: :: RING_3:59

for R being non empty right_complementable add-associative right_zeroed doubleLoopStr

for a being Element of R holds 0 '*' a = 0. R

for a being Element of R holds 0 '*' a = 0. R

proof end;

theorem Th59: :: RING_3:60

for R being non empty right_complementable add-associative right_zeroed doubleLoopStr

for a being Element of R holds 1 '*' a = a

for a being Element of R holds 1 '*' a = a

proof end;

theorem Th60: :: RING_3:61

for R being non empty right_complementable add-associative right_zeroed doubleLoopStr

for a being Element of R holds (- 1) '*' a = - a

for a being Element of R holds (- 1) '*' a = - a

proof end;

Lm5: for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for a being Element of R

for i being Integer holds (i + 1) '*' a = (i '*' a) + a

proof end;

Lm6: for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for a being Element of R

for i being Integer holds (i - 1) '*' a = (i '*' a) - a

proof end;

theorem Th61: :: RING_3:62

for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for a being Element of R

for i, j being Integer holds (i + j) '*' a = (i '*' a) + (j '*' a)

for a being Element of R

for i, j being Integer holds (i + j) '*' a = (i '*' a) + (j '*' a)

proof end;

theorem Th62: :: RING_3:63

for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for a being Element of R

for i being Integer holds (- i) '*' a = - (i '*' a)

for a being Element of R

for i being Integer holds (- i) '*' a = - (i '*' a)

proof end;

theorem Th63: :: RING_3:64

for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for a being Element of R

for i, j being Integer holds (i - j) '*' a = (i '*' a) - (j '*' a)

for a being Element of R

for i, j being Integer holds (i - j) '*' a = (i '*' a) - (j '*' a)

proof end;

theorem Th64: :: RING_3:65

for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for a being Element of R

for i, j being Integer holds (i * j) '*' a = i '*' (j '*' a)

for a being Element of R

for i, j being Integer holds (i * j) '*' a = i '*' (j '*' a)

proof end;

theorem :: RING_3:66

for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for a being Element of R

for i, j being Integer holds i '*' (j '*' a) = j '*' (i '*' a)

for a being Element of R

for i, j being Integer holds i '*' (j '*' a) = j '*' (i '*' a)

proof end;

theorem Th66: :: RING_3:67

for R being non empty right_complementable Abelian add-associative right_zeroed distributive left_unital doubleLoopStr

for i, j being Integer holds (i * j) '*' (1. R) = (i '*' (1. R)) * (j '*' (1. R))

for i, j being Integer holds (i * j) '*' (1. R) = (i '*' (1. R)) * (j '*' (1. R))

proof end;

theorem :: RING_3:68

for R being Ring

for S being b_{1} -homomorphic Ring

for f being Homomorphism of R,S

for a being Element of R

for i being Integer holds f . (i '*' a) = i '*' (f . a)

for S being b

for f being Homomorphism of R,S

for a being Element of R

for i being Integer holds f . (i '*' a) = i '*' (f . a)

proof end;

definition

let R, S be Ring;

end;
attr S is R -monomorphic means :Def3: :: RING_3:def 3

ex f being Function of R,S st

( f is RingHomomorphism & f is monomorphism );

ex f being Function of R,S st

( f is RingHomomorphism & f is monomorphism );

:: deftheorem Def3 defines -monomorphic RING_3:def 3 :

for R, S being Ring holds

( S is R -monomorphic iff ex f being Function of R,S st

( f is RingHomomorphism & f is monomorphism ) );

for R, S being Ring holds

( S is R -monomorphic iff ex f being Function of R,S st

( f is RingHomomorphism & f is monomorphism ) );

registration

let R be Ring;

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

end;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital V190() V191() V192() V193() R -monomorphic for Ring;

existence ex b

proof end;

registration

let R be comRing;

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

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

end;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital V190() V191() V192() V193() R -monomorphic for comRing;

existence ex b

proof end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital V190() V191() V192() V193() R -monomorphic for Ring;

existence ex b

proof end;

registration

let R be domRing;

ex b_{1} being domRing st b_{1} is R -monomorphic

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

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

end;
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like V190() V191() V192() V193() R -monomorphic for domRing;

existence ex b

proof end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital V190() V191() V192() V193() R -monomorphic for comRing;

existence ex b

proof end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital V190() V191() V192() V193() R -monomorphic for Ring;

existence ex b

proof end;

registration

let R be Field;

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

ex b_{1} being domRing st b_{1} is R -monomorphic

ex b_{1} being comRing st b_{1} is R -monomorphic
cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital V190() V191() V192() V193() R -monomorphic for Ring;

existence

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

end;
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_invertible unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like V141() V190() V191() V192() V193() PID Euclidian factorial R -monomorphic for Field;

existence ex b

proof end;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like V190() V191() V192() V193() R -monomorphic for domRing;

existence ex b

proof end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital V190() V191() V192() V193() R -monomorphic for comRing;

existence ex b

proof end;

ex b

proof end;

registration

let R be Ring;

let S be R -monomorphic Ring;

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

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

end;
let S be R -monomorphic Ring;

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

existence ex b

( b

proof end;

definition

let R be Ring;

let S be R -monomorphic Ring;

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

end;
let S be R -monomorphic Ring;

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

registration

let R be Ring;

let S be R -monomorphic Ring;

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

end;
let S be R -monomorphic Ring;

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

coherence for b

proof end;

registration

let R be Ring;

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

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

coherence for b

proof end;

registration

let R be Ring;

let S be R -monomorphic Ring;

let f be Monomorphism of R,S;

reducibility

(f ") " = f by FUNCT_1:43;

end;
let S be R -monomorphic Ring;

let f be Monomorphism of R,S;

reducibility

(f ") " = f by FUNCT_1:43;

theorem Th68: :: RING_3:69

for R being Ring

for S being b_{1} -homomorphic Ring

for T being b_{2} -homomorphic Ring

for f being Homomorphism of R,S

for g being Homomorphism of S,T holds ker f c= ker (g * f)

for S being b

for T being b

for f being Homomorphism of R,S

for g being Homomorphism of S,T holds ker f c= ker (g * f)

proof end;

theorem Th69: :: RING_3:70

for R being Ring

for S being b_{1} -homomorphic Ring

for T being b_{2} -monomorphic Ring

for f being Homomorphism of R,S

for g being Monomorphism of S,T holds ker f = ker (g * f)

for S being b

for T being b

for f being Homomorphism of R,S

for g being Monomorphism of S,T holds ker f = ker (g * f)

proof end;

definition

let R, S be Ring;

end;
attr S is R -isomorphic means :Def4: :: RING_3:def 4

ex f being Function of R,S st

( f is RingHomomorphism & f is isomorphism );

ex f being Function of R,S st

( f is RingHomomorphism & f is isomorphism );

:: deftheorem Def4 defines -isomorphic RING_3:def 4 :

for R, S being Ring holds

( S is R -isomorphic iff ex f being Function of R,S st

( f is RingHomomorphism & f is isomorphism ) );

for R, S being Ring holds

( S is R -isomorphic iff ex f being Function of R,S st

( f is RingHomomorphism & f is isomorphism ) );

registration

let R be Ring;

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

end;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital V190() V191() V192() V193() R -isomorphic for Ring;

existence ex b

proof end;

registration

let R be comRing;

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

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

end;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital V190() V191() V192() V193() R -isomorphic for comRing;

existence ex b

proof end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital V190() V191() V192() V193() R -isomorphic for Ring;

existence ex b

proof end;

registration

let R be domRing;

ex b_{1} being domRing st b_{1} is R -isomorphic

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

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

end;
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like V190() V191() V192() V193() R -isomorphic for domRing;

existence ex b

proof end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital V190() V191() V192() V193() R -isomorphic for comRing;

existence ex b

proof end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital V190() V191() V192() V193() R -isomorphic for Ring;

existence ex b

proof end;

registration

let R be Field;

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

ex b_{1} being domRing st b_{1} is R -isomorphic

ex b_{1} being comRing st b_{1} is R -isomorphic
cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital V190() V191() V192() V193() R -isomorphic for Ring;

existence

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

end;
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_invertible unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like V141() V190() V191() V192() V193() PID Euclidian factorial R -isomorphic for Field;

existence ex b

proof end;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like V190() V191() V192() V193() R -isomorphic for domRing;

existence ex b

proof end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital V190() V191() V192() V193() R -isomorphic for comRing;

existence ex b

proof end;

ex b

proof end;

registration

let R be Ring;

let S be R -isomorphic Ring;

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

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

end;
let S be R -isomorphic Ring;

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

existence ex b

( b

proof end;

definition

let R be Ring;

let S be R -isomorphic Ring;

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

end;
let S be R -isomorphic Ring;

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

definition

let R be Ring;

let S be R -isomorphic Ring;

let f be Isomorphism of R,S;

:: original: "

redefine func f " -> Function of S,R;

coherence

f " is Function of S,R

end;
let S be R -isomorphic Ring;

let f be Isomorphism of R,S;

:: original: "

redefine func f " -> Function of S,R;

coherence

f " is Function of S,R

proof end;

Lm7: for R being Ring

for S being b

for f being Isomorphism of R,S holds

( f " is additive & f " is multiplicative & f " is unity-preserving & f " is isomorphism )

proof end;

registration

let R be Ring;

let S be R -isomorphic Ring;

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

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

end;
let S be R -isomorphic Ring;

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

existence ex b

( b

proof end;

definition

let R be Ring;

let S be R -isomorphic Ring;

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

end;
let S be R -isomorphic Ring;

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

registration

let R be Ring;

let S be R -isomorphic Ring;

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

end;
let S be R -isomorphic Ring;

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

coherence for b

proof end;

registration

let R be Ring;

for b_{1} being R -isomorphic Ring holds b_{1} is R -monomorphic

end;
cluster non empty right_complementable associative Abelian add-associative right_zeroed well-unital distributive R -isomorphic -> R -monomorphic R -isomorphic for Ring;

coherence for b

proof end;

theorem Th72: :: RING_3:73

for R being Ring

for S being b_{1} -isomorphic Ring

for f being Isomorphism of R,S holds f " is Isomorphism of S,R by Lm7;

for S being b

for f being Isomorphism of R,S holds f " is Isomorphism of S,R by Lm7;

registration

let R be comRing;

for b_{1} being R -isomorphic Ring holds b_{1} is commutative

end;
cluster non empty right_complementable associative Abelian add-associative right_zeroed well-unital distributive R -isomorphic -> commutative R -isomorphic for Ring;

coherence for b

proof end;

registration

let R be domRing;

for b_{1} being R -isomorphic Ring holds

( not b_{1} is degenerated & b_{1} is domRing-like )

end;
cluster non empty right_complementable associative Abelian add-associative right_zeroed well-unital distributive R -isomorphic -> non degenerated domRing-like R -isomorphic for Ring;

coherence for b

( not b

proof end;

registration

let F be Field;

for b_{1} being F -isomorphic Ring holds b_{1} is almost_left_invertible

end;
cluster non empty right_complementable associative Abelian add-associative right_zeroed well-unital distributive F -isomorphic -> almost_left_invertible F -isomorphic for Ring;

coherence for b

proof end;

theorem :: RING_3:75

for E, F being Field holds

( E includes F iff ex K being strict Subfield of E st K,F are_isomorphic )

( E includes F iff ex K being strict Subfield of E st K,F are_isomorphic )

proof end;

definition

let R be Ring;

ex b_{1} being Nat st

( ( b_{1} '*' (1. R) = 0. R & b_{1} <> 0 & ( for m being positive Nat st m < b_{1} holds

m '*' (1. R) <> 0. R ) ) or ( b_{1} = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) )

for b_{1}, b_{2} being Nat st ( ( b_{1} '*' (1. R) = 0. R & b_{1} <> 0 & ( for m being positive Nat st m < b_{1} holds

m '*' (1. R) <> 0. R ) ) or ( b_{1} = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) ) & ( ( b_{2} '*' (1. R) = 0. R & b_{2} <> 0 & ( for m being positive Nat st m < b_{2} holds

m '*' (1. R) <> 0. R ) ) or ( b_{2} = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) ) holds

b_{1} = b_{2}

end;
func Char R -> Nat means :Def5: :: RING_3:def 5

( ( it '*' (1. R) = 0. R & it <> 0 & ( for m being positive Nat st m < it holds

m '*' (1. R) <> 0. R ) ) or ( it = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) );

existence ( ( it '*' (1. R) = 0. R & it <> 0 & ( for m being positive Nat st m < it holds

m '*' (1. R) <> 0. R ) ) or ( it = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) );

ex b

( ( b

m '*' (1. R) <> 0. R ) ) or ( b

proof end;

uniqueness for b

m '*' (1. R) <> 0. R ) ) or ( b

m '*' (1. R) <> 0. R ) ) or ( b

b

proof end;

:: deftheorem Def5 defines Char RING_3:def 5 :

for R being Ring

for b_{2} being Nat holds

( b_{2} = Char R iff ( ( b_{2} '*' (1. R) = 0. R & b_{2} <> 0 & ( for m being positive Nat st m < b_{2} holds

m '*' (1. R) <> 0. R ) ) or ( b_{2} = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) ) );

for R being Ring

for b

( b

m '*' (1. R) <> 0. R ) ) or ( b

definition
end;

:: deftheorem Def6 defines -characteristic RING_3:def 6 :

for n being Nat

for R being Ring holds

( R is n -characteristic iff Char R = n );

for n being Nat

for R being Ring holds

( R is n -characteristic iff Char R = n );

Lm8: for i being Integer holds i '*' (1. INT.Ring) = i

proof end;

registration
end;

registration

let n be Nat;

ex b_{1} being comRing st b_{1} is n -characteristic

end;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital V190() V191() V192() V193() n -characteristic for comRing;

existence ex b

proof end;

registration
end;

definition

let R be Ring;

{ n where n is positive Nat : n '*' (1. R) = 0. R } is Subset of NAT

end;
func CharSet R -> Subset of NAT equals :: RING_3:def 7

{ n where n is positive Nat : n '*' (1. R) = 0. R } ;

coherence { n where n is positive Nat : n '*' (1. R) = 0. R } ;

{ n where n is positive Nat : n '*' (1. R) = 0. R } is Subset of NAT

proof end;

:: deftheorem defines CharSet RING_3:def 7 :

for R being Ring holds CharSet R = { n where n is positive Nat : n '*' (1. R) = 0. R } ;

for R being Ring holds CharSet R = { n where n is positive Nat : n '*' (1. R) = 0. R } ;

registration
end;

theorem :: RING_3:81

for p being Prime

for R being b_{1} -characteristic Ring

for n being positive Nat holds

( n is Element of CharSet R iff p divides n )

for R being b

for n being positive Nat holds

( n is Element of CharSet R iff p divides n )

proof end;

definition

let R be Ring;

ex b_{1} being Function of INT.Ring,R st

for x being Element of INT.Ring holds b_{1} . x = x '*' (1. R)

for b_{1}, b_{2} being Function of INT.Ring,R st ( for x being Element of INT.Ring holds b_{1} . x = x '*' (1. R) ) & ( for x being Element of INT.Ring holds b_{2} . x = x '*' (1. R) ) holds

b_{1} = b_{2}

end;
func canHom_Int R -> Function of INT.Ring,R means :Def8: :: RING_3:def 8

for x being Element of INT.Ring holds it . x = x '*' (1. R);

existence for x being Element of INT.Ring holds it . x = x '*' (1. R);

ex b

for x being Element of INT.Ring holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines canHom_Int RING_3:def 8 :

for R being Ring

for b_{2} being Function of INT.Ring,R holds

( b_{2} = canHom_Int R iff for x being Element of INT.Ring holds b_{2} . x = x '*' (1. R) );

for R being Ring

for b

( b

registration

let R be Ring;

coherence

( canHom_Int R is additive & canHom_Int R is multiplicative & canHom_Int R is unity-preserving )

end;
coherence

( canHom_Int R is additive & canHom_Int R is multiplicative & canHom_Int R is unity-preserving )

proof end;

registration

for b_{1} being Ring holds b_{1} is INT.Ring -homomorphic
end;

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

coherence for b

proof end;

theorem Th81: :: RING_3:82

for R being Ring

for n being non negative Element of INT.Ring holds

( Char R = n iff ker (canHom_Int R) = {n} -Ideal )

for n being non negative Element of INT.Ring holds

( Char R = n iff ker (canHom_Int R) = {n} -Ideal )

proof end;

registration
end;

registration

let R be 0 -characteristic Ring;

ex b_{1} being Function of INT.Ring,R st

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

end;
cluster Relation-like the carrier of INT.Ring -defined the carrier of R -valued Function-like non empty V14( the carrier of INT.Ring) quasi_total unity-preserving additive monomorphism multiplicative for Function of ,;

existence ex b

( b

proof end;

registration

let n be Nat;

let R be n -characteristic Ring;

for b_{1} being Ring st b_{1} is R -monomorphic holds

b_{1} is n -characteristic

for b_{1} being Subring of R holds b_{1} is n -characteristic

end;
let R be n -characteristic Ring;

cluster non empty right_complementable associative Abelian add-associative right_zeroed well-unital distributive R -monomorphic -> n -characteristic for Ring;

coherence for b

b

proof end;

coherence for b

proof end;

Lm9: for n being Nat holds n '*' (1. F_Complex) = n

proof end;

registration
end;

registration
end;

registration
end;

registration

ex b_{1} being Field st b_{1} is 0 -characteristic
end;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_invertible unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like V141() V190() V191() V192() V193() PID Euclidian INT.Ring -homomorphic factorial 0 -characteristic for Field;

existence ex b

proof end;

registration

let p be Prime;

ex b_{1} being Field st b_{1} is p -characteristic

end;
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_invertible unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like V141() V190() V191() V192() V193() PID Euclidian INT.Ring -homomorphic factorial p -characteristic for Field;

existence ex b

proof end;

registration
end;

registration

let F be 0 -characteristic Field;

coherence

for b_{1} being Subfield of F holds b_{1} is 0 -characteristic

end;
coherence

for b

proof end;

registration

let p be Prime;

let F be p -characteristic Field;

coherence

for b_{1} being Subfield of F holds b_{1} is p -characteristic

end;
let F be p -characteristic Field;

coherence

for b

proof end;

definition

let F be Field;

{ x where x is Element of F : for K being Subfield of F holds x in K } is Subset of F

end;
func carrier/\ F -> Subset of F equals :: RING_3:def 9

{ x where x is Element of F : for K being Subfield of F holds x in K } ;

coherence { x where x is Element of F : for K being Subfield of F holds x in K } ;

{ x where x is Element of F : for K being Subfield of F holds x in K } is Subset of F

proof end;

:: deftheorem defines carrier/\ RING_3:def 9 :

for F being Field holds carrier/\ F = { x where x is Element of F : for K being Subfield of F holds x in K } ;

for F being Field holds carrier/\ F = { x where x is Element of F : for K being Subfield of F holds x in K } ;

definition

let F be Field;

ex b_{1} being strict doubleLoopStr st

( the carrier of b_{1} = carrier/\ F & the addF of b_{1} = the addF of F || (carrier/\ F) & the multF of b_{1} = the multF of F || (carrier/\ F) & the OneF of b_{1} = 1. F & the ZeroF of b_{1} = 0. F )

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

b_{1} = b_{2}
;

end;
func PrimeField F -> strict doubleLoopStr means :Def10: :: RING_3:def 10

( the carrier of it = carrier/\ F & the addF of it = the addF of F || (carrier/\ F) & the multF of it = the multF of F || (carrier/\ F) & the OneF of it = 1. F & the ZeroF of it = 0. F );

existence ( the carrier of it = carrier/\ F & the addF of it = the addF of F || (carrier/\ F) & the multF of it = the multF of F || (carrier/\ F) & the OneF of it = 1. F & the ZeroF of it = 0. F );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def10 defines PrimeField RING_3:def 10 :

for F being Field

for b_{2} being strict doubleLoopStr holds

( b_{2} = PrimeField F iff ( the carrier of b_{2} = carrier/\ F & the addF of b_{2} = the addF of F || (carrier/\ F) & the multF of b_{2} = the multF of F || (carrier/\ F) & the OneF of b_{2} = 1. F & the ZeroF of b_{2} = 0. F ) );

for F being Field

for b

( b

Lm10: for F being Field

for x being Element of (PrimeField F) holds x is Element of F

proof end;

Lm11: for F being Field

for a, b being Element of F

for x, y being Element of (PrimeField F) st a = x & b = y holds

a + b = x + y

proof end;

Lm12: for F being Field

for a, b being Element of F

for x, y being Element of (PrimeField F) st a = x & b = y holds

a * b = x * y

proof end;

registration

let F be Field;

coherence

( PrimeField F is Abelian & PrimeField F is add-associative & PrimeField F is right_zeroed & PrimeField F is right_complementable )

end;
coherence

( PrimeField F is Abelian & PrimeField F is add-associative & PrimeField F is right_zeroed & PrimeField F is right_complementable )

proof end;

registration

let F be Field;

coherence

( PrimeField F is associative & PrimeField F is well-unital & PrimeField F is distributive & PrimeField F is almost_left_invertible )

end;
coherence

( PrimeField F is associative & PrimeField F is well-unital & PrimeField F is distributive & PrimeField F is almost_left_invertible )

proof end;

definition

let F be Field;

:: original: PrimeField

redefine func PrimeField F -> strict Subfield of F;

coherence

PrimeField F is strict Subfield of F

end;
:: original: PrimeField

redefine func PrimeField F -> strict Subfield of F;

coherence

PrimeField F is strict Subfield of F

proof end;

Lm13: for F being Field

for K being Subfield of F holds carrier/\ F c= the carrier of K

proof end;

theorem Th91: :: RING_3:92

for F, K being Field holds

( K = PrimeField F iff ( K is strict Subfield of F & ( for E being strict Subfield of K holds E = K ) ) )

( K = PrimeField F iff ( K is strict Subfield of F & ( for E being strict Subfield of K holds E = K ) ) )

proof end;

theorem Th92: :: RING_3:93

for F, K being Field holds

( K = PrimeField F iff ( K is strict Subfield of F & ( for E being Subfield of F holds K is Subfield of E ) ) )

( K = PrimeField F iff ( K is strict Subfield of F & ( for E being Subfield of F holds K is Subfield of E ) ) )

proof end;

registration
end;

theorem Th96: :: RING_3:97

for F being 0 -characteristic Field

for i, j being non zero Integer st j divides i holds

(i div j) '*' (1. F) = (i '*' (1. F)) * ((j '*' (1. F)) ")

for i, j being non zero Integer st j divides i holds

(i div j) '*' (1. F) = (i '*' (1. F)) * ((j '*' (1. F)) ")

proof end;

definition

let x be Element of F_Rat;

:: original: denominator

redefine func denominator x -> positive Element of INT.Ring;

coherence

denominator x is positive Element of INT.Ring by INT_1:def 2;

:: original: numerator

redefine func numerator x -> Element of INT.Ring;

coherence

numerator x is Element of INT.Ring by INT_1:def 2;

end;
:: original: denominator

redefine func denominator x -> positive Element of INT.Ring;

coherence

denominator x is positive Element of INT.Ring by INT_1:def 2;

:: original: numerator

redefine func numerator x -> Element of INT.Ring;

coherence

numerator x is Element of INT.Ring by INT_1:def 2;

definition

let F be Field;

ex b_{1} being Function of F_Rat,F st

for x being Element of F_Rat holds b_{1} . x = ((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x))

for b_{1}, b_{2} being Function of F_Rat,F st ( for x being Element of F_Rat holds b_{1} . x = ((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x)) ) & ( for x being Element of F_Rat holds b_{2} . x = ((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x)) ) holds

b_{1} = b_{2}

end;
func canHom_Rat F -> Function of F_Rat,F means :Def11: :: RING_3:def 11

for x being Element of F_Rat holds it . x = ((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x));

existence for x being Element of F_Rat holds it . x = ((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x));

ex b

for x being Element of F_Rat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines canHom_Rat RING_3:def 11 :

for F being Field

for b_{2} being Function of F_Rat,F holds

( b_{2} = canHom_Rat F iff for x being Element of F_Rat holds b_{2} . x = ((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x)) );

for F being Field

for b

( b

registration

let F be 0 -characteristic Field;

coherence

( canHom_Rat F is additive & canHom_Rat F is multiplicative )

end;
coherence

( canHom_Rat F is additive & canHom_Rat F is multiplicative )

proof end;

registration

for b_{1} being 0 -characteristic Field holds b_{1} is F_Rat -monomorphic
end;

cluster non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive 0 -characteristic -> F_Rat -monomorphic 0 -characteristic for Field;

coherence for b

proof end;

registration

ex b_{1} being Field st

( b_{1} is 0 -characteristic & b_{1} is F_Rat -homomorphic )
;

end;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_invertible unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like V141() V190() V191() V192() V193() PID Euclidian INT.Ring -homomorphic F_Rat -homomorphic factorial 0 -characteristic for Field;

existence ex b

( b

theorem Th98: :: RING_3:99

for F being F_Rat -homomorphic 0 -characteristic Field

for f being Homomorphism of F_Rat,F holds f = canHom_Rat F

for f being Homomorphism of F_Rat,F holds f = canHom_Rat F

proof end;

definition

let F be Field;

let S be F -homomorphic Field;

let f be Homomorphism of F,S;

:: original: Image

redefine func Image f -> strict Subfield of S;

coherence

Image f is strict Subfield of S

end;
let S be F -homomorphic Field;

let f be Homomorphism of F,S;

:: original: Image

redefine func Image f -> strict Subfield of S;

coherence

Image f is strict Subfield of S

proof end;

registration
end;

theorem Th104: :: RING_3:105

for p being Prime

for R being b_{1} -characteristic Ring

for i being Integer holds i '*' (1. R) = (i mod p) '*' (1. R)

for R being b

for i being Integer holds i '*' (1. R) = (i mod p) '*' (1. R)

proof end;

definition

let p be Prime;

let F be Field;

(canHom_Int F) | the carrier of (Z/ p) is Function of (Z/ p),F

end;
let F be Field;

func canHom_Z/ (p,F) -> Function of (Z/ p),F equals :: RING_3:def 12

(canHom_Int F) | the carrier of (Z/ p);

coherence (canHom_Int F) | the carrier of (Z/ p);

(canHom_Int F) | the carrier of (Z/ p) is Function of (Z/ p),F

proof end;

:: deftheorem defines canHom_Z/ RING_3:def 12 :

for p being Prime

for F being Field holds canHom_Z/ (p,F) = (canHom_Int F) | the carrier of (Z/ p);

for p being Prime

for F being Field holds canHom_Z/ (p,F) = (canHom_Int F) | the carrier of (Z/ p);

Lm14: for p being Prime

for F being Field

for x being Element of (Z/ p)

for y being Element of INT.Ring st x = y holds

(canHom_Z/ (p,F)) . x = y '*' (1. F)

proof end;

registration
end;

registration

let p be Prime;

let F be p -characteristic Field;

coherence

( canHom_Z/ (p,F) is additive & canHom_Z/ (p,F) is multiplicative )

end;
let F be p -characteristic Field;

coherence

( canHom_Z/ (p,F) is additive & canHom_Z/ (p,F) is multiplicative )

proof end;

registration

let p be Prime;

for b_{1} being p -characteristic Field holds b_{1} is Z/ p -monomorphic

end;
cluster non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive p -characteristic -> Z/ p -monomorphic p -characteristic for Field;

coherence for b

proof end;

registration

let p be Prime;

ex b_{1} being Field st

( b_{1} is p -characteristic & b_{1} is Z/ p -homomorphic )
;

coherence

Z/ p is Z/ p -homomorphic ;

end;
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_invertible unital associative commutative Abelian add-associative right_zeroed V110() right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like V141() V190() V191() V192() V193() PID Euclidian INT.Ring -homomorphic Z/ p -homomorphic factorial p -characteristic for Field;

existence ex b

( b

coherence

Z/ p is Z/ p -homomorphic ;

theorem Th105: :: RING_3:106

for p being Prime

for F being Z/ b_{1} -homomorphic b_{1} -characteristic Field

for f being Homomorphism of (Z/ p),F holds f = canHom_Z/ (p,F)

for F being Z/ b

for f being Homomorphism of (Z/ p),F holds f = canHom_Z/ (p,F)

proof end;

registration
end;

registration

let p be Prime;

let F be p -characteristic Field;

coherence

canHom_Z/ (p,(PrimeField F)) is onto

end;
let F be p -characteristic Field;

coherence

canHom_Z/ (p,(PrimeField F)) is onto

proof end;

theorem :: RING_3:109

theorem :: RING_3:111

theorem :: RING_3:112

for p being Prime

for F being b_{1} -characteristic Field

for E being Field st F includes E holds

E includes Z/ p

for F being b

for E being Field st F includes E holds

E includes Z/ p

proof end;

theorem :: RING_3:115

for F being strict Field holds

( F is prime iff ( F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic ) )

( F is prime iff ( F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic ) )

proof end;