let n, k be Nat; for A, B being object st A <> B holds
card (DominatedElection (A,n,B,k)) = card (DominatedElection (0,n,1,k))
let A, B be object ; ( A <> B implies card (DominatedElection (A,n,B,k)) = card (DominatedElection (0,n,1,k)) )
assume A1:
A <> B
; card (DominatedElection (A,n,B,k)) = card (DominatedElection (0,n,1,k))
set T = (A,B) --> (0,1);
set W = (0,1) --> (A,B);
A2:
dom ((A,B) --> (0,1)) = {A,B}
by FUNCT_4:62;
A3:
rng ((A,B) --> (0,1)) = {0,1}
by A1, FUNCT_4:64;
A4:
rng ((0,1) --> (A,B)) = {A,B}
by FUNCT_4:64;
A5:
dom ((0,1) --> (A,B)) = {0,1}
by FUNCT_4:62;
A6:
A is set
by TARSKI:1;
A7:
B is set
by TARSKI:1;
A8:
rng (A .--> 0) = {0}
by A6, FUNCOP_1:88;
A9:
rng (B .--> 1) = {1}
by A7, FUNCOP_1:88;
A10:
rng (0 .--> A) = {A}
by A6, FUNCOP_1:88;
A11:
rng (1 .--> B) = {B}
by A7, FUNCOP_1:88;
A12:
(A .--> 0) +* (B .--> 1) is one-to-one
by A8, A9, ZFMISC_1:11, FUNCT_4:92;
A13:
(0 .--> A) +* (1 .--> B) is one-to-one
by A10, A11, A1, ZFMISC_1:11, FUNCT_4:92;
A14:
(A,B) --> (0,1) is one-to-one
by A12, FUNCT_4:def 4;
A15:
(0,1) --> (A,B) is one-to-one
by A13, FUNCT_4:def 4;
A16:
((A,B) --> (0,1)) . A = 0
by A1, FUNCT_4:63;
A17:
((A,B) --> (0,1)) . B = 1
by FUNCT_4:63;
A18:
((0,1) --> (A,B)) . 0 = A
by FUNCT_4:63;
A19:
((0,1) --> (A,B)) . 1 = B
by FUNCT_4:63;
defpred S1[ object , object ] means for f being FinSequence st f = $1 holds
((A,B) --> (0,1)) * f = $2;
A20:
for x being object st x in DominatedElection (A,n,B,k) holds
ex y being object st
( y in DominatedElection (0,n,1,k) & S1[x,y] )
proof
let x be
object ;
( x in DominatedElection (A,n,B,k) implies ex y being object st
( y in DominatedElection (0,n,1,k) & S1[x,y] ) )
assume A21:
x in DominatedElection (
A,
n,
B,
k)
;
ex y being object st
( y in DominatedElection (0,n,1,k) & S1[x,y] )
x in Election (
A,
n,
B,
k)
by A21;
then reconsider f =
x as
Element of
(n + k) -tuples_on {A,B} ;
A22:
len f = n + k
by CARD_1:def 7;
A23:
dom f = Seg (len f)
by FINSEQ_1:def 3;
rng f c= {A,B}
;
then A24:
dom (((A,B) --> (0,1)) * f) = Seg (len f)
by A23, A2, RELAT_1:27;
A25:
rng (((A,B) --> (0,1)) * f) c= {0,1}
by A3, RELAT_1:26;
reconsider Tf =
((A,B) --> (0,1)) * f as
FinSequence ;
reconsider Tf =
Tf as
FinSequence of
{0,1} by A25, FINSEQ_1:def 4;
len Tf = len f
by A24, FINSEQ_1:def 3;
then reconsider Tf =
Tf as
Element of
(n + k) -tuples_on {0,1} by A22, FINSEQ_2:92;
take
Tf
;
( Tf in DominatedElection (0,n,1,k) & S1[x,Tf] )
Tf is
0 ,
n,1,
k -dominated-election
proof
A26:
A in dom ((A,B) --> (0,1))
by A2, TARSKI:def 2;
A27:
B in dom ((A,B) --> (0,1))
by A2, TARSKI:def 2;
Coim (
Tf,
0)
= Coim (
f,
A)
by A26, Th7, A14, A16;
then
card (Coim (Tf,0)) = n
by A21, Def1;
hence
Tf in Election (
0,
n,1,
k)
by Def1;
BALLOT_1:def 2 for i being Nat st i > 0 holds
card ((Tf | i) " {0}) > card ((Tf | i) " {1})
let i be
Nat;
( i > 0 implies card ((Tf | i) " {0}) > card ((Tf | i) " {1}) )
assume A28:
i > 0
;
card ((Tf | i) " {0}) > card ((Tf | i) " {1})
A29:
Tf | i = ((A,B) --> (0,1)) * (f | i)
by RELAT_1:83;
then A30:
Coim (
(Tf | i),
0)
= Coim (
(f | i),
A)
by A26, Th7, A14, A16;
A31:
Coim (
(Tf | i),1)
= Coim (
(f | i),
B)
by A29, A27, Th7, A14, A17;
f is
A,
n,
B,
k -dominated-election
by A21, Def3;
hence
card ((Tf | i) " {0}) > card ((Tf | i) " {1})
by A28, A30, A31;
verum
end;
hence
(
Tf in DominatedElection (
0,
n,1,
k) &
S1[
x,
Tf] )
by Def3;
verum
end;
consider C being Function of (DominatedElection (A,n,B,k)),(DominatedElection (0,n,1,k)) such that
A32:
for x being object st x in DominatedElection (A,n,B,k) holds
S1[x,C . x]
from FUNCT_2:sch 1(A20);
DominatedElection (0,n,1,k) c= rng C
proof
let x be
object ;
TARSKI:def 3 ( not x in DominatedElection (0,n,1,k) or x in rng C )
assume A33:
x in DominatedElection (
0,
n,1,
k)
;
x in rng C
then
x in Election (
0,
n,1,
k)
;
then reconsider f =
x as
Element of
(n + k) -tuples_on {0,1} ;
A34:
len f = n + k
by CARD_1:def 7;
A35:
dom f = Seg (len f)
by FINSEQ_1:def 3;
A36:
rng f c= {0,1}
;
then A37:
dom (((0,1) --> (A,B)) * f) = Seg (len f)
by A35, A5, RELAT_1:27;
A38:
rng (((0,1) --> (A,B)) * f) c= {A,B}
by A4, RELAT_1:26;
reconsider Wf =
((0,1) --> (A,B)) * f as
FinSequence by A37, FINSEQ_1:def 2;
reconsider Wf =
Wf as
FinSequence of
{A,B} by A38, FINSEQ_1:def 4;
len Wf = len f
by A37, FINSEQ_1:def 3;
then reconsider Wf =
Wf as
Element of
(n + k) -tuples_on {A,B} by A34, FINSEQ_2:92;
Wf is
A,
n,
B,
k -dominated-election
proof
A39:
0 in dom ((0,1) --> (A,B))
by A5, TARSKI:def 2;
A40:
1
in dom ((0,1) --> (A,B))
by A5, TARSKI:def 2;
Coim (
Wf,
A)
= Coim (
f,
0)
by A39, Th7, A15, A18;
then
card (Coim (Wf,A)) = n
by A33, Def1;
hence
Wf in Election (
A,
n,
B,
k)
by Def1;
BALLOT_1:def 2 for i being Nat st i > 0 holds
card ((Wf | i) " {A}) > card ((Wf | i) " {B})
let i be
Nat;
( i > 0 implies card ((Wf | i) " {A}) > card ((Wf | i) " {B}) )
assume A41:
i > 0
;
card ((Wf | i) " {A}) > card ((Wf | i) " {B})
A42:
Wf | i = ((0,1) --> (A,B)) * (f | i)
by RELAT_1:83;
then A43:
Coim (
(Wf | i),
A)
= Coim (
(f | i),
0)
by A39, Th7, A15, A18;
A44:
Coim (
(Wf | i),
B)
= Coim (
(f | i),1)
by A42, A40, Th7, A15, A19;
f is
0 ,
n,1,
k -dominated-election
by A33, Def3;
hence
card ((Wf | i) " {A}) > card ((Wf | i) " {B})
by A41, A43, A44;
verum
end;
then A45:
Wf in DominatedElection (
A,
n,
B,
k)
by Def3;
then A46:
Wf in dom C
by FUNCT_2:def 1, A33;
C . Wf =
((A,B) --> (0,1)) * Wf
by A45, A32
.=
(((0,1) --> (A,B)) ") * (((0,1) --> (A,B)) * f)
by A6, A7, A1, NECKLACE:10
.=
((((0,1) --> (A,B)) ") * ((0,1) --> (A,B))) * f
by RELAT_1:36
.=
(id {0,1}) * f
by A15, A5, FUNCT_1:39
.=
f
by RELAT_1:53, A36
;
hence
x in rng C
by A46, FUNCT_1:def 3;
verum
end;
then A47:
DominatedElection (0,n,1,k) = rng C
;
per cases
( DominatedElection (0,n,1,k) = {} or DominatedElection (0,n,1,k) <> {} )
;
suppose A48:
DominatedElection (
0,
n,1,
k)
= {}
;
card (DominatedElection (A,n,B,k)) = card (DominatedElection (0,n,1,k))
DominatedElection (
A,
n,
B,
k)
= {}
proof
assume
DominatedElection (
A,
n,
B,
k)
<> {}
;
contradiction
then consider x being
object such that A49:
x in DominatedElection (
A,
n,
B,
k)
by XBOOLE_0:def 1;
ex
y being
object st
(
y in DominatedElection (
0,
n,1,
k) &
S1[
x,
y] )
by A20, A49;
hence
contradiction
by A48;
verum
end; hence
card (DominatedElection (A,n,B,k)) = card (DominatedElection (0,n,1,k))
by A48;
verum end; suppose
DominatedElection (
0,
n,1,
k)
<> {}
;
card (DominatedElection (A,n,B,k)) = card (DominatedElection (0,n,1,k))then A50:
dom C = DominatedElection (
A,
n,
B,
k)
by FUNCT_2:def 1;
C is
one-to-one
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom C or not x2 in dom C or not C . x1 = C . x2 or x1 = x2 )
assume that A51:
x1 in dom C
and A52:
x2 in dom C
and A53:
C . x1 = C . x2
;
x1 = x2
A54:
x1 in Election (
A,
n,
B,
k)
by A50, A51;
x2 in Election (
A,
n,
B,
k)
by A50, A52;
then reconsider x1 =
x1,
x2 =
x2 as
Element of
(n + k) -tuples_on {A,B} by A54;
A55:
len x1 = n + k
by CARD_1:def 7;
A56:
len x2 = n + k
by CARD_1:def 7;
A57:
dom x1 = Seg (n + k)
by A55, FINSEQ_1:def 3;
A58:
dom x2 = Seg (n + k)
by A56, FINSEQ_1:def 3;
A59:
rng x1 c= dom ((A,B) --> (0,1))
by A2;
A60:
rng x2 c= dom ((A,B) --> (0,1))
by A2;
A61:
(
A,
B)
--> (
0,1) is
one-to-one
by A12, FUNCT_4:def 4;
A62:
C . x1 = ((A,B) --> (0,1)) * x1
by A51, A32;
C . x2 = ((A,B) --> (0,1)) * x2
by A52, A32;
hence
x1 = x2
by A62, A57, A58, A59, A60, A61, A53, FUNCT_1:27;
verum
end; hence
card (DominatedElection (A,n,B,k)) = card (DominatedElection (0,n,1,k))
by WELLORD2:def 4, A47, A50, CARD_1:5;
verum end;