let R be Ring; :: thesis: for n being non negative Element of INT.Ring holds
( Char R = n iff ker (canHom_Int R) = {n} -Ideal )
let n be non negative Element of INT.Ring; :: thesis: ( Char R = n iff ker (canHom_Int R) = {n} -Ideal )
set f = canHom_Int R;
reconsider k = n as Integer ;
A1: now :: thesis: ( Char R = n implies ker (canHom_Int R) = {n} -Ideal )
assume A2: Char R = n ; :: thesis: ker (canHom_Int R) = {n} -Ideal
reconsider k = k as Nat ;
per cases ( k = 0 or k > 0 ) ;
suppose A3: k = 0 ; :: thesis: ker (canHom_Int R) = {n} -Ideal
then A4: {n} -Ideal = {(0. INT.Ring)} by IDEAL_1:47;
now :: thesis: for x1, x2 being object st x1 in the carrier of INT.Ring & x2 in the carrier of INT.Ring & (canHom_Int R) . x1 = (canHom_Int R) . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in the carrier of INT.Ring & x2 in the carrier of INT.Ring & (canHom_Int R) . x1 = (canHom_Int R) . x2 implies x1 = x2 )
assume A5: ( x1 in the carrier of INT.Ring & x2 in the carrier of INT.Ring & (canHom_Int R) . x1 = (canHom_Int R) . x2 ) ; :: thesis: x1 = x2
then reconsider y1 = x1, y2 = x2 as Integer ;
y1 '*' (1. R) = (canHom_Int R) . y1 by A5, Def8
.= y2 '*' (1. R) by A5, Def8 ;
then A6: 0. R = (y1 '*' (1. R)) - (y2 '*' (1. R)) by RLVECT_1:15
.= (y1 - y2) '*' (1. R) by Th63 ;
now :: thesis: not y1 - y2 <> 0
assume y1 - y2 <> 0 ; :: thesis: contradiction
then A7: y1 <> y2 ;
ex n being positive Nat st n '*' (1. R) = 0. R
proof
per cases ( y1 - y2 > 0 or 0 < y2 - y1 ) by A7, XREAL_1:55;
suppose y1 - y2 > 0 ; :: thesis: ex n being positive Nat st n '*' (1. R) = 0. R
hence ex n being positive Nat st n '*' (1. R) = 0. R by A6; :: thesis: verum
end;
suppose A8: 0 < y2 - y1 ; :: thesis: ex n being positive Nat st n '*' (1. R) = 0. R
(y2 - y1) '*' (1. R) = (0 - (y1 - y2)) '*' (1. R)
.= - ((y1 - y2) '*' (1. R)) by Th62
.= 0. R by A6 ;
hence ex n being positive Nat st n '*' (1. R) = 0. R by A8; :: thesis: verum
end;
end;
end;
hence contradiction by Def5, A2, A3; :: thesis: verum
end;
hence x1 = x2 ; :: thesis: verum
end;
then canHom_Int R is one-to-one by FUNCT_2:19;
hence ker (canHom_Int R) = {n} -Ideal by A4, RING_2:12; :: thesis: verum
end;
suppose A9: k > 0 ; :: thesis: ker (canHom_Int R) = {n} -Ideal
A10: now :: thesis: for x being object st x in {n} -Ideal holds
x in ker (canHom_Int R)
let x be object ; :: thesis: ( x in {n} -Ideal implies x in ker (canHom_Int R) )
assume x in {n} -Ideal ; :: thesis: x in ker (canHom_Int R)
then x in { (n * r) where r is Element of INT.Ring : verum } by IDEAL_1:64;
then consider r being Element of INT.Ring such that
A11: x = n * r ;
(canHom_Int R) . x = ((canHom_Int R) . n) * ((canHom_Int R) . r) by A11, GROUP_6:def 6
.= (n '*' (1. R)) * ((canHom_Int R) . r) by Def8
.= (0. R) * ((canHom_Int R) . r) by A2, Def5, A9
.= 0. R ;
hence x in ker (canHom_Int R) by A11; :: thesis: verum
end;
now :: thesis: for x being object st x in ker (canHom_Int R) holds
x in {n} -Ideal
let x be object ; :: thesis: ( x in ker (canHom_Int R) implies x in {n} -Ideal )
assume x in ker (canHom_Int R) ; :: thesis: x in {n} -Ideal
then consider y being Element of INT.Ring such that
A12: ( y = x & (canHom_Int R) . y = 0. R ) ;
reconsider d = y div n, r = y mod n as Element of INT.Ring ;
A13: y mod n < n by A9, INT_1:58;
A14: y = (d * n) + r by A9, INT_1:59;
y mod n in NAT by INT_1:3, INT_1:57;
then reconsider rr = y mod n as Nat ;
0. R = ((canHom_Int R) . (d * n)) + ((canHom_Int R) . r) by A12, A14, VECTSP_1:def 20
.= (((canHom_Int R) . d) * ((canHom_Int R) . n)) + ((canHom_Int R) . r) by GROUP_6:def 6
.= (((canHom_Int R) . d) * (n '*' (1. R))) + ((canHom_Int R) . r) by Def8
.= (((canHom_Int R) . d) * (0. R)) + ((canHom_Int R) . r) by Def5, A9, A2
.= (y mod n) '*' (1. R) by Def8 ;
then rr = 0 by A13, Def5, A2;
then y in { (n * a) where a is Element of INT.Ring : verum } by A14;
hence x in {n} -Ideal by A12, IDEAL_1:64; :: thesis: verum
end;
hence ker (canHom_Int R) = {n} -Ideal by A10, TARSKI:2; :: thesis: verum
end;
end;
end;
now :: thesis: ( ker (canHom_Int R) = {n} -Ideal implies Char R = n )
assume A15: ker (canHom_Int R) = {n} -Ideal ; :: thesis: Char R = n
per cases ( n = 0 or n <> 0 ) ;
suppose A16: n = 0 ; :: thesis: Char R = n
then ker (canHom_Int R) = {(0. INT.Ring)} by A15, IDEAL_1:47;
then A17: canHom_Int R is monomorphism by RING_2:12;
now :: thesis: for n being positive Nat holds not n '*' (1. R) = 0. R
assume ex n being positive Nat st n '*' (1. R) = 0. R ; :: thesis: contradiction
then consider k being positive Nat such that
A18: k '*' (1. R) = 0. R ;
reconsider kk = k as Element of INT.Ring by INT_1:def 2;
(canHom_Int R) . kk = 0. R by A18, Def8
.= (canHom_Int R) . (0. INT.Ring) by RING_2:6 ;
hence contradiction by A17, FUNCT_2:19; :: thesis: verum
end;
hence Char R = n by A16, Def5; :: thesis: verum
end;
suppose A19: n <> 0 ; :: thesis: Char R = n
reconsider l = n as positive Nat by A19;
n in ker (canHom_Int R) by A15, IDEAL_1:66;
then consider y being Element of INT.Ring such that
A20: ( y = n & (canHom_Int R) . y = 0. R ) ;
(canHom_Int R) . n = n '*' (1. R) by Def8;
then A21: n in CharSet R by A19, A20;
now :: thesis: for x being Nat st x in CharSet R holds
n <= x
let x be Nat; :: thesis: ( x in CharSet R implies n <= x )
assume x in CharSet R ; :: thesis: n <= x
then consider m being positive Nat such that
A22: ( x = m & m '*' (1. R) = 0. R ) ;
reconsider a = m as Element of INT.Ring by INT_1:def 2;
(canHom_Int R) . a = 0. R by A22, Def8;
then a in {n} -Ideal by A15;
then a in { (n * r) where r is Element of INT.Ring : verum } by IDEAL_1:64;
then consider q being Element of INT.Ring such that
A23: a = n * q ;
reconsider qq = q as Integer ;
now :: thesis: not n > a
assume n > a ; :: thesis: contradiction
then l / l > (l * qq) / l by A23, XREAL_1:74;
then 1 > qq * (l / l) by XCMPLX_1:60;
then 1 > qq * 1 by XCMPLX_1:60;
then qq + 1 <= 1 by INT_1:7;
then (qq + 1) - 1 <= 1 - 1 by XREAL_1:13;
hence contradiction by A23; :: thesis: verum
end;
hence n <= x by A22; :: thesis: verum
end;
then n = min* (CharSet R) by A21, NAT_1:def 1;
hence Char R = n by Th79; :: thesis: verum
end;
end;
end;
hence ( Char R = n iff ker (canHom_Int R) = {n} -Ideal ) by A1; :: thesis: verum