:: Characteristic of Rings; Prime Fields
:: by Christoph Schwarzweller and Artur Korni{\l}owicz
::
:: Received August 14, 2015
:: Copyright (c) 2015-2021 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)

proof end;

theorem Th2: :: RING_3:2

addcomplex || REAL = addreal

proof end;

theorem Th3: :: RING_3:3

multcomplex || REAL = multreal

proof end;

theorem Th4: :: RING_3:4

addrat || INT = addint

proof end;

theorem Th5: :: RING_3:5

multrat || INT = multint

proof end;

theorem Th6: :: RING_3:6

for n being Nat
for i being Integer st n divides i holds
i div n = i / n

proof end;

theorem Th7: :: RING_3:7

for n being Nat
for i being Integer holds i div (i gcd n) = i / (i gcd n)

proof end;

theorem Th8: :: RING_3:8

for n being Nat
for i being Integer holds n div (n gcd i) = n / (n gcd i)

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)

proof end;

theorem Th10: :: RING_3:10

for m being Nat
for i being Integer holds i / m = (i div (i gcd m)) / (m div (i gcd m))

proof end;

theorem Th11: :: RING_3:11

for m being Nat
for i being Integer st 0 < m & m * i divides m & not i = 1 holds
i = - 1

proof end;

theorem :: RING_3:12

for m, n being Nat st 0 < m & m * n divides m holds
n = 1

proof end;

theorem :: RING_3:13

for m being Nat
for i being Integer st m divides i holds
i div m divides i

proof end;

theorem Th14: :: RING_3:14

for m being Nat
for i being Integer st m <> 0 holds
(i div (i gcd m)) gcd (m div (i gcd m)) = 1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

proof end;

theorem :: RING_3:29

for p being Rational holds denominator p = (denominator p) div ((numerator p) gcd (denominator p))

proof end;

theorem :: RING_3:30

for p being Rational holds numerator p = (numerator p) div ((numerator p) gcd (denominator p))

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

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

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

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

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

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

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

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

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

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

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

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

proof end;

set I = INT.Ring ;

registration

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 the carrier of INT.Ring;

existence
ex b₁ being Element of INT.Ring st b₁ is positive ;

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 the carrier of INT.Ring;

existence
ex b₁ being Element of INT.Ring st b₁ is negative

proof end;

end;

registration

let a be non zero Element of F_Rat;
let x be Rational;

identify / a with x " when a = x;

