:: Fundamental Types of Metric Affine Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received April 17, 1991
:: Copyright (c) 1991-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 ANALMETR, SUBSET_1, SYMSP_1, AFF_2, VECTSP_1, TRANSGEO, ANALOAF,
DIRAF, STRUCT_0, AFF_1, INCSP_1, CONAFFM, CONMETR, RLVECT_1, ARYTM_1,
ARYTM_3, REAL_1, RELAT_1, CARD_1, MCART_1, SUPINF_2, PARSP_1, EUCLMETR;
notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, STRUCT_0, REAL_1,
RLVECT_1, ANALOAF, DIRAF, AFF_1, AFF_2, ANALMETR, GEOMTRAP, PAPDESAF,
CONMETR, CONAFFM;
constructors REAL_1, AFF_1, AFF_2, TRANSLAC, GEOMTRAP, CONAFFM, CONMETR;
registrations ANALMETR, PAPDESAF, ORDINAL1, XREAL_0, STRUCT_0;
requirements NUMERALS, SUBSET, ARITHM;
equalities RLVECT_1;
theorems RLVECT_1, AFF_1, AFF_4, AFPROJ, ANALOAF, ANALMETR, GEOMTRAP,
PAPDESAF, CONMETR, CONAFFM, AFF_2, RLSUB_2, XCMPLX_1;
begin
definition
let IT be OrtAfSp;
attr IT is Euclidean means
for a,b,c,d being Element
of IT st a,b _|_ c,d & b,c _|_ a,d holds b,d _|_ a,c;
end;
definition
let IT be OrtAfSp;
attr IT is Pappian means
:Def2:
the AffinStruct of IT is Pappian;
end;
definition
let IT be OrtAfSp;
attr IT is Desarguesian means
:Def3:
the AffinStruct of IT is Desarguesian;
end;
definition
let IT be OrtAfSp;
attr IT is Fanoian means
:Def4:
the AffinStruct of IT is Fanoian;
end;
definition
let IT be OrtAfSp;
attr IT is Moufangian means
:Def5:
the AffinStruct of IT is Moufangian;
end;
definition
let IT be OrtAfSp;
attr IT is translation means
:Def6:
the AffinStruct of IT is translational;
end;
definition
let IT be OrtAfSp;
attr IT is Homogeneous means
for o,a,a1,b,b1,c,c1 being Element of IT
st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 &
not o,c // o,a & not o,a // o,b holds b,c _|_ b1,c1;
end;
reserve MS for OrtAfPl;
reserve MP for OrtAfSp;
theorem Th1:
for a,b,c being Element of MP st not LIN a,b,c holds a<>b & b<>c & a<>c
proof
let a,b,c be Element of MP such that
A1: not LIN a,b,c;
reconsider b9=b,a9=a,c9=c as Element of the AffinStruct of MP;
assume not thesis;
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A1,ANALMETR:40;
end;
theorem Th2:
for a,b,c,d being Element of MS, K being Subset of the carrier of
MS st a,b _|_ K & c,d _|_ K holds a,b // c,d & a,b // d,c
proof
let a,b,c,d be Element of MS, K be Subset of MS such that
A1: a,b _|_ K and
A2: c,d _|_ K;
reconsider K9=K as Subset of the AffinStruct of MS;
K is being_line by A1,ANALMETR:44;
then K9 is being_line by ANALMETR:43;
then consider p9,q9 being Element of the AffinStruct of MS such that
A3: p9 in K9 & q9 in K9 and
A4: p9 <> q9 by AFF_1:19;
reconsider p=p9,q=q9 as Element of MS;
a,b _|_ p,q & c,d _|_ p,q by A1,A2,A3,ANALMETR:53;
hence a,b // c,d by A4,ANALMETR:63;
hence thesis by ANALMETR:59;
end;
theorem
for a,b being Element of MS, A,K being Subset of the carrier of MS st
a<>b & (a,b _|_ K or b,a _|_ K) & a,b _|_ A holds K // A
proof
let a,b be Element of MS, A,K be Subset of MS such that
A1: a<>b and
A2: a,b _|_ K or b,a _|_ K and
A3: a,b _|_ A;
a,b _|_ K by A2,ANALMETR:49;
then consider p,q being Element of MS such that
A4: p<>q & K = Line(p,q) and
A5: a,b _|_ p,q by ANALMETR:def 13;
consider r,s being Element of MS such that
A6: r<>s & A = Line(r,s) and
A7: a,b _|_ r,s by A3,ANALMETR:def 13;
p,q // r,s by A1,A5,A7,ANALMETR:63;
hence thesis by A4,A6,ANALMETR:def 15;
end;
theorem Th4:
for x,y,z being Element of MP st LIN x,y,z holds LIN x,z,y & LIN
y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x
proof
let x,y,z be Element of MP such that
A1: LIN x,y,z;
reconsider x9=x,y9=y,z9=z as Element of the AffinStruct of MP;
A2: LIN x9,y9,z9 by A1,ANALMETR:40;
then
A3: LIN y9,z9,x9 & LIN z9,x9,y9 by AFF_1:6;
A4: LIN z9,y9,x9 by A2,AFF_1:6;
LIN x9,z9,y9 & LIN y9,x9,z9 by A2,AFF_1:6;
hence thesis by A3,A4,ANALMETR:40;
end;
theorem Th5:
for a,b,c being Element of MS st not LIN a,b,c ex d being Element
of MS st d,a _|_ b,c & d,b _|_ a,c
proof
let a,b,c be Element of MS;
set A=Line(a,c),K=Line(b,c);
reconsider A9=A,K9=K as Subset of the AffinStruct of MS;
reconsider a9=a,b9=b,c9=c as Element of the AffinStruct of MS;
K9=Line(b9,c9) by ANALMETR:41;
then
A1: b9 in K9 & c9 in K9 by AFF_1:15;
assume
A2: not LIN a,b,c;
then a<>c by Th1;
then A is being_line by ANALMETR:def 12;
then consider P being Subset of MS such that
A3: b in P and
A4: A _|_ P by CONMETR:3;
b<>c by A2,Th1;
then K is being_line by ANALMETR:def 12;
then consider Q being Subset of MS such that
A5: a in Q and
A6: K _|_ Q by CONMETR:3;
reconsider P9=P,Q9=Q as Subset of the AffinStruct of MS;
Q is being_line by A6,ANALMETR:44;
then
A7: Q9 is being_line by ANALMETR:43;
A8: A9=Line(a9,c9) by ANALMETR:41;
then
A9: c9 in A9 by AFF_1:15;
A10: not P9 // Q9
proof
assume not thesis;
then P // Q by ANALMETR:46;
then A _|_ Q by A4,ANALMETR:52;
then A // K by A6,ANALMETR:65;
then A9 // K9 by ANALMETR:46;
then b9 in A9 by A9,A1,AFF_1:45;
then LIN a9,c9,b9 by A8,AFF_1:def 2;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A2,ANALMETR:40;
end;
P is being_line by A4,ANALMETR:44;
then P9 is being_line by ANALMETR:43;
then consider d9 being Element of the AffinStruct of MS such that
A11: d9 in P9 & d9 in Q9 by A7,A10,AFF_1:58;
reconsider d=d9 as Element of MS;
take d;
a9 in A9 by A8,AFF_1:15;
hence thesis by A3,A4,A5,A6,A9,A1,A11,ANALMETR:56;
end;
theorem Th6:
for a,b,c,d1,d2 being Element of MS st not LIN a,b,c & d1,a _|_ b
,c & d1,b _|_ a,c & d2,a _|_ b,c & d2,b _|_ a,c holds d1=d2
proof
let a,b,c,d1,d2 be Element of MS such that
A1: not LIN a,b,c and
A2: d1,a _|_ b,c and
A3: d1,b _|_ a,c and
A4: d2,a _|_ b,c and
A5: d2,b _|_ a,c;
reconsider a9=a,b9=b,c9=c,d19=d1,d29=d2 as Element of the AffinStruct of MS;
assume
A6: d1<>d2;
b<>c by A1,Th1;
then d1,a // d2,a by A2,A4,ANALMETR:63;
then d19,a9 // d29,a9 by ANALMETR:36;
then a9,d19 // a9, d29 by AFF_1:4;
then LIN a9,d19,d29 by AFF_1:def 1;
then
A7: LIN d19,d29,a9 by AFF_1:6;
a<>c by A1,Th1;
then d1,b // d2,b by A3,A5,ANALMETR:63;
then d19,b9 // d29,b9 by ANALMETR:36;
then b9,d19 // b9,d29 by AFF_1:4;
then LIN b9,d19,d29 by AFF_1:def 1;
then
A8: LIN d19,d29,b9 by AFF_1:6;
set X9=Line(a9,b9);
reconsider X=X9 as Subset of MS;
A9: b<>a by A1,Th1;
then
A10: X9 is being_line by AFF_1:def 3;
then
A11: X is being_line by ANALMETR:43;
A12: a9 in X9 by AFF_1:15;
A13: b9 in X9 by AFF_1:15;
LIN d19,d29,d29 by AFF_1:7;
then
A14: d2 in X by A6,A9,A7,A8,A10,A12,A13,AFF_1:8,25;
LIN d19,d29,d19 by AFF_1:7;
then
A15: d1 in X by A6,A9,A7,A8,A10,A12,A13,AFF_1:8,25;
a<>d1 or a<>d2 by A6;
then
A16: b,c _|_ X by A2,A4,A12,A15,A14,A11,ANALMETR:55;
b<>d1 or b<>d2 by A6;
then a,c _|_ X by A3,A5,A13,A15,A14,A11,ANALMETR:55;
then a,c // b,c by A16,Th2;
then a9,c9 // b9,c9 by ANALMETR:36;
then c9,b9 // c9,a9 by AFF_1:4;
then LIN c9,b9,a9 by AFF_1:def 1;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A1,ANALMETR:40;
end;
theorem Th7:
for a,b,c,d being Element of MS st a,b _|_ c,d & b,c _|_ a,d &
LIN a,b,c holds (a=c or a=b or b=c)
proof
let a,b,c,d be Element of MS such that
A1: a,b _|_ c,d and
A2: b,c _|_ a,d and
A3: LIN a,b,c;
assume
A4: not thesis;
LIN c,b,a by A3,Th4;
then c,b // c,a by ANALMETR:def 10;
then a,c // b,c by ANALMETR:59;
then
A5: a,c _|_ a,d by A2,A4,ANALMETR:62;
reconsider a9=a,b9=b,c9=c,d9=d as Element of the AffinStruct of MS;
LIN a9,b9,c9 by A3,ANALMETR:40;
then consider A9 being Subset of the AffinStruct of MS such that
A6: A9 is being_line and
A7: a9 in A9 and
A8: b9 in A9 and
A9: c9 in A9 by AFF_1:21;
reconsider A=A9 as Subset of MS;
A10: A is being_line by A6,ANALMETR:43;
then
A11: c,d _|_ A by A1,A4,A7,A8,ANALMETR:55;
a,b // a,c by A3,ANALMETR:def 10;
then a,c _|_ c,d by A1,A4,ANALMETR:62;
then c,d // a,d by A4,A5,ANALMETR:63;
then d,c // d,a by ANALMETR:59;
then LIN d,c,a by ANALMETR:def 10;
then LIN a,c,d by Th4;
then LIN a9,c9,d9 by ANALMETR:40;
then d in A by A4,A6,A7,A9,AFF_1:25;
then
A12: c =d by A9,A11,ANALMETR:51;
a,d _|_ A by A2,A4,A8,A9,A10,ANALMETR:55;
hence contradiction by A4,A7,A9,A12,ANALMETR:51;
end;
theorem Th8:
MS is Euclidean iff MS is satisfying_3H
proof
A1: now
assume
A2: MS is satisfying_3H;
now
let a,b,c,d be Element of MS such that
A3: a,b _|_ c,d and
A4: b,c _|_ a,d;
A5: now
A6: d,a _|_ c,b & d,c _|_ a,b by A3,A4,ANALMETR:61;
assume
A7: not LIN a,b,c;
then consider d1 being Element of MS such that
A8: d1,a _|_ b,c and
A9: d1,b _|_ a,c & d1,c _|_ a,b by A2,CONAFFM:def 3;
A10: not LIN a,c,b by A7,Th4;
d1,a _|_ c,b by A8,ANALMETR:61;
then d,b _|_ a,c by A9,A6,A10,Th6;
hence b,d _|_ a,c by ANALMETR:61;
end;
now
A11: a=c implies b,d _|_ a,c by ANALMETR:58;
A12: b=c implies b,d _|_ a,c by A3,ANALMETR:61;
assume
A13: LIN a,b,c;
a=b implies b,d _|_ a,c by A4,ANALMETR:61;
hence b,d _|_ a,c by A3,A4,A13,A11,A12,Th7;
end;
hence b,d _|_ a,c by A5;
end;
hence MS is Euclidean;
end;
now
assume
A14: MS is Euclidean;
now
let a,b,c be Element of MS;
assume not LIN a,b,c;
then consider d being Element of MS such that
A15: d,a _|_ b,c & d,b _|_ a,c by Th5;
take d;
b,c _|_ a,d & c,a _|_ b,d by A15,ANALMETR:61;
then c,d _|_ b,a by A14;
hence d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b by A15,ANALMETR:61;
end;
hence MS is satisfying_3H by CONAFFM:def 3;
end;
hence thesis by A1;
end;
theorem Th9:
MS is Homogeneous iff MS is satisfying_ODES
by CONAFFM:def 4;
Lm1: MS is satisfying_PAP iff the AffinStruct of MS is Pappian
proof
set AS=the AffinStruct of MS;
A1: now
assume
A2: MS is satisfying_PAP;
now
let M,N be Subset of AS, o,a,b,c,a9,b9,c9 be Element of
AS such that
A3: M is being_line & N is being_line and
A4: M<>N and
A5: o in M & o in N and
A6: o<>a and
A7: o<>a9 & o<>b and
A8: o<>b9 & o<>c & o<>c9 & a in M and
A9: b in M and
A10: c in M and
A11: a9 in N and
A12: b9 in N & c9 in N and
A13: a,b9 // b,a9 and
A14: b,c9 // c,b9;
reconsider M9=M,N9=N as Subset of MS;
reconsider a1=a,b1=b,c1=c,a19=a9,b19=b9,c19=c9 as Element
of MS;
A15: b1,c19 // c1,b19 by A14,ANALMETR:36;
a1,b19 // b1,a19 by A13,ANALMETR:36;
then
A16: b1,a19 // a1,b19 by ANALMETR:59;
A17: M9 is being_line & N9 is being_line by A3,ANALMETR:43;
then ( not a19 in M9)& not b1 in N9 by A4,A5,A7,A9,A11,CONMETR:5;
then c1,a19 // a1,c19 by A2,A5,A6,A8,A9,A10,A11,A12,A17,A16,A15,
CONMETR:def 2;
then a1,c19 // c1,a19 by ANALMETR:59;
hence a,c9 // c,a9 by ANALMETR:36;
end;
hence the AffinStruct of MS is Pappian by AFF_2:def 2;
end;
now
assume
A18: the AffinStruct of MS is Pappian;
now
let o,a1,a2,a3,b1,b2,b3 be Element of MS, M,N be Subset of the carrier
of MS such that
A19: M is being_line & N is being_line and
A20: o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in
N & b3 in N & ( not b2 in M)& not a3 in N & o<>a1 & o<>a2 and
o<>a3 and
A21: o<>b1 and
o<>b2 and
A22: o<>b3 and
A23: a3,b2 // a2,b1 and
A24: a3,b3 // a1,b1;
reconsider M9=M,N9=N as Subset of AS;
reconsider a=a1,b=a2,c = a3,a9=b1,b9=b2,c9=b3 as Element
of AS;
A25: c,c9 // a,a9 by A24,ANALMETR:36;
a2,b1 // a3,b2 by A23,ANALMETR:59;
then
A26: b,a9 // c,b9 by ANALMETR:36;
M9 is being_line & N9 is being_line by A19,ANALMETR:43;
then b,c9 // a,b9 by A18,A20,A21,A22,A26,A25,AFF_2:def 2;
then a2,b3 // a1,b2 by ANALMETR:36;
hence a1,b2 // a2,b3 by ANALMETR:59;
end;
hence MS is satisfying_PAP by CONMETR:def 2;
end;
hence thesis by A1;
end;
theorem Th10:
MS is Pappian iff MS is satisfying_PAP
by Lm1;
Lm2: MS is satisfying_DES iff the AffinStruct of MS is Desarguesian
proof
set AS=the AffinStruct of MS;
A1: now
assume
A2: MS is satisfying_DES;
now
let A,P,C be Subset of AS, o,a,b,c,a9,b9,c9 be Element of
AS such that
A3: o in A and
A4: o in P and
A5: o in C and
A6: o<>a and
A7: o<>b and
A8: o<>c and
A9: a in A and
A10: a9 in A and
A11: b in P and
A12: b9 in P and
A13: c in C and
A14: c9 in C and
A15: A is being_line and
A16: P is being_line and
A17: C is being_line and
A18: A<>P and
A19: A<>C and
A20: a,b // a9,b9 and
A21: a,c // a9,c9;
now
reconsider o1=o,a1=a,b1=b,c1=c,a19=a9,b19=b9,c19=c9 as Element of MS;
assume that
A22: o<>a9 and
A23: a<>a9;
A24: a1,b1 // a19,b19 & a1,c1 // a19,c19 by A20,A21,ANALMETR:36;
A25: b<>b9 by A3,A4,A6,A7,A9,A10,A11,A15,A16,A18,A20,A23,AFF_4:9;
now
assume LIN b,b9,a;
then a in P by A11,A12,A16,A25,AFF_1:25;
hence contradiction by A3,A4,A6,A9,A15,A16,A18,AFF_1:18;
end;
then
A26: not LIN b1,b19,a1 by ANALMETR:40;
LIN o,a,a9 by A3,A9,A10,A15,AFF_1:21;
then
A27: LIN o1,a1,a19 by ANALMETR:40;
now
assume LIN a,a9,c;
then c in A by A9,A10,A15,A23,AFF_1:25;
hence contradiction by A3,A5,A8,A13,A15,A17,A19,AFF_1:18;
end;
then
A28: not LIN a1,a19,c1 by ANALMETR:40;
LIN o,b,b9 by A4,A11,A12,A16,AFF_1:21;
then
A29: LIN o1,b1,b19 by ANALMETR:40;
LIN o,c,c9 by A5,A13,A14,A17,AFF_1:21;
then
A30: LIN o1,c1,c19 by ANALMETR:40;
o1<>b19 & o1<>c19 by A3,A4,A5,A6,A7,A8,A9,A10,A11,A13,A15,A16,A17,A18
,A19,A20,A21,A22,AFF_4:8;
then b1,c1 // b19,c19 by A2,A6,A7,A8,A22,A27,A29,A30,A24,A26,A28,
CONAFFM:def 1;
hence b,c // b9,c9 by ANALMETR:36;
end;
hence
b,c // b9,c9 by A3,A4,A5,A6,A7,A8,A9,A11,A12,A13,A14,A15,A16,A17,A18,A19
,A20,A21,AFPROJ:50;
end;
hence AS is Desarguesian by AFF_2:def 4;
end;
now
assume
A31: AS is Desarguesian;
now
let o,a,a1,b,b1,c,c1 be Element of MS such that
A32: o<>a and
o<>a1 and
A33: o<>b and
o<>b1 and
A34: o<>c and
o<>c1 and
A35: not LIN b,b1,a and
A36: not LIN a,a1,c and
A37: LIN o,a,a1 and
A38: LIN o,b,b1 and
A39: LIN o,c,c1 and
A40: a,b // a1,b1 & a,c // a1,c1;
reconsider o9=o,a9=a,b9=b,c9=c,a19=a1,b19=b1, c19=c1 as Element of AS;
LIN o9,a9,a19 by A37,ANALMETR:40;
then consider A being Subset of AS such that
A41: A is being_line and
A42: o9 in A and
A43: a9 in A and
A44: a19 in A by AFF_1:21;
LIN o9,c9,c19 by A39,ANALMETR:40;
then consider C being Subset of AS such that
A45: C is being_line & o9 in C and
A46: c9 in C and
A47: c19 in C by AFF_1:21;
A48: A<>C
proof
assume A=C;
then LIN a9,a19,c9 by A41,A43,A44,A46,AFF_1:21;
hence contradiction by A36,ANALMETR:40;
end;
LIN o9,b9,b19 by A38,ANALMETR:40;
then consider P being Subset of AS such that
A49: P is being_line and
A50: o9 in P and
A51: b9 in P & b19 in P by AFF_1:21;
A52: A<>P
proof
assume A=P;
then LIN b9,b19,a9 by A43,A49,A51,AFF_1:21;
hence contradiction by A35,ANALMETR:40;
end;
a9,b9 // a19,b19 & a9,c9 // a19,c19 by A40,ANALMETR:36;
then b9,c9 // b19,c19 by A31,A32,A33,A34,A41,A42,A43,A44,A49,A50,A51,A45
,A46,A47,A52,A48,AFF_2:def 4;
hence b,c // b1,c1 by ANALMETR:36;
end;
hence MS is satisfying_DES by CONAFFM:def 1;
end;
hence thesis by A1;
end;
theorem Th11:
MS is Desarguesian iff MS is satisfying_DES
by Lm2;
theorem
MS is Moufangian iff MS is satisfying_TDES
proof
set AS=the AffinStruct of MS;
A1: now
assume
A2: MS is satisfying_TDES;
now
let K be Subset of AS, o,a,b,c,a9,b9,c9 be Element of AS
such that
A3: K is being_line and
A4: o in K and
A5: c in K and
A6: c9 in K and
A7: not a in K and
A8: o<>c and
A9: a<>b and
A10: LIN o,a,a9 and
A11: LIN o,b,b9 and
A12: a,b // a9,b9 and
A13: a,c // a9,c9 and
A14: a,b // K;
reconsider o1=o,a1=a,b1=b,c1=c,a19=a9,b19=b9,c19=c9 as Element of MS;
A15: o1<>b1 & a1,c1 // a19,c19 by A4,A7,A13,A14,AFF_1:35,ANALMETR:36;
A16: not LIN o,a,c
proof
assume not thesis;
then LIN o,c,a by AFF_1:6;
hence contradiction by A3,A4,A5,A7,A8,AFF_1:25;
end;
A17: not LIN o,a,b
proof
set M=Line(a,b);
assume not thesis;
then LIN a,b,o by AFF_1:6;
then
A18: o in M by AFF_1:def 2;
a in M & M // K by A9,A14,AFF_1:15,def 5;
then a in K by A4,A18,AFF_1:45;
hence contradiction by A3,A4,A5,A16,AFF_1:21;
end;
a,b // o,c by A3,A4,A5,A8,A14,AFF_1:27;
then b,a // o,c by AFF_1:4;
then
A19: b1,a1 // o1,c1 by ANALMETR:36;
A20: LIN o1,a1,a19 & LIN o1,b1,b19 by A10,A11,ANALMETR:40;
a1,b1 // a19,b19 by A12,ANALMETR:36;
then
A21: b1,a1 // b19,a19 by ANALMETR:59;
A22: LIN o,c,c9 by A3,A4,A5,A6,AFF_1:21;
then
A23: LIN o1,c1,c19 by ANALMETR:40;
A24: now
assume
A25: a9<>o;
A26: now
assume
A27: a<>a9;
A28: not LIN a1,a19,c1
proof
assume not thesis;
then
A29: LIN a,a9,c by ANALMETR:40;
LIN a,a9,o & LIN a,a9,a by A10,AFF_1:6,7;
hence contradiction by A16,A27,A29,AFF_1:8;
end;
A30: not LIN a1,a19,b1
proof
assume not thesis;
then
A31: LIN a,a9,b by ANALMETR:40;
LIN a,a9,o & LIN a,a9,a by A10,AFF_1:6,7;
hence contradiction by A17,A27,A31,AFF_1:8;
end;
c,a // c9,a9 & not LIN o,c,a by A13,A16,AFF_1:4,6;
then
A32: o1<>c19 by A10,A25,AFF_1:55;
b,a // b9,a9 & not LIN o,b,a by A12,A17,AFF_1:4,6;
then o1<>b19 by A10,A25,AFF_1:55;
then b1,c1 // b19,c19 by A2,A4,A7,A8,A20,A23,A21,A19,A15,A25,A32,A28
,A30,CONMETR:def 5;
hence b,c // b9,c9 by ANALMETR:36;
end;
now
A33: LIN o,c,c by AFF_1:7;
assume
A34: a=a9;
then a,c // a9,c by AFF_1:2;
then
A35: c =c9 by A10,A13,A22,A16,A33,AFF_1:56;
A36: LIN o,b,b by AFF_1:7;
a,b // a9,b by A34,AFF_1:2;
then b=b9 by A10,A11,A12,A17,A36,AFF_1:56;
hence b,c // b9,c9 by A35,AFF_1:2;
end;
hence b,c // b9,c9 by A26;
end;
now
assume a9=o;
then b9=o & c9=o by A11,A12,A13,A22,A16,A17,AFF_1:55;
hence b,c // b9,c9 by AFF_1:3;
end;
hence b,c // b9,c9 by A24;
end;
then AS is Moufangian by AFF_2:def 7;
hence MS is Moufangian;
end;
now
assume MS is Moufangian;
then
A37: AS is Moufangian;
now
let o,a,a1,b,b1,c,c1 be Element of MS such that
o<>a and
o<>a1 and
A38: o<>b and
o<>b1 and
A39: o<>c and
o<>c1 and
A40: not LIN b,b1,a and
A41: not LIN b,b1,c and
A42: LIN o,a,a1 and
A43: LIN o,b,b1 and
A44: LIN o,c,c1 and
A45: a,b // a1,b1 and
A46: a,b // o,c and
A47: b,c // b1,c1;
reconsider o9=o,a9=a,a19=a1,b9=b,b19=b1,c9=c,c19=c1 as Element of AS;
set K=Line(o9,c9);
A48: K is being_line by A39,AFF_1:def 3;
a9,b9 // o9,c9 by A46,ANALMETR:36;
then a9,b9 // K by A39,AFF_1:def 4;
then
A49: b9,a9 // K by AFF_1:34;
a9,b9 // a19,b19 by A45,ANALMETR:36;
then
A50: b9,a9 // b19,a19 by AFF_1:4;
A51: c9 in K by AFF_1:15;
A52: LIN o9,a9,a19 & b9,c9 // b19,c19 by A42,A47,ANALMETR:36,40;
A53: b9<>a9 by A40,Th1;
A54: o9 in K by AFF_1:15;
A55: LIN o9,b9,b19 by A43,ANALMETR:40;
A56: not b9 in K
proof
assume
A57: b9 in K;
then b19 in K by A38,A48,A54,A55,AFF_1:25;
then LIN b9,b19,c9 by A48,A51,A57,AFF_1:21;
hence contradiction by A41,ANALMETR:40;
end;
LIN o9,c9,c19 by A44,ANALMETR:40;
then c19 in K by A39,A48,A54,A51,AFF_1:25;
then a9,c9 // a19,c19 by A37,A39,A48,A54,A51,A55,A56,A49,A50,A52,A53,
AFF_2:def 7;
hence a,c // a1,c1 by ANALMETR:36;
end;
hence MS is satisfying_TDES by CONMETR:def 5;
end;
hence thesis by A1;
end;
Lm3: MS is satisfying_des iff the AffinStruct of MS is translational
proof
set AS=the AffinStruct of MS;
A1: now
assume
A2: MS is satisfying_des;
now
let A,P,C be Subset of AS, a,b,c,a9,b9,c9 be Element of AS such that
A3: A // P and
A4: A // C and
A5: a in A and
A6: a9 in A and
A7: b in P and
A8: b9 in P and
A9: c in C and
A10: c9 in C and
A11: A is being_line and
A12: P is being_line and
A13: C is being_line and
A14: A<>P and
A15: A<>C and
A16: a,b // a9,b9 and
A17: a,c // a9,c9;
A18: not a in C by A4,A5,A15,AFF_1:45;
A19: now
reconsider aa=a,a1=a9,bb=b,b1=b9,cc=c,c1=c9 as Element of MS;
a,a9 // b,b9 by A3,A5,A6,A7,A8,AFF_1:39;
then
A20: aa,a1 // bb,b1 by ANALMETR:36;
a,a9 // c,c9 by A4,A5,A6,A9,A10,AFF_1:39;
then
A21: aa,a1 // cc,c1 by ANALMETR:36;
assume
A22: a<>a9;
A23: not LIN aa,a1,bb
proof
assume not thesis;
then LIN a,a9,b by ANALMETR:40;
then b in A by A5,A6,A11,A22,AFF_1:25;
hence contradiction by A3,A7,A14,AFF_1:45;
end;
A24: not LIN aa,a1,cc
proof
assume not thesis;
then LIN a,a9,c by ANALMETR:40;
then c in A by A5,A6,A11,A22,AFF_1:25;
hence contradiction by A4,A9,A15,AFF_1:45;
end;
aa,bb // a1,b1 & aa,cc // a1,c1 by A16,A17,ANALMETR:36;
then bb,cc // b1,c1 by A2,A23,A24,A20,A21,CONMETR:def 8;
hence b,c // b9,c9 by ANALMETR:36;
end;
A25: not a in P by A3,A5,A14,AFF_1:45;
now
assume
A26: a=a9;
then LIN a,c,c9 by A17,AFF_1:def 1;
then LIN c,c9,a by AFF_1:6;
then
A27: c = c9 by A9,A10,A13,A18,AFF_1:25;
LIN a,b,b9 by A16,A26,AFF_1:def 1;
then LIN b,b9,a by AFF_1:6;
then b = b9 by A7,A8,A12,A25,AFF_1:25;
hence b,c // b9,c9 by A27,AFF_1:2;
end;
hence b,c // b9,c9 by A19;
end;
hence AS is translational by AFF_2:def 11;
end;
now
assume
A28: AS is translational;
now
let a,a1,b,b1,c,c1 be Element of MS such that
A29: ( not LIN a,a1,b)& not LIN a,a1,c and
A30: a,a1 // b,b1 and
A31: a,a1 // c,c1 and
A32: a,b // a1,b1 & a,c // a1,c1;
reconsider a9=a,a19=a1,b9=b,b19=b1,c9=c,c19=c1 as Element of AS;
A33: a9,a19 // b9,b19 by A30,ANALMETR:36;
A34: a9,b9 // a19,b19 & a9,c9 // a19,c19 by A32,ANALMETR:36;
A35: a9,a19 // c9,c19 by A31,ANALMETR:36;
set A=Line(a9,a19);
A36: not a9,a19 // a9,b9 & not a9,a19 // a9,c9
proof
assume not thesis;
then a,a1 // a,b or a,a1 // a,c by ANALMETR:36;
hence contradiction by A29,ANALMETR:def 10;
end;
then
A37: a9<>a19 by AFF_1:3;
then
A38: A is being_line by AFF_1:def 3;
then consider C being Subset of AS such that
A39: c9 in C and
A40: A // C by AFF_1:49;
A41: C is being_line by A40,AFF_1:36;
A42: a9 in A & a19 in A by AFF_1:15;
then
A43: A<>C by A36,A38,A39,AFF_1:51;
A44: a9,a19 // A by A38,A42,AFF_1:23;
then a9,a19 // C by A40,AFF_1:43;
then c9,c19 // C by A35,A37,AFF_1:32;
then
A45: c19 in C by A39,A41,AFF_1:23;
consider P being Subset of AS such that
A46: b9 in P and
A47: A // P by A38,AFF_1:49;
A48: P is being_line by A47,AFF_1:36;
a9,a19 // P by A44,A47,AFF_1:43;
then b9,b19 // P by A33,A37,AFF_1:32;
then
A49: b19 in P by A46,A48,AFF_1:23;
A<>P by A36,A38,A42,A46,AFF_1:51;
then
b9,c9 // b19,c19 by A28,A34,A38,A42,A46,A47,A39,A40,A48,A41,A49,A45,A43,
AFF_2:def 11;
hence b,c // b1,c1 by ANALMETR:36;
end;
hence MS is satisfying_des by CONMETR:def 8;
end;
hence thesis by A1;
end;
theorem
MS is translation iff MS is satisfying_des
by Lm3;
theorem Th14:
MS is Homogeneous implies MS is Desarguesian
proof
assume MS is Homogeneous;
then MS is satisfying_ODES by Th9;
then MS is satisfying_DES by CONAFFM:1;
hence thesis by Th11;
end;
theorem Th15:
MS is Euclidean Desarguesian implies MS is Pappian
proof
assume MS is Euclidean Desarguesian;
then MS is satisfying_3H & MS is satisfying_DES by Th8,Th11;
then MS is satisfying_PAP by CONMETR:13,15;
hence thesis by Th10;
end;
reserve V for RealLinearSpace;
reserve w,y,u,v for VECTOR of V;
theorem Th16:
for o,c,c1,a,a1,a2 being Element of MS st not LIN o,c,a & o<>c1
& o,c _|_ o,c1 & o,a _|_ o,a1 & o,a _|_ o,a2 & c,a _|_ c1,a1 & c,a _|_ c1,a2
holds a1=a2
proof
let o,c,c1,a,a1,a2 be Element of MS such that
A1: not LIN o,c,a and
A2: o<>c1 & o,c _|_ o,c1 and
A3: o,a _|_ o,a1 & o,a _|_ o,a2 and
A4: c,a _|_ c1,a1 & c,a _|_ c1,a2;
reconsider o9=o,a19=a1,a29=a2,c19=c1 as Element of the AffinStruct of MS;
assume
A5: a1<>a2;
o<>a by A1,Th1;
then o,a1 // o,a2 by A3,ANALMETR:63;
then o9,a19 // o9,a29 by ANALMETR:36;
then LIN o9,a19, a29 by AFF_1:def 1;
then
A6: LIN a19,a29,o9 by AFF_1:6;
a<>c by A1,Th1;
then c1,a1 // c1,a2 by A4,ANALMETR:63;
then c19,a19 // c19,a29 by ANALMETR:36;
then LIN c19,a19,a29 by AFF_1:def 1;
then
A7: LIN a19,a29,c19 by AFF_1:6;
LIN a19,a29,a29 by AFF_1:7;
then LIN o9,c19,a29 by A5,A6,A7,AFF_1:8;
then o9,c19 // o9,a29 by AFF_1:def 1;
then o,c1 // o,a2 by ANALMETR:36;
then
A8: o,c _|_ o,a2 by A2,ANALMETR:62;
LIN a19,a29,a19 by AFF_1:7;
then LIN o9,c19,a19 by A5,A6,A7,AFF_1:8;
then o9,c19 // o9,a19 by AFF_1:def 1;
then o,c1 // o,a1 by ANALMETR:36;
then
A9: o,c _|_ o,a1 by A2,ANALMETR:62;
o<>a1 or o<>a2 by A5;
then o,c // o,a by A3,A9,A8,ANALMETR:63;
hence contradiction by A1,ANALMETR:def 10;
end;
theorem
for o,c,c1,a being Element of MS st not LIN o,c,a ex a1 being Element
of MS st o,a _|_ o,a1 & c,a _|_ c1,a1
proof
let o,c,c1,a be Element of MS such that
A1: not LIN o,c,a;
set X=Line(c,a),Y=Line(o,a);
c <>a by A1,Th1;
then
A2: X is being_line by ANALMETR:def 12;
then consider X9 being Subset of MS such that
A3: c1 in X9 and
A4: X _|_ X9 by CONMETR:3;
o<>a by A1,Th1;
then Y is being_line by ANALMETR:def 12;
then consider Y9 being Subset of MS such that
A5: o in Y9 and
A6: Y _|_ Y9 by CONMETR:3;
reconsider X1=X9,Y1=Y9 as Subset of the AffinStruct of MS;
Y9 is being_line by A6,ANALMETR:44;
then
A7: Y1 is being_line by ANALMETR:43;
reconsider o9=o,c9=c,a9=a as Element of the AffinStruct of MS;
A8: X=Line(c9,a9) by ANALMETR:41;
then
A9: a in X by AFF_1:15;
Y=Line(o9,a9) by ANALMETR:41;
then
A10: o in Y & a in Y by AFF_1:15;
A11: c in X by A8,AFF_1:15;
not X9 // Y9
proof
reconsider X1=X,Y1=Y as Subset of the carrier of the AffinStruct of MS;
assume not thesis;
then X9 _|_ Y by A6,ANALMETR:52;
then X // Y by A4,ANALMETR:65;
then X1 // Y1 by ANALMETR:46;
then
A12: o in X by A9,A10,AFF_1:45;
a in X by A8,AFF_1:15;
hence contradiction by A1,A2,A11,A12,CONMETR:4;
end;
then
A13: not X1 // Y1 by ANALMETR:46;
X9 is being_line by A4,ANALMETR:44;
then X1 is being_line by ANALMETR:43;
then consider a19 being Element of the AffinStruct of MS such that
A14: a19 in X1 & a19 in Y1 by A7,A13,AFF_1:58;
reconsider a1=a19 as Element of MS;
take a1;
thus thesis by A3,A4,A5,A6,A11,A9,A10,A14,ANALMETR:56;
end;
Lm4: for u,v,y being VECTOR of V holds (u-y)-(v-y)=u-v & (u+y)-(v+y) = u-v
proof
let u,v,y be VECTOR of V;
thus (u-y)-(v-y) = (u-y)+(y-v) by RLVECT_1:33
.= u-v by ANALOAF:1;
thus (u+y)-(v+y) = (u-(-y))-(v+y) by RLVECT_1:17
.= (u-(-y))-(v-(-y)) by RLVECT_1:17
.= (u-(-y))+((-y)-v) by RLVECT_1:33
.= u-v by ANALOAF:1;
end;
Lm5: Gen w,y implies
for a,b,c being Real holds PProJ(w,y,a*w+b*y,(c*b)*w+(-c*
a)*y) = 0 & a*w+b*y,(c*b)*w+(-c*a)*y are_Ort_wrt w,y
proof
assume
A1: Gen w,y;
let a,b,c be Real;
reconsider a,b,c as Real;
A2: pr2(w,y,a*w+b*y)=b & pr2(w,y,(c*b)*w+(-c*a)*y) = -c*a
by A1,GEOMTRAP:def 5;
pr1(w,y,a*w+b*y)=a & pr1(w,y,(c*b)*w+(-c*a)*y) = c*b
by A1,GEOMTRAP:def 4;
then PProJ (w,y,a*w+b*y,(c*b)*w+(-c*a)*y) = a*(b*c)+b*(-c*a) by A2,
GEOMTRAP:def 6
.= 0;
hence thesis by A1,GEOMTRAP:32;
end;
theorem Th18:
for a,b being Real st Gen w,y & 0.V<>u & 0.V<>v & u,v
are_Ort_wrt w,y & u=a*w+b*y
ex c being Real st c <>0 & v=(c*b)*w+(-c*a)*y
proof
let a,b be Real such that
A1: Gen w,y and
A2: 0.V<>u and
A3: 0.V<>v and
A4: u,v are_Ort_wrt w,y and
A5: u=a*w+b*y;
set v9=b*w+(-a)*y;
v9= (1*b)*w+(-1*a)*y;
then u,v9 are_Ort_wrt w,y by A1,A5,Lm5;
then consider a1,b1 being Real such that
A6: a1*v = b1*v9 and
A7: a1<>0 or b1<>0 by A1,A2,A4,ANALMETR:9;
A8: now
assume
A9: a1=0;
then 0.V = b1*v9 by A6,RLVECT_1:10;
then v9=0.V by A7,A9,RLVECT_1:11;
then b=0 & -a=0 by A1,ANALMETR:def 1;
then u= 0.V + 0*y by A5,RLVECT_1:10
.= 0.V + 0.V by RLVECT_1:10
.= 0.V by RLVECT_1:4;
hence contradiction by A2;
end;
take c =a1"*b1;
A10: now
assume
A11: b1=0;
then 0.V = a1*v by A6,RLVECT_1:10;
hence contradiction by A3,A7,A11,RLVECT_1:11;
end;
now
assume c =0;
then a1"=0 by A10,XCMPLX_1:6;
hence contradiction by A8,XCMPLX_1:202;
end;
hence c <>0;
thus v=(a1")*(b1*v9) by A6,A8,ANALOAF:5
.= c*v9 by RLVECT_1:def 7
.= c*(b*w) + c*((-a)*y) by RLVECT_1:def 5
.= (c*b)*w + c*((-a)*y) by RLVECT_1:def 7
.= (c*b)*w + (c*(-a))*y by RLVECT_1:def 7
.= (c*b)*w + (-c*a)*y;
end;
theorem Th19:
Gen w,y & 0.V<>u & 0.V<>v & u,v are_Ort_wrt w,y implies ex c
being Real st for a,b being Real holds a*w+b*y,(c*b)*w+(-c*a)*y are_Ort_wrt w,y
& (a*w+b*y)-u,((c*b)*w+(-c*a)*y)-v are_Ort_wrt w,y
proof
assume that
A1: Gen w,y and
A2: 0.V<>u & 0.V<>v and
A3: u,v are_Ort_wrt w,y;
consider a1,a2 being Real such that
A4: u=a1*w+a2*y by A1,ANALMETR:def 1;
reconsider a1,a2 as Real;
consider c being Real such that
c <>0 and
A5: v=(c*a2)*w+(-c*a1)*y by A1,A2,A3,A4,Th18;
reconsider c as Real;
take c;
let a,b be Real;
set u9=a*w+b*y,v9=(c*b)*w+(-c*a)*y;
A6: pr1(w,y,u9)=a & pr2(w,y,u9)=b by A1,GEOMTRAP:def 4,def 5;
A7: pr1(w,y,v9) = c*b & pr2(w,y,v9) = -c*a by A1,GEOMTRAP:def 4,def 5;
pr1(w,y,u)=a1 & pr2(w,y,u)=a2 by A1,A4,GEOMTRAP:def 4,def 5;
then
A8: PProJ(w,y,u,v9) = a1*(c*b)+a2*(-c*a) by A7,GEOMTRAP:def 6;
pr1(w,y,v)=c*a2 & pr2(w,y,v)=-c*a1 by A1,A5,GEOMTRAP:def 4,def 5;
then
A9: PProJ(w,y,u9,v) = (c*a2)*a+(-c*a1)*b by A6,GEOMTRAP:def 6;
thus a*w+b*y,(c*b)*w+(-c*a)*y are_Ort_wrt w,y by A1,Lm5;
PProJ(w,y,(a*w+b*y)-u,((c*b)*w+(-c*a)*y)-v) = PProJ(w,y,u9-u,v9)-PProJ(
w,y,u9-u,v) by A1,GEOMTRAP:30
.= (PProJ(w,y,u9,v9)-PProJ(w,y,u,v9)) - PProJ(w,y,u9-u,v) by A1,GEOMTRAP:30
.= (0 - PProJ(w,y,u,v9)) - PProJ(w,y,u9-u,v) by A1,Lm5
.= (-PProJ(w,y,u,v9)) - (PProJ(w,y,u9,v) - PProJ(w,y,u,v)) by A1,
GEOMTRAP:30
.= (-PProJ(w,y,u,v9)) - (PProJ(w,y,u9,v) - 0) by A1,A3,GEOMTRAP:32
.= (-1)*(PProJ(w,y,u,v9) + PProJ(w,y,u9,v));
hence thesis by A1,A8,A9,GEOMTRAP:32;
end;
Lm6: for w,y being VECTOR of V,a,b,c,d being Real
holds (a*w+b*y)-(c*w+d*y) = (a-c)*w+(b-d)*y
proof
let w,y be VECTOR of V, a,b,c,d be Real;
thus (a*w+b*y)-(c*w+d*y) = b*y+(a*w-(c*w+d*y)) by RLVECT_1:def 3
.= b*y+((a*w-c*w)-d*y) by RLVECT_1:27
.= b*y+((a-c)*w-d*y) by RLVECT_1:35
.= ((a-c)*w+b*y)-d*y by RLVECT_1:def 3
.= (a-c)*w+(b*y-d*y) by RLVECT_1:def 3
.= (a-c)*w+(b-d)*y by RLVECT_1:35;
end;
Lm7: Gen w,y implies
for a,b,c,d being Real st a*w + c*y = b*w + d*y holds a =
b & c = d
proof
assume
A1: Gen w,y;
let a,b,c,d be Real;
assume a*w+c*y=b*w+d*y;
then 0.V = (a*w+c*y)-(b*w+d*y) by RLVECT_1:15
.= (a-b)*w+(c-d)*y by Lm6;
then -b + a =0 & -d + c = 0 by A1,ANALMETR:def 1;
hence thesis;
end;
theorem Th20:
Gen w,y & MS = AMSpace(V,w,y) implies MS is satisfying_LIN
proof
assume that
A1: Gen w,y and
A2: MS=AMSpace(V,w,y);
now
let o,a,a1,b,b1,c,c1 be Element of MS such that
A3: o<>a and
o<>a1 and
A4: o<>b and
o<>b1 and
A5: o<>c and
A6: o<>c1 and
a<>b and
A7: o,c _|_ o,c1 and
A8: o,a _|_ o,a1 and
A9: o,b _|_ o,b1 and
A10: not LIN o,c,a and
A11: LIN o,a,b and
LIN o,a1,b1 and
A12: a,c _|_ a1,c1 and
A13: b,c _|_ b1,c1;
reconsider q=o,u1=a,u2=b,u3=c,v3=c1 as VECTOR of V by A2,ANALMETR:19;
consider A1,A2 being Real such that
A14: u1-q=A1*w+A2*y by A1,ANALMETR:def 1;
reconsider A1,A2 as Real;
A15: not LIN o,c,b
proof
reconsider o9=o,a9=a,b9=b,c9=c as Element of the AffinStruct of MS;
assume LIN o,c,b;
then LIN o9,c9,b9 by ANALMETR:40;
then
A16: LIN o9,b9,c9 by AFF_1:6;
LIN o9,a9,b9 by A11,ANALMETR:40;
then
A17: LIN o9,b9,a9 by AFF_1:6;
LIN o9,b9,o9 by AFF_1:7;
then LIN o9,c9,a9 by A4,A16,A17,AFF_1:8;
hence contradiction by A10,ANALMETR:40;
end;
q,u3,q,v3 are_Ort_wrt w,y by A2,A7,ANALMETR:21;
then
A18: u3-q,v3-q are_Ort_wrt w,y by ANALMETR:def 3;
u3-q<>0.V & v3-q<>0.V by A5,A6,RLVECT_1:21;
then consider r being Real such that
A19: for a9,b9 being Real holds a9*w+b9*y,(r*b9)*w+(-r*a9)*y
are_Ort_wrt w,y & (a9*w+b9*y)-(u3-q),((r*b9)*w+(-r*a9)*y)-(v3-q) are_Ort_wrt w,
y by A1,A18,Th19;
o,a // o,b by A11,ANALMETR:def 10;
then q,u1 '||' q,u2 by A2,GEOMTRAP:4;
then q,u1 // q,u2 or q,u1 // u2,q by GEOMTRAP:def 1;
then consider a9,b9 being Real such that
A20: a9*(u1-q)=b9*(u2-q) and
A21: a9<>0 or b9<>0 by ANALMETR:14;
consider B1,B2 being Real such that
A22: u2-q=B1*w+B2*y by A1,ANALMETR:def 1;
reconsider a9,b9,B1,B2 as Real;
set s=b9"*a9;
A23: u1-q<>0.V by A3,RLVECT_1:21;
now
assume
A24: b9=0;
then 0.V = a9*(u1-q) by A20,RLVECT_1:10;
hence contradiction by A23,A21,A24,RLVECT_1:11;
end;
then
A25: u2-q = b9"*(a9*(u1-q)) by A20,ANALOAF:5
.= s*(u1-q) by RLVECT_1:def 7;
then B1*w+B2*y = s*(A1*w)+s*(A2*y) by A14,A22,RLVECT_1:def 5
.= (s*A1)*w + s*(A2*y) by RLVECT_1:def 7
.= (s*A1)*w+(s*A2)*y by RLVECT_1:def 7;
then
A26: B1=s*A1 & B2=s*A2 by A1,Lm7;
set v19=((r*A2)*w+(-r*A1)*y)+q,v29=((r*B2)*w+(-r*B1)*y)+q;
reconsider a19=v19,b19=v29 as Element of MS by A2,ANALMETR:19;
A27: v29-q = (r*B2)*w+(-r*B1)*y by RLSUB_2:61
.= (r*B2)*w+(r*B1)*(-y) by RLVECT_1:24
.= (r*(s*A2))*w - (r*(s*A1))*y by A26,RLVECT_1:25
.= r*((s*A2)*w) - (r*(s*A1))*y by RLVECT_1:def 7
.= r*((s*A2)*w) - r*((s*A1)*y) by RLVECT_1:def 7
.= r*((s*A2)*w - (s*A1)*y) by RLVECT_1:34
.= r*(s*(A2*w) - (s*A1)*y) by RLVECT_1:def 7
.= r*(s*(A2*w) - s*(A1*y)) by RLVECT_1:def 7
.= r*(s*(A2*w - A1*y)) by RLVECT_1:34
.= (s*r)*(A2*w - A1*y) by RLVECT_1:def 7
.= s*(r*(A2*w - A1*y)) by RLVECT_1:def 7
.= s*(r*(A2*w) - r*(A1*y)) by RLVECT_1:34
.= s*((r*A2)*w - r*(A1*y)) by RLVECT_1:def 7
.= s*((r*A2)*w + - (r*A1)*y) by RLVECT_1:def 7
.= s*( (r*A2)*w + (r*A1)*(-y)) by RLVECT_1:25
.= s*((r*A2)*w + (-r*A1)*y) by RLVECT_1:24
.= s*(v19-q) by RLSUB_2:61;
A28: v29-q=(r*B2)*w+(-r*B1)*y by RLSUB_2:61;
then u2-q,v29-q are_Ort_wrt w,y by A19,A22;
then q,u2,q,v29 are_Ort_wrt w,y by ANALMETR:def 3;
then
A29: o,b _|_ o,b19 by A2,ANALMETR:21;
1*(u2-v29) = u2-v29 by RLVECT_1:def 8
.= s*(u1-q)-s*(v19-q) by A25,A27,Lm4
.= s*((u1-q)-(v19-q)) by RLVECT_1:34
.= s*(u1-v19) by Lm4;
then v19,u1 // v29,u2 or v19,u1 // u2,v29 by ANALMETR:14;
then v19,u1 '||' v29,u2 by GEOMTRAP:def 1;
then
A30: a19,a // b19,b by A2,GEOMTRAP:4;
A31: v19-q=(r*A2)*w+(-r*A1)*y by RLSUB_2:61;
then u1-q,v19-q are_Ort_wrt w,y by A19,A14;
then q,u1,q,v19 are_Ort_wrt w,y by ANALMETR:def 3;
then
A32: o,a _|_ o,a19 by A2,ANALMETR:21;
(u2-q)-(u3-q)=u2-u3 & (v29-q)-(v3-q)=v29-v3 by Lm4;
then u2-u3,v29-v3 are_Ort_wrt w,y by A19,A22,A28;
then u3,u2,v3,v29 are_Ort_wrt w,y by ANALMETR:def 3;
then
A33: c,b _|_ c1,b19 by A2,ANALMETR:21;
c,b _|_ c1,b1 by A13,ANALMETR:61;
then
A34: b1=b19 by A6,A7,A9,A15,A29,A33,Th16;
(u1-q)-(u3-q)=u1-u3 & (v19-q)-(v3-q)=v19-v3 by Lm4;
then u1-u3,v19-v3 are_Ort_wrt w,y by A19,A14,A31;
then u3,u1,v3,v19 are_Ort_wrt w,y by ANALMETR:def 3;
then
A35: c,a _|_ c1,a19 by A2,ANALMETR:21;
c,a _|_ c1,a1 by A12,ANALMETR:61;
then a1=a19 by A6,A7,A8,A10,A32,A35,Th16;
hence a,a1 // b,b1 by A34,A30,ANALMETR:59;
end;
hence thesis by CONAFFM:def 5;
end;
theorem Th21:
for o,a,a1,b,b1,c,c1 being Element of MS st o,b _|_ o,b1 & o,c
_|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b & o=
a1 holds b,c _|_ b1,c1
proof
let o,a,a1,b,b1,c,c1 be Element of MS such that
A1: o,b _|_ o,b1 and
A2: o,c _|_ o,c1 and
A3: a,b _|_ a1,b1 and
A4: a,c _|_ a1,c1 and
A5: not o,c // o,a and
A6: not o,a // o,b and
A7: o=a1;
A8: o=c1
proof
assume o<>c1;
then a,c // o,c by A2,A4,A7,ANALMETR:63;
then c,a // c,o by ANALMETR:59;
then LIN c,a,o by ANALMETR:def 10;
then LIN o,c,a by Th4;
hence contradiction by A5,ANALMETR:def 10;
end;
o=b1
proof
assume o<>b1;
then a,b // o,b by A1,A3,A7,ANALMETR:63;
then b,a // b,o by ANALMETR:59;
then LIN b,a,o by ANALMETR:def 10;
then LIN o,a,b by Th4;
hence contradiction by A6,ANALMETR:def 10;
end;
hence thesis by A8,ANALMETR:58;
end;
theorem Th22:
Gen w,y & MS = AMSpace(V,w,y) implies MS is Homogeneous
proof
assume that
A1: Gen w,y and
A2: MS=AMSpace(V,w,y);
now
let o,a,a1,b,b1,c,c1 be Element of MS such that
A3: o,a _|_ o,a1 and
A4: o,b _|_ o,b1 and
A5: o,c _|_ o,c1 and
A6: a,b _|_ a1,b1 and
A7: a,c _|_ a1,c1 and
A8: ( not o,c // o,a)& not o,a // o,b;
reconsider q=o,u1=a,u2=b,u3=c,v1=a1 as VECTOR of V by A2,ANALMETR:19;
A9: not LIN o,a,b & not LIN o,a,c
proof
assume not thesis;
then o,a // o,b or o,a // o,c by ANALMETR:def 10;
hence contradiction by A8,ANALMETR:59;
end;
then
A10: o<>a by Th1;
now
q,u1,q,v1 are_Ort_wrt w,y by A2,A3,ANALMETR:21;
then
A11: u1-q,v1-q are_Ort_wrt w,y by ANALMETR:def 3;
A12: u1-q<>0.V by A10,RLVECT_1:21;
assume
A13: o<>a1;
then v1-q<>0.V by RLVECT_1:21;
then consider r being Real such that
A14: for a9,b9 being Real holds a9*w+b9*y,(r*b9)*w+(-r*a9)*y
are_Ort_wrt w,y & (a9*w+b9*y)-(u1-q),((r*b9)*w+(-r*a9)*y)-(v1-q) are_Ort_wrt w,
y by A1,A11,A12,Th19;
consider B1,B2 being Real such that
A15: u2-q=B1*w+B2*y by A1,ANALMETR:def 1;
consider A1,A2 being Real such that
A16: u3-q=A1*w+A2*y by A1,ANALMETR:def 1;
reconsider B1,B2,A1,A2 as Real;
set v39=((r*A2)*w+(-r*A1)*y)+q,v29=((r*B2)*w+(-r*B1)*y)+q;
reconsider c19=v39,b19=v29 as Element of MS by A2,ANALMETR:19;
A17: v29-q=(r*B2)*w+(-r*B1)*y by RLSUB_2:61;
(u2-q)-(u1-q)=u2-u1 & (v29-q)-(v1-q)=v29-v1 by Lm4;
then u2-u1,v29-v1 are_Ort_wrt w,y by A14,A15,A17;
then u1,u2,v1,v29 are_Ort_wrt w,y by ANALMETR:def 3;
then
A18: a,b _|_ a1,b19 by A2,ANALMETR:21;
u2-q,v29-q are_Ort_wrt w,y by A14,A15,A17;
then q,u2,q,v29 are_Ort_wrt w,y by ANALMETR:def 3;
then o,b _|_ o,b19 by A2,ANALMETR:21;
then
A19: b1=b19 by A3,A4,A6,A9,A13,A18,Th16;
A20: v39-q=(r*A2)*w+(-r*A1)*y by RLSUB_2:61;
u3-u2 = (A1*w+A2*y)-(B1*w+B2*y) by A16,A15,Lm4
.= (A1-B1)*w+(A2-B2)*y by Lm6;
then
A21: pr1(w,y,u3-u2)=A1-B1 & pr2(w,y,u3-u2)=A2-B2 by A1,GEOMTRAP:def 4,def 5;
v39-v29 = ((r*A2)*w+(r*(-A1))*y) - ((r*B2)*w+(-r*B1)*y) by Lm4
.= (r*A2-r*B2)*w + (r*(-A1)-r*(-B1))*y by Lm6
.= (r*(A2-B2))*w + (r*(B1 -A1))*y;
then pr1(w,y,v39-v29)=r*(A2-B2) & pr2(w,y,v39-v29)=r*(B1-A1) by A1,
GEOMTRAP:def 4,def 5;
then
PProJ (w,y,u3-u2,v39-v29) = (A1-B1)*(r*(A2-B2)) + (A2-B2)*(r*(B1-A1
)) by A21,GEOMTRAP:def 6
.=0;
then u3-u2,v39-v29 are_Ort_wrt w,y by A1,GEOMTRAP:32;
then
A22: u2,u3,v29,v39 are_Ort_wrt w,y by ANALMETR:def 3;
(u3-q)-(u1-q)=u3-u1 & (v39-q)-(v1-q)=v39-v1 by Lm4;
then u3-u1,v39-v1 are_Ort_wrt w,y by A14,A16,A20;
then u1,u3,v1,v39 are_Ort_wrt w,y by ANALMETR:def 3;
then
A23: a,c _|_ a1,c19 by A2,ANALMETR:21;
u3-q,v39-q are_Ort_wrt w,y by A14,A16,A20;
then q,u3,q,v39 are_Ort_wrt w,y by ANALMETR:def 3;
then o,c _|_ o,c19 by A2,ANALMETR:21;
then c1=c19 by A3,A5,A7,A9,A13,A23,Th16;
hence b,c _|_ b1,c1 by A2,A19,A22,ANALMETR:21;
end;
hence b,c _|_ b1,c1 by A4,A5,A6,A7,A8,Th21;
end;
hence thesis;
end;
registration
cluster Euclidean Pappian Desarguesian Homogeneous translation Fanoian
Moufangian for OrtAfPl;
existence
proof
consider V such that
A1: ex w,y st Gen w,y by ANALMETR:3;
consider w,y such that
A2: Gen w,y by A1;
reconsider MS=AMSpace(V,w,y) as OrtAfPl by A2,ANALMETR:34;
A3: MS is satisfying_3H by A2,Th20,CONAFFM:6;
for a,b being Real st a*w + b*y = 0.V
holds a=0 & b=0 by A2,ANALMETR:def 1;
then reconsider OAS=OASpace(V) as OAffinSpace by ANALOAF:26;
take MS;
A4: the AffinStruct of MS=Lambda(OAS) by ANALMETR:20;
then
A5: the AffinStruct of MS is Moufangian & the AffinStruct of MS
is translational by PAPDESAF:16,17;
the AffinStruct of MS is Pappian & the AffinStruct of MS is Desarguesian
by A4,PAPDESAF:13,14;
hence thesis by A2,A3,A4,A5,Th8,Th22;
end;
end;
registration
cluster Euclidean Pappian Desarguesian Homogeneous translation Fanoian
Moufangian for OrtAfSp;
existence
proof
set MS = the Euclidean Pappian Desarguesian Homogeneous translation Fanoian
Moufangian OrtAfPl;
MS is Euclidean Pappian Desarguesian Homogeneous translation Fanoian
Moufangian;
hence thesis;
end;
end;
theorem
Gen w,y & MS=AMSpace(V,w,y) implies MS is Euclidean Pappian
Desarguesian Homogeneous translation Fanoian Moufangian OrtAfPl
proof
assume that
A1: Gen w,y and
A2: MS=AMSpace(V,w,y);
reconsider MS9=AMSpace(V,w,y) as OrtAfPl by A2;
A3: MS9 is satisfying_3H by A1,Th20,CONAFFM:6;
for a,b being Real st a*w + b*y = 0.V
holds a=0 & b=0 by A1,ANALMETR:def 1;
then reconsider OAS=OASpace(V) as OAffinSpace by ANALOAF:26;
A4: the AffinStruct of MS9=Lambda(OAS) by ANALMETR:20;
then
A5: the AffinStruct of MS9 is Moufangian &
the AffinStruct of MS9 is translational by PAPDESAF:16,17;
the AffinStruct of MS9 is Pappian & the AffinStruct of
MS9 is Desarguesian by A4,PAPDESAF:13,14;
hence thesis by A1,A2,A3,A4,A5,Def2,Def3,Def4,Def5,Def6,Th8,Th22;
end;
registration
let MS be Pappian OrtAfPl;
cluster the AffinStruct of MS -> Pappian;
correctness by Def2;
end;
registration
let MS be Desarguesian OrtAfPl;
cluster the AffinStruct of MS -> Desarguesian;
correctness by Def3;
end;
registration
let MS be Moufangian OrtAfPl;
cluster the AffinStruct of MS -> Moufangian;
correctness by Def5;
end;
registration
let MS be translation OrtAfPl;
cluster the AffinStruct of MS -> translational;
correctness by Def6;
end;
registration
let MS be Fanoian OrtAfPl;
cluster the AffinStruct of MS -> Fanoian;
correctness by Def4;
end;
registration
let MS be Homogeneous OrtAfPl;
cluster the AffinStruct of MS -> Desarguesian;
correctness
proof
MS is Desarguesian by Th14;
hence thesis;
end;
end;
registration
let MS be Euclidean Desarguesian OrtAfPl;
cluster the AffinStruct of MS -> Pappian;
correctness
proof
MS is Pappian by Th15;
hence thesis;
end;
end;
registration
let MS be Pappian OrtAfSp;
cluster the AffinStruct of MS -> Pappian;
correctness by Def2;
end;
registration
let MS be Desarguesian OrtAfSp;
cluster the AffinStruct of MS -> Desarguesian;
correctness by Def3;
end;
registration
let MS be Moufangian OrtAfSp;
cluster the AffinStruct of MS -> Moufangian;
correctness by Def5;
end;
registration
let MS be translation OrtAfSp;
cluster the AffinStruct of MS -> translational;
correctness by Def6;
end;
registration
let MS be Fanoian OrtAfSp;
cluster the AffinStruct of MS -> Fanoian;
correctness by Def4;
end;