let m be Element of NAT ; for X being finite set st X is_CRS_of m holds
( card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds
not [x,y] in Cong m ) )
let X be finite set ; ( X is_CRS_of m implies ( card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds
not [x,y] in Cong m ) ) )
assume
X is_CRS_of m
; ( card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds
not [x,y] in Cong m ) )
then consider fp being FinSequence of INT such that
A1:
X = rng fp
and
A2:
len fp = m
and
A3:
for b being Nat st b in dom fp holds
fp . b in Class ((Cong m),(b -' 1))
;
A4:
for x, y being Integer st x in X & y in X & x <> y holds
not [x,y] in Cong m
proof
let x,
y be
Integer;
( x in X & y in X & x <> y implies not [x,y] in Cong m )
assume that A5:
x in X
and A6:
y in X
and A7:
x <> y
;
not [x,y] in Cong m
consider a being
object such that A8:
a in dom fp
and A9:
x = fp . a
by A1, A5, FUNCT_1:def 3;
reconsider a =
a as
Element of
NAT by A8;
x in Class (
(Cong m),
(a -' 1))
by A3, A8, A9;
then
[(a -' 1),x] in Cong m
by EQREL_1:18;
then A10:
a -' 1,
x are_congruent_mod m
by Def1;
consider b being
object such that A11:
b in dom fp
and A12:
y = fp . b
by A1, A6, FUNCT_1:def 3;
reconsider b =
b as
Element of
NAT by A11;
A13:
b in Seg m
by A2, A11, FINSEQ_1:def 3;
then A14:
b >= 1
by FINSEQ_1:1;
y in Class (
(Cong m),
(b -' 1))
by A3, A11, A12;
then
[(b -' 1),y] in Cong m
by EQREL_1:18;
then
b -' 1,
y are_congruent_mod m
by Def1;
then A15:
y,
b -' 1
are_congruent_mod m
by INT_1:14;
assume
[x,y] in Cong m
;
contradiction
then
x,
y are_congruent_mod m
by Def1;
then
x,
b -' 1
are_congruent_mod m
by A15, INT_1:15;
then
a -' 1,
b -' 1
are_congruent_mod m
by A10, INT_1:15;
then A16:
m divides (a -' 1) - (b -' 1)
;
A17:
a in Seg m
by A2, A8, FINSEQ_1:def 3;
then A18:
a >= 1
by FINSEQ_1:1;
b <= m
by A13, FINSEQ_1:1;
then
a - b >= 1
- m
by A18, XREAL_1:13;
then A19:
a - b > - m
by XREAL_1:145;
a <= m
by A17, FINSEQ_1:1;
then
a - b <= m - 1
by A14, XREAL_1:13;
then
a - b < m
by XREAL_1:147;
then
|.(a - b).| < m
by A19, SEQ_2:1;
then A20:
|.(a - b).| < |.m.|
by ABSVALUE:def 1;
A21:
(a -' 1) - (b -' 1) =
(a - 1) - (b -' 1)
by A18, XREAL_1:233
.=
(a - 1) - (b - 1)
by A14, XREAL_1:233
.=
a - b
;
hence
contradiction
by A7, A9, A12;
verum
end;
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 A22:
a in dom fp
and A23:
b in dom fp
and A24:
fp . a = fp . b
;
a = b
reconsider a =
a,
b =
b as
Element of
NAT by A22, A23;
A25:
b in Seg m
by A2, A23, FINSEQ_1:def 3;
then A26:
b >= 1
by FINSEQ_1:1;
reconsider l =
fp . a,
ll =
fp . b as
Element of
INT by A22, A23, FINSEQ_2:11;
fp . b in Class (
(Cong m),
(b -' 1))
by A3, A23;
then
[(b -' 1),(fp . b)] in Cong m
by EQREL_1:18;
then
b -' 1,
ll are_congruent_mod m
by Def1;
then A27:
l,
b -' 1
are_congruent_mod m
by A24, INT_1:14;
A28:
a in Seg m
by A2, A22, FINSEQ_1:def 3;
then A29:
a >= 1
by FINSEQ_1:1;
then A30:
(a -' 1) - (b -' 1) =
(a - 1) - (b -' 1)
by XREAL_1:233
.=
(a - 1) - (b - 1)
by A26, XREAL_1:233
.=
a - b
;
b <= m
by A25, FINSEQ_1:1;
then
a - b >= 1
- m
by A29, XREAL_1:13;
then A31:
a - b > - m
by XREAL_1:145;
a <= m
by A28, FINSEQ_1:1;
then
a - b <= m - 1
by A26, XREAL_1:13;
then
a - b < m
by XREAL_1:147;
then
|.(a - b).| < m
by A31, SEQ_2:1;
then A32:
|.(a - b).| < |.m.|
by ABSVALUE:def 1;
fp . a in Class (
(Cong m),
(a -' 1))
by A3, A22;
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 A27, INT_1:15;
then A33:
m divides a - b
by A30;
now not a <> bassume
a <> b
;
contradictionthen
a - b <> 0
;
hence
contradiction
by A33, A32, Th6;
verum end;
hence
a = b
;
verum
end;
then
fp is one-to-one
;
hence
( card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds
not [x,y] in Cong m ) )
by A1, A2, A4, FINSEQ_4:62; verum