let m be Element of NAT ; for X being finite Subset of INT st card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds
not [x,y] in Cong m ) holds
X is_CRS_of m
let X be finite Subset of INT; ( card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds
not [x,y] in Cong m ) implies X is_CRS_of m )
assume that
A1:
card X = m
and
A2:
for x, y being Integer st x in X & y in X & x <> y holds
not [x,y] in Cong m
; X is_CRS_of m
per cases
( X is empty or not X is empty )
;
suppose
not
X is
empty
;
X is_CRS_of mthen reconsider X =
X as non
empty finite Subset of
INT ;
defpred S1[
Nat,
set ]
means $2
in Class (
(Cong m),
($1 -' 1));
A3:
X <> {}
;
A4:
for
a being
Nat st
a in Seg m holds
ex
y being
Element of
X st
S1[
a,
y]
proof
set Y =
Segm m;
let a be
Nat;
( a in Seg m implies ex y being Element of X st S1[a,y] )
assume A5:
a in Seg m
;
ex y being Element of X st S1[a,y]
a <= m
by A5, FINSEQ_1:1;
then A6:
a - 1
< m
by XREAL_1:147;
consider fp being
FinSequence such that A7:
len fp = m
and A8:
for
b being
Element of
NAT st
b in dom fp holds
fp . b in X
and A9:
fp is
one-to-one
by A1, Th51;
for
b being
Nat st
b in dom fp holds
fp . b in X
by A8;
then reconsider fp =
fp as
FinSequence of
X by FINSEQ_2:12;
defpred S2[
Nat,
set ]
means fp . $1
in Class (
(Cong m),$2);
A10:
for
c being
Element of
NAT st
c in Seg m holds
ex
r being
Element of
Segm m st
S2[
c,
r]
proof
let c be
Element of
NAT ;
( c in Seg m implies ex r being Element of Segm m st S2[c,r] )
assume
c in Seg m
;
ex r being Element of Segm m st S2[c,r]
consider q,
r being
Integer such that A11:
fp . c = (m * q) + r
and A12:
r >= 0
and A13:
r < m
by A1, Th13;
(fp . c) mod m = r mod m
by A11, NAT_D:61;
then
r,
fp . c are_congruent_mod m
by A1, NAT_D:64;
then A14:
[r,(fp . c)] in Cong m
by Def1;
reconsider r =
r as
Element of
NAT by A12, INT_1:3;
reconsider r =
r as
Element of
Segm m by A13, NAT_1:44;
take
r
;
S2[c,r]
thus
S2[
c,
r]
by A14, EQREL_1:18;
verum
end;
reconsider Y =
Segm m as non
empty set by A1, A3;
A15:
for
c being
Nat st
c in Seg m holds
ex
r being
Element of
Y st
S2[
c,
r]
by A10;
consider fr being
FinSequence of
Y such that A16:
(
dom fr = Seg m & ( for
c being
Nat st
c in Seg m holds
S2[
c,
fr . c] ) )
from FINSEQ_1:sch 5(A15);
for
x1,
x2 being
object st
x1 in dom fr &
x2 in dom fr &
fr . x1 = fr . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom fr & x2 in dom fr & fr . x1 = fr . x2 implies x1 = x2 )
assume that A17:
x1 in dom fr
and A18:
x2 in dom fr
and A19:
fr . x1 = fr . x2
;
x1 = x2
(
fp . x1 in Class (
(Cong m),
(fr . x1)) &
fp . x2 in Class (
(Cong m),
(fr . x1)) )
by A16, A17, A18, A19;
then A20:
[(fp . x1),(fp . x2)] in Cong m
by EQREL_1:22;
assume A21:
x1 <> x2
;
contradiction
reconsider x1 =
x1,
x2 =
x2 as
Element of
NAT by A17, A18;
A22:
x1 in dom fp
by A7, A16, A17, FINSEQ_1:def 3;
then A23:
fp . x1 in X
by FINSEQ_2:11;
A24:
x2 in dom fp
by A7, A16, A18, FINSEQ_1:def 3;
then A25:
fp . x2 in X
by FINSEQ_2:11;
fp . x1 <> fp . x2
by A9, A21, A22, A24;
hence
contradiction
by A2, A20, A23, A25;
verum
end;
then
fr is
one-to-one
;
then A26:
card (rng fr) =
len fr
by FINSEQ_4:62
.=
m
by A16, FINSEQ_1:def 3
;
reconsider Y =
Y as
finite set ;
a >= 1
by A5, FINSEQ_1:1;
then
a -' 1
< m
by A6, XREAL_1:233;
then A27:
a -' 1
in Y
by NAT_1:44;
card Y = m
;
then
rng fr = Y
by A26, CARD_2:102;
then consider w being
object such that A28:
w in dom fr
and A29:
fr . w = a -' 1
by A27, FUNCT_1:def 3;
reconsider w =
w as
Element of
NAT by A28;
w in dom fp
by A7, A16, A28, FINSEQ_1:def 3;
then reconsider y =
fp . w as
Element of
X by FINSEQ_2:11;
take
y
;
S1[a,y]
thus
S1[
a,
y]
by A16, A28, A29;
verum
end; consider fp being
FinSequence of
X such that A30:
(
dom fp = Seg m & ( for
a being
Nat st
a in Seg m holds
S1[
a,
fp . a] ) )
from FINSEQ_1:sch 5(A4);
A31:
rng fp c= X
by FINSEQ_1:def 4;
A32:
len fp = m
by A30, FINSEQ_1:def 3;
for
a,
b being
object st
a in dom fp &
b in dom fp &
fp . a = fp . b holds
a = b
proof
let a,
b be
object ;
( a in dom fp & b in dom fp & fp . a = fp . b implies a = b )
assume that A33:
a in dom fp
and A34:
b in dom fp
and A35:
fp . a = fp . b
;
a = b
reconsider a =
a,
b =
b as
Element of
NAT by A33, A34;
A36:
b >= 1
by A30, A34, FINSEQ_1:1;
A37:
a >= 1
by A30, A33, FINSEQ_1:1;
then A38:
(a -' 1) - (b -' 1) =
(a - 1) - (b -' 1)
by XREAL_1:233
.=
(a - 1) - (b - 1)
by A36, XREAL_1:233
.=
a - b
;
reconsider l =
fp . a,
ll =
fp . b as
Element of
INT by A33, A34, FINSEQ_2:11;
fp . b in Class (
(Cong m),
(b -' 1))
by A30, A34;
then
[(b -' 1),(fp . b)] in Cong m
by EQREL_1:18;
then
b -' 1,
ll are_congruent_mod m
by Def1;
then A39:
l,
b -' 1
are_congruent_mod m
by A35, INT_1:14;
b <= m
by A30, A34, FINSEQ_1:1;
then
a - b >= 1
- m
by A37, XREAL_1:13;
then A40:
a - b > - m
by XREAL_1:145;
a <= m
by A30, A33, FINSEQ_1:1;
then
a - b <= m - 1
by A36, XREAL_1:13;
then
a - b < m
by XREAL_1:147;
then
|.(a - b).| < m
by A40, SEQ_2:1;
then A41:
|.(a - b).| < |.m.|
by ABSVALUE:def 1;
fp . a in Class (
(Cong m),
(a -' 1))
by A30, A33;
then
[(a -' 1),(fp . a)] in Cong m
by EQREL_1:18;
then
a -' 1,
l are_congruent_mod m
by Def1;
then
a -' 1,
b -' 1
are_congruent_mod m
by A39, INT_1:15;
then A42:
m divides a - b
by A38;
now not a <> bassume
a <> b
;
contradictionthen
a - b <> 0
;
hence
contradiction
by A42, A41, Th6;
verum end;
hence
a = b
;
verum
end; then
fp is
one-to-one
;
then
card X = card (rng fp)
by A1, A32, FINSEQ_4:62;
then
X = rng fp
by A31, CARD_2:102;
hence
X is_CRS_of m
by A30, A32;
verum end;