compatibility
( a = x implies / a = x " )

proof end;

end;

registration

let a be Element of F_Rat;
let b be non zero Element of F_Rat;
let x, y be Rational;

identify a / b with x / y when a = x, b = y;

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

end;

registration

let F be Field;

reduce (1. F) " to 1. F;

reducibility
(1. F) " = 1. F by EC_PF_2:2;

end;

definition

let R, S be Ring;

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 ;

end;

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

notation

let R, S be Ring;
synonym R includes S for R includes_an_isomorphic_copy_of S;

end;

definition

let R, S be Ring;
:: original: is_ringisomorph_to
redefine pred R,S are_isomorphic ;
reflexivity
for R being Ring holds R24(b₁,b₁)

proof end;

end;

theorem Lm1: :: RING_3:43

for E being Field
for F being Subfield of E holds F is Subring of E

proof end;

theorem Th43: :: RING_3:44

for R, S, T being Ring st R,S are_isomorphic & S,T are_isomorphic holds
R,T are_isomorphic

proof end;

theorem :: RING_3:45

for F being Field
for R being Subring of F holds
( R is Subfield of F iff R is Field )

proof end;

theorem :: RING_3:46

for E being Field
for F being strict Subfield of E holds E includes F

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;

theorem :: RING_3:47

INT.Ring is Subring of F_Rat by Lm4, C0SP1:def 3;

theorem Th47: :: RING_3:48

F_Real is Subfield of F_Complex by Lm2, EC_PF_1:2;

registration

let R be domRing;

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 V192() V193() V194() V195() R -homomorphic for doubleLoopStr ;

existence
ex b₁ being domRing st b₁ is R -homomorphic

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 V192() V193() V194() V195() R -homomorphic for doubleLoopStr ;

existence
ex b₁ being comRing st b₁ is R -homomorphic

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 V192() V193() V194() V195() R -homomorphic for doubleLoopStr ;

existence
ex b₁ being Ring st b₁ is R -homomorphic

proof end;

end;

registration

let R be Field;

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 V192() V193() V194() V195() R -homomorphic for doubleLoopStr ;

existence
ex b₁ being domRing st b₁ is R -homomorphic

proof end;

end;

registration

let F be Field;
let R be F -homomorphic Ring;
let f be Homomorphism of F,R;

cluster Image f -> almost_left_invertible ;

coherence
Image f is almost_left_invertible

proof end;

end;

registration

let F be domRing;
let E be F -homomorphic domRing;
let f be Homomorphism of F,E;

cluster Image f -> non degenerated ;

coherence
not Image f is degenerated

proof end;

end;

theorem Th48: :: RING_3:49

for R being Ring
for E being b₁ -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

proof end;

theorem Th49: :: RING_3:50

for R being Ring
for E being b₁ -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

proof end;

theorem Th50: :: RING_3:51

for R being Ring
for E being b₁ -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

proof end;

theorem :: RING_3:52

for R being Ring
for E being b₁ -homomorphic Ring
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₁ -homomorphic Ring
for K being Subring of R
for EK being b₃ -homomorphic Ring
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₁ -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

proof end;

theorem Th54: :: RING_3:55

for F being Field
for E being b₁ -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

proof end;

theorem Th55: :: RING_3:56

for F being Field
for E being b₁ -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

proof end;

theorem Th56: :: RING_3:57

for F being Field
for E being b₁ -homomorphic Field
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₁ -homomorphic Field
for K being Subfield of F
for EK being b₃ -homomorphic Field
for f being Homomorphism of F,E st E = EK holds
f | K is Homomorphism of K,EK

proof end;

notation

let n be Nat;
synonym Z/ n for INT.Ring n;

end;

registration

let n be Nat;

cluster Z/ n -> finite ;

coherence
Z/ n is finite ;

end;

registration

let n be non trivial Nat;

cluster Z/ n -> non degenerated ;

coherence
not Z/ n is degenerated

proof end;

end;

registration

let n be positive Nat;

cluster Z/ n -> right_complementable Abelian add-associative right_zeroed ;

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

proof end;

end;

registration

let n be positive Nat;

cluster Z/ n -> associative commutative well-unital distributive ;

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

proof end;

end;

registration

let p be Prime;

cluster Z/ p -> almost_left_invertible ;

coherence
Z/ p is almost_left_invertible ;

end;

definition

let R be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
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 b₁ being Element of R ex n being Nat st
( ( i = n & b₁ = n * a ) or ( i = - n & b₁ = - (n * a) ) )

proof end;

uniqueness
for b₁, b₂ being Element of R st ex n being Nat st
( ( i = n & b₁ = n * a ) or ( i = - n & b₁ = - (n * a) ) ) & ex n being Nat st
( ( i = n & b₂ = n * a ) or ( i = - n & b₂ = - (n * a) ) ) holds
b₁ = b₂

proof end;

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₄ being Element of R holds
( b₄ = i '*' a iff ex n being Nat st
( ( i = n & b₄ = n * a ) or ( i = - n & b₄ = - (n * a) ) ) );

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

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

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

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)

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)

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)

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)

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)

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

proof end;

theorem :: RING_3:68

for R being Ring
for S being b₁ -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)

proof end;

definition

let R, S be Ring;

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

end;

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

registration

let R be Ring;

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 V192() V193() V194() V195() R -monomorphic for doubleLoopStr ;

existence
ex b₁ being Ring st b₁ is R -monomorphic

proof end;

end;

registration

let R be comRing;

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 V192() V193() V194() V195() R -monomorphic for doubleLoopStr ;

existence
ex b₁ being comRing st b₁ is R -monomorphic

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 V192() V193() V194() V195() R -monomorphic for doubleLoopStr ;

existence
ex b₁ being Ring st b₁ is R -monomorphic

proof end;

end;

registration

let R be domRing;

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 V192() V193() V194() V195() R -monomorphic for doubleLoopStr ;

existence
ex b₁ being domRing st b₁ is R -monomorphic

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 V192() V193() V194() V195() R -monomorphic for doubleLoopStr ;

