let X be OrtAfPl; :: thesis: ( X is satisfying_DES iff Af X is Desarguesian )
A1:
( X is satisfying_DES implies Af X is Desarguesian )
proof
assume A2:
X is
satisfying_DES
;
:: thesis: Af X is Desarguesian
now let A,
M,
N be
Subset of
(Af X);
:: thesis: for o, a, b, c, a1, b1, c1 being Element of (Af X) st o in A & o in M & o in N & o <> a & o <> b & o <> c & a in A & a1 in A & b in M & b1 in M & c in N & c1 in N & A is being_line & M is being_line & N is being_line & A <> M & A <> N & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1let o,
a,
b,
c,
a1,
b1,
c1 be
Element of
(Af X);
:: thesis: ( o in A & o in M & o in N & o <> a & o <> b & o <> c & a in A & a1 in A & b in M & b1 in M & c in N & c1 in N & A is being_line & M is being_line & N is being_line & A <> M & A <> N & a,b // a1,b1 & a,c // a1,c1 implies b,c // b1,c1 )assume that A3:
o in A
and A4:
o in M
and A5:
o in N
and A6:
o <> a
and A7:
o <> b
and A8:
o <> c
and A9:
a in A
and A10:
a1 in A
and A11:
b in M
and A12:
b1 in M
and A13:
c in N
and A14:
c1 in N
and A15:
A is
being_line
and A16:
M is
being_line
and A17:
N is
being_line
and A18:
A <> M
and A19:
A <> N
and A20:
a,
b // a1,
b1
and A21:
a,
c // a1,
c1
;
:: thesis: b,c // b1,c1reconsider o' =
o,
a' =
a,
a1' =
a1,
b' =
b,
b1' =
b1,
c' =
c,
c1' =
c1 as
Element of
X by ANALMETR:47;
o,
b // o,
b1
by A4, A11, A12, A16, AFF_1:53, AFF_1:55;
then A22:
LIN o,
b,
b1
by AFF_1:def 1;
then A23:
LIN o',
b',
b1'
by ANALMETR:55;
o,
a // o,
a1
by A3, A9, A10, A15, AFF_1:53, AFF_1:55;
then A24:
LIN o,
a,
a1
by AFF_1:def 1;
o,
c // o,
c1
by A5, A13, A14, A17, AFF_1:53, AFF_1:55;
then A25:
LIN o,
c,
c1
by AFF_1:def 1;
then A26:
LIN o',
c',
c1'
by ANALMETR:55;
assume A27:
not
b,
c // b1,
c1
;
:: thesis: contradictionA28:
( not
LIN b',
b1',
a' & not
LIN a',
a1',
c' )
proof
A29:
a <> a1
proof
assume A30:
a = a1
;
:: thesis: contradiction
A31:
c = c1
proof
A32:
not
LIN o,
a,
c
proof
assume
LIN o,
a,
c
;
:: thesis: contradiction
then
c in A
by A3, A6, A9, A15, AFF_1:39;
then A33:
o,
c // A
by A3, A15, AFF_1:66;
o,
c // N
by A5, A13, A17, AFF_1:66;
hence
contradiction
by A3, A5, A8, A19, A33, AFF_1:59, AFF_1:67;
:: thesis: verum
end;
assume
c <> c1
;
:: thesis: contradiction
hence
contradiction
by A21, A25, A30, A32, AFF_1:23;
:: thesis: verum
end;
b = b1
proof
A34:
not
LIN o,
a,
b
proof
assume
LIN o,
a,
b
;
:: thesis: contradiction
then
b in A
by A3, A6, A9, A15, AFF_1:39;
then A35:
o,
b // A
by A3, A15, AFF_1:66;
o,
b // M
by A4, A11, A16, AFF_1:66;
hence
contradiction
by A3, A4, A7, A18, A35, AFF_1:59, AFF_1:67;
:: thesis: verum
end;
assume
b <> b1
;
:: thesis: contradiction
hence
contradiction
by A20, A22, A30, A34, AFF_1:23;
:: thesis: verum
end;
hence
contradiction
by A27, A31, AFF_1:11;
:: thesis: verum
end;
A36:
b <> b1
proof
A37:
not
LIN o,
b,
a
proof
assume
LIN o,
b,
a
;
:: thesis: contradiction
then
a in M
by A4, A7, A11, A16, AFF_1:39;
then A38:
o,
a // M
by A4, A16, AFF_1:66;
o,
a // A
by A3, A9, A15, AFF_1:66;
hence
contradiction
by A3, A4, A6, A18, A38, AFF_1:59, AFF_1:67;
:: thesis: verum
end;
assume
b = b1
;
:: thesis: contradiction
then
b,
a // b,
a1
by A20, AFF_1:13;
hence
contradiction
by A24, A29, A37, AFF_1:23;
:: thesis: verum
end;
assume
(
LIN b',
b1',
a' or
LIN a',
a1',
c' )
;
:: thesis: contradiction
then
(
LIN b,
b1,
a or
LIN a,
a1,
c )
by ANALMETR:55;
then
(
a in M or
c in A )
by A9, A10, A11, A12, A15, A16, A29, A36, AFF_1:39;
then A39:
(
o,
a // M or
o,
c // A )
by A3, A4, A15, A16, AFF_1:66;
A40:
o,
c // N
by A5, A13, A17, AFF_1:66;
o,
a // A
by A3, A9, A15, AFF_1:66;
hence
contradiction
by A3, A4, A5, A6, A8, A18, A19, A39, A40, AFF_1:59, AFF_1:67;
:: thesis: verum
end; A41:
a',
c' // a1',
c1'
by A21, ANALMETR:48;
A42:
a',
b' // a1',
b1'
by A20, ANALMETR:48;
A43:
(
o' <> a1' &
o' <> b1' &
o' <> c1' )
proof
A44:
now assume A45:
o' = a1'
;
:: thesis: contradictionA46:
o = c1
proof
A47:
not
LIN c,
a,
o
proof
assume
LIN c,
a,
o
;
:: thesis: contradiction
then
LIN o,
a,
c
by AFF_1:15;
then
c in A
by A3, A6, A9, A15, AFF_1:39;
then A48:
o,
c // A
by A3, A15, AFF_1:66;
o,
c // N
by A5, A13, A17, AFF_1:66;
hence
contradiction
by A3, A5, A8, A19, A48, AFF_1:59, AFF_1:67;
:: thesis: verum
end;
assume A49:
o <> c1
;
:: thesis: contradiction
A50:
o,
c // o,
c1
by A5, A13, A14, A17, AFF_1:53, AFF_1:55;
then
a,
c // o,
c
by A21, A45, A49, AFF_1:14;
then
c,
a // c,
o
by AFF_1:13;
then
LIN c,
a,
o
by AFF_1:def 1;
then
LIN o,
a,
c
by AFF_1:15;
then
o,
a // o,
c
by AFF_1:def 1;
then
o,
a // o,
c1
by A8, A50, AFF_1:14;
then
LIN o,
a,
c1
by AFF_1:def 1;
then
LIN a,
o,
c1
by AFF_1:15;
then A51:
a,
o // a,
c1
by AFF_1:def 1;
LIN c,
o,
c1
by A25, AFF_1:15;
hence
contradiction
by A49, A47, A51, AFF_1:23;
:: thesis: verum
end;
o = b1
proof
A52:
not
LIN b,
a,
o
proof
assume
LIN b,
a,
o
;
:: thesis: contradiction
then
LIN o,
a,
b
by AFF_1:15;
then
b in A
by A3, A6, A9, A15, AFF_1:39;
then A53:
o,
b // A
by A3, A15, AFF_1:66;
o,
b // M
by A4, A11, A16, AFF_1:66;
hence
contradiction
by A3, A4, A7, A18, A53, AFF_1:59, AFF_1:67;
:: thesis: verum
end;
assume A54:
o <> b1
;
:: thesis: contradiction
A55:
o,
b1 // o,
b
by A4, A11, A12, A16, AFF_1:53, AFF_1:55;
then
a,
b // o,
b
by A20, A45, A54, AFF_1:14;
then
b,
a // b,
o
by AFF_1:13;
then
LIN b,
a,
o
by AFF_1:def 1;
then
LIN o,
a,
b
by AFF_1:15;
then
o,
a // o,
b
by AFF_1:def 1;
then
o,
a // o,
b1
by A7, A55, AFF_1:14;
then
LIN o,
a,
b1
by AFF_1:def 1;
then
LIN a,
o,
b1
by AFF_1:15;
then A56:
a,
o // a,
b1
by AFF_1:def 1;
LIN b,
o,
b1
by A22, AFF_1:15;
hence
contradiction
by A54, A52, A56, AFF_1:23;
:: thesis: verum
end; hence
contradiction
by A27, A46, AFF_1:12;
:: thesis: verum end;
A57:
now A58:
not
LIN a,
b,
o
proof
assume
LIN a,
b,
o
;
:: thesis: contradiction
then
LIN o,
a,
b
by AFF_1:15;
then
b in A
by A3, A6, A9, A15, AFF_1:39;
then A59:
o,
b // A
by A3, A15, AFF_1:66;
o,
b // M
by A4, A11, A16, AFF_1:66;
hence
contradiction
by A3, A4, A7, A18, A59, AFF_1:59, AFF_1:67;
:: thesis: verum
end; A60:
a1,
o // a,
o
by A3, A9, A10, A15, AFF_1:53, AFF_1:55;
assume
o' = b1'
;
:: thesis: contradictionthen
a,
b // a,
o
by A20, A44, A60, AFF_1:14;
then
LIN a,
b,
o
by AFF_1:def 1;
then
LIN o,
b,
a
by AFF_1:15;
then
o,
b // o,
a
by AFF_1:def 1;
then
o,
b // a,
o
by AFF_1:13;
then
o,
b // a1,
o
by A6, A60, AFF_1:14;
then
o,
b // o,
a1
by AFF_1:13;
then
LIN o,
b,
a1
by AFF_1:def 1;
then
LIN b,
o,
a1
by AFF_1:15;
then A61:
b,
o // b,
a1
by AFF_1:def 1;
LIN a,
o,
a1
by A24, AFF_1:15;
hence
contradiction
by A44, A58, A61, AFF_1:23;
:: thesis: verum end;
A62:
now A63:
not
LIN a,
c,
o
proof
assume
LIN a,
c,
o
;
:: thesis: contradiction
then
LIN o,
a,
c
by AFF_1:15;
then
c in A
by A3, A6, A9, A15, AFF_1:39;
then A64:
o,
c // A
by A3, A15, AFF_1:66;
o,
c // N
by A5, A13, A17, AFF_1:66;
hence
contradiction
by A3, A5, A8, A19, A64, AFF_1:59, AFF_1:67;
:: thesis: verum
end; A65:
a1,
o // a,
o
by A3, A9, A10, A15, AFF_1:53, AFF_1:55;
assume
o' = c1'
;
:: thesis: contradictionthen
a,
c // a,
o
by A21, A44, A65, AFF_1:14;
then
LIN a,
c,
o
by AFF_1:def 1;
then
LIN o,
c,
a
by AFF_1:15;
then
o,
c // o,
a
by AFF_1:def 1;
then
o,
c // a,
o
by AFF_1:13;
then
o,
c // a1,
o
by A6, A65, AFF_1:14;
then
o,
c // o,
a1
by AFF_1:13;
then
LIN o,
c,
a1
by AFF_1:def 1;
then
LIN c,
o,
a1
by AFF_1:15;
then A66:
c,
o // c,
a1
by AFF_1:def 1;
LIN a,
o,
a1
by A24, AFF_1:15;
hence
contradiction
by A44, A63, A66, AFF_1:23;
:: thesis: verum end;
assume
( not
o' <> a1' or not
o' <> b1' or not
o' <> c1' )
;
:: thesis: contradiction
hence
contradiction
by A44, A57, A62;
:: thesis: verum
end;
LIN o',
a',
a1'
by A24, ANALMETR:55;
then
b',
c' // b1',
c1'
by A2, A6, A7, A8, A23, A26, A43, A28, A42, A41, CONAFFM:def 1;
hence
contradiction
by A27, ANALMETR:48;
:: thesis: verum end;
hence
Af X is
Desarguesian
by AFF_2:def 4;
:: thesis: verum
end;
( Af X is Desarguesian implies X is satisfying_DES )
proof
assume A67:
Af X is
Desarguesian
;
:: thesis: X is satisfying_DES
now let o',
a',
a1',
b',
b1',
c',
c1' be
Element of
X;
:: thesis: ( o' <> a' & o' <> a1' & o' <> b' & o' <> b1' & o' <> c' & o' <> c1' & not LIN b',b1',a' & not LIN a',a1',c' & LIN o',a',a1' & LIN o',b',b1' & LIN o',c',c1' & a',b' // a1',b1' & a',c' // a1',c1' implies b',c' // b1',c1' )assume that A68:
o' <> a'
and
o' <> a1'
and A69:
o' <> b'
and
o' <> b1'
and A70:
o' <> c'
and
o' <> c1'
and A71:
not
LIN b',
b1',
a'
and A72:
not
LIN a',
a1',
c'
and A73:
LIN o',
a',
a1'
and A74:
LIN o',
b',
b1'
and A75:
LIN o',
c',
c1'
and A76:
a',
b' // a1',
b1'
and A77:
a',
c' // a1',
c1'
;
:: thesis: b',c' // b1',c1'reconsider o =
o',
a =
a',
a1 =
a1',
b =
b',
b1 =
b1',
c =
c',
c1 =
c1' as
Element of
(Af X) by ANALMETR:47;
A78:
not
LIN a,
a1,
c
by A72, ANALMETR:55;
A79:
a,
c // a1,
c1
by A77, ANALMETR:48;
A80:
a,
b // a1,
b1
by A76, ANALMETR:48;
LIN o,
b,
b1
by A74, ANALMETR:55;
then consider M being
Subset of
(Af X) such that A81:
M is
being_line
and A82:
o in M
and A83:
b in M
and A84:
b1 in M
by AFF_1:33;
LIN o,
c,
c1
by A75, ANALMETR:55;
then consider N being
Subset of
(Af X) such that A85:
N is
being_line
and A86:
o in N
and A87:
c in N
and A88:
c1 in N
by AFF_1:33;
LIN o,
a,
a1
by A73, ANALMETR:55;
then consider A being
Subset of
(Af X) such that A89:
A is
being_line
and A90:
o in A
and A91:
a in A
and A92:
a1 in A
by AFF_1:33;
A93:
not
LIN b,
b1,
a
by A71, ANALMETR:55;
(
A <> M &
A <> N )
proof
assume
( not
A <> M or not
A <> N )
;
:: thesis: contradiction
then
(
b,
b1 // b,
a or
a,
a1 // a,
c )
by A89, A91, A92, A83, A84, A87, AFF_1:53, AFF_1:55;
hence
contradiction
by A93, A78, AFF_1:def 1;
:: thesis: verum
end; then
b,
c // b1,
c1
by A67, A68, A69, A70, A89, A90, A91, A92, A81, A82, A83, A84, A85, A86, A87, A88, A80, A79, AFF_2:def 4;
hence
b',
c' // b1',
c1'
by ANALMETR:48;
:: thesis: verum end;
hence
X is
satisfying_DES
by CONAFFM:def 1;
:: thesis: verum
end;
hence
( X is satisfying_DES iff Af X is Desarguesian )
by A1; :: thesis: verum