:: The Friendship Theorem
:: by Karol P\kak
::
:: Received May 15, 2012
:: Copyright (c) 2012-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RELAT_1, TARSKI, XBOOLE_0, ZFMISC_1, RELAT_2, FUNCT_1, SUBSET_1,
FINSET_1, NUMBERS, NAT_1, INT_1, ARYTM_3, CARD_1, XXREAL_0, ARYTM_1,
INT_2, CARD_2, FINSEQ_1, ORDINAL4, FINSEQ_2, XCMPLX_0, NEWTON, RFINSEQ,
FRIENDS1;
notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, RELAT_2, ENUMSET1, FUNCT_1,
ORDINAL1, SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, CARD_1, CARD_2, NUMBERS,
XCMPLX_0, XXREAL_0, INT_1, INT_2, FINSEQ_1, FINSEQ_2, NEWTON, RFINSEQ,
NAT_D;
constructors RELAT_2, DOMAIN_1, RELSET_1, NAT_1, REAL_1, CARD_2, WELLORD2,
FINSEQ_2, NEWTON, RFINSEQ, NAT_D;
registrations RELAT_1, FINSEQ_2, XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1,
FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, FINSEQ_1, NEWTON;
requirements SUBSET, BOOLE, NUMERALS, REAL, ARITHM;
definitions XBOOLE_0, TARSKI, RELAT_1, FUNCT_1;
equalities CARD_2, RELAT_1, FINSEQ_1, ORDINAL1;
expansions XBOOLE_0;
theorems TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, RELAT_2, INT_2, INT_1, SIMPLEX1,
CARD_2, CARD_1, FINSET_1, XBOOLE_1, FUNCT_1, FUNCT_2, WELLORD2, FINSEQ_6,
NAT_D, INT_4, NAT_3, INT_5, NAT_1, XREAL_1, XXREAL_0, NEWTON, FINSEQ_5,
FINSEQ_3, RFINSEQ, FINSEQ_1, FINSEQ_2, SUBSET_1, XTUPLE_0;
schemes CLASSES1, RELAT_1, NAT_1, FUNCT_2;
begin :: Preliminaries
reserve x,y,z for object, X for set,
i,k,n,m for Nat,
R for Relation,
P for finite Relation,
p,q for FinSequence;
registration
let P; let x be object;
cluster Im(P,x) -> finite;
coherence
proof
Im(P,x) c= rng P
proof
let y be object;
assume y in Im(P,x);
then [x,y] in P by RELAT_1:169;
hence thesis by XTUPLE_0:def 13;
end;
hence thesis;
end;
end;
Lm1: n*k = n*`k & n+k=n+`k
proof
A1: k = card k;
n=card n;
then n*`k = card (n*k) & n+`k = card (n+k)
by A1,CARD_2:39,CARD_2:38;
hence thesis;
end;
theorem Th1:
card R = card (R~)
proof
defpred Q[object,object] means for x,y st [x,y]=$1 holds [y,x]=$2;
A1:for x being object st x in R ex y being object st Q[x,y]
proof
let x be object;
assume x in R;
then consider y,z being object such that
A2:[y,z]=x by RELAT_1:def 1;
take zy=[z,y];
let w,t be object;
assume A3: [w,t]=x;
then w=y by A2,XTUPLE_0:1;
hence thesis by A3,A2,XTUPLE_0:1;
end;
consider h be Function such that
A4:dom h=R &
for x being object st x in R holds Q[x,h.x] from CLASSES1:sch 1(A1 );
A5: h is one-to-one
proof
let x1,x2 be object;
assume that A6: x1 in dom h
and A7: x2 in dom h
and A8: h.x1=h.x2;
consider y2,z2 be object such that
A9:x2=[y2,z2] by A4,A7,RELAT_1:def 1;
A10: h.x2 = [z2,y2] by A7,A9,A4;
consider y1,z1 be object such that
A11:x1=[y1,z1] by A6,A4,RELAT_1:def 1;
A12: h.x1 = [z1,y1] by A11,A6,A4;
then z1=z2 by A10,A8,XTUPLE_0:1;
hence thesis by A12,A10,A8,XTUPLE_0:1,A11,A9;
end;
A13:rng h c= R~
proof
let y be object;
assume y in rng h;
then consider x being object such that
A14: x in dom h
and A15: h.x=y by FUNCT_1:def 3;
consider t,r be object such that
A16:x=[t,r] by A4,A14,RELAT_1:def 1;
h.x =[r,t] by A14,A16,A4;
hence thesis by A14,A16,A4,RELAT_1:def 7,A15;
end;
R~ c= rng h
proof
let y,z be object;
assume [y,z] in R~;
then A17: [z,y] in R by RELAT_1:def 7;
then h.[z,y] = [y,z] by A4;
hence thesis by A17,A4,FUNCT_1:def 3;
end;
then rng h = R~ by A13;
hence thesis by A5,WELLORD2:def 4,A4,CARD_1:5;
end;
Lm2:R is irreflexive implies not [x,x] in R
proof
assume A1: R is irreflexive;
assume A2:[x,x] in R;
then x in field R by RELAT_1:15;
hence contradiction by A1,RELAT_2:def 10,A2,RELAT_2:def 2;
end;
Lm3:R is symmetric & [x,y] in R implies [y,x] in R
proof
assume A1: R is symmetric;
assume A2:[x,y] in R;
then x in field R & y in field R by RELAT_1:15;
hence thesis by A1,RELAT_2:def 11,RELAT_2:def 3,A2;
end;
theorem Th2:
R is symmetric implies R.:X = R"X
proof
assume A1:R is symmetric;
hereby
let y be object;
assume y in R.:X;
then consider z being object such that
A2: [z,y] in R
and A3: z in X by RELAT_1:def 13;
[y,z] in R by A2,A1,Lm3;
hence y in R"X by A3,RELAT_1:def 14;
end;
let y be object;
assume y in R"X;
then consider z being object such that
A4: [y,z] in R
and A5: z in X by RELAT_1:def 14;
[z,y] in R by A4,A1,Lm3;
hence y in R.:X by A5,RELAT_1:def 13;
end;
Lm4: not k in dom p implies (p /^k)^(p|k) = p
proof
assume not k in dom p; then
per cases by FINSEQ_3:25;
suppose k <1;
then k=0 by NAT_1:14;
then p|k={} & p/^ k = p by FINSEQ_5:28;
hence thesis by FINSEQ_1:34;
end;
suppose k > len p;
then p/^k = {} & p|k=p by RFINSEQ:def 1,FINSEQ_1:58;
hence thesis by FINSEQ_1:34;
end;
end;
theorem Th3:
(p /^k)^(p|k) = (q /^n)^(q|n) & k <= n & n <= len p
implies p = (q /^(n-'k)) ^ (q| (n-'k))
proof
assume A1: (p /^k)^(p|k) = (q /^n)^(q|n);
set nk=n-'k;
set L=len p;
set R=rng p\/rng q \/{1};
R = rng p\/(rng q \/{1}) & R=rng q\/(rng p \/{1}) by XBOOLE_1:4;
then reconsider P=p,Q=q as FinSequence of R
by XBOOLE_1:7,FINSEQ_1:def 4;
set p1k = P/^k,pk=P|k,q1n = Q/^n,qn=Q|n;
assume A2:k <= n;
then A3:n-k=n-'k by XREAL_1:233;
then A4:nk+k=n;
A5:nk <= nk+k by NAT_1:11;
then A6: n-'nk=n-nk by XREAL_1:233,A3;
qn ^ q1n = q by RFINSEQ:8;
then A7: len q1n+len qn = len q by FINSEQ_1:22;
A8:qn = (qn|nk)^(qn /^ nk) by RFINSEQ:8;
assume A9:n <=L;
then reconsider Lk=L-k,Ln=L-n as Nat by A2,XXREAL_0:2,NAT_1:21;
A10: len (p1k^pk) = len p1k+len pk by FINSEQ_1:22;
A11: pk^p1k = p by RFINSEQ:8;
then len p1k+len pk = L by FINSEQ_1:22;
then L=len q by A7,A10, FINSEQ_1:22,A1;
then A12: len q1n = Ln by A9,RFINSEQ:def 1;
A13:p1k = (p1k|Ln)^(p1k /^ Ln) by RFINSEQ:8;
then A14:q1n^qn = (p1k|Ln)^((p1k /^ Ln)^pk) by A1,FINSEQ_1:32;
k <= L by A9,A2,XXREAL_0:2;
then A15: len p1k = Lk by RFINSEQ:def 1;
then len (p1k|Ln)= Ln by A2,XREAL_1:10,FINSEQ_1:59;
then A16:p1k|Ln = (q1n^qn) |Ln by A14,FINSEQ_5:23
.= q1n by A12,FINSEQ_5:23;
Lk>= Ln by A2,XREAL_1:10;
then A17:len (p1k /^ Ln) = Lk-Ln by A15,RFINSEQ:def 1;
A18:qn|nk = ((p1k /^ Ln)^pk) |nk by A16,A14,FINSEQ_1:33
.= (p1k /^ Ln) by A17,FINSEQ_5:23,A3;
qn = (p1k /^ Ln)^pk by A16,A14,FINSEQ_1:33;
then (qn /^ nk) = pk by A18,A8,FINSEQ_1:33;
hence p = ((Q/^nk) |k) ^ (q1n ^ qn|nk)
by A6,FINSEQ_5:80,A3,A13,A16,A18,A11
.= ((Q/^nk) |k) ^ ((Q/^nk/^k) ^ qn|nk) by FINSEQ_6:81,A4
.= ((Q/^nk) |k ^ (Q/^nk/^k)) ^ (qn|nk) by FINSEQ_1:32
.= Q/^nk ^ (qn|nk) by RFINSEQ:8
.= q/^nk ^ q|nk by A5,FINSEQ_1:82,A3;
end;
theorem Th4:
n in dom q & p = (q /^n)^(q|n) implies
q = (p/^(len p-'n))^p| (len p-'n)
proof
assume that A1: n in dom q
and A2: p = (q /^n)^(q|n);
set L=len p;
set R=rng p\/rng q \/{1};
set Ln=L-'n;
R = rng p\/(rng q \/{1}) & R=rng q\/(rng p \/{1}) by XBOOLE_1:4;
then reconsider P=p,Q=q as FinSequence of R
by XBOOLE_1:7,FINSEQ_1:def 4;
set q1n = Q/^n,qn=Q|n,pL=P|Ln,p1L=P/^Ln;
A3: qn ^ q1n = q by RFINSEQ:8;
then len q1n+len qn = len q by FINSEQ_1:22;
then A4:L=len q by FINSEQ_1:22,A2;
then A5:n <= L by FINSEQ_3:25,A1; then
L-n=L-'n by XREAL_1:233;
then A7: len q1n = Ln by A4,A5,RFINSEQ:def 1;
A8: p = pL^p1L by RFINSEQ:8;
pL = (q /^n) by A2,A7,FINSEQ_5:23;
hence thesis by A2,A8,FINSEQ_1:33,A3;
end;
theorem Th5:
(p /^k)^(p|k) = (q /^n)^(q|n) implies
ex i st p = (q /^i) ^ (q|i)
proof
assume A1: (p /^k)^(p|k) = (q /^n)^(q|n);
set L=len p;
set R=rng p\/rng q \/{1};
R = rng p\/(rng q \/{1}) & R=rng q\/(rng p \/{1}) by XBOOLE_1:4;
then reconsider P=p,Q=q as FinSequence of R
by XBOOLE_1:7,FINSEQ_1:def 4;
set p1k = P/^k,pk=P|k,q1n = Q/^n,qn=Q|n;
pk^p1k = p by RFINSEQ:8;
then A2: len p1k+len pk = L by FINSEQ_1:22;
qn ^ q1n = q by RFINSEQ:8;
then A3: len q1n+len qn = len q by FINSEQ_1:22;
len (p1k^pk) = len p1k+len pk by FINSEQ_1:22;
then A4:L=len q by A2,A3, FINSEQ_1:22,A1;
per cases;
suppose not k in dom p;
then p = (q /^n)^(q|n) by A1,Lm4;
hence thesis;
end;
suppose A5:not n in dom q & k in dom p;
then q = (p /^k)^(p|k) by Lm4,A1;
then p = (q/^(len q-'k))^(q| (len q-'k)) by A5,Th4;
hence thesis;
end;
suppose A6:n in dom q & k in dom p & k <= n;
then n <= len p by A4,FINSEQ_3:25;
then p = (q /^(n-'k))^(q| (n-'k)) by A6,A1,Th3;
hence thesis;
end;
suppose A7:n in dom q & k in dom p & k > n;
then A8: k-'n = k-n by XREAL_1:233;
then k-'n <> 0 by A7;
then A9: k-'n >=1 by NAT_1:14;
A10: k <= len p by A7,FINSEQ_3:25;
k-'n <= k-'n+n by NAT_1:11;
then k-'n <= len p by A8,XXREAL_0:2,A10;
then A11: k-'n in dom p by A9,FINSEQ_3:25;
q = (p /^(k-'n))^(p| (k-'n)) by A10,A4,A7,A1,Th3;
then p = (q/^(len q-'(k-'n)))^q| (len q-'(k-'n)) by A11,Th4;
hence thesis;
end;
end;
scheme Sch{X()->non empty set,n() -> non zero Nat, P[set]}:
ex C be Cardinal st n()*`C =
card {F where F is Element of n()-tuples_on X():P[F]}
provided
A1: for p,q be FinSequence of X() st p^q is n() -element & P[p^q]
holds P[q^p]
and
A2: for p be Element of n()-tuples_on X() st P[p]
for i be Nat st i < n() & p = (p/^i)^(p|i) holds i = 0
proof
set T=n()-tuples_on X();
set XX={F where F is Element of T:P[F]};
per cases;
suppose A3:XX is empty;
0=n()*`0 by CARD_2:20;
hence thesis by A3;
end;
suppose XX is non empty;
deffunc F(object) ={p^q where p,q is Element of X()*:q^p=$1};
A4:for x being object st x in XX holds F(x) in bool XX
proof
let x be object;
assume x in XX;
then consider pq be Element of T such that
A5: x=pq
and A6: P[pq];
F(x) c= XX
proof
let y be object;
A7: len pq = n() by CARD_1:def 7;
assume y in F(x);
then consider p1,q1 be Element of X()* such that
A8: y=p1^q1
and A9: q1^p1=pq by A5;
len pq = len q1+len p1 by A9,FINSEQ_1:22;
then len (p1^q1) = n() by A7,FINSEQ_1:22;
then A10: p1^q1 is Element of T by FINSEQ_2:92;
P[p1^q1] by A6,A9,A1;
hence thesis by A10,A8;
end;
hence thesis;
end;
consider F be Function of XX,bool XX such that
A11:for x being object st x in XX holds F.x=F(x) from FUNCT_2:sch 2(A4);
set FF=F~;
A12:dom F = XX by FUNCT_2:def 1;
A13: n() in Seg n() by FINSEQ_1:3;
for x being object st x in rng F holds card Im(FF,x)=n()
proof
let x be object;
assume x in rng F;
then consider y being object such that
A14: y in dom F
and A15: F.y=x by FUNCT_1:def 3;
consider p be Element of T such that
A16: y=p
and A17: P[p] by A14,A12;
A18:x=F(p) by A14,A15,A16,A11;
defpred Q[object,object] means
for i be Nat st i=$1 holds $2=(p/^i)^(p|i);
A19:len p = n() by CARD_1:def 7;
then p/^ n() = {} & p|n()=p by RFINSEQ:27,FINSEQ_1:58;
then A20:p = (p/^ n())^(p|n()) by FINSEQ_1:34;
A21:for i be object st i in Seg n()
ex q be object st q in Im(FF,x) & Q[i,q]
proof
let i be object;
assume i in Seg n();
then reconsider I= i as Nat;
set q=p/^I;
take qp= q^(p|I);
A22: p=(p|I)^q by RFINSEQ:8;
then len p = len (p|I)+ len q by FINSEQ_1:22;
then A23:len qp = n() by FINSEQ_1:22,A19;
then A24: qp is Element of T by FINSEQ_2:92;
A25:F(p) c= F(qp)
proof
let t be object;
assume t in F(p);
then consider t1,t2 be Element of X()* such that
A26: t=t1^t2
and A27: p = t2^t1;
reconsider t12=t as Element of X()* by A26,FINSEQ_1:def 11;
set LT=len t1;
A28: t12 = (t12|LT)^(t12/^LT) by RFINSEQ:8;
t12|LT = t1 by A26,FINSEQ_5:23;
then (t12/^LT)^(t12|LT) = (p/^ n())^(p|n())
by A27,A28,A26,FINSEQ_1:33,A20;
then A29:ex k2 be Nat st (t12 /^k2)^(t12|k2) = p by Th5;
qp/^ n() = {} & qp|n()=qp by A23,RFINSEQ:27,FINSEQ_1:58;
then (p/^I)^(p|I) = (qp/^ n())^(qp|n()) by FINSEQ_1:34;
then ex k1 be Nat st (qp /^k1)^(qp|k1) = p by Th5;
then consider k3 be Nat such that
A30: (t12 /^k3)^(t12|k3) = qp by A29,Th5;
(t12 /^k3) in X()* & (t12|k3) in X()* by FINSEQ_1:def 11;
then (t12|k3)^(t12 /^k3) in F(qp) by A30;
hence thesis by RFINSEQ:8;
end;
P[qp] by A1,A17,A22;
then A31:qp in dom F by A24,A12;
then F.qp=F(qp) by A11;
then [qp,F(qp)] in F by FUNCT_1:def 2,A31;
then A32:[F(qp),qp] in FF by RELAT_1:def 7;
F(qp)c=F(p)
proof
let t be object;
assume t in F(qp);
then consider t1,t2 be Element of X()* such that
A33: t=t1^t2
and A34: q^(p|I) = t2^t1;
reconsider t12=t as Element of X()* by A33,FINSEQ_1:def 11;
set LT=len t1;
A35: t12 = (t12|LT)^(t12/^LT) by RFINSEQ:8;
t12|LT = t1 by A33,FINSEQ_5:23;
then (t12/^LT)^(t12|LT) = (p/^I)^(p|I)
by A34,A35,A33,FINSEQ_1:33;
then consider k be Nat such that
A36: (t12 /^k)^(t12|k) = p by Th5;
(t12 /^k) in X()* & (t12|k) in X()* by FINSEQ_1:def 11;
then (t12|k)^(t12 /^k) in F(p) by A36;
hence thesis by RFINSEQ:8;
end;
then F(qp)=F(p) by A25;
hence thesis by A32,RELAT_1:169,A18;
end;
consider PR be Function of Seg n(),Im(FF,x) such that
A37:for i be object st i in Seg n() holds Q[i,PR.i]
from FUNCT_2:sch 1(A21);
[y,x] in F by A14,A15,FUNCT_1:def 2;
then [x,y] in FF by RELAT_1:def 7;
then y in Im(FF,x) by RELAT_1:169;
then A38:dom PR = Seg n() by FUNCT_2:def 1;
Im(FF,x) c= rng PR
proof
let z be object;
assume z in Im(FF,x);
then [x,z] in FF by RELAT_1:169;
then A39:[z,x] in F by RELAT_1:def 7;
then A40:z in dom F by XTUPLE_0:def 12;
then A41: F.z = F(z) by A11;
consider Z be Element of T such that
A42: z=Z
and P[Z] by A40,A12;
A43: Z in X()* & <*>X() in X()* by FINSEQ_1:def 11;
A44: Z=Z^<*>X() & <*>X()^Z=Z by FINSEQ_1:34;
x is set by TARSKI:1;
then F.z=x by A40,A39,FUNCT_1:def 2;
then z in F(p) by A44,A43,A41,A42,A18;
then consider z1,z2 be Element of X()* such that
A45: z=z1^z2
and A46: z2^z1 = p;
set L=len z2;
A47: p|L = z2 by A46,FINSEQ_5:23;
L+len z1 = len p by A46,FINSEQ_1:22;
then A48:L <= len p by NAT_1:11;
A49: p = (p|L)^(p/^L) by RFINSEQ:8;
then A50:z1 = p/^L by A47,A46,FINSEQ_1:33;
per cases by NAT_1:14;
suppose L=0;
then A51:p|L={};
then p/^L = p by A49,FINSEQ_1:34;
then z = p by A45,A51,A47,A50,FINSEQ_1:34;
then z = PR.n() by A13,A37, A20;
hence thesis by A13,A38,FUNCT_1:def 3;
end;
suppose L>=1;
then A52:L in Seg n() by A19,A48;
then PR.L = z by A47,A50,A45,A37;
hence thesis by A52,A38, FUNCT_1:def 3;
end;
end;
then A53:rng PR = Im(FF,x);
PR is one-to-one
proof
let i1,i2 be object;
assume that
A54: i1 in dom PR
and A55: i2 in dom PR
and A56: PR.i1=PR.i2;
reconsider i1,i2 as Nat by A54,A55,A38;
A57: 1<= i1 by A54,FINSEQ_1:1;
A58: 1<= i2 by A55,FINSEQ_1:1;
A59: i2 <= n() by A55,FINSEQ_1:1;
A60: PR.i2= (p/^i2)^(p|i2) & PR.i1=(p/^i1)^(p|i1) by A55,A37,A54;
then
reconsider P1=PR.i1, P2 = PR.i2 as Element of X()*
by FINSEQ_1:def 11;
A61: i1 <= n() by A54,FINSEQ_1:1;
A62:n()-1 < n()-0 by XREAL_1:15;
per cases;
suppose i1 <= i2;
then A63: p = (p /^(i2-'i1))^(p| (i2-'i1))
& i2-'i1=i2-i1 by Th3,A19,A59,A60,A56,XREAL_1:233;
i2-i1 <= n()-1 by A57,A59, XREAL_1:13;
then i2-i1 < n() by XXREAL_0:2,A62;
then i2-i1 = 0 by A17,A2,A63;
hence thesis;
end;
suppose i2 <= i1;
then A64: p = (p /^(i1-'i2))^(p| (i1-'i2)) &
i1-'i2=i1-i2 by Th3,A19,A61,A60,A56,XREAL_1:233;
i1-i2 <= n()-1 by A61,A58, XREAL_1:13;
then i1-i2 < n() by XXREAL_0:2,A62;
then i1-i2 = 0 by A17,A2,A64;
hence thesis;
end;
end;
hence card Im(FF,x) = card Seg n()
by A53,A38,WELLORD2:def 4,CARD_1:5
.=n() by FINSEQ_1:57;
end;
then A65:card FF = card (FF| (dom FF\rng F)) +` n()*` card rng F
by SIMPLEX1:1;
dom FF = rng F by RELAT_1:20;
then dom FF\rng F={} by XBOOLE_1:37;
then card (FF| (dom FF\rng F))=0;
then n()*` card rng F=card FF by A65,CARD_2:18
.= card F by Th1
.= card XX by A12,CARD_1:62;
hence thesis;
end;
end;
theorem Th6:
for X be non empty set, A be non empty finite Subset of X
for P be Function of X,bool X st
for x st x in X holds card (P.x)=n holds
card {F where F is Element of (k+1)-tuples_on X:
F.1 in A & for i st i in Seg k holds F.(i+1) in P.(F.i)}
=
card A * (n |^ k)
proof
let X be non empty set;
let A be non empty finite Subset of X;
let P be Function of X,bool X such that
A1:for x st x in X holds card (P.x)=n;
defpred D[Function,Nat] means $1.1 in A & for i st i in Seg $2 holds
$1.(i+1) in P.($1.i);
defpred R[Nat] means card {F where F is Element of ($1+1)-tuples_on X:
D[F,$1]} = card A * (n |^ $1);
A2: dom P = X by FUNCT_2:def 1;
A3: for k st R[k] holds R[k+1]
proof
let k;
set k1=k+1,k2=k1+1;
set F2={F where F is Element of k2-tuples_on X: D[F,k1]};
set F1={F where F is Element of k1-tuples_on X: D[F,k]};
defpred P[object,object] means
for f be FinSequence st $2=f holds f|k1 =$1;
assume A4:R[k];
then reconsider F1 as finite set;
consider PP be Relation such that
A5: for x,y being object
holds [x,y] in PP iff x in F1 & y in F2 & P[x,y]
from RELAT_1:sch 1;
for x st x in F1 holds card Im(PP,x) = n
proof
defpred FF[object,object] means
for f be FinSequence st f=$1 holds f.k2=$2;
let x;
assume x in F1;
then consider xx be Element of k1-tuples_on X such that
A6: x=xx
and A7: D[xx,k];
A8:for y being object st y in Im(PP,x)
ex z being object st z in P.(xx.k1) & FF[y,z]
proof
let y being object such that
A9:y in Im(PP,x);
A10: [x,y] in PP by RELAT_1:169,A9;
then y in F2 by A5;
then consider yy be Element of (k1+1)-tuples_on X such that
A11: y=yy
and A12: D[yy,k1];
take z=yy.(k1+1);
A13: yy.(k1+1) in P.(yy.k1) by FINSEQ_1:3,A12;
yy|k1=xx by A11, A10,A5,A6;
hence thesis by FINSEQ_1:3,FUNCT_1:49,A13,A11;
end;
consider ff be Function of Im(PP,x),P.(xx.k1) such that
A14:for z being object st z in Im(PP,x) holds FF[z,ff.z]
from FUNCT_2:sch 1(A8);
A15:len xx = k1 by CARD_1:def 7;
k1 in Seg k1 by FINSEQ_1:3;
then k1 in dom xx by A15,FINSEQ_1:def 3;
then A16: xx.k1 in rng xx by FUNCT_1:def 3;
then A17: card (P.(xx.k1)) = n by A1;
A18: P.(xx.k1) in rng P by A16,A2,FUNCT_1:def 3;
P.(xx.k1) c= rng ff
proof
let z be object such that
A19: z in P.(xx.k1);
reconsider Z=z as Element of X by A18,A19;
set xz= xx^<*Z*>;
A20: len xz=len xx+1 by FINSEQ_2:16;
A21:xz|k1=xx by FINSEQ_5:23,A15;
A22: ( P[xx,xz])& xx in F1 by FINSEQ_5:23,A15, A7;
reconsider xz as Element of (k1+1)-tuples_on X by A20,A15,FINSEQ_2:92;
A23: for i st i in Seg k1 holds xz.(i+1) in P.(xz.i)
proof
let i;
assume A24: i in Seg k1;
then A25: 1 <= i by FINSEQ_1:1;
A26: i <=k1 by A24,FINSEQ_1:1;
per cases by A26,NAT_1:8;
suppose A27: i <=k;
1<=1+i by NAT_1: 11;
then i+1 in dom xx by A27,XREAL_1:6,A15, FINSEQ_3:25;
then A28: xz.(i+1)=xx.(i+1) by FINSEQ_1:def 7;
i<k1 by A27,NAT_1: 13;
then A29: i in dom xx by A25,A15, FINSEQ_3:25;
xx.(i+1) in P.(xx.i) by A27,A25,FINSEQ_1:1,A7;
hence thesis by A28, A29,FINSEQ_1:def 7;
end;
suppose A30:i = k1;
then xz.i=xx.i by A21, FINSEQ_1:3,FUNCT_1:49;
hence thesis by A30,FINSEQ_1:42, A15,A19;
end;
end;
1 <= k1 by NAT_1:11;
then 1 in dom xx by FINSEQ_3:25,A15;
then xz.1=xx.1 by FINSEQ_1:def 7;
then xz in F2 by A23, A7;
then A31: [xx,xz] in PP by A5,A22;
then A32:xz in Im(PP,xx) by RELAT_1:169;
ex d be object st d in P.(xx.k1) & FF[xz,d]
by A31,RELAT_1:169,A6,A8;
then A33: dom ff = Im(PP,xx) by FUNCT_2:def 1,A6;
ff.xz = xz.(k1+1) by A31,RELAT_1:169,A14,A6
.= z by FINSEQ_1:42,A15;
hence thesis by A33,A32,FUNCT_1:def 3;
end;
then A34:P.(xx.k1) = rng ff;
per cases;
suppose A35:P.(xx.k1) is empty;
Im(PP,x) is empty
proof
assume Im(PP,x) is non empty;
then consider d be object such that
A36:d in Im(PP,x);
ex z being object st z in P.(xx.k1) & FF[d,z] by A36,A8;
hence contradiction by A35;
end;
hence thesis by A35, A16,A1;
end;
suppose A37: P.(xx.k1) is non empty;
A38: ff is one-to-one
proof
let x1,x2 be object;
assume that
A39: x1 in dom ff
and A40: x2 in dom ff
and A41: ff.x1=ff.x2;
A42: [xx,x1] in PP by A39,RELAT_1:169,A6;
then x1 in F2 by A5;
then consider f1 be Element of (k1+1)-tuples_on X such that
A43: x1=f1
and D[f1,k1];
A44: len f1 = k1+1 by CARD_1 :def 7;
f1|k1 = xx by A42,A43,A5;
then A45: f1 = xx^<*f1.k2*> by A44, FINSEQ_3:55;
A46: [xx,x2] in PP by A40,RELAT_1:169,A6;
then x2 in F2 by A5;
then consider f2 be Element of (k1+1)-tuples_on X such that
A47: x2=f2
and D[f2,k1];
A48: len f2=k1+1 by CARD_1: def 7;
f2|k1 = xx by A46,A47,A5;
then A49: f2 = xx^<*f2.k2*> by A48, FINSEQ_3:55;
f1.k2 =ff.x1 by A39,A14,A43;
hence thesis by A45,A49, A40,A14,A47,A41, A43;
end;
dom ff = Im(PP,x) by A37,FUNCT_2:def 1;
hence thesis by A38,A34,WELLORD2:def 4,CARD_1:5,A17;
end;
end;
then A50:card PP = card (PP| (dom PP\F1)) +`n*`card F1 by SIMPLEX1:1;
dom PP c= F1
proof
let y be object;
assume y in dom PP;
then ex z being object st [y,z] in PP by XTUPLE_0:def 12;
hence thesis by A5;
end;
then dom PP\F1={} by XBOOLE_1:37;
then card (PP| (dom PP\F1))=0;
then card PP = n*`card F1 by A50,CARD_2:18;
then A51:card PP = n * card F1 by Lm1
.= (card A)*(n*(n|^k)) by A4
.= (card A)*(n|^k1) by NEWTON:6;
A52:for f2 be Element of k2-tuples_on X st D[f2,k1] holds
[f2|k1,f2] in PP
proof
let f2 be Element of k2-tuples_on X such that
A53: D[f2,k1];
A54:f2 in F2 by A53;
set f1=f2|k1;
A55:P[f1,f2];
len f2 = k2 & k1 < k2 by CARD_1:def 7, NAT_1:13;
then len f1 = k1 by FINSEQ_1:59;
then reconsider f1 as Element of k1-tuples_on X by FINSEQ_2:92;
A56: for i st i in Seg k holds f1.(i+1) in P.(f1.i)
proof
let i;
set i1=i+1;
assume A57: i in Seg k;
then A58: 1<= i by FINSEQ_1:1;
A59: i <= k by A57,FINSEQ_1:1;
then i <k1 by NAT_1:13;
then A60: f2.i1 in P.(f2.i) & f2.i=f1.i
by A58,FINSEQ_1:1,A53,FUNCT_1 :49;
1<=i1 by NAT_1:11;
then i1 in Seg k1 by A59,XREAL_1:6,FINSEQ_1:1;
hence thesis by A60,FUNCT_1:49;
end;
1<= k1 by NAT_1:11;
then 1 in Seg k1;
then D[f1,k] by A56,FUNCT_1:49, A53;
then f1 in F1;
hence thesis by A54,A55,A5;
end;
per cases;
suppose n=0;
then A61:n|^k1=0 by NAT_1:11,NEWTON:11;
then A62:PP is empty by A51;
F2 is empty
proof
assume F2 is non empty;
then consider x2 be object such that
A63:x2 in F2;
ex f2 be Element of k2-tuples_on X st x2=f2 & D[f2,k1] by A63;
hence contradiction by A52,A62;
end;
hence thesis by A61;
end;
suppose A64:n>0;
defpred PR[object,object] means for x,y st $1=[x,y] holds $2=y;
A65:for y being object st y in PP ex z being object st z in F2 & PR[y,z]
proof
let y be object;
assume A66:y in PP;
then consider y1,y2 be object such that
A67: y=[y1,y2] by RELAT_1:def 1;
take y2;
thus thesis by XTUPLE_0:1,A66,A67,A5;
end;
consider pr be Function of PP,F2 such that
A68:for y being object st y in PP holds PR[y,pr.y] from FUNCT_2:sch 1(A65);
A69:pr is one-to-one
proof
let x1,x2 be object;
assume that
A70: x1 in dom pr
and A71: x2 in dom pr
and A72: pr.x1=pr.x2;
consider y1,z1 be object such that
A73:x1=[y1,z1] by A70,RELAT_1:def 1;
A74: pr.x1=z1 by A68,A70,A73;
consider y2,z2 be object such that
A75:x2=[y2,z2] by A71,RELAT_1:def 1;
A76: pr.x2 =z2 by A68,A71,A75;
z1 in F2 by A73,A70,A5;
then consider f1 be Element of k2-tuples_on X such that
A77: z1=f1
and D[f1,k1];
f1|k1 = y1 by A73,A70,A5,A77;
hence thesis by A71,A5,A75,A72,A73, A74,A76,A77;
end;
F2 is non empty
proof
n|^k1>0 by NEWTON:83,A64;
then PP is non empty by A51, XREAL_1:129;
then consider x being object such that
A78:x in PP;
ex y,z being object st x=[y,z] by RELAT_1:def 1,A78;
hence thesis by A78,A5;
end;
then A79:dom pr = PP by FUNCT_2:def 1;
F2 c= rng pr
proof
let x2 be object;
assume x2 in F2;
then consider f2 be Element of k2-tuples_on X such that
A80: x2=f2
and A81: D[f2,k1];
[f2|k1,f2] in PP & pr.[f2|k1,f2] = f2 by A81,A52,A68;
hence thesis by A79,FUNCT_1:def 3,A80;
end;
then F2 = rng pr;
hence thesis by A69,A79,WELLORD2:def 4,A51,CARD_1:5;
end;
end;
A82: R[0]
proof
deffunc P(object) = <*$1*>;
set F0={F where F is Element of (0+1)-tuples_on X: D[F,0]};
A83:for x being object st x in A holds P(x) in F0
proof
let x be object;
assume A84:x in A;
A85: len P(x) = 1 by FINSEQ_1:39;
rng P(x) ={x} by FINSEQ_1:38;
then P(x) is FinSequence of X by A84,ZFMISC_1:31,FINSEQ_1:def 4;
then reconsider Px=P(x) as Element of (0+1)-tuples_on X
by A85,FINSEQ_2:133;
D[Px,0] by A84;
hence thesis;
end;
consider f be Function of A,F0 such that
A86: for x being object st x in A holds f.x = P(x) from FUNCT_2:sch 2(A83);
P(the Element of A) in F0 by A83;
then A87:dom f = A by FUNCT_2:def 1;
F0 c= rng f
proof
let x be object;
assume x in F0;
then A88:ex F be Element of (0+1)-tuples_on X st x=F & D[F,0];
then consider y be Element of X such that
A89: x=<*y*> by FINSEQ_2:97;
f.y = x by A88,A89,A86;
hence thesis by A88,A89,A87,FUNCT_1:def 3;
end;
then A91: rng f = F0;
A92:f is one-to-one
proof
let x1,x2 be object;
assume that
A93: x1 in dom f & x2 in dom f
and A94: f.x1=f.x2;
A95: f.x1=P(x1) & f.x2=P(x2) by A93,A86;
P(x1).1=x1;
hence thesis by A95,FINSEQ_1:40,A94;
end;
n|^0 =1 by NEWTON:4;
hence thesis by A91,WELLORD2:def 4,A87,A92,CARD_1:5;
end;
for k holds R[k] from NAT_1:sch 2(A82,A3);
hence thesis;
end;
theorem Th7:
len p is prime & (ex i st 0 < i & i < len p & p = (p/^i) ^ (p|i))
implies rng p c= {p.1}
proof
set L=len p;
assume A1:L is prime;
reconsider P=p as FinSequence of rng p \/{1} by XBOOLE_1:7,FINSEQ_1:def 4;
given j be Nat such that
A2: 0 < j
and A3: j < L
and A4: p = (p/^j)^(p|j);
defpred P[Nat] means p.1 = p.((j*$1 mod L)+1);
set p1j=p/^j,pj=p|j;
A5:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A6:P[k];
set k1=k+1,jk=(j*k mod L);
j*k1=j*k+j;
then A7:j*k1 mod L = jk+j mod L by NAT_D:23;
A8: len pj = j by A3,FINSEQ_1:59;
A9: len p1j = L-j by A3,RFINSEQ:def 1;
jk+1<=L by NAT_D:1, A3,NAT_1:13;
then A10:jk+1 in dom p by NAT_1:11,FINSEQ_3:25;
per cases by A4,A10,FINSEQ_1:25;
suppose A11:jk+1 in dom p1j;
then jk+1 <= L-j by A9,FINSEQ_3:25;
then jk+1+j <= L-j+j by XREAL_1:6;
then jk+j+1 <= L;
then jk+j < L by NAT_1:13;
then A12: jk+j mod L = jk+j by NAT_D:24;
p.(jk+1) = p1j.(jk+1) by A11,A4,FINSEQ_1:def 7
.= p.(jk+1+j) by A3,A11,RFINSEQ:def 1;
hence thesis by A12,A7,A6;
end;
suppose ex n be Nat st n in dom pj & jk+1=len p1j + n;
then consider n be Nat such that
A13: n in dom pj
and A14: jk+1=len p1j + n;
len pj >= n by A13,FINSEQ_3:25;
then A15: n < L by A8,A3,XXREAL_0:2;
reconsider n1=n-1 as Nat by A13,FINSEQ_3:25,NAT_1:21;
n1 < n1+1 by NAT_1 :13;
then A16:n1 < L by A15,XXREAL_0:2;
jk+j = 1*L+n1 by A14,A9;
then A17: jk+j mod L = n1 mod L by NAT_D:21
.= n1 by A16,NAT_D:24;
p.(jk+1) = pj.n by A4,A13,A14,FINSEQ_1:def 7
.= p.n by A13,FUNCT_1:47;
hence thesis by A17,A7,A6;
end;
end;
j*0 mod L = 0 by NAT_D:26;
then A18: P[0];
A19:for k be Nat holds P[k] from NAT_1:sch 2(A18,A5);
let y be object;
assume y in rng p;
then consider m be object such that
A20: m in dom p
and A21: p.m=y by FUNCT_1:def 3;
reconsider m as Nat by A20;
A22: m <= L by A20,FINSEQ_3:25;
reconsider m1=m-1 as Nat by A20,FINSEQ_3:25,NAT_1:21;
per cases;
suppose m=1;
hence thesis by A21,TARSKI:def 1;
end;
suppose m<>1;
j gcd L =1
proof
j gcd L divides L by INT_2:def 2;
then A23: j gcd L = 1 or j gcd L = L by A1,INT_2:def 4;
assume j gcd L <>1;
then L divides j by A23,INT_2:def 2;
hence contradiction by A2,NAT_D:7, A3;
end;
then consider n be Nat such that
A24: (j*n-m1) mod L=0 by INT_2:def 3, A3,INT_4:16;
A25:m1+1=m;
then m1 < L by A22,NAT_1:13;
then m1 mod L=m1 by NAT_D:24;
then j*n mod L = m1 by A3,INT_4:22,A24;
then p.1 = p.m by A25,A19;
hence thesis by TARSKI:def 1,A21;
end;
end;
begin :: The Friendship Graph
definition
let R;
let x be Element of field R;
attr x is universal_friend means :Def1:
for y st y in field R\{x} holds [x,y] in R;
end;
definition
let R be Relation;
attr R is with_universal_friend means
ex x be Element of field R st x is universal_friend;
end;
notation
let R be Relation;
antonym R is without_universal_friend for R is with_universal_friend;
end;
definition
let R be Relation;
attr R is friendship_graph_like means :Def3:
for x,y being object st x in field R & y in field R & x <> y
ex z being object st Im(R,x) /\ Coim(R,y) ={z};
end;
registration
cluster finite symmetric irreflexive friendship_graph_like for Relation;
existence
proof
set R=the empty Relation,F=field R;
for x,y being object
holds x in F & y in F & [x,y] in R implies [ y,x] in R;
then
A1:R is symmetric by RELAT_2:def 3,def 11;
for x being object holds x in F implies not [x,x] in R;
then A2:R is irreflexive by RELAT_2:def 2,def 10;
for x,y being object st x in F & y in F & x <> y
ex z being object st Im(R,x) /\ Coim(R,y) ={z};
hence thesis by A1,A2,Def3;
end;
end;
::$N Friendship graph
::$L https://en.wikipedia.org/wiki/Friendship_graph Friendship graph
definition
mode Friendship_Graph is finite symmetric irreflexive friendship_graph_like
Relation;
end;
reserve FSG for Friendship_Graph;
Lm5:for t be object holds P is friendship_graph_like & x<>y & [x,z] in P &
[z,y] in P & [x,t] in P & [t,y] in P implies z=t
proof
let t be object;
assume that A1: ( P is friendship_graph_like)& x<>y
and A2: [x,z] in P
and A3: [z,y] in P
and A4: [x,t] in P
and A5: [t,y] in P;
x in field P & y in field P by A2,RELAT_1:15, A3;
then consider d be object such that
A6:Im(P,x)/\Coim(P,y)={d} by A1;
A7: y in {y} by TARSKI:def 1;
then A8: t in Coim(P,y) by RELAT_1:def 14, A5;
A9: z in Coim(P,y) by A7,RELAT_1:def 14,A3;
z in Im(P,x) by A2,RELAT_1:169;
then z in {d} by A9,A6,XBOOLE_0:def 4;
then A10: z=d by TARSKI:def 1;
t in Im(P,x) by A4,RELAT_1:169;
then t in {d} by A8,A6,XBOOLE_0:def 4;
hence thesis by A10,TARSKI:def 1;
end;
theorem Th8:
2 divides card Im(FSG,x)
proof
set I=Im(FSG,x);
defpred Q[object,object] means
ex y st [$1,y] in FSG & y in I & $2={$1,y};
A1:for x being object st x in I ex y being object st Q[x,y]
proof
let y be object;
assume y in I;
then A2:[x,y] in FSG by RELAT_1:169;
then A3: x<>y & x in field FSG by Lm2,RELAT_1:15;
y in field FSG by A2,RELAT_1:15;
then consider z being object such that
A4: I/\Coim(FSG,y)={z} by A3,Def3;
take {y,z};
A5: z in {z} by TARSKI:def 1;
Coim(FSG,y) =Im(FSG,y) by Th2;
then z in Im(FSG,y) by A5,A4,XBOOLE_0:def 4;
then A6: [y,z] in FSG by RELAT_1:169;
z in I by A5,A4,XBOOLE_0:def 4;
hence thesis by A6;
end;
consider h be Function such that
A7:dom h=I & for x being object st x in I holds Q[x,h.x]
from CLASSES1:sch 1( A1 );
reconsider R=rng h as finite set by A7,FINSET_1:8;
set H=h~;
for x st x in R holds card Im(H,x)=2
proof
let y;
assume y in R;
then consider z be object such that
A8: z in dom h
and A9: h.z=y by FUNCT_1:def 3;
consider w be object such that
A10: [z,w] in FSG
and A11: w in I
and A12: y ={z,w} by A7,A8,A9;
consider t be object such that
A13: [w,t] in FSG
and A14: t in I
and A15: h.w={w,t} by A11,A7;
t=z
proof
A16:[x,w] in FSG by A11,RELAT_1:169;
then A17: x<>w & x in field FSG by Lm2,RELAT_1:15;
w in field FSG by A16,RELAT_1:15;
then consider r be object such that
A18: Im(FSG,x)/\Coim(FSG,w)={r} by A17,Def3;
A19: Coim(FSG,w)=Im(FSG,w) by Th2;
then t in Coim(FSG,w) by RELAT_1:169,A13;
then t in {r} by A14,A18,XBOOLE_0:def 4;
then A20: t=r by TARSKI:def 1;
[w,z] in FSG by A10,Lm3;
then z in Coim(FSG,w) by A19,RELAT_1:169;
then z in {r} by A7,A8,A18,XBOOLE_0:def 4;
hence thesis by A20,TARSKI:def 1;
end;
then [w,y] in h by A12,A15,A11,A7,FUNCT_1:def 2;
then [y,w] in H by RELAT_1:def 7;
then A21:w in Im(H,y) by RELAT_1:169;
reconsider y as set by TARSKI:1;
A22:Im(H,y) c= y
proof
let u be object;
assume u in Im(H,y);
then [y,u] in H by RELAT_1:169;
then A23:[u,y] in h by RELAT_1:def 7;
then A24: u in dom h by XTUPLE_0:def 12;
then h.u = y by FUNCT_1:def 2,A23;
then ex r be object st [u,r] in FSG & r in I & y={u,r} by A24, A7;
hence thesis by TARSKI:def 2;
end;
[z,y] in h by A8,A9,FUNCT_1:def 2;
then [y,z] in H by RELAT_1:def 7;
then z in Im(H,y) by RELAT_1:169;
then y c= Im(H,y) by A12,A21,ZFMISC_1:32;
then A25: y = Im(H,y) by A22;
z<>w by A10,Lm2;
hence thesis by A25, A12, CARD_2:57;
end;
then A26:card H = card (H| (dom H\R)) +` 2*`card R by SIMPLEX1:1;
dom H = R by RELAT_1:20;
then dom H\R={} by XBOOLE_1:37;
then card (H| (dom H\R))=0;
then card H = 2 *`card R by A26,CARD_2:18;
then 2 *card R =card H by Lm1
.= card h by Th1
.=card I by A7,CARD_1:62;
hence thesis by INT_1:def 3;
end;
theorem Th9:
x in field FSG & y in field FSG &
not [x,y] in FSG implies card Im(FSG,x) = card Im(FSG,y)
proof
set cx = card Im(FSG,x), cy = card Im(FSG,y);
A1: for x,y st x in field FSG & y in field FSG & x<>y & not [x,y] in FSG
holds card Im(FSG,x)-1 <= card Im(FSG,y)
proof
let x,y;
assume that
A2:x in field FSG
and A3:y in field FSG
and A4: x<>y
and A5: not [x,y] in FSG;
consider z being object such that
A6: Im(FSG,x)/\Coim(FSG,y) = {z} by A2,A3,A4,Def3;
defpred Q[object,object] means [$1,$2] in FSG & [$2,y] in FSG;
set Ix=Im(FSG,x),Iy=Im(FSG,y);
A7:for r be object st r in Ix\{z} ex t be object st Q[r,t]
proof
let r be object;
assume r in Ix\{z};
then A8:[x,r] in FSG by RELAT_1:169;
then r in field FSG by RELAT_1:15;
then consider t be object such that
A9: Im(FSG,r) /\ Coim(FSG,y) ={t} by A8,A5,A3,Def3;
take t;
A10: t in {t} by TARSKI:def 1;
Coim(FSG,y)=Iy by Th2;
then t in Iy by A10,A9,XBOOLE_0:def 4;
then A11: [y,t] in FSG by RELAT_1:169;
t in Im(FSG,r) by A10,A9,XBOOLE_0:def 4;
hence thesis by RELAT_1:169, A11,Lm3;
end;
consider h be Function such that
A12:dom h=Ix\{z} & for w be object st w in Ix\{z} holds Q[w,h.w]
from CLASSES1:sch 1(A7);
A13: rng h c= Iy
proof
let t be object;
assume t in rng h;
then ex r be object st r in dom h & h.r=t by FUNCT_1:def 3;
then [t,y] in FSG by A12;
then [y,t] in FSG by Lm3;
hence thesis by RELAT_1:169;
end;
z in {z} by TARSKI:def 1;
then A14:z in Ix by A6,XBOOLE_0:def 4;
not z in Ix\{z} by ZFMISC_1:56;
then A15: 1+ card (Ix\{z}) = card ((Ix\{z})\/{z}) by CARD_2:41
.= card Ix by ZFMISC_1:116,A14;
for x1,x2 be object st x1 in dom h & x2 in dom h & h.x1=h.x2 holds x1=x2
proof
let x1,x2 be object such that
A16: x1 in dom h
and A17: x2 in dom h
and A18: h.x1=h.x2;
A19: [x1,h.x1] in FSG & [x2,h.x1] in FSG by A12,A16,A17,A18;
A20: h.x1 <> x & [x,x1] in FSG by A12,A16,A5,RELAT_1:169;
[x,x2] in FSG by A12,A17,RELAT_1:169;
hence thesis by A20,Lm5,A19;
end;
then Segm card (Ix\{z}) c= Segm card Iy by A13,FUNCT_1:def 4,A12,CARD_1:10;
hence thesis by A15,NAT_1:39;
end;
assume that
A21: x in field FSG & y in field FSG
and A22: not [x,y] in FSG;
A23:not [y,x] in FSG by A22,Lm3;
per cases;
suppose x=y or cx=cy;
hence thesis;
end;
suppose A24:x<>y & cx<>cy;
A25: cx+1-1=cx;
cy -1 <=cx by A24,A1,A21,A23;
then A26: cy <= cx+1 by A25,XREAL_1:9;
A27:not 2 divides 1 by INT_2:13;
A28: cy+1-1=cy;
cx-1 <= cy by A24,A1,A21,A22;
then A29: cx <= cy+1 by A28,XREAL_1:9;
A30: 2 divides cx & 2 divides cy by Th8;
per cases by XXREAL_0:1,A26;
suppose cy < cx+1;
then cy <= cx by NAT_1:13;
then cy < cx by A24,XXREAL_0:1;
then cy+1 <= cx by NAT_1:13;
then cy+1 = cx by A29,XXREAL_0:1;
hence thesis by A27, A30,INT_2:1;
end;
suppose cy = cx+1;
hence thesis by A30,A27,INT_2:1;
end;
end;
end;
theorem Th10:
FSG is without_universal_friend & x in field FSG
implies card Im(FSG,x) > 2
proof
assume A1: FSG is without_universal_friend;
set I=Im(FSG,x);
assume A2:x in field FSG;
assume A3:card I <= 2;
reconsider xx=x as Element of field FSG by A2;
card I = 0 or ... or card I = 2 by A3; then
per cases;
suppose A4:card I=0;
xx is universal_friend
proof
let y;
assume A5: y in field FSG\{xx};
then xx<>y by ZFMISC_1:56;
then consider z being object such that
A6: I/\Coim(FSG,y) ={z} by A5,Def3;
z in {z} by TARSKI:def 1;
then z in I by A6,XBOOLE_0:def 4;
hence thesis by A4;
end;
hence thesis by A1;
end;
suppose card I=1;
hence thesis by Th8,INT_2:13;
end;
suppose A7:card I=2;
then consider y1,y2 be object such that
A8: y1<>y2
and A9: I={y1,y2} by CARD_2:60;
consider z1 be object such that
A10: z1 in field FSG\{x}
and A11: not [xx,z1] in FSG by A1,Def1;
A12: z1<>x by A10,ZFMISC_1:56;
then consider p be object such that
A13: I/\Coim(FSG,z1)={p} by A10, A2,Def3;
A14: for y1,y2 be object st y1<>y2 & I={y1,y2} holds
I/\Im(FSG,z1) <> {y1}
proof
let y1,y2 be object such that A15: y1<>y2
and A16: I={y1,y2};
A17: y1 in {y1} by TARSKI:def 1;
assume A18:I/\Im(FSG,z1) = {y1};
then y1 in Im(FSG,z1) by A17,XBOOLE_0:def 4;
then A19:[z1,y1] in FSG by RELAT_1:169;
then y1 in field FSG & z1<>y1 by RELAT_1:15,Lm2;
then consider t be object such that
A20: Im(FSG,y1)/\Coim(FSG,z1)={t} by Def3,A10;
A21: t in {t} by TARSKI:def 1;
then t in Im(FSG,y1) by A20,XBOOLE_0:def 4;
then A22: [y1,t] in FSG by RELAT_1:169;
then A23: y1<>t by Lm2;
A24: y1 in I by A16,TARSKI:def 2;
then A25: [x,y1] in FSG by RELAT_1:169;
then A26: x<>y1 & y1 in field FSG by Lm2,RELAT_1:15;
then consider x1x be object such that
A27:I/\Coim(FSG,y1) ={x1x} by A2,Def3;
A28: x1x in {x1x} by TARSKI:def 1;
then A29: x1x in I by A27,XBOOLE_0:def 4;
Coim(FSG,y1)=Im(FSG,y1) by Th2;
then x1x in Im(FSG,y1) by A28,A27,XBOOLE_0:def 4;
then A30:[y1,x1x] in FSG by RELAT_1:169;
then y1 <>x1x by Lm2;
then A31:[y1,y2] in FSG by A29,A16,TARSKI:def 2,A30;
y2 in I by A16,TARSKI:def 2;
then A32: [xx,y2] in FSG by RELAT_1:169;
consider z2 be object such that
A33: z2 in field FSG\{y1}
and A34: not [y1,z2] in FSG by A26,A1,Def1;
A35: Coim(FSG,z2) = Im(FSG,z2) by Th2;
z1<>z2 by A19,Lm3,A34;
then consider w be object such that
A36: Im(FSG,z2)/\Coim(FSG,z1)={w} by A10, A33,Def3;
A37: Coim(FSG,z1) = Im(FSG,z1) by Th2;
then A38: t in Im(FSG,z1) by A21,A20,XBOOLE_0:def 4;
A39: w in {w} by TARSKI:def 1;
then A40: w in Im(FSG,z1) by A36,A37,XBOOLE_0:def 4;
w in Im(FSG,z2) by A39,A36,XBOOLE_0:def 4;
then A41: [z2,w] in FSG by RELAT_1:169;
A42: [z1,w] in FSG by A40,RELAT_1:169;
A43: t<>w
proof
x <> z2 by A34, A25,Lm3;
then consider s be object such that
A44: I/\Coim(FSG,z2) ={s} by A2, A33,Def3;
A45: s in {s} by TARSKI:def 1;
then s in Im(FSG,z2) by A35,A44,XBOOLE_0:def 4;
then [z2,s] in FSG by RELAT_1:169;
then A46:[s,z2] in FSG by Lm3;
assume A47:t=w;
A48: [x,y1] in FSG & [y1,z1] in FSG by A24,RELAT_1:169, A19,Lm3;
A49: y1<>z2 & [w,z2] in FSG by A33,ZFMISC_1:56, A41,Lm3;
s in I by A45,A44,XBOOLE_0:def 4;
then [y2,z2] in FSG by A46,A34,A16,TARSKI:def 2;
then y2 = t by A49,A47,A31,A22,Lm5;
then [y2,z1] in FSG by A42,Lm3,A47;
hence contradiction by A48, A32,Lm5,A12,A15;
end;
y1<>w by A41,Lm3,A34;
then A50:card {y1,t,w} =3 by A43,CARD_2:58,A23;
A51: y1 in Im(FSG,z1) by A17,A18,XBOOLE_0:def 4;
card Im(FSG,z1)=2 by A11, A10,Th9,A7;
hence thesis by ZFMISC_1:133, A38,A40,A51,NAT_1:43,A50;
end;
Coim(FSG,z1)=Im(FSG,z1) by Th2;
then A52: p<>y1 & p<>y2 by A14,A13,A8,A9;
p in {p} by TARSKI:def 1;
then p in I by XBOOLE_0:def 4,A13;
hence thesis by A52,A9,TARSKI:def 2;
end;
end;
theorem Th11:
FSG is without_universal_friend & x in field FSG & y in field FSG
implies card Im(FSG,x) = card Im(FSG,y)
proof
assume that
A1: FSG is without_universal_friend
and A2: x in field FSG
and A3: y in field FSG;
per cases;
suppose not [x,y] in FSG;
hence thesis by A2,A3,Th9;
end;
suppose A4:[x,y] in FSG;
then x<>y by Lm2;
then A5: card {x,y}=2 by CARD_2:57;
x <>y by A4,Lm2;
then consider z being object such that
A6:Im(FSG,x)/\Coim(FSG,y)={z} by A2,A3,Def3;
A7: z in {z} by TARSKI:def 1;
then A8: z in Im(FSG,x) by A6,XBOOLE_0:def 4;
then A9: [x,z] in FSG by RELAT_1:169;
then A10: z in field FSG by RELAT_1:15;
Coim(FSG,y)=Im(FSG,y) by Th2;
then A11: z in Im(FSG,y) by A7,A6,XBOOLE_0:def 4;
then A12: [y,z] in FSG by RELAT_1:169;
then [z,y] in FSG by Lm3;
then A13: y in Im(FSG,z) by RELAT_1:169;
[z,x] in FSG by A9,Lm3;
then x in Im(FSG,z) by RELAT_1:169;
then card (Im(FSG,z)\{x,y}) = card Im(FSG,z) - card {x,y}
by A13,ZFMISC_1:32,CARD_2:44;
then card (Im(FSG,z)\{x,y}) > 2-2 by A5, A10,A1,Th10,XREAL_1:9;
then card (Im(FSG,z)\{x,y}) > 0;
then Im(FSG,z)\{x,y} is non empty;
then consider w be object such that
A14: w in Im(FSG,z)\{x,y};
A15: [z,w] in FSG by A14,RELAT_1:169;
then A16: w in field FSG by RELAT_1:15;
A17: not w in {x,y} by A14,XBOOLE_0:def 5;
A18: x<>z by A9,Lm2;
A19:not [x,w] in FSG
proof
A20: [w,z] in FSG & [y,z] in FSG by A15,Lm3, A11,RELAT_1:169;
assume [x,w] in FSG;
then y=w by A20, A4,Lm5,A18;
hence thesis by A17,TARSKI:def 2;
end;
A21: y<>z by A12,Lm2;
not [y,w] in FSG
proof
assume A22: [y,w] in FSG;
[x,z] in FSG by A8,RELAT_1:169;
then x=w by A22,A15,A4,Lm5,A21;
hence thesis by A17,TARSKI:def 2;
end;
hence card Im(FSG,y)=card Im(FSG,w) by A3,A16,Th9
.= card Im(FSG,x) by A2,Th9,A19,A16;
end;
end;
theorem Th12:
FSG is without_universal_friend & x in field FSG
implies card field FSG = 1 + card Im(FSG,x) * (card Im(FSG,x)-1)
proof
defpred FSGR[object,object] means for x,y st $1=[x,y] holds $2=y;
assume that
A1: FSG is without_universal_friend and
A2: x in field FSG;
set I=Im(FSG,x),F=field FSG, FI=F\({x}\/I);
defpred R[object,object] means
$1 in I & [$1,$2] in FSG & not [x,$2] in FSG;
consider RR be Relation such that
A3:for y,z being object holds [y,z] in RR iff y in I & z in FI & R[y,z]
from RELAT_1:sch 1;
card I > 2 by Th10,A1,A2;
then reconsider cI=card I-2 as Element of NAT by NAT_1:21;
for y st y in I holds card Im(RR,y)=cI
proof
let y be object;
x in {x} by TARSKI:def 1;
then x in {x}\/I by XBOOLE_0:def 3;
then not x in FI by XBOOLE_0:def 5;
then A4: not [y,x] in RR by A3;
assume A5:y in I;
then A6:[x,y] in FSG by RELAT_1:169;
then A7: x<>y by Lm2;
y in F by A6,RELAT_1:15;
then consider z being object such that
A8:I/\Coim(FSG,y) = {z} by A7,Def3,A2;
A9: z in {z} by TARSKI:def 1;
then A10: z in I by XBOOLE_0:def 4, A8;
then A11: [x,z] in FSG by RELAT_1:169;
Coim(FSG,y) = Im(FSG,y) by Th2;
then A12: z in Im(FSG,y) by A9,XBOOLE_0:def 4, A8;
then A13: [y,z] in FSG by RELAT_1:169;
A14: Im(FSG,y)\{z,x} c= Im(RR,y)
proof
let d be object;
assume A15: d in Im(FSG,y)\{z,x};
then A16: not d in {z,x} by XBOOLE_0:def 5;
A17: [y,d] in FSG by A15,RELAT_1:169;
then A18: d in F by RELAT_1:15;
A19: not d in I
proof
A20: [d,y] in FSG & [z,y] in FSG by A17,Lm3, A13;
assume d in I;
then [x,d] in FSG by RELAT_1:169;
then d = z by A20, A11,Lm5,A7;
hence thesis by A16,TARSKI:def 2;
end;
A21: not [x,d] in FSG
proof
assume A22: [x,d] in FSG;
A23: [d,y] in FSG & [x,z] in FSG by A17,Lm3, A10,RELAT_1:169;
[z,y] in FSG by A13,Lm3;
then d=z by A22,A23,Lm5,A7;
hence thesis by A16,TARSKI:def 2;
end;
d<>x by A16,TARSKI:def 2;
then not d in {x} by TARSKI:def 1;
then not d in I\/{x} by A19,XBOOLE_0:def 3;
then d in FI by A18,XBOOLE_0:def 5;
then [y,d] in RR by A3, A21,A5, A15,RELAT_1:169;
hence thesis by RELAT_1:169;
end;
A24: not [y,z] in RR by A11,A3;
Im(RR,y) c= Im(FSG,y)\{x,z}
proof
let d be object;
assume
A25:d in Im(RR,y);
then [y,d] in RR by RELAT_1:169;
then [y,d] in FSG by A3;
then A26: d in Im(FSG,y) by RELAT_1:169;
d<>x & d<>z by A25, A4,RELAT_1:169, A24;
then not d in {x,z} by TARSKI:def 2;
hence thesis by A26,XBOOLE_0:def 5;
end;
then A27:Im(RR,y) = Im(FSG,y)\{x,z} by A14;
y in F by A6,RELAT_1:15;
then A28: card Im(FSG,x) = card Im(FSG,y) by A1,A2,Th11;
[y,x] in FSG by A6,Lm3;
then x in Im(FSG,y) by RELAT_1:169;
then A29: card (Im(FSG,y)\{x,z}) = card Im(FSG,y) - card {x,z}
by ZFMISC_1:32,A12,CARD_2:44;
x<>z by A11,Lm2;
hence thesis by A28,A27,A29,CARD_2:57;
end;
then A30:card RR = card(RR| (dom RR\I)) +` cI*`card I by SIMPLEX1:1;
dom RR c= I
proof
let y be object;
assume y in dom RR;
then ex z being object st [y,z] in RR by XTUPLE_0:def 12;
hence thesis by A3;
end;
then (dom RR)\I={} by XBOOLE_1:37;
then card(RR| (dom RR\I))=0;
then A31:card RR = cI*`card I by A30,CARD_2:18
.= cI*card I by Lm1;
A32:for y being object st y in RR ex z being object st FSGR[y,z]
proof
let y being object such that A33:y in RR;
consider z,t be object such that
A34:[z,t] =y by A33,RELAT_1:def 1;
take t;
thus thesis by XTUPLE_0:1,A34;
end;
consider pr be Function such that
A35: dom pr = RR & for x being object st x in RR holds FSGR[x,pr.x]
from CLASSES1:sch 1 (A32);
A36: pr is one-to-one
proof
let x1,x2 be object;
assume that
A37: x1 in dom pr
and A38: x2 in dom pr
and A39: pr.x1=pr.x2;
consider y1,t1 be object such that
A40: x1=[y1,t1] by A37,A35,RELAT_1:def 1;
t1 in FI by A40,A35,A37,A3;
then not t1 in {x}\/I by XBOOLE_0:def 5;
then not t1 in {x} by XBOOLE_0:def 3;
then A41: t1<>x by TARSKI:def 1;
consider y2,t2 be object such that
A42: x2=[y2,t2] by A35,RELAT_1:def 1,A38;
A43: t1=pr.x1 & [y1,t1] in FSG by A37,A40,A35,A3;
A44: t2 = pr.x2 & [y2,t2] in FSG by A38,A42,A35,A3;
y2 in I by A42,A35,A38,A3;
then A45: [x,y2] in FSG by RELAT_1:169;
y1 in I by A40,A35,A37,A3;
then [x,y1] in FSG by RELAT_1:169;
hence thesis by A41,A39,A43,A44,A45,Lm5,A40,A42;
end;
A46: FI c= rng pr
proof
let z be object;
assume A47:z in FI;
then A48: not z in {x}\/I by XBOOLE_0:def 5;
then A49: not z in I by XBOOLE_0:def 3;
not z in {x} by A48,XBOOLE_0:def 3;
then z<>x by TARSKI:def 1;
then consider t be object such that
A50:I/\Coim(FSG,z) = {t} by A2, A47,Def3;
A51: t in {t} by TARSKI:def 1;
Coim(FSG,z)=Im(FSG,z) by Th2;
then t in Im(FSG,z) by A51,A50,XBOOLE_0:def 4;
then [z,t] in FSG by RELAT_1:169;
then R[t,z] by A49,RELAT_1:169,Lm3, A51,A50,XBOOLE_0:def 4;
then [t,z] in RR & pr.[t,z] = z by A3,A47,A35;
hence thesis by A35,FUNCT_1:def 3;
end;
rng pr c= FI
proof
let z be object;
assume z in rng pr;
then consider t be object such that
A52: t in dom pr
and A53: pr.t=z by FUNCT_1:def 3;
consider t1,t2 be object such that
A54:t=[t1,t2] by A52,A35,RELAT_1:def 1;
pr.t = t2 by A52,A54,A35;
hence thesis by A52,A54,A35,A3,A53;
end;
then rng pr = FI by A46;
then A55:cI*card I = card FI by WELLORD2:def 4,A36,A35,CARD_1:5, A31;
A56: I c= F
proof
let z be object;
assume z in I;
then [x,z] in FSG by RELAT_1:169;
hence thesis by RELAT_1:15;
end;
not [x,x] in FSG by Lm2;
then A57: card ({x}\/I) = card I+1 by RELAT_1:169,CARD_2:41;
{x} c= F by A2,ZFMISC_1:31;
then cI*card I=card F -card ({x}\/I) by A56,XBOOLE_1:8,CARD_2:44,A55;
then card F = cI*card I + (card I+1) by A57;
hence thesis;
end;
theorem
for x,y be Element of field FSG st x is universal_friend & x <> y
holds
ex z being object st Im(FSG,y) = {x,z} & Im(FSG,z) = {x,y}
proof
set F= field FSG;
let x,y be Element of F such that
A1: x is universal_friend
and A2: x <> y;
A3: F is non empty
proof
assume F is empty;
then x={} & y={} by SUBSET_1:def 1;
hence thesis by A2;
end;
then A4:y in F\{x} by A2,ZFMISC_1:56;
consider z being object such that
A5: {z} = Im(FSG,x)/\Coim(FSG,y) by A2,A3,Def3;
A6: z in {z} by TARSKI:def 1;
then z in Im(FSG,x) by A5,XBOOLE_0:def 4;
then A7: [x,z] in FSG by RELAT_1:169;
then A8: [z,x] in FSG by Lm3;
then A9: x in Im(FSG,z) by RELAT_1:169;
Coim(FSG,y) = Im(FSG,y) by Th2;
then A10: z in Im(FSG,y) by A6,A5,XBOOLE_0:def 4;
then A11: [y,z] in FSG by RELAT_1:169;
A12: Im(FSG,y) c= {x,z}
proof
let d be object;
assume d in Im(FSG,y);
then A13:[y,d] in FSG by RELAT_1:169;
assume A14: not d in {x,z};
then A15: d<>x by TARSKI:def 2;
d in F by A13,RELAT_1:15;
then d in F\{x} by A15,ZFMISC_1:56;
then [x,d] in FSG by A1;
then A16: [d,x] in FSG by Lm3;
d<>z by A14,TARSKI:def 2;
hence thesis by A16,A2,A13,Lm5,A11,A8;
end;
take z;
[x,y] in FSG by A1,A4;
then A17: [y,x] in FSG by Lm3;
then x in Im(FSG,y) by RELAT_1:169;
then {x,z} c= Im(FSG,y) by A10,ZFMISC_1:32;
hence Im(FSG,y) = {x,z} by A12;
A18: [z,y] in FSG by A11,Lm3;
A19: Im(FSG,z) c= {x,y}
proof
let d be object;
assume d in Im(FSG,z);
then A20:[z,d] in FSG by RELAT_1:169;
assume A21: not d in {x,y};
then A22: d<>x by TARSKI:def 2;
d in F by A20,RELAT_1:15;
then d in F\{x} by A22,ZFMISC_1:56;
then [x,d] in FSG by A1;
then A23: [d,x] in FSG by Lm3;
A24: x<>z by A7,Lm2;
d<>y by A21,TARSKI:def 2;
hence thesis by A23,A24,A20,Lm5,A17, A18;
end;
y in Im(FSG,z) by A18,RELAT_1:169;
then {x,y} c= Im(FSG,z) by A9,ZFMISC_1:32;
hence thesis by A19;
end;
begin :: The Friendship Theorem
::$N Friendship theorem
::$L https://en.wikipedia.org/wiki/Friendship_graph Friendship graph
theorem
FSG is non empty implies FSG is with_universal_friend
proof
set F=field FSG;
defpred Q1[FinSequence] means for i be Nat st 1<= i & i < len $1
holds [$1.i,$1.(i+1)] in FSG;
deffunc W(object) = Im(FSG,$1);
assume A1:FSG is non empty without_universal_friend;
then consider x be object such that
A2:x in F by XBOOLE_0:def 1;
reconsider F as non empty finite set by A2;
set m = card Im(FSG,x);
reconsider m1=m-1 as Nat by Th10,A1,A2,NAT_1:20;
m1 +1 >2 by Th10,A1,A2;
then consider p be Element of NAT such that
A3: p is prime
and A4: p divides m1 by NAT_1:13,INT_2:31;
A5:p>1 by A3,INT_2:def 4;
reconsider p as non zero Element of NAT by A3,INT_2:def 4;
A6: 2 divides m by Th8;
A7: p >2
proof
A8: m1+1=m;
assume A9:p <= 2;
p >= 1+1 by A5,NAT_1:13;
then 2 divides m1 by A9,XXREAL_0:1,A4;
then 2 divides 1 by A8,INT_2:1,A6;
hence contradiction by INT_2:13;
end;
then reconsider p2 =p-2 as Nat by NAT_1:21;
reconsider p1 =p-1 as Nat by NAT_1:20, A3,INT_2:def 4;
set T1=p1-tuples_on F;
set XFSG1 = {f where f is Element of T1:Q1[f] & f.1=f.p1};
set XFSG2 = {f where f is Element of T1:Q1[f] & f.1<>f.p1};
defpred C[object,object] means
for f be FinSequence st f=$1 holds $2=f|p1;
A10:for x being object st x in F holds W(x) in bool F
proof
let x be object;
assume x in F;
W(x) c= F
proof
let y be object;
assume y in W(x);
then [x,y] in FSG by RELAT_1:169;
hence thesis by RELAT_1:15;
end;
hence thesis;
end;
consider IM be Function of F,bool F such that
A11:for x being object st x in F holds IM.x=W(x) from FUNCT_2:sch 2(A10);
A12:for x st x in F holds card (IM.x)=m
proof
let y;
assume A13:y in F;
hence card (IM.y) = card W(y) by A11
.= m by A2,Th11,A1,A13;
end;
defpred Q[FinSequence] means [$1.p,$1.1] in FSG & Q1[$1];
set T = p-tuples_on F;
set XT={f where f is Element of T:Q[f]};
set XFSG = {f where f is Element of (p2+1)-tuples_on F: f.1 in F &
for i be Nat st i in Seg p2 holds f.(i+1) in IM.(f.i)};
F c= F;
then A14:card XFSG = card F * (m|^p2) by A12,Th6;
then reconsider XFSG as finite set;
A15:for f be Element of p1-tuples_on F holds f in XFSG iff Q1[f]
proof
let f be Element of T1;
A16: len f = p2+1 by CARD_1:def 7;
hereby
assume f in XFSG;
then A17: ex g be Element of T1 st f=g & g.1 in F &
for i be Nat st i in Seg p2 holds g.(i+1) in IM.(g.i);
thus Q1[f]
proof
let i such that
A18: 1<= i
and A19: i < len f;
i in dom f by A18,A19,FINSEQ_3:25;
then f.i in rng f by FUNCT_1:def 3;
then A20: W(f.i)=IM.(f.i) by A11;
i <= p2 by A19,A16,NAT_1:13;
then i in Seg p2 by A18;
hence thesis by A17,A20,RELAT_1:169;
end;
end;
assume A21:Q1[f];
A22: for i be Nat st i in Seg p2 holds f.(i+1) in IM.(f.i)
proof
let i be Nat;
assume A23: i in Seg p2;
then A24: 1 <= i by FINSEQ_1:1;
i <= p2 by A23,FINSEQ_1:1;
then A25: i < p2+1 by NAT_1:13;
then i in dom f by A24,A16,FINSEQ_3:25;
then A26: f.i in rng f by FUNCT_1:def 3;
[f.i,f.(i+1)] in FSG by A24,A25,A21,A16;
then f.(i+1) in W(f.i) by RELAT_1:169;
hence thesis by A26,A11;
end;
1<= len f by A16,NAT_1:11;
then 1 in dom f by FINSEQ_3:25;
then f.1 in rng f by FUNCT_1:def 3;
hence thesis by A22;
end;
A27:XFSG1 c= XFSG
proof
let x be object;
assume x in XFSG1;
then ex f be Element of T1 st x= f & Q1[f] & f.1=f.p1;
hence thesis by A15;
end;
A28:XFSG2 c= XFSG
proof
let x be object;
assume x in XFSG2;
then ex f be Element of T1 st x= f & Q1[f] & f.1<>f.p1;
hence thesis by A15;
end;
then reconsider XFSG1,XFSG2 as finite set by A27;
A29:p>1 by A3,INT_2:def 4;
then not p divides (m1+1) by A4,NEWTON:39;
then A30: not p divides (m|^p2) by A3,NAT_3:5;
A31:XFSG1 misses XFSG2
proof
assume XFSG1 meets XFSG2;
then consider x being object such that
A32: x in XFSG1 & x in XFSG2 by XBOOLE_0:3;
( ex f be Element of T1 st x= f & Q1[f] & f.1=f.p1)&
ex f be Element of T1 st x= f & Q1[f] & f.1<>f.p1 by A32;
hence contradiction;
end;
A33:for x being object st x in XT ex y being object st y in XFSG & C[x,y]
proof
let x be object;
assume x in XT;
then consider f be Element of T such that
A34: x=f
and A35: Q[f];
set g = f|p1;
A36:len f = p1+1 by CARD_1:def 7;
then p1 < len f by NAT_1:13;
then A37:len g = p1 by FINSEQ_1:59;
then reconsider g as Element of T1 by FINSEQ_2:92;
take g;
Q1[g]
proof
let i be Nat;
assume that
A38: 1 <= i
and A39: i < len g;
i in dom g by A38,A39, FINSEQ_3:25;
then A40: f.i=g.i by FUNCT_1:47;
i < len f by A39, A36,NAT_1:13,A37;
then A41: [f.i,f.(i+1)] in FSG by A38,A35;
1 < i+1 & i+1<= len g by A38,NAT_1:13, A39;
then i+1 in dom g by FINSEQ_3:25;
hence thesis by A40,FUNCT_1:47,A41;
end;
hence thesis by A15,A34;
end;
consider FSGR be Function of XT,XFSG such that
A42: for x being object st x in XT holds C[x,FSGR.x] from FUNCT_2:sch 1(A33);
reconsider pr=FSGR~ as Relation;
m>2 by Th10,A1,A2;
then m|^p2>0 by NEWTON:83;
then A43: XFSG is non empty by XREAL_1:129,A14;
then A44:dom FSGR=XT by FUNCT_2:def 1;
A45: XFSG c= XFSG1\/XFSG2
proof
let x be object;
assume A46:x in XFSG;
then consider f be Element of (p2+1)-tuples_on F such that
A47: x=f
and f.1 in F &
for i be Nat st i in Seg p2 holds f.(i+1) in IM.(f.i);
A48: f.1=f.p1 or f.1<>f.p1;
Q1[f] by A15,A46,A47;
then f in XFSG1 or f in XFSG2 by A48;
hence thesis by XBOOLE_0:def 3,A47;
end;
A49:p=p1+1;
then A50: p1>=1 by A29,NAT_1:13;
A51:for f be Element of T1 st Q1[f] & [f.p1,y] in FSG & [y,f.1] in FSG
holds f^<*y*> in XT
proof
let f be Element of T1 such that
A52: Q1[f]
and A53: [f.p1,y] in FSG
and A54: [y,f.1] in FSG;
set fy = f^<*y*>;
y in F by A53,RELAT_1:15;
then <*y*> is FinSequence of F by FINSEQ_1:74;
then A55: fy is FinSequence of F by FINSEQ_1:75;
A56: len fy = p1+1 by CARD_1:def 7;
A57:len f = p1 by CARD_1:def 7;
then A58:fy.p=y by FINSEQ_1:42;
reconsider fy as Element of T by A55,A56,FINSEQ_2:92;
A59: Q1[fy]
proof
let i such that
A60: 1 <= i
and A61: i < len fy;
A62:i <= p1 by A61,A56,NAT_1:13;
then A63:i in dom f by A60,A57,FINSEQ_3:25;
then A64:f.i=fy.i by FINSEQ_1:def 7;
per cases by A62,XXREAL_0:1;
suppose i=p1;
hence thesis by A58, A63,FINSEQ_1:def 7,A53;
end;
suppose A65: i<p1;
then i+1<= p1 by NAT_1:13;
then A66: i+1 in dom f by NAT_1:11,A57,FINSEQ_3:25;
[f.i,f.(i+1)] in FSG by A65,A57,A52,A60;
hence thesis by A66,FINSEQ_1:def 7,A64;
end;
end;
1 in dom f by A50,A57,FINSEQ_3:25;
then [fy.p,fy.1] in FSG by FINSEQ_1:def 7,A58,A54;
hence thesis by A59;
end;
A67:for f be Element of T1 st Q1[f] & f.1 = f.p1
for y st y in Im(FSG,f.1) holds f^<*y*> in XT
proof
let f be Element of T1 such that
A68: Q1[f] & f.1 = f.p1;
let y such that
A69: y in Im(FSG,f.1);
A70:[f.1,y] in FSG by RELAT_1:169,A69;
then [y,f.1] in FSG by Lm3;
hence thesis by A68,A70,A51;
end;
A71:for x st x in XFSG1 holds card Im(pr,x) = m
proof
let x;
assume x in XFSG1;
then consider f be Element of T1 such that
A72: f=x
and A73: Q1[f] & f.1 = f.p1;
deffunc D(object) = f^<*$1*>;
A74:len f = p1 by CARD_1:def 7;
A75:for y being object st y in Im(FSG,f.1) holds D(y) in Im(pr,f)
proof
let y be object;
assume A76:y in Im(FSG,f.1);
then A77:D(y) in XT by A67,A73;
then consider fy be Element of T such that
A78: D(y) = fy
and Q[fy];
reconsider yy=<*y*> as FinSequence of F by A78,FINSEQ_1:36;
FSGR.D(y) = (f^yy) |p1 by A76,A67,A73,A42
.= f by A74,FINSEQ_5:23;
then [fy,f] in FSGR by A77,A78, A44,FUNCT_1:def 2;
then [f,fy] in pr by RELAT_1:def 7;
hence thesis by A78,RELAT_1:169;
end;
consider d be Function of Im(FSG,f.1),Im(pr,f) such that
A79: for y being object st y in Im(FSG,f.1) holds d.y = D(y)
from FUNCT_2:sch 2(A75);
A80:d is one-to-one
proof
let x1,x2 be object;
assume that
A81: x1 in dom d
and A82: x2 in dom d & d.x1=d.x2;
d.x1=D(x1) by A81,A79;
then D(x1)=D(x2) by A82,A79;
hence thesis by FINSEQ_2:17;
end;
A83:1 in dom f by A74,A50,FINSEQ_3:25;
then f.1 in rng f by FUNCT_1:def 3;
then A84:card Im(FSG,f.1)=m by A1,Th11,A2;
then Im(FSG,f.1) is non empty by Th10,A1,A2;
then ex xx be object st xx in Im(FSG,f.1);
then Im(pr,f) is non empty by A75;
then A85:dom d = Im(FSG,f.1) by FUNCT_2:def 1;
Im(pr,f) c=rng d
proof
let y be object;
assume y in Im(pr,f);
then [f,y] in pr by RELAT_1:169;
then A86: [y,f] in FSGR by RELAT_1:def 7;
then A87:y in dom FSGR by XTUPLE_0:def 12;
then consider g be Element of T such that
A88: y=g
and A89: Q[g] by A44;
A90: len g = p1+1 by CARD_1:def 7;
f =FSGR.y by A87,A86,FUNCT_1:def 2;
then g|p1 = f by A87,A42,A88;
then A91:g = f ^ <*g.p*> by A90,FINSEQ_3:55;
then g.1 = f.1 by A83,FINSEQ_1:def 7;
then A92: [f.1,g.p] in FSG by A89,Lm3;
then g.p in dom d by RELAT_1:169,A85;
then d.(g.p) in rng d by FUNCT_1:def 3;
hence thesis by A92,RELAT_1:169,A91,A79,A88;
end;
then Im(pr,f) =rng d;
hence thesis by A85,A80,WELLORD2:def 4,A84,CARD_1:5,A72;
end;
XFSG1\/XFSG2 c= XFSG by A27,XBOOLE_1:8,A28;
then A93:XFSG = XFSG1\/XFSG2 by A45;
then card XFSG = card XFSG1+card XFSG2 by A31,CARD_2:40;
then A94:(1+ m*m1) * (m|^p2) = card XFSG1+card XFSG2 by A14, A1,A2,Th12;
A95:for f be Element of T1 st Q1[f] & f.1 <> f.p1 ex y st y in F &
f^<*y*> in XT
proof
let f be Element of T1 such that
A96: Q1[f]
and A97: f.1 <> f.p1;
A98: len f =p1 by CARD_1:def 7;
then p1 in dom f by A50,FINSEQ_3:25;
then A99: f.p1 in rng f by FUNCT_1:def 3;
1 in dom f by A98,A50,FINSEQ_3:25;
then f.1 in rng f by FUNCT_1:def 3;
then consider w be object such that
A100: {w} = Im(FSG,f.p1)/\Coim(FSG,f.1) by A99, A97,Def3;
take w;
A101: w in {w} by TARSKI:def 1;
Coim(FSG,f.1) =Im(FSG,f.1) by Th2;
then w in Im(FSG,f.1) by A101,A100,XBOOLE_0:def 4;
then [f.1,w] in FSG by RELAT_1:169;
then A102: [w,f.1] in FSG by Lm3;
w in Im(FSG,f.p1) by A101,A100,XBOOLE_0:def 4;
then [f.p1,w] in FSG by RELAT_1:169;
hence thesis by A102,A51,A96,RELAT_1:15;
end;
A103:for x st x in XFSG2 holds card Im(pr | XFSG2,x) = 1
proof
let x such that
A104:x in XFSG2;
consider f be Element of T1 such that
A105: x = f
and A106: Q1[f]
and A107: f.1<>f.p1 by A104;
consider y such that
y in F
and A109: f^<*y*> in XT by A95,A106,A107;
A111:len f = p1 by CARD_1:def 7;
A112: Im(pr | XFSG2,f) c= {f^<*y*>}
proof
let z be object;
consider w be Element of T such that
A113: w = f^<*y*>
and A114: Q[w] by A109;
A115: w.p = y by A113,A111, FINSEQ_1:42;
A116: p1 in dom f by A50,A111,FINSEQ_3:25;
then A117: w.p1=f.p1 by A113,FINSEQ_1:def 7;
A118: 1 in dom f by A50,A111,FINSEQ_3:25;
then A119: w.1=f.1 by A113,FINSEQ_1:def 7;
assume z in Im(pr | XFSG2,f);
then [f,z] in pr | XFSG2 by RELAT_1:169;
then [f,z] in pr by RELAT_1:def 11;
then A120: [z,f] in FSGR by RELAT_1:def 7;
then A121:z in dom FSGR by XTUPLE_0:def 12;
then z in XT;
then consider g be Element of T such that
A122: g=z
and A123: Q[g];
A124: p1 < p by A49,NAT_1:13;
f = FSGR.z by A121,FUNCT_1:def 2, A120;
then A125: f = g|p1 by A121,A42,A122;
then A126: g.1=f.1 by A118,FUNCT_1:47;
len w = p by CARD_1:def 7;
then A127: [w.p1,w.p] in FSG by A49,A29,NAT_1:13,A124,A114;
A128: len g = p by CARD_1:def 7;
then A129: g = f^<*g.p*> by A125,FINSEQ_3:55;
A130: g.p1=f.p1 by A116,A125,FUNCT_1:47;
[g.p1,g.p] in FSG by A49,A29,NAT_1:13,A124,A123,A128;
then g.p = w.p by A119,A126,A117,A130,A123,A114,A107,A127,Lm5;
hence thesis by A129,A115,A122,TARSKI:def 1;
end;
FSGR.(f^<*y*>) = (f^<*y*>) | p1 by A42,A109
.= f by FINSEQ_5:23,A111;
then [f^<*y*>,f] in FSGR by FUNCT_1:def 2,A44,A109;
then [f,f^<*y*>] in pr by RELAT_1:def 7;
then [f,f^<*y*>] in pr|XFSG2 by A105,A104,RELAT_1:def 11;
then f^<*y*> in Im(pr | XFSG2,f) by RELAT_1:169;
then Im(pr | XFSG2,f) = {f^<*y*>} by A112,ZFMISC_1:33;
hence thesis by A105,CARD_1:30;
end;
dom (pr|XFSG2) \ XFSG2 = {} by RELAT_1:58,XBOOLE_1:37;
then card ((pr| XFSG2) | (dom (pr|XFSG2) \ XFSG2 ))=0;
then A131: card (pr|XFSG2) = 0 +` (1 *` card XFSG2) by A103,SIMPLEX1:1
.= 1*` card XFSG2 by CARD_2:18
.= card XFSG2 by CARD_2:21;
XFSG c= rng FSGR
proof
let xp be object;
assume A132: xp in XFSG;
per cases by A132, A45,XBOOLE_0:def 3;
suppose xp in XFSG1;
then consider f be Element of T1 such that
A133: xp=f
and A134: Q1[f] & f.1 = f.p1;
len f = p1 by CARD_1:def 7;
then 1 in dom f by A50,FINSEQ_3:25;
then f.1 in rng f by FUNCT_1:def 3;
then card Im(FSG,f.1)=m by A1,Th11,A2;
then Im(FSG,f.1) is non empty by Th10,A1,A2;
then consider y be object such that
A135:y in Im(FSG,f.1);
set fy=y;
set fy=f^<*y*>;
f^<*y*> in XT by A67,A134,A135;
then A136: FSGR.fy in rng FSGR by A44,FUNCT_1:def 3;
[f.1,y] in FSG by A135,RELAT_1:169;
then y in F by RELAT_1:15;
then <*y*> is FinSequence of F by FINSEQ_1:74;
then A138: len fy = p1+1 & fy is FinSequence of F
by CARD_1:def 7,FINSEQ_1:75;
A139: len f = p1 by CARD_1:def 7;
FSGR.fy = fy|p1 by A42, A67,A134,A135;
hence thesis by A139,FINSEQ_5:23,A133,A136;
reconsider fy as Element of T by A138,FINSEQ_2:92;
end;
suppose xp in XFSG2;
then consider f be Element of T1 such that
A140: xp=f
and A141: Q1[f] & f.1 <> f.p1;
consider y such that
A142: y in F
and A143: f^<*y*> in XT by A141,A95;
set fy=f^<*y*>;
A144: FSGR.fy = fy|p1 & FSGR.fy in rng FSGR
by A42,A143,A44,FUNCT_1:def 3;
<*y*> is FinSequence of F by A142,FINSEQ_1:74;
then len fy = p1+1 & fy is FinSequence of F
by CARD_1:def 7,FINSEQ_1:75;
then reconsider fy as Element of T by FINSEQ_2:92;
len f = p1 by CARD_1:def 7;
hence thesis by FINSEQ_5:23,A140,A144;
end;
end;
then XFSG = rng FSGR;
then dom pr = XFSG by RELAT_1:20;
then dom pr \ XFSG1=XFSG2 by XBOOLE_1:88,A93,A31;
then
A146:card pr = card XFSG2 +` (m *` card XFSG1) by A131,A71,SIMPLEX1:1
.= card XFSG2 +` (m * card XFSG1) by Lm1
.= card XFSG2 + m*card XFSG1 by Lm1;
A147:for f1,f2 be FinSequence of F st f1^f2 is p -element & Q[f1^f2]
holds Q[f2^f1]
proof
let f1,f2 be FinSequence of F;
assume that
A148: f1^f2 is p -element
and A149: Q[f1^f2];
set f12=f1^f2,f21=f2^f1,L1=len f1,L2=len f2;
A150: len f12 = p by CARD_1:def 7,A148;
A151: len f21 = L2+L1 by FINSEQ_1:22;
A152: len f12 = L1+L2 by FINSEQ_1:22;
per cases;
suppose f1={} or f2={};
then f12=f2 & f21=f2 or f12=f1 & f21=f1 by FINSEQ_1:34;
hence thesis by A149;
end;
suppose A153: f1<>{} & f2 <>{};
then L2 >= 1 by FINSEQ_1:20;
then A154: 1 in dom f2 by FINSEQ_3:25;
then A155: f12.(L1+1) = f2.1 by FINSEQ_1:def 7;
A156: L1+1 <= p by A153,FINSEQ_1:20,A150,A152,XREAL_1:6;
A157: L1 >= 1 by A153,FINSEQ_1:20;
then A158: 1 in dom f1 by FINSEQ_3:25;
A159: L1 in dom f1 by A157,FINSEQ_3:25;
then A160: f21.p = f1.L1 by A150,A152,FINSEQ_1:def 7;
f12.L1 = f1.L1 by A159,FINSEQ_1:def 7;
then [f1.L1,f2.1] in FSG by A156,NAT_1:13,A149,A157,A155, A150;
hence [f21.p,f21.1] in FSG by A160, A154,FINSEQ_1:def 7;
let i;
assume that
A161: 1<= i
and A162: i < len f21;
A163:i in dom f21 by A161,A162,FINSEQ_3:25;
per cases by A163,FINSEQ_1:25;
suppose A164:i in dom f2;
then A165: i <= L2 by FINSEQ_3:25;
A166: f21.i = f2.i by A164,FINSEQ_1:def 7;
per cases;
suppose A167: i = L2;
A168: f1.1 = f12.1 by A158,FINSEQ_1:def 7;
f2.i = f12.p by A167,A150,A152,A164,FINSEQ_1:def 7;
hence thesis by A168, A167,A158,FINSEQ_1:def 7,A149,A166;
end;
suppose A169: i <>L2;
A170: 1+0 <= L1+i by XREAL_1:7,A157;
A171: i < L2 by A169,A165,XXREAL_0:1;
then L1+i < p by A150,A152,XREAL_1:6;
then A172: [f12.(L1+i),f12.(L1+i+1)] in FSG by A170,A149, A150;
A173: f12.(L1+i)=f2.i by A164, FINSEQ_1:def 7;
i+1<=L2 by A171, NAT_1:13;
then A174: i+1 in dom f2 by NAT_1:11,FINSEQ_3:25;
then f12.(L1+(i+1)) = f2.(i+1) by FINSEQ_1:def 7;
hence thesis by A174, FINSEQ_1:def 7, A172,A173, A166;
end;
end;
suppose ex n be Nat st n in dom f1 & i=L2 + n;
then consider n be Nat such that
A175: n in dom f1
and
A176: i=L2 + n;
A177: f21.i = f1.n & f12.n = f1.n by A175,A176,FINSEQ_1:def 7;
A178: 1<= n by A175,FINSEQ_3:25;
A179: n < L1 by A176,A162,A151,XREAL_1:6;
then A180: n+0 < L1+L2 by XREAL_1:8;
n+1 <= L1 by A179,NAT_1:13;
then A181: n+1 in dom f1 by NAT_1:11,FINSEQ_3:25;
i+1 = L2+(n+1) by A176;
then A182: f21.(i+1) = f1.(n+1) by A181,FINSEQ_1:def 7;
f12.(n+1) = f1.(n+1) by A181,FINSEQ_1:def 7;
hence thesis by A178,A180,A149,A152,A177,A182;
end;
end;
end;
A183:for f1 be Element of T st Q[f1] for i be Nat st i < p &
f1 = (f1/^i)^(f1|i) holds i = 0
proof
let f1 be Element of T such that
A184:Q[f1];
A185: len f1 = p by CARD_1:def 7;
then 2 in dom f1 by A7,FINSEQ_3: 25;
then A186: f1.2 in rng f1 by FUNCT_1:def 3;
let i be Nat such that
A187: i < p & f1 = (f1/^i)^(f1|i) & i <> 0;
rng f1 c= {f1.1} by A187,A185,A3,Th7;
then A188: f1.2 =f1.1 by A186,TARSKI:def 1;
[f1.1,f1.(1+1)] in FSG by A3,INT_2:def 4,A184,A185;
hence contradiction by A188,Lm2;
end;
consider C be Cardinal such that
A189:p*`C = card XT from Sch(A147,A183);
A190:card pr = card FSGR by Th1
.= card dom FSGR by CARD_1:62
.= card XT by A43,FUNCT_2:def 1;
then C is finite by A146,A189;
then reconsider C as Nat;
p*C = card XFSG2 + m*card XFSG1 by A189,Lm1,A146,A190;
then A191:p divides (1+ m*m1) * (m|^p2) + (m-1) *card XFSG1
by A94,INT_1:def 3;
not p divides m*m1 +1 by A4,INT_2:2,NEWTON:39,A29;
then A192: not p divides (1+ m*m1) * (m|^p2) by A30,A3,INT_5:7;
p divides m1 *card XFSG1 by A4,INT_2:2;
hence contradiction by A192,INT_2:1,A191;
end;