existence
ex b₁ being comRing st b₁ is R -monomorphic

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 V192() V193() V194() V195() R -monomorphic for doubleLoopStr ;

existence
ex b₁ being Ring st b₁ is R -monomorphic

proof end;

end;

registration

let R be Field;

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 V143() V192() V193() V194() V195() PID Euclidian factorial R -monomorphic for doubleLoopStr ;

existence
ex b₁ being Field st b₁ is R -monomorphic

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 V192() V193() V194() V195() R -monomorphic for doubleLoopStr ;

existence
ex b₁ being domRing st b₁ is R -monomorphic

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 V192() V193() V194() V195() R -monomorphic for doubleLoopStr ;

existence
ex b₁ being comRing st b₁ is R -monomorphic

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 V192() V193() V194() V195() R -monomorphic for doubleLoopStr ;

existence
ex b₁ being Ring st b₁ is R -monomorphic

proof end;

end;

registration

let R be Ring;
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 Element of bool [: the carrier of R, the carrier of S:];

existence
ex b₁ being Function of R,S st
( b₁ is additive & b₁ is multiplicative & b₁ is unity-preserving & b₁ is monomorphism )

proof end;

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;

registration

let R be Ring;
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 doubleLoopStr ;

coherence
for b₁ being S -monomorphic Ring holds b₁ is R -monomorphic

proof end;

end;

registration

let R be Ring;

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

coherence
for b₁ being R -monomorphic Ring holds b₁ is R -homomorphic

proof end;

end;

registration

let R be Ring;
let S be R -monomorphic Ring;
let f be Monomorphism of R,S;

reduce (f ") " to f;

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

end;

theorem Th68: :: RING_3:69

for R being Ring
for S being b₁ -homomorphic Ring
for T being b₂ -homomorphic Ring
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₁ -homomorphic Ring
for T being b₂ -monomorphic Ring
for f being Homomorphism of R,S
for g being Monomorphism of S,T holds ker f = ker (g * f)

proof end;

theorem Th70: :: RING_3:71

for R being Ring
for S being Subring of R holds R is S -monomorphic

proof end;

theorem Th71: :: RING_3:72

for R, S being Ring holds
( S is b₁ -monomorphic Ring iff S includes R )

proof end;

definition

let R, S be Ring;

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

end;

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

registration

let R be Ring;

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 V192() V193() V194() V195() R -isomorphic for doubleLoopStr ;

existence
ex b₁ being Ring st b₁ is R -isomorphic

proof end;

end;

registration

let R be comRing;

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 V192() V193() V194() V195() R -isomorphic for doubleLoopStr ;

existence
ex b₁ being comRing st b₁ is R -isomorphic

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 V192() V193() V194() V195() R -isomorphic for doubleLoopStr ;

existence
ex b₁ being Ring st b₁ is R -isomorphic

proof end;

end;

registration

let R be domRing;

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 V192() V193() V194() V195() R -isomorphic for doubleLoopStr ;

existence
ex b₁ being domRing st b₁ is R -isomorphic

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 V192() V193() V194() V195() R -isomorphic for doubleLoopStr ;

existence
ex b₁ being comRing st b₁ is R -isomorphic

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 V192() V193() V194() V195() R -isomorphic for doubleLoopStr ;

existence
ex b₁ being Ring st b₁ is R -isomorphic

proof end;

end;

registration

let R be Field;

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 V143() V192() V193() V194() V195() PID Euclidian factorial R -isomorphic for doubleLoopStr ;

existence
ex b₁ being Field st b₁ is R -isomorphic

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 V192() V193() V194() V195() R -isomorphic for doubleLoopStr ;

existence
ex b₁ being domRing st b₁ is R -isomorphic

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 V192() V193() V194() V195() R -isomorphic for doubleLoopStr ;

existence
ex b₁ being comRing st b₁ is R -isomorphic

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 V192() V193() V194() V195() R -isomorphic for doubleLoopStr ;

existence
ex b₁ being Ring st b₁ is R -isomorphic

proof end;

end;

registration

let R be Ring;
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 Element of bool [: the carrier of R, the carrier of S:];

existence
ex b₁ being Function of R,S st
( b₁ is additive & b₁ is multiplicative & b₁ is unity-preserving & b₁ is isomorphism )

proof end;

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;

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

proof end;

end;

Lm7: for R being Ring
for S being b₁ -isomorphic Ring
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;

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 Element of bool [: the carrier of S, the carrier of R:];

existence
ex b₁ being Function of S,R st
( b₁ is additive & b₁ is multiplicative & b₁ is unity-preserving & b₁ is isomorphism )

proof end;

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;

registration

let R be Ring;
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 doubleLoopStr ;

coherence
for b₁ being S -isomorphic Ring holds b₁ is R -isomorphic

proof end;

end;

registration

let R be Ring;

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

coherence
for b₁ being R -isomorphic Ring holds b₁ is R -monomorphic

proof end;

end;

theorem Th72: :: RING_3:73

for R being Ring
for S being b₁ -isomorphic Ring
for f being Isomorphism of R,S holds f " is Isomorphism of S,R by Lm7;

theorem :: RING_3:74

for R being Ring
for S being b₁ -isomorphic Ring holds R is S -isomorphic

proof end;

registration

let R be comRing;

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

coherence
for b₁ being R -isomorphic Ring holds b₁ is commutative

proof end;

end;

registration

let R be domRing;

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

coherence
for b₁ being R -isomorphic Ring holds
( not b₁ is degenerated & b₁ is domRing-like )

proof end;

end;

registration

let F be Field;

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

coherence
for b₁ being F -isomorphic Ring holds b₁ is almost_left_invertible

proof end;

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 )

