let k be Element of NAT ; for X being non empty set st 0 < k & k + 1 c= card X holds
G_ (k,X) is Desarguesian
let X be non empty set ; ( 0 < k & k + 1 c= card X implies G_ (k,X) is Desarguesian )
assume that
A1:
0 < k
and
A2:
k + 1 c= card X
; G_ (k,X) is Desarguesian
let o, b1, a1, b2, a2, b3, a3, r, s, t be POINT of (G_ (k,X)); INCPROJ:def 13 for b1, b2, b3, b4, b5, b6, b7, b8, b9 being Element of the Lines of (G_ (k,X)) holds
( not {o,b1,a1} on b1 or not {o,a2,b2} on b2 or not {o,a3,b3} on b3 or not {a3,a2,t} on b4 or not {a3,r,a1} on b5 or not {a2,s,a1} on b6 or not {t,b2,b3} on b7 or not {b1,r,b3} on b8 or not {b1,s,b2} on b9 or not b1,b2,b3 are_mutually_distinct or o = a1 or o = a2 or o = a3 or o = b1 or o = b2 or o = b3 or a1 = b1 or a2 = b2 or a3 = b3 or ex b10 being Element of the Lines of (G_ (k,X)) st {r,s,t} on b10 )
let C1, C2, C3, A1, A2, A3, B1, B2, B3 be LINE of (G_ (k,X)); ( not {o,b1,a1} on C1 or not {o,a2,b2} on C2 or not {o,a3,b3} on C3 or not {a3,a2,t} on A1 or not {a3,r,a1} on A2 or not {a2,s,a1} on A3 or not {t,b2,b3} on B1 or not {b1,r,b3} on B2 or not {b1,s,b2} on B3 or not C1,C2,C3 are_mutually_distinct or o = a1 or o = a2 or o = a3 or o = b1 or o = b2 or o = b3 or a1 = b1 or a2 = b2 or a3 = b3 or ex b1 being Element of the Lines of (G_ (k,X)) st {r,s,t} on b1 )
assume that
A3:
{o,b1,a1} on C1
and
A4:
{o,a2,b2} on C2
and
A5:
{o,a3,b3} on C3
and
A6:
{a3,a2,t} on A1
and
A7:
{a3,r,a1} on A2
and
A8:
{a2,s,a1} on A3
and
A9:
{t,b2,b3} on B1
and
A10:
{b1,r,b3} on B2
and
A11:
{b1,s,b2} on B3
and
A12:
C1,C2,C3 are_mutually_distinct
and
A13:
o <> a1
and
A14:
( o <> a2 & o <> a3 )
and
A15:
o <> b1
and
A16:
( o <> b2 & o <> b3 )
and
A17:
a1 <> b1
and
A18:
a2 <> b2
and
A19:
a3 <> b3
; ex b1 being Element of the Lines of (G_ (k,X)) st {r,s,t} on b1
A20:
o on C1
by A3, INCSP_1:2;
A21:
b2 on C2
by A4, INCSP_1:2;
then A22:
b2 c= C2
by A1, A2, Th10;
A23:
a2 on C2
by A4, INCSP_1:2;
then A24:
{a2,b2} on C2
by A21, INCSP_1:1;
A25:
o on C2
by A4, INCSP_1:2;
then A26:
{o,b2} on C2
by A21, INCSP_1:1;
A27:
{o,a2} on C2
by A25, A23, INCSP_1:1;
A28:
( a3 on A1 & a2 on A1 )
by A6, INCSP_1:2;
A29:
b3 on B2
by A10, INCSP_1:2;
A30:
b3 on C3
by A5, INCSP_1:2;
then A31:
b3 c= C3
by A1, A2, Th10;
A32:
a3 on C3
by A5, INCSP_1:2;
then A33:
{a3,b3} on C3
by A30, INCSP_1:1;
A34:
o on C3
by A5, INCSP_1:2;
then A35:
{o,b3} on C3
by A30, INCSP_1:1;
A36:
{o,a3} on C3
by A34, A32, INCSP_1:1;
A37:
( a3 on A2 & a1 on A2 )
by A7, INCSP_1:2;
A38:
b1 on B3
by A11, INCSP_1:2;
A39:
C1 <> C3
by A12, ZFMISC_1:def 5;
A40:
b1 on B2
by A10, INCSP_1:2;
A41:
C2 <> C3
by A12, ZFMISC_1:def 5;
A42:
b3 on B1
by A9, INCSP_1:2;
A43:
C1 <> C2
by A12, ZFMISC_1:def 5;
A44:
b2 on B1
by A9, INCSP_1:2;
A45:
a1 on C1
by A3, INCSP_1:2;
then A46:
a1 c= C1
by A1, A2, Th10;
A47:
b1 on C1
by A3, INCSP_1:2;
then A48:
{o,b1} on C1
by A20, INCSP_1:1;
A49:
b2 on B3
by A11, INCSP_1:2;
A50:
{a1,b1} on C1
by A47, A45, INCSP_1:1;
A51:
( not a1 on B2 & not a2 on B3 & not a3 on B1 )
proof
assume
(
a1 on B2 or
a2 on B3 or
a3 on B1 )
;
contradiction
then
(
{a1,b1} on B2 or
{a2,b2} on B3 or
{a3,b3} on B1 )
by A42, A40, A49, INCSP_1:1;
then
(
b3 on C1 or
b1 on C2 or
b2 on C3 )
by A17, A18, A19, A44, A29, A38, A50, A24, A33, INCSP_1:def 10;
then
(
{o,b3} on C1 or
{o,b1} on C2 or
{o,b2} on C3 )
by A20, A25, A34, INCSP_1:1;
hence
contradiction
by A15, A16, A48, A26, A35, A43, A41, A39, INCSP_1:def 10;
verum
end;
A52:
( s on A3 & s on B3 )
by A8, A11, INCSP_1:2;
A53:
t on B1
by A9, INCSP_1:2;
A54:
( r on A2 & r on B2 )
by A7, A10, INCSP_1:2;
A55:
t on A1
by A6, INCSP_1:2;
A56:
a1 on A3
by A8, INCSP_1:2;
A57:
a2 on A3
by A8, INCSP_1:2;
A58:
the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 }
by A1, A2, Def1;
A59:
{o,a1} on C1
by A20, A45, INCSP_1:1;
A60:
( not o on A1 & not o on B1 & not o on A2 & not o on B2 & not o on A3 & not o on B3 )
proof
assume
(
o on A1 or
o on B1 or
o on A2 or
o on B2 or
o on A3 or
o on B3 )
;
contradiction
then
( (
{o,a2} on A1 &
{o,a3} on A1 ) or (
{o,b2} on B1 &
{o,b3} on B1 ) or (
{o,a1} on A2 &
{o,a3} on A2 ) or (
{o,b1} on B2 &
{o,b3} on B2 ) or (
{o,a2} on A3 &
{o,a1} on A3 ) or (
{o,b2} on B3 &
{o,b1} on B3 ) )
by A28, A37, A57, A56, A44, A42, A40, A29, A38, A49, INCSP_1:1;
then
( (
A1 = C2 &
A1 = C3 ) or (
B1 = C2 &
B1 = C3 ) or (
A2 = C1 &
A2 = C3 ) or (
B2 = C1 &
B2 = C3 ) or (
A3 = C2 &
A3 = C1 ) or (
B3 = C2 &
B3 = C1 ) )
by A13, A14, A15, A16, A59, A27, A36, A48, A26, A35, INCSP_1:def 10;
hence
contradiction
by A12, ZFMISC_1:def 5;
verum
end;
then consider salpha being POINT of (G_ (k,X)) such that
A61:
( salpha on A3 & salpha on B3 )
and
A62:
salpha = (a1 /\ b1) \/ (a2 /\ b2)
by A1, A2, A20, A47, A45, A25, A23, A21, A57, A56, A38, A49, A43, A51, Th12;
consider ralpha being POINT of (G_ (k,X)) such that
A63:
( ralpha on B2 & ralpha on A2 )
and
A64:
ralpha = (a1 /\ b1) \/ (a3 /\ b3)
by A1, A2, A20, A47, A45, A34, A32, A30, A37, A40, A29, A39, A51, A60, Th12;
A65:
((a1 /\ b1) \/ (a3 /\ b3)) \/ (a2 /\ b2) = (a1 /\ b1) \/ ((a3 /\ b3) \/ (a2 /\ b2))
by XBOOLE_1:4;
consider talpha being POINT of (G_ (k,X)) such that
A66:
( talpha on A1 & talpha on B1 )
and
A67:
talpha = (a2 /\ b2) \/ (a3 /\ b3)
by A1, A2, A25, A23, A21, A34, A32, A30, A28, A44, A42, A41, A51, A60, Th12;
A68:
( A1 <> B1 & A2 <> B2 )
by A6, A7, A51, INCSP_1:2;
A69:
( r = ralpha & s = salpha & t = talpha )
proof
A70:
(
{s,salpha} on A3 &
{s,salpha} on B3 )
by A52, A61, INCSP_1:1;
A71:
(
{r,ralpha} on A2 &
{r,ralpha} on B2 )
by A54, A63, INCSP_1:1;
assume A72:
(
r <> ralpha or
s <> salpha or
t <> talpha )
;
contradiction
(
{t,talpha} on A1 &
{t,talpha} on B1 )
by A55, A53, A66, INCSP_1:1;
hence
contradiction
by A57, A51, A68, A72, A71, A70, INCSP_1:def 10;
verum
end;
then
r \/ s = (((a3 /\ b3) \/ (a1 /\ b1)) \/ (a1 /\ b1)) \/ (a2 /\ b2)
by A62, A64, XBOOLE_1:4;
then
r \/ s = ((a3 /\ b3) \/ ((a1 /\ b1) \/ (a1 /\ b1))) \/ (a2 /\ b2)
by XBOOLE_1:4;
then A73:
(r \/ s) \/ t = ((a1 /\ b1) \/ (a3 /\ b3)) \/ (a2 /\ b2)
by A67, A69, A65, XBOOLE_1:7, XBOOLE_1:12;
a2 c= C2
by A1, A2, A23, Th10;
then A74:
a2 \/ b2 c= C2
by A22, XBOOLE_1:8;
r c= r \/ (s \/ t)
by XBOOLE_1:7;
then A75:
r c= (r \/ s) \/ t
by XBOOLE_1:4;
C1 in the Lines of (G_ (k,X))
;
then consider C11 being Subset of X such that
A76:
( C11 = C1 & card C11 = k + 1 )
by A58;
reconsider C1 = C1 as finite set by A76;
A77:
b1 c= C1
by A1, A2, A47, Th10;
then
a1 \/ b1 c= C1
by A46, XBOOLE_1:8;
then A78:
card (a1 \/ b1) c= k + 1
by A76, CARD_1:11;
A79:
the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k }
by A1, A2, Def1;
o in the Points of (G_ (k,X))
;
then A80:
ex o1 being Subset of X st
( o1 = o & card o1 = k )
by A79;
b1 in the Points of (G_ (k,X))
;
then A81:
ex b11 being Subset of X st
( b11 = b1 & card b11 = k )
by A79;
a3 in the Points of (G_ (k,X))
;
then A82:
ex a13 being Subset of X st
( a13 = a3 & card a13 = k )
by A79;
then A83:
card a3 = (k - 1) + 1
;
t in the Points of (G_ (k,X))
;
then A84:
ex t1 being Subset of X st
( t1 = t & card t1 = k )
by A79;
then A85:
t is finite
;
a2 in the Points of (G_ (k,X))
;
then A86:
ex a12 being Subset of X st
( a12 = a2 & card a12 = k )
by A79;
then A87:
card a2 = (k - 1) + 1
;
s in the Points of (G_ (k,X))
;
then A88:
ex s1 being Subset of X st
( s1 = s & card s1 = k )
by A79;
then A89:
s is finite
;
a1 in the Points of (G_ (k,X))
;
then A90:
ex a11 being Subset of X st
( a11 = a1 & card a11 = k )
by A79;
then
k + 1 c= card (a1 \/ b1)
by A81, A17, Th1;
then A91:
card (a1 \/ b1) = (k - 1) + (2 * 1)
by A78, XBOOLE_0:def 10;
A92:
k - 1 is Element of NAT
by A1, NAT_1:20;
C2 in the Lines of (G_ (k,X))
;
then
ex C12 being Subset of X st
( C12 = C2 & card C12 = k + 1 )
by A58;
then A93:
card (a2 \/ b2) c= k + 1
by A74, CARD_1:11;
b2 in the Points of (G_ (k,X))
;
then A94:
ex b12 being Subset of X st
( b12 = b2 & card b12 = k )
by A79;
then
k + 1 c= card (a2 \/ b2)
by A86, A18, Th1;
then A95:
card (a2 \/ b2) = (k - 1) + (2 * 1)
by A93, XBOOLE_0:def 10;
then A96:
card (a2 /\ b2) = k - 1
by A92, A94, A87, Th2;
A97:
card (a2 /\ b2) = (k - 2) + 1
by A92, A94, A95, A87, Th2;
A98:
card a1 = (k - 1) + 1
by A90;
then A99:
card (a1 /\ b1) = k - 1
by A92, A81, A91, Th2;
a3 c= C3
by A1, A2, A32, Th10;
then A100:
a3 \/ b3 c= C3
by A31, XBOOLE_1:8;
s c= s \/ (r \/ t)
by XBOOLE_1:7;
then A101:
s c= (r \/ s) \/ t
by XBOOLE_1:4;
0 + 1 < k + 1
by A1, XREAL_1:8;
then
1 <= (k - 1) + 1
by NAT_1:13;
then
( 1 <= k - 1 or k = 1 )
by A92, NAT_1:8;
then A102:
( 1 + 1 <= (k - 1) + 1 or k = 1 )
by XREAL_1:6;
A103:
o c= C1
by A1, A2, A20, Th10;
A104:
not k = 1
proof
assume A105:
k = 1
;
contradiction
then consider z1 being
object such that A106:
o = {z1}
by A80, CARD_2:42;
consider z3 being
object such that A107:
b1 = {z3}
by A81, A105, CARD_2:42;
consider z2 being
object such that A108:
a1 = {z2}
by A90, A105, CARD_2:42;
o \/ a1 c= C1
by A103, A46, XBOOLE_1:8;
then
(o \/ a1) \/ b1 c= C1
by A77, XBOOLE_1:8;
then
{z1,z2} \/ b1 c= C1
by A106, A108, ENUMSET1:1;
then A109:
{z1,z2,z3} c= C1
by A107, ENUMSET1:3;
card {z1,z2,z3} = 3
by A13, A15, A17, A106, A108, A107, CARD_2:58;
then
Segm 3
c= Segm (card C1)
by A109, CARD_1:11;
hence
contradiction
by A76, A105, NAT_1:39;
verum
end;
then A110:
k - 2 is Element of NAT
by A102, NAT_1:21;
C3 in the Lines of (G_ (k,X))
;
then
ex C13 being Subset of X st
( C13 = C3 & card C13 = k + 1 )
by A58;
then A111:
card (a3 \/ b3) c= k + 1
by A100, CARD_1:11;
b3 in the Points of (G_ (k,X))
;
then A112:
ex b13 being Subset of X st
( b13 = b3 & card b13 = k )
by A79;
then
k + 1 c= card (a3 \/ b3)
by A82, A19, Th1;
then A113:
card (a3 \/ b3) = (k - 1) + (2 * 1)
by A111, XBOOLE_0:def 10;
then A114:
card (a3 /\ b3) = k - 1
by A92, A112, A83, Th2;
r in the Points of (G_ (k,X))
;
then A115:
ex r1 being Subset of X st
( r1 = r & card r1 = k )
by A79;
then
r \/ s c= X
by A88, XBOOLE_1:8;
then A116:
(r \/ s) \/ t c= X
by A84, XBOOLE_1:8;
A117:
card (a3 /\ b3) = (k - 2) + 1
by A92, A112, A113, A83, Th2;
A118:
card (a1 /\ b1) = (k - 2) + 1
by A92, A81, A91, A98, Th2;
card ((a1 /\ b1) \/ (a2 /\ b2)) = (k - 2) + (2 * 1)
by A62, A69, A88;
then A119:
card ((a1 /\ b1) /\ (a2 /\ b2)) = k - 2
by A110, A118, A97, Th2;
card ((a2 /\ b2) \/ (a3 /\ b3)) = (k - 2) + (2 * 1)
by A67, A69, A84;
then A120:
card ((a2 /\ b2) /\ (a3 /\ b3)) = k - 2
by A110, A97, A117, Th2;
card ((a1 /\ b1) \/ (a3 /\ b3)) = (k - 2) + (2 * 1)
by A64, A69, A115;
then A121:
card ((a1 /\ b1) /\ (a3 /\ b3)) = k - 2
by A110, A118, A117, Th2;
A122:
t c= (r \/ s) \/ t
by XBOOLE_1:7;
A123:
( k = 2 implies ex O being LINE of (G_ (k,X)) st {r,s,t} on O )
proof
assume
k = 2
;
ex O being LINE of (G_ (k,X)) st {r,s,t} on O
then
card ((r \/ s) \/ t) = k + 1
by A99, A96, A114, A73, A121, A120, A119, Th7;
then
(r \/ s) \/ t in the
Lines of
(G_ (k,X))
by A58, A116;
then consider O being
LINE of
(G_ (k,X)) such that A124:
O = (r \/ s) \/ t
;
A125:
t on O
by A1, A2, A122, A124, Th10;
(
r on O &
s on O )
by A1, A2, A75, A101, A124, Th10;
then
{r,s,t} on O
by A125, INCSP_1:2;
hence
ex
O being
LINE of
(G_ (k,X)) st
{r,s,t} on O
;
verum
end;
A126:
r is finite
by A115;
A127:
( 3 <= k implies ex O being LINE of (G_ (k,X)) st {r,s,t} on O )
proof
A128:
(
card ((r \/ s) \/ t) = k + 1 implies ex
O being
LINE of
(G_ (k,X)) st
{r,s,t} on O )
proof
assume
card ((r \/ s) \/ t) = k + 1
;
ex O being LINE of (G_ (k,X)) st {r,s,t} on O
then
(r \/ s) \/ t in the
Lines of
(G_ (k,X))
by A58, A116;
then consider O being
LINE of
(G_ (k,X)) such that A129:
O = (r \/ s) \/ t
;
A130:
t on O
by A1, A2, A122, A129, Th10;
(
r on O &
s on O )
by A1, A2, A75, A101, A129, Th10;
then
{r,s,t} on O
by A130, INCSP_1:2;
hence
ex
O being
LINE of
(G_ (k,X)) st
{r,s,t} on O
;
verum
end;
A131:
(
card ((r \/ s) \/ t) = k implies ex
O being
LINE of
(G_ (k,X)) st
{r,s,t} on O )
proof
assume A132:
card ((r \/ s) \/ t) = k
;
ex O being LINE of (G_ (k,X)) st {r,s,t} on O
then A133:
t = (r \/ s) \/ t
by A84, A126, A89, A85, CARD_2:102, XBOOLE_1:7;
(
r = (r \/ s) \/ t &
s = (r \/ s) \/ t )
by A115, A88, A126, A89, A85, A75, A101, A132, CARD_2:102;
then
{r,s,t} on A1
by A55, A133, INCSP_1:2;
hence
ex
O being
LINE of
(G_ (k,X)) st
{r,s,t} on O
;
verum
end;
assume
3
<= k
;
ex O being LINE of (G_ (k,X)) st {r,s,t} on O
hence
ex
O being
LINE of
(G_ (k,X)) st
{r,s,t} on O
by A99, A96, A114, A73, A102, A121, A120, A119, A128, A131, Th7;
verum
end;
( k = 2 or 2 <= k - 1 )
by A92, A104, A102, NAT_1:8;
then
( k = 2 or 2 + 1 <= (k - 1) + 1 )
by XREAL_1:6;
hence
ex b1 being Element of the Lines of (G_ (k,X)) st {r,s,t} on b1
by A123, A127; verum