let X be OrtAfPl; ( X is satisfying_DES iff AffinStruct(# the U1 of X, the CONGR of X #) is Desarguesian )
A1:
( X is satisfying_DES implies AffinStruct(# the U1 of X, the CONGR of X #) is Desarguesian )
proof
assume A2:
X is
satisfying_DES
;
AffinStruct(# the U1 of X, the CONGR of X #) is Desarguesian
now for A, M, N being Subset of AffinStruct(# the U1 of X, the CONGR of X #)
for o, a, b, c, a1, b1, c1 being Element of AffinStruct(# the U1 of X, the CONGR of 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 A,
M,
N be
Subset of
AffinStruct(# the
U1 of
X, the
CONGR of
X #);
for o, a, b, c, a1, b1, c1 being Element of AffinStruct(# the U1 of X, the CONGR of 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
AffinStruct(# the
U1 of
X, the
CONGR of
X #);
( 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
;
b,c // b1,c1reconsider o9 =
o,
a9 =
a,
a19 =
a1,
b9 =
b,
b19 =
b1,
c9 =
c,
c19 =
c1 as
Element of
X ;
o,
b // o,
b1
by A4, A11, A12, A16, AFF_1:39, AFF_1:41;
then A22:
LIN o,
b,
b1
by AFF_1:def 1;
then A23:
LIN o9,
b9,
b19
by ANALMETR:40;
o,
a // o,
a1
by A3, A9, A10, A15, AFF_1:39, AFF_1:41;
then A24:
LIN o,
a,
a1
by AFF_1:def 1;
o,
c // o,
c1
by A5, A13, A14, A17, AFF_1:39, AFF_1:41;
then A25:
LIN o,
c,
c1
by AFF_1:def 1;
then A26:
LIN o9,
c9,
c19
by ANALMETR:40;
assume A27:
not
b,
c // b1,
c1
;
contradictionA28:
( not
LIN b9,
b19,
a9 & not
LIN a9,
a19,
c9 )
proof
A29:
a <> a1
proof
assume A30:
a = a1
;
contradiction
A31:
c = c1
proof
A32:
not
LIN o,
a,
c
proof
assume
LIN o,
a,
c
;
contradiction
then
c in A
by A3, A6, A9, A15, AFF_1:25;
then A33:
o,
c // A
by A3, A15, AFF_1:52;
o,
c // N
by A5, A13, A17, AFF_1:52;
hence
contradiction
by A3, A5, A8, A19, A33, AFF_1:45, AFF_1:53;
verum
end;
assume
c <> c1
;
contradiction
hence
contradiction
by A21, A25, A30, A32, AFF_1:14;
verum
end;
b = b1
proof
A34:
not
LIN o,
a,
b
proof
assume
LIN o,
a,
b
;
contradiction
then
b in A
by A3, A6, A9, A15, AFF_1:25;
then A35:
o,
b // A
by A3, A15, AFF_1:52;
o,
b // M
by A4, A11, A16, AFF_1:52;
hence
contradiction
by A3, A4, A7, A18, A35, AFF_1:45, AFF_1:53;
verum
end;
assume
b <> b1
;
contradiction
hence
contradiction
by A20, A22, A30, A34, AFF_1:14;
verum
end;
hence
contradiction
by A27, A31, AFF_1:2;
verum
end;
A36:
b <> b1
proof
A37:
not
LIN o,
b,
a
proof
assume
LIN o,
b,
a
;
contradiction
then
a in M
by A4, A7, A11, A16, AFF_1:25;
then A38:
o,
a // M
by A4, A16, AFF_1:52;
o,
a // A
by A3, A9, A15, AFF_1:52;
hence
contradiction
by A3, A4, A6, A18, A38, AFF_1:45, AFF_1:53;
verum
end;
assume
b = b1
;
contradiction
then
b,
a // b,
a1
by A20, AFF_1:4;
hence
contradiction
by A24, A29, A37, AFF_1:14;
verum
end;
assume
(
LIN b9,
b19,
a9 or
LIN a9,
a19,
c9 )
;
contradiction
then
(
LIN b,
b1,
a or
LIN a,
a1,
c )
by ANALMETR:40;
then
(
a in M or
c in A )
by A9, A10, A11, A12, A15, A16, A29, A36, AFF_1:25;
then A39:
(
o,
a // M or
o,
c // A )
by A3, A4, A15, A16, AFF_1:52;
A40:
o,
c // N
by A5, A13, A17, AFF_1:52;
o,
a // A
by A3, A9, A15, AFF_1:52;
hence
contradiction
by A3, A4, A5, A6, A8, A18, A19, A39, A40, AFF_1:45, AFF_1:53;
verum
end; A41:
a9,
c9 // a19,
c19
by A21, ANALMETR:36;
A42:
a9,
b9 // a19,
b19
by A20, ANALMETR:36;
A43:
(
o9 <> a19 &
o9 <> b19 &
o9 <> c19 )
proof
A44:
now not o9 = a19assume A45:
o9 = a19
;
contradictionA46:
o = c1
proof
A47:
not
LIN c,
a,
o
proof
assume
LIN c,
a,
o
;
contradiction
then
LIN o,
a,
c
by AFF_1:6;
then
c in A
by A3, A6, A9, A15, AFF_1:25;
then A48:
o,
c // A
by A3, A15, AFF_1:52;
o,
c // N
by A5, A13, A17, AFF_1:52;
hence
contradiction
by A3, A5, A8, A19, A48, AFF_1:45, AFF_1:53;
verum
end;
assume A49:
o <> c1
;
contradiction
A50:
o,
c // o,
c1
by A5, A13, A14, A17, AFF_1:39, AFF_1:41;
then
a,
c // o,
c
by A21, A45, A49, AFF_1:5;
then
c,
a // c,
o
by AFF_1:4;
then
LIN c,
a,
o
by AFF_1:def 1;
then
LIN o,
a,
c
by AFF_1:6;
then
o,
a // o,
c
by AFF_1:def 1;
then
o,
a // o,
c1
by A8, A50, AFF_1:5;
then
LIN o,
a,
c1
by AFF_1:def 1;
then
LIN a,
o,
c1
by AFF_1:6;
then A51:
a,
o // a,
c1
by AFF_1:def 1;
LIN c,
o,
c1
by A25, AFF_1:6;
hence
contradiction
by A49, A47, A51, AFF_1:14;
verum
end;
o = b1
proof
A52:
not
LIN b,
a,
o
proof
assume
LIN b,
a,
o
;
contradiction
then
LIN o,
a,
b
by AFF_1:6;
then
b in A
by A3, A6, A9, A15, AFF_1:25;
then A53:
o,
b // A
by A3, A15, AFF_1:52;
o,
b // M
by A4, A11, A16, AFF_1:52;
hence
contradiction
by A3, A4, A7, A18, A53, AFF_1:45, AFF_1:53;
verum
end;
assume A54:
o <> b1
;
contradiction
A55:
o,
b1 // o,
b
by A4, A11, A12, A16, AFF_1:39, AFF_1:41;
then
a,
b // o,
b
by A20, A45, A54, AFF_1:5;
then
b,
a // b,
o
by AFF_1:4;
then
LIN b,
a,
o
by AFF_1:def 1;
then
LIN o,
a,
b
by AFF_1:6;
then
o,
a // o,
b
by AFF_1:def 1;
then
o,
a // o,
b1
by A7, A55, AFF_1:5;
then
LIN o,
a,
b1
by AFF_1:def 1;
then
LIN a,
o,
b1
by AFF_1:6;
then A56:
a,
o // a,
b1
by AFF_1:def 1;
LIN b,
o,
b1
by A22, AFF_1:6;
hence
contradiction
by A54, A52, A56, AFF_1:14;
verum
end; hence
contradiction
by A27, A46, AFF_1:3;
verum end;
A57:
now not o9 = b19A58:
not
LIN a,
b,
o
proof
assume
LIN a,
b,
o
;
contradiction
then
LIN o,
a,
b
by AFF_1:6;
then
b in A
by A3, A6, A9, A15, AFF_1:25;
then A59:
o,
b // A
by A3, A15, AFF_1:52;
o,
b // M
by A4, A11, A16, AFF_1:52;
hence
contradiction
by A3, A4, A7, A18, A59, AFF_1:45, AFF_1:53;
verum
end; A60:
a1,
o // a,
o
by A3, A9, A10, A15, AFF_1:39, AFF_1:41;
assume
o9 = b19
;
contradictionthen
a,
b // a,
o
by A20, A44, A60, AFF_1:5;
then
LIN a,
b,
o
by AFF_1:def 1;
then
LIN o,
b,
a
by AFF_1:6;
then
o,
b // o,
a
by AFF_1:def 1;
then
o,
b // a,
o
by AFF_1:4;
then
o,
b // a1,
o
by A6, A60, AFF_1:5;
then
o,
b // o,
a1
by AFF_1:4;
then
LIN o,
b,
a1
by AFF_1:def 1;
then
LIN b,
o,
a1
by AFF_1:6;
then A61:
b,
o // b,
a1
by AFF_1:def 1;
LIN a,
o,
a1
by A24, AFF_1:6;
hence
contradiction
by A44, A58, A61, AFF_1:14;
verum end;
A62:
now not o9 = c19A63:
not
LIN a,
c,
o
proof
assume
LIN a,
c,
o
;
contradiction
then
LIN o,
a,
c
by AFF_1:6;
then
c in A
by A3, A6, A9, A15, AFF_1:25;
then A64:
o,
c // A
by A3, A15, AFF_1:52;
o,
c // N
by A5, A13, A17, AFF_1:52;
hence
contradiction
by A3, A5, A8, A19, A64, AFF_1:45, AFF_1:53;
verum
end; A65:
a1,
o // a,
o
by A3, A9, A10, A15, AFF_1:39, AFF_1:41;
assume
o9 = c19
;
contradictionthen
a,
c // a,
o
by A21, A44, A65, AFF_1:5;
then
LIN a,
c,
o
by AFF_1:def 1;
then
LIN o,
c,
a
by AFF_1:6;
then
o,
c // o,
a
by AFF_1:def 1;
then
o,
c // a,
o
by AFF_1:4;
then
o,
c // a1,
o
by A6, A65, AFF_1:5;
then
o,
c // o,
a1
by AFF_1:4;
then
LIN o,
c,
a1
by AFF_1:def 1;
then
LIN c,
o,
a1
by AFF_1:6;
then A66:
c,
o // c,
a1
by AFF_1:def 1;
LIN a,
o,
a1
by A24, AFF_1:6;
hence
contradiction
by A44, A63, A66, AFF_1:14;
verum end;
assume
( not
o9 <> a19 or not
o9 <> b19 or not
o9 <> c19 )
;
contradiction
hence
contradiction
by A44, A57, A62;
verum
end;
LIN o9,
a9,
a19
by A24, ANALMETR:40;
then
b9,
c9 // b19,
c19
by A2, A6, A7, A8, A23, A26, A43, A28, A42, A41, CONAFFM:def 1;
hence
contradiction
by A27, ANALMETR:36;
verum end;
hence
AffinStruct(# the
U1 of
X, the
CONGR of
X #) is
Desarguesian
by AFF_2:def 4;
verum
end;
( AffinStruct(# the U1 of X, the CONGR of X #) is Desarguesian implies X is satisfying_DES )
proof
assume A67:
AffinStruct(# the
U1 of
X, the
CONGR of
X #) is
Desarguesian
;
X is satisfying_DES
now for o9, a9, a19, b9, b19, c9, c19 being Element of X st o9 <> a9 & o9 <> a19 & o9 <> b9 & o9 <> b19 & o9 <> c9 & o9 <> c19 & not LIN b9,b19,a9 & not LIN a9,a19,c9 & LIN o9,a9,a19 & LIN o9,b9,b19 & LIN o9,c9,c19 & a9,b9 // a19,b19 & a9,c9 // a19,c19 holds
b9,c9 // b19,c19let o9,
a9,
a19,
b9,
b19,
c9,
c19 be
Element of
X;
( o9 <> a9 & o9 <> a19 & o9 <> b9 & o9 <> b19 & o9 <> c9 & o9 <> c19 & not LIN b9,b19,a9 & not LIN a9,a19,c9 & LIN o9,a9,a19 & LIN o9,b9,b19 & LIN o9,c9,c19 & a9,b9 // a19,b19 & a9,c9 // a19,c19 implies b9,c9 // b19,c19 )assume that A68:
o9 <> a9
and
o9 <> a19
and A69:
o9 <> b9
and
o9 <> b19
and A70:
o9 <> c9
and
o9 <> c19
and A71:
not
LIN b9,
b19,
a9
and A72:
not
LIN a9,
a19,
c9
and A73:
LIN o9,
a9,
a19
and A74:
LIN o9,
b9,
b19
and A75:
LIN o9,
c9,
c19
and A76:
a9,
b9 // a19,
b19
and A77:
a9,
c9 // a19,
c19
;
b9,c9 // b19,c19reconsider o =
o9,
a =
a9,
a1 =
a19,
b =
b9,
b1 =
b19,
c =
c9,
c1 =
c19 as
Element of
AffinStruct(# the
U1 of
X, the
CONGR of
X #) ;
A78:
not
LIN a,
a1,
c
by A72, ANALMETR:40;
A79:
a,
c // a1,
c1
by A77, ANALMETR:36;
A80:
a,
b // a1,
b1
by A76, ANALMETR:36;
LIN o,
b,
b1
by A74, ANALMETR:40;
then consider M being
Subset of
AffinStruct(# the
U1 of
X, the
CONGR of
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:21;
LIN o,
c,
c1
by A75, ANALMETR:40;
then consider N being
Subset of
AffinStruct(# the
U1 of
X, the
CONGR of
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:21;
LIN o,
a,
a1
by A73, ANALMETR:40;
then consider A being
Subset of
AffinStruct(# the
U1 of
X, the
CONGR of
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:21;
A93:
not
LIN b,
b1,
a
by A71, ANALMETR:40;
(
A <> M &
A <> N )
proof
assume
( not
A <> M or not
A <> N )
;
contradiction
then
(
b,
b1 // b,
a or
a,
a1 // a,
c )
by A89, A91, A92, A83, A84, A87, AFF_1:39, AFF_1:41;
hence
contradiction
by A93, A78, AFF_1:def 1;
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
b9,
c9 // b19,
c19
by ANALMETR:36;
verum end;
hence
X is
satisfying_DES
by CONAFFM:def 1;
verum
end;
hence
( X is satisfying_DES iff AffinStruct(# the U1 of X, the CONGR of X #) is Desarguesian )
by A1; verum