proof end;

definition

let R be Ring;

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
ex b₁ being Nat st
( ( b₁ '*' (1. R) = 0. R & b₁ <> 0 & ( for m being positive Nat st m < b₁ holds
m '*' (1. R) <> 0. R ) ) or ( b₁ = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) )

proof end;

uniqueness
for b₁, b₂ being Nat st ( ( b₁ '*' (1. R) = 0. R & b₁ <> 0 & ( for m being positive Nat st m < b₁ holds
m '*' (1. R) <> 0. R ) ) or ( b₁ = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) ) & ( ( b₂ '*' (1. R) = 0. R & b₂ <> 0 & ( for m being positive Nat st m < b₂ holds
m '*' (1. R) <> 0. R ) ) or ( b₂ = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines Char RING_3:def 5 :
for R being Ring
for b₂ being Nat holds
( b₂ = Char R iff ( ( b₂ '*' (1. R) = 0. R & b₂ <> 0 & ( for m being positive Nat st m < b₂ holds
m '*' (1. R) <> 0. R ) ) or ( b₂ = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) ) );

definition

let n be Nat;
let R be Ring;

attr R is n -characteristic means :Def6: :: RING_3:def 6
Char R = n;

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

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

proof end;

theorem Th75: :: RING_3:76

Char INT.Ring = 0

proof end;

theorem Th76: :: RING_3:77

for n being positive Nat holds Char (Z/ n) = n

proof end;

registration

cluster INT.Ring -> 0 -characteristic ;

coherence
INT.Ring is 0 -characteristic by Th75;

end;

registration

let n be positive Nat;

cluster Z/ n -> n -characteristic ;

coherence
Z/ n is n -characteristic by Th76;

end;

registration

let n be Nat;

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 V192() V193() V194() V195() n -characteristic for doubleLoopStr ;

existence
ex b₁ being comRing st b₁ is n -characteristic

proof end;

end;

registration

let n be positive Nat;
let R be n -characteristic Ring;

cluster Char R -> positive ;

coherence
Char R is positive by Def6;

end;

definition

let R be Ring;

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 } is Subset of NAT

proof end;

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

registration

let n be positive Nat;
let R be n -characteristic Ring;

cluster CharSet R -> non empty ;

coherence
not CharSet R is empty

proof end;

end;

theorem Th77: :: RING_3:78

for R being Ring holds
( Char R = 0 iff CharSet R = {} )

proof end;

theorem Th78: :: RING_3:79

for n being positive Nat
for R being b₁ -characteristic Ring holds Char R = min (CharSet R)

proof end;

theorem Th79: :: RING_3:80

for R being Ring holds Char R = min* (CharSet R)

proof end;

theorem :: RING_3:81

for p being Prime
for R being b₁ -characteristic Ring
for n being positive Nat holds
( n is Element of CharSet R iff p divides n )

proof end;

definition

let R be Ring;

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
ex b₁ being Function of INT.Ring,R st
for x being Element of INT.Ring holds b₁ . x = x '*' (1. R)

proof end;

uniqueness
for b₁, b₂ being Function of INT.Ring,R st ( for x being Element of INT.Ring holds b₁ . x = x '*' (1. R) ) & ( for x being Element of INT.Ring holds b₂ . x = x '*' (1. R) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines canHom_Int RING_3:def 8 :
for R being Ring
for b₂ being Function of INT.Ring,R holds
( b₂ = canHom_Int R iff for x being Element of INT.Ring holds b₂ . x = x '*' (1. R) );

registration

let R be Ring;

cluster canHom_Int R -> unity-preserving additive multiplicative ;

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

proof end;

end;

registration

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

coherence
for b₁ being Ring holds b₁ is INT.Ring -homomorphic

proof end;

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 )

proof end;

theorem Th82: :: RING_3:83

for R being Ring holds
( Char R = 0 iff canHom_Int R is monomorphism )

proof end;

registration

let R be 0 -characteristic Ring;

cluster canHom_Int R -> monomorphism ;

coherence
canHom_Int R is monomorphism

proof end;

end;

registration

let R be 0 -characteristic Ring;

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 Element of bool [: the carrier of INT.Ring, the carrier of R:];

existence
ex b₁ being Function of INT.Ring,R st
( b₁ is additive & b₁ is multiplicative & b₁ is unity-preserving & b₁ is monomorphism )

proof end;

end;

theorem Th83: :: RING_3:84

for R being Ring
for f being Homomorphism of INT.Ring,R holds f = canHom_Int R

proof end;

theorem :: RING_3:85

for f being Homomorphism of INT.Ring,INT.Ring holds f = id INT.Ring

proof end;

theorem Th85: :: RING_3:86

for R being domRing holds
( Char R = 0 or Char R is prime )

proof end;

theorem :: RING_3:87

for R being Ring
for S being b₁ -homomorphic Ring holds Char S divides Char R

proof end;

theorem Th87: :: RING_3:88

for R being Ring
for S being b₁ -monomorphic Ring holds Char S = Char R

proof end;

theorem Th88: :: RING_3:89

for R being Ring
for S being Subring of R holds Char S = Char R

proof end;

registration

let n be Nat;
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 doubleLoopStr ;

coherence
for b₁ being Ring st b₁ is R -monomorphic holds
b₁ is n -characteristic

proof end;

cluster -> n -characteristic for Subring of R;

coherence
for b₁ being Subring of R holds b₁ is n -characteristic

proof end;

end;

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

proof end;

registration

cluster F_Complex -> 0 -characteristic ;

coherence
F_Complex is 0 -characteristic

proof end;

end;

registration

cluster F_Real -> 0 -characteristic ;

coherence
F_Real is 0 -characteristic

proof end;

end;

registration

cluster F_Rat -> 0 -characteristic ;

coherence
F_Rat is 0 -characteristic

proof end;

end;

registration

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 V143() V192() V193() V194() V195() PID Euclidian INT.Ring -homomorphic factorial 0 -characteristic for doubleLoopStr ;

existence
ex b₁ being Field st b₁ is 0 -characteristic

proof end;

end;

registration

let p be Prime;

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 V143() V192() V193() V194() V195() PID Euclidian INT.Ring -homomorphic factorial p -characteristic for doubleLoopStr ;

existence
ex b₁ being Field st b₁ is p -characteristic

proof end;

end;

registration

let p be Prime;
let R be p -characteristic domRing;

cluster Char R -> prime ;

coherence
Char R is prime by Th85;

end;

registration

let F be 0 -characteristic Field;

cluster -> 0 -characteristic for Subfield of F;

coherence
for b₁ being Subfield of F holds b₁ is 0 -characteristic

proof end;

end;

registration

let p be Prime;
let F be p -characteristic Field;

cluster -> p -characteristic for Subfield of F;

coherence
for b₁ being Subfield of F holds b₁ is p -characteristic

proof end;

end;

definition

let F be Field;

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 } is Subset of F

proof end;

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

definition

let F be Field;

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
ex b₁ being strict doubleLoopStr st
( the carrier of b₁ = carrier/\ F & the addF of b₁ = the addF of F || (carrier/\ F) & the multF of b₁ = the multF of F || (carrier/\ F) & the OneF of b₁ = 1. F & the ZeroF of b₁ = 0. F )

proof end;

uniqueness
for b₁, b₂ being strict doubleLoopStr st the carrier of b₁ = carrier/\ F & the addF of b₁ = the addF of F || (carrier/\ F) & the multF of b₁ = the multF of F || (carrier/\ F) & the OneF of b₁ = 1. F & the ZeroF of b₁ = 0. F & the carrier of b₂ = carrier/\ F & the addF of b₂ = the addF of F || (carrier/\ F) & the multF of b₂ = the multF of F || (carrier/\ F) & the OneF of b₂ = 1. F & the ZeroF of b₂ = 0. F holds
b₁ = b₂ ;

end;

:: deftheorem Def10 defines PrimeField RING_3:def 10 :
for F being Field
for b₂ being strict doubleLoopStr holds
( b₂ = PrimeField F iff ( the carrier of b₂ = carrier/\ F & the addF of b₂ = the addF of F || (carrier/\ F) & the multF of b₂ = the multF of F || (carrier/\ F) & the OneF of b₂ = 1. F & the ZeroF of b₂ = 0. F ) );

registration

let F be Field;

cluster PrimeField F -> non degenerated strict ;

coherence
not PrimeField F is degenerated

proof end;

end;

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;

cluster PrimeField F -> right_complementable strict Abelian add-associative right_zeroed ;

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

proof end;

end;

registration

let F be Field;

cluster PrimeField F -> strict commutative ;

coherence
PrimeField F is commutative

proof end;

end;

registration

let F be Field;

cluster PrimeField F -> almost_left_invertible strict associative well-unital distributive ;

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

proof end;

end;

definition

let F be Field;
:: original: PrimeField
redefine func PrimeField F -> strict Subfield of F;
coherence
PrimeField F is strict Subfield of F

proof end;

end;

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

proof end;

theorem Th89: :: RING_3:90

for F being Field
for E being strict Subfield of PrimeField F holds E = PrimeField F

proof end;

theorem Th90: :: RING_3:91

for F being Field
for E being Subfield of F holds PrimeField F is Subfield of E

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

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

proof end;

theorem :: RING_3:94

for E being Field
for F being Subfield of E holds PrimeField F = PrimeField E

proof end;

theorem :: RING_3:95

for F being Field holds PrimeField (PrimeField F) = PrimeField F by Th91;

registration

let F be Field;

cluster PrimeField F -> strict prime ;

coherence
PrimeField F is prime

proof end;

end;

theorem :: RING_3:96

for F being Field holds
( F is prime iff F = PrimeField F ) by EC_PF_1:def 2;

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

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;

definition

let F be Field;

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
ex b₁ being Function of F_Rat,F st
for x being Element of F_Rat holds b₁ . x = ((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x))

proof end;

uniqueness
for b₁, b₂ being Function of F_Rat,F st ( for x being Element of F_Rat holds b₁ . x = ((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x)) ) & ( for x being Element of F_Rat holds b₂ . x = ((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines canHom_Rat RING_3:def 11 :
for F being Field
for b₂ being Function of F_Rat,F holds
( b₂ = canHom_Rat F iff for x being Element of F_Rat holds b₂ . x = ((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x)) );

registration

let F be Field;

cluster canHom_Rat F -> unity-preserving ;

coherence
canHom_Rat F is unity-preserving

proof end;

end;

registration

let F be 0 -characteristic Field;

cluster canHom_Rat F -> additive multiplicative ;

coherence
( canHom_Rat F is additive & canHom_Rat F is multiplicative )

proof end;

end;

registration

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

coherence
for b₁ being 0 -characteristic Field holds b₁ is F_Rat -monomorphic

proof end;

end;

theorem Th97: :: RING_3:98

for F being Field holds canHom_Int F = (canHom_Rat F) | INT

proof end;

registration

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 V143() V192() V193() V194() V195() PID Euclidian INT.Ring -homomorphic F_Rat -homomorphic factorial 0 -characteristic for doubleLoopStr ;

existence
ex b₁ being Field st
( b₁ is 0 -characteristic & b₁ is F_Rat -homomorphic ) ;

end;

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

proof end;

registration

cluster F_Rat -> F_Rat -homomorphic ;

coherence
F_Rat is F_Rat -homomorphic ;

end;

registration

let F be 0 -characteristic Field;

cluster PrimeField F -> strict F_Rat -homomorphic ;

coherence
PrimeField F is F_Rat -homomorphic ;

end;

theorem :: RING_3:100

for f being Homomorphism of F_Rat,F_Rat holds f = id F_Rat

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

proof end;

end;

registration

let F be 0 -characteristic Field;

cluster canHom_Rat (PrimeField F) -> onto ;

coherence
canHom_Rat (PrimeField F) is onto

proof end;

end;

theorem Th100: :: RING_3:101

for F being 0 -characteristic Field holds F_Rat , PrimeField F are_isomorphic

proof end;

theorem :: RING_3:102

PrimeField F_Rat = F_Rat by GAUSSINT:26;

theorem :: RING_3:103

for F being 0 -characteristic Field holds F includes F_Rat by Th71;

theorem :: RING_3:104

for F being 0 -characteristic Field
for E being Field st F includes E holds
E includes F_Rat

proof end;

theorem Th104: :: RING_3:105

for p being Prime
for R being b₁ -characteristic Ring
for i being Integer holds i '*' (1. R) = (i mod p) '*' (1. R)

proof end;

definition

let p be Prime;
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) is Function of (Z/ p),F

proof end;

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

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

let p be Prime;
let F be Field;

cluster canHom_Z/ (p,F) -> unity-preserving ;

coherence
canHom_Z/ (p,F) is unity-preserving

proof end;

end;

registration

let p be Prime;
let F be p -characteristic Field;

cluster canHom_Z/ (p,F) -> additive multiplicative ;

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

proof end;

end;

registration

let p be Prime;

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

coherence
for b₁ being p -characteristic Field holds b₁ is Z/ p -monomorphic

proof end;

end;

registration

let p be Prime;

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 V143() V192() V193() V194() V195() PID Euclidian INT.Ring -homomorphic Z/ p -homomorphic factorial p -characteristic for doubleLoopStr ;

existence
ex b₁ being Field st
( b₁ is p -characteristic & b₁ is Z/ p -homomorphic ) ;

cluster Z/ p -> Z/ p -homomorphic ;

coherence
Z/ p is Z/ p -homomorphic ;

end;

theorem Th105: :: RING_3:106

for p being Prime
for F being Z/ b₁ -homomorphic b₁ -characteristic Field
for f being Homomorphism of (Z/ p),F holds f = canHom_Z/ (p,F)

proof end;

theorem :: RING_3:107

for p being Prime
for f being Homomorphism of (Z/ p),(Z/ p) holds f = id (Z/ p)

proof end;

registration

let p be Prime;
let F be p -characteristic Field;

cluster PrimeField F -> strict Z/ p -homomorphic ;

coherence
PrimeField F is Z/ p -homomorphic ;

end;

registration

let p be Prime;
let F be p -characteristic Field;

cluster canHom_Z/ (p,(PrimeField F)) -> onto ;

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

proof end;

end;

theorem Th107: :: RING_3:108

for p being Prime
for F being b₁ -characteristic Field holds Z/ p, PrimeField F are_isomorphic

proof end;

theorem :: RING_3:109

for p being Prime
for F being strict Subfield of Z/ p holds F = Z/ p by EC_PF_1:def 2;

theorem :: RING_3:110

for p being Prime holds PrimeField (Z/ p) = Z/ p by EC_PF_1:def 2;

theorem :: RING_3:111

for p being Prime
for F being b₁ -characteristic Field holds F includes Z/ p by Th71;

theorem :: RING_3:112

for p being Prime
for F being b₁ -characteristic Field
for E being Field st F includes E holds
E includes Z/ p

proof end;

registration

let p be Prime;

cluster Z/ p -> prime ;

coherence
Z/ p is prime ;

end;

theorem :: RING_3:113

for F being Field holds
( Char F = 0 iff PrimeField F, F_Rat are_isomorphic )

proof end;

theorem :: RING_3:114

for p being Prime
for F being Field holds
( Char F = p iff PrimeField F, Z/ p are_isomorphic )

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

proof end;