:: Fano-Desargues Parallelity Spaces
:: by Eugeniusz Kusak and Wojciech Leo\'nczuk
::
:: Received March 23, 1990
:: Copyright (c) 1990-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 RLVECT_1, ALGSTR_0, XBOOLE_0, SUBSET_1, ARYTM_1, SUPINF_2,
ARYTM_3, VECTSP_1, PARSP_1, ZFMISC_1, STRUCT_0, RELAT_1, GROUP_1,
MESFUNC1, PARSP_2, RECDEF_2, PENCIL_1;
notations TARSKI, ZFMISC_1, XTUPLE_0, SUBSET_1, MCART_1, DOMAIN_1, STRUCT_0,
ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, PARSP_1;
constructors DOMAIN_1, PARSP_1, XTUPLE_0;
registrations STRUCT_0, VECTSP_1, PARSP_1, XTUPLE_0, MCART_1;
theorems MCART_1, VECTSP_1, PARSP_1, RLVECT_1, GROUP_1;
begin
:: 1. A CONSTRUCTION OF A MODEL OF A FANO-DESARGUES SPACE
Lm1: for F being add-associative right_zeroed right_complementable non empty
addLoopStr, a,b being Element of F holds a - b = 0.F implies a = b
proof
let F be add-associative right_zeroed right_complementable non empty
addLoopStr, a,b be Element of F;
assume a - b = 0.F;
then a + -b = 0.F by RLVECT_1:def 11;
then a = - -b by RLVECT_1:6;
hence thesis by RLVECT_1:17;
end;
Lm2: for F being add-associative right_zeroed right_complementable non empty
addLoopStr, x,y being Element of F holds (x+(-y)=0.F iff x=y) & (x-y=0.F iff x
=y)
proof
let F be add-associative right_zeroed right_complementable non empty
addLoopStr, x,y be Element of F;
A1: x+(-y)=0.F implies x=y
proof
assume x+(-y)=0.F;
then x+((-y)+y)=0.F+y by RLVECT_1:def 3;
then x+0.F=0.F+y by RLVECT_1:5;
then x=0.F+y by RLVECT_1:4;
hence thesis by RLVECT_1:4;
end;
A2: x-y=0.F implies x=y
proof
assume x-y=0.F;
then x+(-y)+y=0.F+y by RLVECT_1:def 11;
then x+((-y)+y)=0.F+y by RLVECT_1:def 3;
then x+0.F=0.F+y by RLVECT_1:5;
then x=0.F+y by RLVECT_1:4;
hence thesis by RLVECT_1:4;
end;
x=y implies x-y=0.F
proof
assume x=y;
then x-y=y+(-y) by RLVECT_1:def 11;
hence thesis by RLVECT_1:5;
end;
hence thesis by A1,A2,RLVECT_1:5;
end;
reserve F for Field;
theorem Th1:
MPS(F) is ParSp
proof
for a,b,c,d,p,q,r,s being Element of MPS(F) holds a,b '||' b,a & a,b
'||' c,c & (a,b '||' p,q & a,b '||' r,s implies p,q '||' r,s or a=b) & (a,b
'||' a,c implies b,a '||' b,c) & ex x being Element of MPS(F) st a,b '||' c,x &
a,c '||' b,x by PARSP_1:13,14,15,16,17;
hence thesis by PARSP_1:def 12;
end;
reserve a,b,c,d,p,q,r for Element of MPS(F);
reserve e,f,g,h,i,j,k,l,m,n,o,w for Element of [:the carrier of F,the carrier
of F,the carrier of F:];
reserve K,L,M,N,R,S for Element of F;
Lm3: (e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F &
(e`1_3-f`1_3)*(g`3_3-h`3_3) - (
g`1_3-h`1_3)*(e`3_3-f`3_3) = 0.F &
(e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) = 0.F iff
(ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 & K*(e`2_3-f`2_3) = g`2_3-h`2_3 &
K*(e`3_3-f`3_3) = g`3_3-h`3_3)
or e`1_3-f`1_3 = 0.F & e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F
proof
A1: (e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F &
(e`1_3-f`1_3)*(g`3_3-h`3_3) -
(g`1_3-h`1_3)*(e`3_3-f`3_3) = 0.F &
(e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) = 0.F
implies (ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 &
K*(e`2_3-f`2_3) = g`2_3-h`2_3 & K*(e`3_3-f`3_3) =
g`3_3-h`3_3) or e`1_3-f`1_3 = 0.F & e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F
proof
assume that
A2: (e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F and
A3: (e`1_3-f`1_3)*(g`3_3-h`3_3) - (g`1_3-h`1_3)*(e`3_3-f`3_3) = 0.F and
A4: (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) = 0.F;
now
A5: now
assume
A6: e`3_3-f`3_3 <> 0.F;
A7: ((g`3_3-h`3_3)*(e`3_3-f`3_3)")*(e`3_3-f`3_3)
= (g`3_3-h`3_3)*((e`3_3-f`3_3)"*(e`3_3-f`3_3
)) by GROUP_1:def 3
.= (g`3_3-h`3_3)*1_F by A6,VECTSP_1:def 10
.= g`3_3-h`3_3;
A8: ((g`3_3-h`3_3)*(e`3_3-f`3_3)")*(e`2_3-f`2_3)
= ((e`2_3-f`2_3)*(g`3_3-h`3_3))*(e`3_3-f`3_3
)" by GROUP_1:def 3
.= ((g`2_3-h`2_3)*(e`3_3-f`3_3))*(e`3_3-f`3_3)" by A4,Lm1
.= (g`2_3-h`2_3)*((e`3_3-f`3_3)*(e`3_3-f`3_3)") by GROUP_1:def 3
.= (g`2_3-h`2_3)*1_F by A6,VECTSP_1:def 10
.= g`2_3-h`2_3;
((g`3_3-h`3_3)*(e`3_3-f`3_3)")*(e`1_3-f`1_3)
= ((e`1_3-f`1_3)*(g`3_3-h`3_3))*(e`3_3-f`3_3
)" by GROUP_1:def 3
.= ((g`1_3-h`1_3)*(e`3_3-f`3_3))*(e`3_3-f`3_3)" by A3,Lm1
.= (g`1_3-h`1_3)*((e`3_3-f`3_3)*(e`3_3-f`3_3)") by GROUP_1:def 3
.= (g`1_3-h`1_3)*1_F by A6,VECTSP_1:def 10
.= g`1_3-h`1_3;
hence thesis by A8,A7;
end;
A9: now
assume
A10: e`2_3-f`2_3 <> 0.F;
A11: ((g`2_3-h`2_3)*(e`2_3-f`2_3)")*(e`2_3-f`2_3)
= (g`2_3-h`2_3)*((e`2_3-f`2_3)"*(e`2_3-f`2_3
)) by GROUP_1:def 3
.= (g`2_3-h`2_3)*1_F by A10,VECTSP_1:def 10
.= g`2_3-h`2_3;
A12: ((g`2_3-h`2_3)*(e`2_3-f`2_3)")*(e`3_3-f`3_3)
= (e`2_3-f`2_3)"*((g`2_3-h`2_3)*(e`3_3-f`3_3
)) by GROUP_1:def 3
.= (e`2_3-f`2_3)"*((e`2_3-f`2_3)*(g`3_3-h`3_3)) by A4,Lm1
.= ((e`2_3-f`2_3)"*(e`2_3-f`2_3))*(g`3_3-h`3_3) by GROUP_1:def 3
.= (g`3_3-h`3_3)*1_F by A10,VECTSP_1:def 10
.= g`3_3-h`3_3;
((g`2_3-h`2_3)*(e`2_3-f`2_3)")*(e`1_3-f`1_3)
= ((e`1_3-f`1_3)*(g`2_3-h`2_3))*(e`2_3-f`2_3
)" by GROUP_1:def 3
.= ((g`1_3-h`1_3)*(e`2_3-f`2_3))*(e`2_3-f`2_3)" by A2,Lm1
.= (g`1_3-h`1_3)*((e`2_3-f`2_3)*(e`2_3-f`2_3)") by GROUP_1:def 3
.= (g`1_3-h`1_3)*1_F by A10,VECTSP_1:def 10
.= g`1_3-h`1_3;
hence thesis by A11,A12;
end;
now
assume
A13: e`1_3-f`1_3 <> 0.F;
A14: ((g`1_3-h`1_3)*(e`1_3-f`1_3)")*(e`1_3-f`1_3)
= (g`1_3-h`1_3)*((e`1_3-f`1_3)"*(e`1_3-f`1_3)
) by GROUP_1:def 3
.= (g`1_3-h`1_3)*1_F by A13,VECTSP_1:def 10
.= g`1_3-h`1_3;
A15: ((g`1_3-h`1_3)*(e`1_3-f`1_3)")*(e`3_3-f`3_3)
= (e`1_3-f`1_3)"*((g`1_3-h`1_3)*(e`3_3-f`3_3
)) by GROUP_1:def 3
.= (e`1_3-f`1_3)"*((e`1_3-f`1_3)*(g`3_3-h`3_3)) by A3,Lm1
.= ((e`1_3-f`1_3)"*(e`1_3-f`1_3))*(g`3_3-h`3_3) by GROUP_1:def 3
.= (g`3_3-h`3_3)*1_F by A13,VECTSP_1:def 10
.= g`3_3-h`3_3;
((g`1_3-h`1_3)*(e`1_3-f`1_3)")*(e`2_3-f`2_3)
= (e`1_3-f`1_3)"*((g`1_3-h`1_3)*(e`2_3-f`2_3)
) by GROUP_1:def 3
.= (e`1_3-f`1_3)"*((e`1_3-f`1_3)*(g`2_3-h`2_3)) by A2,Lm1
.= ((e`1_3-f`1_3)"*(e`1_3-f`1_3))*(g`2_3-h`2_3) by GROUP_1:def 3
.= (g`2_3-h`2_3)*1_F by A13,VECTSP_1:def 10
.= g`2_3-h`2_3;
hence thesis by A14,A15;
end;
hence thesis by A9,A5;
end;
hence thesis;
end;
(ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 & K*(e`2_3-f`2_3) = g`2_3-h`2_3 &
K*(e`3_3-f`3_3) =
g`3_3-h`3_3) or e`1_3-f`1_3 = 0.F & e`2_3-f`2_3 = 0.F &
e`3_3-f`3_3 = 0.F implies (e`1_3-f`1_3)*(g
`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F &
(e`1_3-f`1_3)*(g`3_3-h`3_3) - (g`1_3-h`1_3)*(e`3_3-f`3_3)
= 0.F & (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) = 0.F
proof
A16: now
given K such that
A17: K*(e`1_3-f`1_3) = g`1_3-h`1_3 and
A18: K*(e`2_3-f`2_3) = g`2_3-h`2_3 & K*(e`3_3-f`3_3) = g`3_3-h`3_3;
A19: (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3)
= (K*(e`2_3-f`2_3))*(e`3_3-f`3_3)
- (K*(e`2_3-f`2_3))*(e`3_3-f`3_3) by A18,GROUP_1:def 3;
(e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3)
= (K*(e`1_3-f`1_3))*(e`2_3-f`2_3)
- (K*(e`1_3 -f`1_3))*(e`2_3-f`2_3) &
(e`1_3-f`1_3)*(g`3_3-h`3_3) - (g`1_3-h`1_3)*(e`3_3-f`3_3) = (K*(e
`1_3-f`1_3))*( e`3_3-f`3_3) - (K*(e`1_3-f`1_3))*(e`3_3-f`3_3)
by A17,A18,GROUP_1:def 3;
hence thesis by A19,RLVECT_1:15;
end;
A20: e`1_3-f`1_3 = 0.F & e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F
implies thesis by RLVECT_1:15;
assume (ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 &
K*(e`2_3-f`2_3) = g`2_3-h`2_3 & K*(e`3_3-f
`3_3) = g`3_3-h`3_3) or e`1_3-f`1_3 = 0.F &
e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F;
hence thesis by A20,A16;
end;
hence thesis by A1;
end;
theorem Th2:
a,b '||' c,d iff ex e,f,g,h st [[a,b],[c,d]] = [[e,f],[g,h]] &
((ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 & K*(e`2_3-f`2_3) = g`2_3-h`2_3 &
K*(e`3_3-f`3_3) = g`3_3-h`3_3) or e`1_3-f
`1_3 = 0.F & e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F )
proof
A1: a,b '||' c,d implies ex e,f,g,h st [[a,b],[c,d]] = [[e,f],[g,h]] &
((ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 & K*(e`2_3-f`2_3) = g`2_3-h`2_3 &
K*(e`3_3-f`3_3) = g`3_3-h`3_3) or e`1_3-f`1_3
= 0.F & e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F )
proof
assume a,b '||' c,d;
then consider e,f,g,h such that
A2: [[a,b],[c,d]] = [[e,f],[g,h]] and
A3: (e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3)
= 0.F & (e`1_3-f`1_3)*(g`3_3-h
`3_3) - (g `1_3 -h`1_3)*(e`3_3-f`3_3) = 0.F &
(e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) =
0.F by PARSP_1:12;
(ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 &
K*(e`2_3-f`2_3) = g`2_3-h`2_3 & K*(e`3_3-f`3_3) =
g`3_3-h`3_3) or e`1_3-f`1_3 = 0.F & e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F
by A3,Lm3;
hence thesis by A2;
end;
(ex e,f,g,h st [[a,b],[c,d]] = [[e,f],[g,h]] &
((ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 &
K*(e`2_3-f`2_3) = g`2_3-h`2_3 &
K*(e`3_3-f`3_3) = g`3_3-h`3_3) or (e`1_3-f`1_3 = 0.F & e`2_3-f`2_3 = 0.
F & e`3_3-f`3_3 = 0.F))) implies a,b '||' c,d
proof
given e,f,g,h such that
A4: [[a,b],[c,d]] = [[e,f],[g,h]] and
A5: (ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 &
K*(e`2_3-f`2_3) = g`2_3-h`2_3 & K*(e`3_3-f
`3_3 ) = g`3_3-h`3_3) or e`1_3-f`1_3 = 0.F &
e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F;
A6: (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) = 0.F by A5,Lm3;
(e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F &
(e`1_3-f`1_3)*(g`3_3-h`3_3)
- (g`1_3 -h`1_3)*(e`3_3-f`3_3) = 0.F by A5,Lm3;
hence thesis by A4,A6,PARSP_1:12;
end;
hence thesis by A1;
end;
theorem Th3:
not a,b '||' a,c & [[a,b],[a,c]]=[[e,f],[e,g]] implies e<>f & e<>g & f<>g
proof
assume
A1: ( not a,b '||' a,c)& [[a,b],[a,c]]=[[e,f],[e,g]];
then
0.F*(e`1_3-f`1_3) <> e`1_3-g`1_3 or 0.F*(e`2_3-f`2_3) <> e`2_3-g`2_3 or
0.F*(e`3_3-f`3_3) <>
e`3_3-g`3_3 by Th2;
then
A2: 0.F <> e`1_3-g`1_3 or 0.F <> e`2_3-g`2_3 or 0.F <> e`3_3-g`3_3;
A3: f<>g
proof
assume
A4: not thesis;
(e`1_3-f`1_3)*1_F <> e`1_3-g`1_3 or (e`2_3-f`2_3)*1_F <> e`2_3-g`2_3 or
(e`3_3-f`3_3)*1_F
<> e`3_3-g`3_3 by A1,Th2;
hence contradiction by A4;
end;
e`1_3-f`1_3 <> 0.F or e`2_3-f`2_3 <> 0.F or e`3_3-f`3_3 <> 0.F by A1,Th2;
hence thesis by A2,A3,RLVECT_1:15;
end;
theorem Th4:
not a,b '||' a,c & [[a,b],[a,c]] = [[e,f],[e,g]] &
K*(e`1_3-f`1_3)=L*(e`1_3-g`1_3
) & K*(e`2_3-f`2_3)=L*(e`2_3-g`2_3) & K*(e`3_3-f`3_3)=L*(e`3_3-g`3_3)
implies K=0.F & L=0.F
proof
assume that
A1: ( not a,b '||' a,c)& [[a,b],[a,c]] = [[e,f],[e,g]] and
A2: K*(e`1_3-f`1_3)=L*(e`1_3-g`1_3) and
A3: K*(e`2_3-f`2_3)=L*(e`2_3-g`2_3) and
A4: K*(e`3_3-f`3_3)=L*(e`3_3-g`3_3);
e=[e`1_3,e`2_3,e`3_3] & g=[g`1_3,g`2_3,g`3_3];
then e`1_3 <> g`1_3 or e`2_3 <> g`2_3 or e`3_3 <> g`3_3 by A1,Th3;
then
A5: e`1_3-g`1_3 <> 0.F or e`2_3-g`2_3 <> 0.F or e`3_3-g`3_3 <> 0.F by Lm2;
K*(e`1_3-f`1_3)*(e`2_3-g`2_3)=L*((e`1_3-g`1_3)*(e`2_3-g`2_3)) &
K*(e`2_3-f`2_3)*(e`1_3-g`1_3)=L*
((e `2_3-g`2_3)*(e`1_3-g`1_3)) by A2,A3,GROUP_1:def 3;
then K*(e`1_3-f`1_3)*(e`2_3-g`2_3)-K*(e`2_3-f`2_3)*(e`1_3-g`1_3) = 0.F
by RLVECT_1:15;
then K*((e`1_3-f`1_3)*(e`2_3-g`2_3))-K*(e`2_3-f`2_3)*(e`1_3-g`1_3) = 0.F
by GROUP_1:def 3;
then K*((e`1_3-f`1_3)*(e`2_3-g`2_3))-K*((e`2_3-f`2_3)*(e`1_3-g`1_3)) = 0.F
by GROUP_1:def 3;
then
A6: K*((e`1_3-f`1_3)*(e`2_3-g`2_3)-(e`1_3-g`1_3)*(e`2_3-f`2_3)) = 0.F
by VECTSP_1:11;
K*(e`1_3-f`1_3)*(e`3_3-g`3_3)=L*((e`1_3-g`1_3)*(e`3_3-g`3_3)) &
K*(e`3_3-f`3_3)*(e`1_3-g`1_3)=L
*((e `3_3-g`3_3)*(e`1_3-g`1_3)) by A2,A4,GROUP_1:def 3;
then K*(e`1_3-f`1_3)*(e`3_3-g`3_3)-K*(e`3_3-f`3_3)*(e`1_3-g`1_3) = 0.F
by RLVECT_1:15;
then K*((e`1_3-f`1_3)*(e`3_3-g`3_3))-K*(e`3_3-f`3_3)*(e`1_3-g`1_3) = 0.F
by GROUP_1:def 3;
then K*((e`1_3-f`1_3)*(e`3_3-g`3_3))-K*((e`3_3-f`3_3)*(e`1_3-g`1_3)) = 0.F
by GROUP_1:def 3;
then
A7: K*((e`1_3-f`1_3)*(e`3_3-g`3_3)-(e`1_3-g`1_3)*(e`3_3-f`3_3)) = 0.F
by VECTSP_1:11;
K*(e`2_3-f`2_3)*(e`3_3-g`3_3)=L*((e`2_3-g`2_3)*(e`3_3-g`3_3)) &
K*(e`3_3-f`3_3)*(e`2_3-g`2_3)=L*
((e `3_3-g`3_3)*(e`2_3-g`2_3)) by A3,A4,GROUP_1:def 3;
then K*(e`2_3-f`2_3)*(e`3_3-g`3_3)-K*(e`3_3-f`3_3)*(e`2_3-g`2_3) = 0.F
by RLVECT_1:15;
then K*((e`2_3-f`2_3)*(e`3_3-g`3_3))-K*(e`3_3-f`3_3)*(e`2_3-g`2_3) = 0.F
by GROUP_1:def 3;
then K*((e`2_3-f`2_3)*(e`3_3-g`3_3))-K*((e`3_3-f`3_3)*(e`2_3-g`2_3)) = 0.F
by GROUP_1:def 3;
then
A8: K*((e`2_3-f`2_3)*(e`3_3-g`3_3)-(e`2_3-g`2_3)*(e`3_3-f`3_3)) = 0.F
by VECTSP_1:11;
A9: (e`1_3-f`1_3)*(e`2_3-g`2_3)-(e`1_3-g`1_3)*(e`2_3-f`2_3) <> 0.F or
(e`2_3-f`2_3)*(e`3_3-g`3_3)-(
e`2_3-g`2_3)*(e`3_3-f`3_3) <> 0.F or
(e`1_3-f`1_3)*(e`3_3-g`3_3)-(e`1_3-g`1_3)*(e`3_3-f`3_3) <> 0.F by A1,PARSP_1:12
;
then
A10: K=0.F by A6,A8,A7,VECTSP_1:12;
then
A11: 0.F=L*(e`3_3-g`3_3) by A4;
0.F=L*(e`1_3-g`1_3) & 0.F=L*(e`2_3-g`2_3) by A2,A3,A10;
hence thesis by A6,A8,A7,A9,A11,A5,VECTSP_1:12;
end;
Lm4: for F being add-associative right_zeroed right_complementable non empty
addLoopStr, a, b, c being Element of F holds (b+a)-(c+a) = b-c
proof
let F be add-associative right_zeroed right_complementable non empty
addLoopStr, a,b,c be Element of F;
thus (b+a)-(c+a) = (b+a)+-(c+a) by RLVECT_1:def 11
.= (b+a)+(-a+-c) by RLVECT_1:31
.= ((b+a)+-a)+-c by RLVECT_1:def 3
.= (b+(a+-a))+-c by RLVECT_1:def 3
.= (b+0.F)+-c by RLVECT_1:def 10
.= b+-c by RLVECT_1:4
.= b-c by RLVECT_1:def 11;
end;
Lm5: (K-L)-(R-L)=K-R
proof
thus (K-L)-(R-L)=(K+(-L))-(R-L) by RLVECT_1:def 11
.= ((-L)+K)-(R+(-L)) by RLVECT_1:def 11
.= K-R by Lm4;
end;
Lm6: K*(N-M)-L*(N-S)=S-M implies (K+(-1_F))*(N-M)=(L+(-1_F))*(N-S)
proof
assume K*(N-M)-L*(N-S) = S-M;
then K*(N-M)-L*(N-S) = S+(-M) by RLVECT_1:def 11
.= S+(-M)+0.F by RLVECT_1:4
.= (-M)+S+(-(N)+N) by RLVECT_1:5
.= S+((-(N)+N)+(-M)) by RLVECT_1:def 3
.= S+(-(N)+(N+(-M))) by RLVECT_1:def 3
.= S+(-(N)+(N-M)) by RLVECT_1:def 11
.= (S+(-(N)))+(N-M) by RLVECT_1:def 3
.= (S-N)+(N-M) by RLVECT_1:def 11;
then K*(N-M)+(-L*(N-S))+L*(N-S) = (S-N)+(N-M)+L*(N-S) by RLVECT_1:def 11;
then K*(N-M)+((-L*(N-S))+L*(N-S)) = (S-N)+(N-M)+L*(N-S) by RLVECT_1:def 3;
then K*(N-M)+0.F = (S-N)+(N-M)+L*(N-S) by RLVECT_1:5;
then K*(N-M) = (S-N)+(N-M)+L*(N-S) by RLVECT_1:4
.= ((S-N)+L*(N-S))+(N-M) by RLVECT_1:def 3;
then K*(N-M)+(-(N-M)) = ((S-N)+L*(N-S))+((N-M)+(-(N-M))) by RLVECT_1:def 3
.= ((S-N)+L*(N-S))+0.F by RLVECT_1:5
.= (S-N)+L*(N-S) by RLVECT_1:4
.= (S+-N)+L*(N-S) by RLVECT_1:def 11
.= L*(N-S)+(-(N-S)) by RLVECT_1:33;
then K*(N-M)+(-(1_F*(N-M))) = L*(N-S)+(-(N-S));
then K*(N-M)+((-1_F)*(N-M)) = L*(N-S)+(-(N-S)) by VECTSP_1:9;
then (K+(-1_F))*(N-M) = L*(N-S)+(-(N-S)) by VECTSP_1:def 7
.= L*(N-S)+(-(1_F*(N-S)))
.= L*(N-S)+((-1_F)*(N-S)) by VECTSP_1:9;
hence thesis by VECTSP_1:def 7;
end;
Lm7: K-L=N-M implies M=L+N-K
proof
assume K-L=N-M;
then M+(K+(-L))=M+(N-M) by RLVECT_1:def 11;
then M+(K+(-L))=M+(N+(-M)) by RLVECT_1:def 11;
then (M+K)+(-L)=M+(N+(-M)) by RLVECT_1:def 3;
then (M+K)+(-L)=(M+N)+(-M) by RLVECT_1:def 3;
then M+K-L=N+M+(-M) by RLVECT_1:def 11;
then M+K-L=N+(M+(-M)) by RLVECT_1:def 3;
then M+K-L=N+0.F by RLVECT_1:5;
then M+K-L+L=N+L by RLVECT_1:4;
then M+K+(-L)+L=N+L by RLVECT_1:def 11;
then M+K+((-L)+L)=N+L by RLVECT_1:def 3;
then M+K+0.F=L+N by RLVECT_1:5;
then M+K+(-K)=L+N+(-K) by RLVECT_1:4;
then M+K+(-K)=L+N-K by RLVECT_1:def 11;
then M+(K+(-K))=L+N-K by RLVECT_1:def 3;
then M+0.F=L+N-K by RLVECT_1:5;
hence thesis by RLVECT_1:4;
end;
theorem Th5:
not a,b '||' a,c & a,b '||' c,d & a,c '||' b,d &
[[a,b],[c,d]] = [[e,f],[g,h]]
implies h`1_3=f`1_3+g`1_3-e`1_3 & h`2_3=f`2_3+g`2_3-e`2_3 &
h`3_3=f`3_3+g`3_3-e`3_3
proof
assume that
A1: not a,b '||' a,c and
A2: a,b '||' c,d and
A3: a,c '||' b,d and
A4: [[a,b],[c,d]]=[[e,f],[g,h]];
consider m,n,o,w such that
A6: [[a,c],[b,d]]=[[m,n],[o,w]] and
A7: ( ex L st L*(m`1_3-n`1_3) = o`1_3-w`1_3 & L*(m`2_3-n`2_3) = o`2_3-w`2_3 &
L*(m`3_3-n
`3_3) = o`3_3-w`3_3) or m`1_3-n`1_3=0.F & m`2_3-n`2_3=0.F &
m`3_3-n`3_3=0.F by A3,Th2;
A8: b=f by A4,MCART_1:93;
then
A9: o=f by A6,MCART_1:93;
d=h by A4,MCART_1:93;
then
A10: w=h by A6,MCART_1:93;
c =g by A4,MCART_1:93;
then
A11: n=g by A6,MCART_1:93;
A12: a=e by A4,MCART_1:93;
then
A13: [[a,b],[a,c]]=[[e,f],[e,g]] by A4,A8,MCART_1:93;
consider i,j,k,l such that
A14: [[a,b],[c,d]]=[[i,j],[k,l]] and
A15: ( ex K st K*(i`1_3-j`1_3) = k`1_3-l`1_3 & K*(i`2_3-j`2_3) = k`2_3-l`2_3 &
K*(i`3_3-j
`3_3) = k`3_3-l`3_3) or i`1_3-j`1_3=0.F & i`2_3-j`2_3=0.F &
i`3_3-j`3_3=0.F by A2,Th2;
A16: e=i & f=j by A4,A14,MCART_1:93;
A17: g=k & h=l by A4,A14,MCART_1:93;
A18: e=m by A12,A6,MCART_1:93;
f=[f`1_3,f`2_3,f`3_3];
then e`1_3<>f`1_3 or e`2_3<>f`2_3 or e`3_3<>f`3_3 by A1,A13,Th3;
then consider K such that
A19: K*(e`1_3-f`1_3) = g`1_3-h`1_3 and
A20: K*(e`2_3-f`2_3) = g`2_3-h`2_3 and
A21: K*(e`3_3-f`3_3) = g`3_3-h`3_3 by A15,A16,A17,Lm2;
g=[g`1_3,g`2_3,g`3_3];
then e`1_3<>g`1_3 or e`2_3<>g`2_3 or e`3_3<>g`3_3 by A1,A13,Th3;
then consider L such that
A22: L*(e`1_3-g`1_3) = f`1_3-h`1_3 and
A23: L*(e`2_3-g`2_3) = f`2_3-h`2_3 and
A24: L*(e`3_3-g`3_3) = f`3_3-h`3_3 by A7,A18,A11,A9,A10,Lm2;
K*(e`2_3-f`2_3)-L*(e`2_3-g`2_3) = g`2_3-f`2_3 by A20,A23,Lm5;
then
A25: (K+(-1_F))*(e`2_3-f`2_3) = (L+(-1_F))*(e`2_3-g`2_3) by Lm6;
K*(e`3_3-f`3_3)-L*(e`3_3-g`3_3) = g`3_3-f`3_3 by A21,A24,Lm5;
then
A26: (K+(-1_F))*(e`3_3-f`3_3) = (L+(-1_F))*(e`3_3-g`3_3) by Lm6;
K*(e`1_3-f`1_3)-L*(e`1_3-g`1_3) = g`1_3-f`1_3 by A19,A22,Lm5;
then (K+(-1_F))*(e`1_3-f`1_3) = (L+(-1_F))*(e`1_3-g`1_3) by Lm6;
then
A27: K+(-1_F)=0.F by A1,A13,A25,A26,Th4;
then (e`2_3-f`2_3)*1_F = g`2_3-h`2_3 by A20,Lm2;
then
A28: e`2_3-f`2_3 = g`2_3-h`2_3;
(e`3_3-f`3_3)*1_F = g`3_3-h`3_3 by A21,A27,Lm2;
then
A29: e`3_3-f`3_3 = g`3_3-h`3_3;
(e`1_3-f`1_3)*1_F = g`1_3- h`1_3 by A19,A27,Lm2;
then e`1_3-f`1_3 = g`1_3-h`1_3;
hence thesis by A28,A29,Lm7;
end;
Lm8: L*K-L*R=R+K implies (L-1_F)*K=(L+1_F)*R
proof
assume L*K-L*R=R+K;
then L*K+(-L*R)+(-K)=R+K+(-K) by RLVECT_1:def 11
.=R+(K+(-K)) by RLVECT_1:def 3
.=R+0.F by RLVECT_1:5
.=R by RLVECT_1:4;
then (L*K+(-K))+(-L*R)=R by RLVECT_1:def 3;
then (L*K+(-(1_F*K)))+(-L*R)=R;
then (L*K+(-1_F)*K)+(-L*R)=R by VECTSP_1:9;
then (L+(-1_F))*K+(-L*R)=R by VECTSP_1:def 7;
then (L-1_F)*K+(-L*R)+L*R=R+L*R by RLVECT_1:def 11;
then (L-1_F)*K+((-L*R)+L*R)=R+L*R by RLVECT_1:def 3;
then (L-1_F)*K+0.F=R+L*R by RLVECT_1:5;
then (L-1_F)*K=L*R+R by RLVECT_1:4
.=L*R+1_F*R;
hence thesis by VECTSP_1:def 7;
end;
Lm9: L*(K-N)=R-S & S=K+N-R implies (L-1_F)*(R-N)=(L+1_F)*(R-K)
proof
assume L*(K-N)=R-S & S=K+N-R;
then
A1: L*(K-N)=R+(-(K+N-R)) by RLVECT_1:def 11
.=R+(R+(-(K+N))) by RLVECT_1:33
.=R+(R+(-K+(-N))) by RLVECT_1:31
.=R+(-N+(R+(-K))) by RLVECT_1:def 3
.=(R+(-N))+(R+(-K)) by RLVECT_1:def 3
.=(R-N)+(R+(-K)) by RLVECT_1:def 11
.=(R-K)+(R-N) by RLVECT_1:def 11;
L*(R-N)-L*(R-K)=L*(R+(-N))-L*(R-K) by RLVECT_1:def 11
.=L*(R+(-N))-L*(R+(-K)) by RLVECT_1:def 11
.=L*(R+(-N))+(-L*(R+(-K))) by RLVECT_1:def 11
.=L*R+L*(-N)+(-L*(R+(-K))) by VECTSP_1:def 7
.=L*R+L*(-N)+((-L)*(R+(-K))) by VECTSP_1:9
.=L*R+L*(-N)+((-L)*R+(-L)*(-K)) by VECTSP_1:def 7
.=L*R+L*(-N)+((-L)*R+L*K) by VECTSP_1:10
.=L*(-N)+L*R+(-L*R+L*K) by VECTSP_1:9
.=L*(-N)+L*R+(-L*R)+L*K by RLVECT_1:def 3
.=L*(-N)+(L*R+(-L*R))+L*K by RLVECT_1:def 3
.=L*(-N)+0.F+L*K by RLVECT_1:5
.=L*K+L*(-N) by RLVECT_1:4
.=L*(K+(-N)) by VECTSP_1:def 7
.=L*(K-N) by RLVECT_1:def 11;
hence thesis by A1,Lm8;
end;
Lm10: K=L+M-N & R=L+S-N implies 1_F*(M-S)=K-R
proof
assume that
A1: K=L+M-N and
A2: R=L+S-N;
-R=-(L+S+(-N)) by A2,RLVECT_1:def 11
.=-(L+S)+(-(-N)) by RLVECT_1:31
.=-(L+S)+N by RLVECT_1:17
.=-L+(-S)+N by RLVECT_1:31;
then K-R=(L+M-N)+(-L+(-S)+N) by A1,RLVECT_1:def 11
.=(M+L+(-N))+(-L+(-S)+N) by RLVECT_1:def 11
.=(M+L+(-N))+(-S+(-L+N)) by RLVECT_1:def 3
.=(M+(L+(-N)))+(-S+(-L+N)) by RLVECT_1:def 3
.=(M+(L-N))+(-S+(-L+N)) by RLVECT_1:def 11
.=(M+(L-N))+(-S+(-L+(-(-N)))) by RLVECT_1:17
.=(M+(L-N))+(-S+(-(L+(-N)))) by RLVECT_1:31
.=(M+(L-N))+(-(L-N)+(-S)) by RLVECT_1:def 11
.=((M+(L-N))+(-(L-N)))+(-S) by RLVECT_1:def 3
.=(M+((L-N)+(-(L-N))))+(-S) by RLVECT_1:def 3
.=(M+0.F)+(-S) by RLVECT_1:5
.=M+(-S) by RLVECT_1:4
.=M*1_F+(-S)
.=M*1_F+(-S)*1_F
.=(M+(-S))*1_F
.=(M-S)*1_F by RLVECT_1:def 11;
hence thesis;
end;
theorem Th6:
ex a,b,c st not a,b '||' a,c
proof
consider e,f,g being Element of [:the carrier of F,the carrier of F,the
carrier of F:] such that
A1: e=[1_F,1_F,0.F] and
A2: f=[-0.F,1_F,0.F] and
A3: g=[1_F,-0.F,0.F];
A4: f`1_3=-0.F & f`2_3=1_F by A2;
A5: g`1_3=1_F & g`2_3=-0.F by A3;
the carrier of MPS(F) = [:the carrier of F,the carrier of F,the carrier
of F:] by PARSP_1:10;
then consider a,b,c being Element of MPS(F) such that
A6: [[a,b],[a,c]]=[[e,f],[e,g]];
take a,b,c;
e`1_3=1_F & e`2_3=1_F by A1;
then
A7: (e`1_3-f`1_3)*(e`2_3-g`2_3)-(e`1_3-g`1_3)*(e`2_3-f`2_3)
= (1.F+(-(-0.F)))*(1.F-(-0.F))-
(1.F-1.F)*(1.F-1.F) by A4,A5,RLVECT_1:def 11
.= (1.F+(-(-0.F)))*(1.F+(-(-0.F)))-(1.F-1.F)*(1.F-1.F) by RLVECT_1:def 11
.= (1.F+0.F)*(1.F+(-(-0.F)))-(1.F-1.F)*(1.F-1.F) by RLVECT_1:17
.= (1.F+0.F)*(1.F+0.F)-(1.F-1.F)*(1.F-1.F) by RLVECT_1:17
.= 1.F*(1.F+0.F)-(1.F-1.F)*(1.F-1.F) by RLVECT_1:4
.= 1.F*1.F-(1.F-1.F)*(1.F-1.F) by RLVECT_1:4
.= 1.F*1.F-0.F*(1.F-1.F) by RLVECT_1:15
.= 1.F*1.F-0.F
.= 1.F-0.F;
now
let e9,f9,g9,h9 be Element of [:the carrier of F,the carrier of F,the
carrier of F:];
assume
A8: [[e9,f9],[g9,h9]]=[[a,b],[a,c]];
then
A9: g9=e & h9=g by A6,MCART_1:93;
e9=e & f9=f by A6,A8,MCART_1:93;
hence (e9`1_3-f9`1_3)*(g9`2_3-h9`2_3) - (g9`1_3-h9`1_3)*(e9`2_3-f9`2_3)
<> 0.F or (e9`1_3-f9
`1_3)*(g9`3_3-h9`3_3) - (g9`1_3-h9`1_3)*(e9`3_3-f9`3_3) <> 0.F or
(e9`2_3-f9`2_3)*(g9`3_3-h9`3_3) - (
g9`2_3-h9`2_3)*(e9`3_3-f9`3_3) <> 0.F by A7,A9,Lm2;
end;
hence thesis by PARSP_1:12;
end;
theorem Th7:
1_F+1_F<>0.F & b,c '||' a,d & a,b '||' c,d & a,c '||' b,d implies
a,b '||' a,c
proof
assume that
A1: 1_F+1_F<>0.F and
A2: b,c '||' a,d and
A3: a,b '||' c,d and
A4: a,c '||' b,d;
assume
A5: not thesis;
consider i,j,k,l such that
A6: [[b,c],[a,d]]=[[i,j],[k,l]] and
A7: (ex L st L*(i`1_3-j`1_3) = k`1_3-l`1_3 & L*(i`2_3-j`2_3) = k`2_3-l`2_3 &
L*(i`3_3-j
`3_3) = k`3_3-l`3_3) or i`1_3-j`1_3 = 0.F & i`2_3-j`2_3 = 0.F &
i`3_3-j`3_3 = 0.F by A2,Th2;
A8: b=i & c =j by A6,MCART_1:93;
A9: a=k & d=l by A6,MCART_1:93;
consider e,f,g,h such that
A10: [[a,b],[c,d]]=[[e,f],[g,h]] and
(ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 & K*(e`2_3-f`2_3) = g`2_3-h`2_3 &
K*(e`3_3-f`3_3 ) =
g`3_3-h`3_3) or e`1_3-f`1_3 = 0.F & e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F
by A3,Th2;
A11: b=f by A10,MCART_1:93;
A12: d=h by A10,MCART_1:93;
A13: c =g by A10,MCART_1:93;
A14: a=e by A10,MCART_1:93;
then
A15: [[a,b],[a,c]]=[[e,f],[e,g]] by A10,A11,MCART_1:93;
f=[f`1_3,f`2_3,f`3_3] & g=[g`1_3,g`2_3,g`3_3];
then i`1_3<>j`1_3 or i`2_3<>j`2_3 or i`3_3<>j`3_3 by A5,A11,A13,A15,A8,Th3;
then consider L such that
A16: L*(f`1_3-g`1_3) = e`1_3-h`1_3 and
A17: L*(f`2_3-g`2_3) = e`2_3-h`2_3 and
A18: L*(f`3_3-g`3_3) = e`3_3-h`3_3 by A14,A11,A13,A12,A7,A8,A9,Lm2;
h`2_3=f`2_3+g`2_3-e`2_3 by A3,A4,A5,A10,Th5;
then
A19: (L-1_F)*(e`2_3-g`2_3)=(L+1_F)*(e`2_3-f`2_3) by A17,Lm9;
h`3_3=f`3_3+g`3_3-e`3_3 by A3,A4,A5,A10,Th5;
then
A20: (L-1_F)*(e`3_3-g`3_3)=(L+1_F)*(e`3_3-f`3_3) by A18,Lm9;
h`1_3=f`1_3+g`1_3-e`1_3 by A3,A4,A5,A10,Th5;
then (L-1_F)*(e`1_3-g`1_3)=(L+1_F)*(e`1_3-f`1_3) by A16,Lm9;
then L+1_F=0.F & L-1_F=0.F by A5,A15,A19,A20,Th4;
then L+1_F-(L-1_F)=0.F+(-0.F) by RLVECT_1:def 11;
then L+1_F-(L-1_F)=0.F by RLVECT_1:5;
then L+1_F+(-(L-1_F))=0.F by RLVECT_1:def 11;
then L+1_F+(1_F+-L)=0.F by RLVECT_1:33;
then (L+1_F+1_F)+(-L)=0.F by RLVECT_1:def 3;
then (1_F+1_F+L)+(-L)=0.F by RLVECT_1:def 3;
then 1_F+1_F+(L+(-L))=0.F by RLVECT_1:def 3;
then 1_F+1_F+0.F=0.F by RLVECT_1:5;
hence contradiction by A1,RLVECT_1:4;
end;
theorem Th8:
not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r
& a,b '||' p,q & a,c '||' p,r implies b,c '||' q,r
proof
assume that
A1: not a,p '||' a,b and
A2: not a,p '||' a,c and
A3: a,p '||' b,q and
A4: a,p '||' c,r and
A5: a,b '||' p,q and
A6: a,c '||' p,r;
consider i,j,k,l such that
A7: [[a,p],[c,r]]=[[i,j],[k,l]] and
(ex L st L*(i`1_3-j`1_3) = k`1_3-l`1_3 & L*(i`2_3-j`2_3) = k`2_3-l`2_3 &
L*(i`3_3-j`3_3 ) =
k`3_3-l`3_3) or i`1_3-j`1_3 = 0.F & i`2_3-j`2_3 = 0.F & i`3_3-j`3_3 = 0.F
by A4,Th2;
consider e,f,g,h such that
A8: [[a,b],[p,q]]=[[e,f],[g,h]] and
(ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 & K*(e`2_3-f`2_3) = g`2_3-h`2_3 &
K*(e`3_3-f`3_3 ) =
g`3_3-h`3_3) or e`1_3-f`1_3 = 0.F & e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F
by A5,Th2;
A9: a=e & p=g by A8,MCART_1:93;
A10: c =k by A7,MCART_1:93;
then
A11: [[a,p],[c,r]]=[[e,g],[k,l]] by A9,A7,MCART_1:93;
then
A12: l`1_3=g`1_3+k`1_3-e`1_3 by A2,A4,A6,Th5;
A13: b=f by A8,MCART_1:93;
then
A14: [[a,p],[b,q]]=[[e,g],[f,h]] by A8,A9,MCART_1:93;
then h`1_3=g`1_3+f`1_3-e`1_3 by A1,A3,A5,Th5;
then
A15: 1_F*(f`1_3-k`1_3)=h`1_3-l`1_3 by A12,Lm10;
A16: l`3_3=g`3_3+k`3_3-e`3_3 by A2,A4,A6,A11,Th5;
A17: l`2_3=g`2_3+k`2_3-e`2_3 by A2,A4,A6,A11,Th5;
h`3_3=g`3_3+f`3_3-e`3_3 by A1,A3,A5,A14,Th5;
then
A18: 1_F*(f`3_3-k`3_3)=h`3_3-l`3_3 by A16,Lm10;
h`2_3=g`2_3+f`2_3-e`2_3 by A1,A3,A5,A14,Th5;
then
A19: 1_F*(f`2_3-k`2_3)=h`2_3-l`2_3 by A17,Lm10;
q=h by A8,MCART_1:93;
then [[b,c],[q,r]]=[[f,k],[h,l]] by A13,A7,A10,MCART_1:93;
hence thesis by A15,A19,A18,Th2;
end;
:: 2. DEFINITION OF A FANO-DESARGUES SPACE
definition
let IT be ParSp;
attr IT is FanodesSp-like means
:Def1:
(ex a,b,c being Element of IT st not
a,b '||' a,c) & (for a,b,c,d being Element of IT holds b,c '||' a,d & a,b '||'
c,d & a,c '||' b,d implies a,b '||' a,c) & for a,b,c,p,q,r being Element of IT
holds not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b
'||' p,q & a,c '||' p,r implies b,c '||' q,r;
end;
registration
cluster strict FanodesSp-like for ParSp;
existence
proof
set FF = the Fanoian Field;
reconsider FdSp=MPS(FF) as ParSp by Th1;
1_FF+1_FF<>0.FF by VECTSP_1:def 19;
then
A1: for a,b,c,d being Element of FdSp holds b,c '||' a,d & a,b '||' c,d &
a,c '||' b,d implies a,b '||' a,c by Th7;
( ex a,b,c being Element of FdSp st not a,b '||' a,c)& for a,b,c,p,q,r
being Element of FdSp holds not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q
& a,p '||' c,r & a,b '||' p,q & a,c '||' p,r implies b, c '||' q,r by Th6,Th8;
then FdSp is FanodesSp-like by A1;
hence thesis;
end;
end;
definition
mode FanodesSp is FanodesSp-like ParSp;
end;
reserve FdSp for FanodesSp;
reserve a,b,c,d,p,q,r,s,o,x,y for Element of FdSp;
:: 3. AXIOMS OF A FANO-DESARGUES PARALLELITY SPACE
theorem Th9:
p<>q implies ex r st not p,q '||' p,r
proof
consider a,b,c such that
A1: not a,b '||' a,c by Def1;
assume p<>q;
then not p,q '||' p,a or not p,q '||' p,b or not p,q '||' p,c by A1,
PARSP_1:38;
hence thesis;
end;
definition
let FdSp,a,b,c;
pred a,b,c are_collinear means
a,b '||' a,c;
end;
theorem Th10:
a,b,c are_collinear implies a,c,b are_collinear & c,b,a
are_collinear & b,a,c are_collinear & b,c,a are_collinear &
c,a,b are_collinear
by PARSP_1:24;
theorem Th11:
not a,b,c are_collinear & a,b '||' p,q & a,c '||' p,r & p<>q & p
<>r implies not p,q,r are_collinear
by PARSP_1:30;
theorem Th12:
a=b or b=c or c =a implies a,b,c are_collinear
by PARSP_1:25;
theorem Th13:
a<>b & a,b,p are_collinear & a,b,q are_collinear & a,b,r
are_collinear implies p,q,r are_collinear
proof
assume that
A1: a<>b and
A2: a,b,p are_collinear and
A3: a,b,q are_collinear and
A4: a,b,r are_collinear;
A5: a,b '||' a,p by A2;
a,b '||' a,r by A4;
then
A6: a,b '||' p,r by A5,PARSP_1:35;
a,b '||' a,q by A3;
then a,b '||' p,q by A5,PARSP_1:35;
then p,q '||' p,r by A1,A6,PARSP_1:def 12;
hence thesis;
end;
theorem Th14:
p<>q implies ex r st not p,q,r are_collinear
proof
assume p<>q;
then consider r such that
A1: not p,q '||' p,r by Th9;
not p,q,r are_collinear by A1;
hence thesis;
end;
theorem Th15:
a,b,c are_collinear & a,b,d are_collinear implies a,b '||' c,d
by PARSP_1:35;
theorem Th16:
not a,b,c are_collinear & a,b '||' c,d implies not a,b,d are_collinear
proof
assume that
A1: not a,b,c are_collinear and
A2: a,b '||' c,d;
A3: now
assume that
A4: c <>d and
A5: a<>d;
a,c '||' c,a & c <>a by A1,PARSP_1:25;
then not c,d,a are_collinear by A1,A2,A4,Th11;
then
A6: not d,c,a are_collinear by Th10;
A7: d,a '||' a,d by PARSP_1:25;
a<>b & d,c '||' a,b by A1,A2,Th12,PARSP_1:23;
hence thesis by A5,A6,A7,Th11;
end;
a <> d by A1,A2,PARSP_1:23;
hence thesis by A1,A3;
end;
theorem Th17:
not a,b,c are_collinear & a,b '||' c,d & c <>d implies
not a,b,x are_collinear or not c,d,x are_collinear
by Th16,PARSP_1:26;
theorem
not o,a,b are_collinear implies not o,a,x are_collinear or not o,b,x
are_collinear or o=x
proof
assume
A1: not o,a,b are_collinear;
now
assume that
A2: o,a,x are_collinear and
A3: o,b,x are_collinear;
a,o,x are_collinear by A2,Th10;
then
A4: a,o '||' a,x;
b,o,x are_collinear by A3,Th10;
then
A5: b,o '||' b,x;
not a,b,o are_collinear by A1,Th10;
then not a,b '||' a,o;
hence thesis by A4,A5,PARSP_1:33;
end;
hence thesis;
end;
theorem
o<>a & o<>b & o,a,b are_collinear & o,a,p are_collinear & o,b,q
are_collinear implies a,b '||' p,q
proof
assume that
A1: o<>a and
A2: o<>b and
A3: o,a,b are_collinear and
A4: o,a,p are_collinear and
A5: o,b,q are_collinear;
A6: now
A7: o,a '||' o,b by A3;
o,a '||' o,p by A4;
then
A8: o,b '||' o,p by A1,A7,PARSP_1:def 12;
o,b '||' o,q by A5;
then o,p '||' o,q by A2,A8,PARSP_1:def 12;
then
A9: o,p '||' p,q by PARSP_1:24;
o,b '||' a,b by A7,PARSP_1:24;
then
A10: a,b '||' o,p by A2,A8,PARSP_1:def 12;
assume o<>p;
hence thesis by A10,A9,PARSP_1:26;
end;
now
assume
A11: o=p;
then p,a '||' p,b by A3;
then
A12: a,b '||' p,b by PARSP_1:24;
p,b '||' p,q by A5,A11;
hence thesis by A2,A11,A12,PARSP_1:26;
end;
hence thesis by A6;
end;
theorem
not a,b '||' c,d & a,b,p are_collinear & a,b,q are_collinear & c,d,p
are_collinear & c,d,q are_collinear implies p=q
proof
assume that
A1: not a,b '||' c,d and
A2: a,b,p are_collinear & a,b,q are_collinear and
A3: c,d,p are_collinear & c,d,q are_collinear;
c,d '||' p,q by A3,Th15;
then
A4: p,q '||' c,d by PARSP_1:23;
a,b '||' p,q by A2,Th15;
then p,q '||' a,b by PARSP_1:23;
hence thesis by A1,A4,PARSP_1:def 12;
end;
theorem
a<>b & a,b,c are_collinear & a,b '||' c,d implies a,c '||' b,d
proof
assume that
A1: a<>b and
A2: a,b,c are_collinear and
A3: a,b '||' c,d;
now
A4: a,b '||' a,c by A2;
then a,b '||' c,b by PARSP_1:24;
then c,b '||' c,d by A1,A3,PARSP_1:def 12;
then
A5: b,c '||' b,d by PARSP_1:24;
assume
A6: b<>c;
b,c '||' a,c by A4,PARSP_1:24;
hence thesis by A6,A5,PARSP_1:def 12;
end;
hence thesis by A3;
end;
theorem
a<>b & a,b,c are_collinear & a,b '||' c,d implies c,b '||' c,d
proof
assume that
A1: a<>b and
A2: a,b,c are_collinear and
A3: a,b '||' c,d;
now
a,b '||' a,c by A2;
then
A4: a,c '||' c,b & a,c '||' c,d by A1,A3,PARSP_1:24,def 12;
assume a<>c;
hence thesis by A4,PARSP_1:def 12;
end;
hence thesis by A3;
end;
theorem
not o,a,c are_collinear & o,a,b are_collinear & o,c,p are_collinear & o,c
,q are_collinear & a,c '||' b,p & a,c '||' b,q implies p=q
by PARSP_1:34;
theorem
a<>b & a,b,c are_collinear & a,b,d are_collinear implies a,c,d are_collinear
by PARSP_1:def 12;
theorem
a,b,c are_collinear & a,c,d are_collinear & a<>c implies b,c,d are_collinear
proof
assume that
A1: a,b,c are_collinear and
A2: a,c,d are_collinear & a<>c;
A3: a,c,c are_collinear by Th12;
a,c,b are_collinear by A1,Th10;
hence thesis by A2,A3,Th13;
end;
definition
let FdSp,a,b,c,d;
pred parallelogram a,b,c,d means
not a,b,c are_collinear & a,b '||' c, d & a,c '||' b,d;
end;
theorem Th26:
parallelogram a,b,c,d implies a<>b & b<>c & c <>a & a<>d & b<>d & c <>d
proof
assume
A1: parallelogram a,b,c,d;
A2: now
assume a=d;
then a,b '||' c,a by A1;
then
A3: a,b '||' a,c by PARSP_1:23;
not a,b,c are_collinear by A1;
hence contradiction by A3;
end;
A4: now
assume c =d;
then a,c '||' b,c by A1;
then c,a '||' c,b by PARSP_1:23;
then
A5: a,b '||' a,c by PARSP_1:24;
not a,b,c are_collinear by A1;
hence contradiction by A5;
end;
A6: now
assume b=d;
then a,b '||' c,b by A1;
then b,a '||' b,c by PARSP_1:23;
then
A7: a,b '||' a,c by PARSP_1:24;
not a,b,c are_collinear by A1;
hence contradiction by A7;
end;
not a,b,c are_collinear by A1;
hence thesis by A2,A6,A4,Th12;
end;
theorem Th27:
parallelogram a,b,c,d implies not a,b,c are_collinear & not b,a,d
are_collinear & not c,d,a are_collinear & not d,c,b are_collinear
proof
A1: a,b '||' b,a & a,c '||' c,a by PARSP_1:25;
assume
A2: parallelogram a,b,c,d;
then
A3: d<>b by Th26;
a,c '||' b,d by A2;
then
A4: a,c '||' d,b by PARSP_1:23;
a,b '||' c,d by A2;
then
A5: a,b '||' d,c by PARSP_1:23;
A6: ( not a,b,c are_collinear)& d<>c by A2,Th26;
A7: a,b '||' c,d & c <>a by A2,Th26;
a,c '||' b,d & b<>a by A2,Th26;
hence thesis by A1,A7,A5,A4,A6,A3,Th11;
end;
theorem Th28:
parallelogram a,b,c,d implies not a,b,c are_collinear & not b,a,d
are_collinear & not c,d,a are_collinear & not d,c,b are_collinear & not a,c,b
are_collinear & not b,a,c are_collinear & not b,c,a are_collinear & not c,a,b
are_collinear & not c,b,a are_collinear & not b,d,a are_collinear & not a,b,d
are_collinear & not a,d,b are_collinear & not d,a,b are_collinear & not d,b,a
are_collinear & not c,a,d are_collinear & not a,c,d are_collinear & not a,d,c
are_collinear & not d,a,c are_collinear & not d,c,a are_collinear & not d,b,c
are_collinear & not b,c,d are_collinear & not b,d,c are_collinear & not c,b,d
are_collinear & not c,d,b are_collinear
proof
assume
A1: parallelogram a,b,c,d;
then
A2: ( not c,d,a are_collinear)& not d,c,b are_collinear by Th27;
( not a,b,c are_collinear)& not b,a,d are_collinear by A1,Th27;
hence thesis by A2,Th10;
end;
theorem Th29:
parallelogram a,b,c,d implies not a,b,x are_collinear or not c,d,
x are_collinear
proof
assume
A1: parallelogram a,b,c,d;
then
A2: c <>d by Th26;
( not a,b,c are_collinear)& a,b '||' c,d by A1;
hence thesis by A2,Th17;
end;
theorem Th30:
parallelogram a,b,c,d implies parallelogram a,c,b,d
by Th28;
theorem Th31:
parallelogram a,b,c,d implies parallelogram c,d,a,b
by PARSP_1:23,Th28;
theorem Th32:
parallelogram a,b,c,d implies parallelogram b,a,d,c
by PARSP_1:23,Th28;
theorem Th33:
parallelogram a,b,c,d implies parallelogram a,c,b,d &
parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b &
parallelogram d,b,c,a & parallelogram b,d,a,c & parallelogram d,c,b,a
proof
assume
A1: parallelogram a,b,c,d;
then parallelogram c,d,a,b by Th31;
then
A2: parallelogram c,a,d,b by Th30;
parallelogram b,a,d,c by A1,Th32;
hence thesis by A1,A2,Th30,Th31;
end;
theorem Th34:
not a,b,c are_collinear implies ex d st parallelogram a,b,c,d
proof
consider d such that
A1: a,b '||' c,d & a,c '||' b,d by PARSP_1:def 12;
assume not a,b,c are_collinear;
then parallelogram a,b,c,d by A1;
hence thesis;
end;
theorem Th35:
parallelogram a,b,c,p & parallelogram a,b,c,q implies p=q
proof
assume that
A1: parallelogram a,b,c,p and
A2: parallelogram a,b,c,q;
a,b '||'c,p by A1;
then
A3: b,c '||' c,b & b,a '||' c,p by PARSP_1:23,25;
a,b '||' c,q by A2;
then
A4: b,a '||' c,q by PARSP_1:23;
a,c '||' b,p by A1;
then
A5: c,a '||' b,p by PARSP_1:23;
a,c '||' b,q by A2;
then
A6: c,a '||' b,q by PARSP_1:23;
not b,c,a are_collinear by A1,Th28;
then not b,c '||' b,a;
hence thesis by A3,A4,A5,A6,PARSP_1:34;
end;
theorem Th36:
parallelogram a,b,c,d implies not a,d '||' b,c
proof
assume
A1: parallelogram a,b,c,d;
then not a,b,c are_collinear;
then
A2: not a,b '||' a,c;
a,b '||' c,d & a,c '||' b,d by A1;
then not b,c '||' a,d by A2,Def1;
hence thesis by PARSP_1:19;
end;
theorem Th37:
parallelogram a,b,c,d implies not parallelogram a,b,d,c
by Th36;
theorem Th38:
a<>b implies ex c st a,b,c are_collinear & c <>a & c <>b
proof
assume a<>b;
then consider p such that
A1: not a,b,p are_collinear by Th14;
consider q such that
A2: parallelogram a,b,p,q by A1,Th34;
not p,q,b are_collinear by A2,Th28;
then consider c such that
A3: parallelogram p,q,b,c by Th34;
A4: p,q '||' b,c by A3;
p<>q & a,b '||' p,q by A2,Th26;
then a,b '||' b,c by A4,PARSP_1:26;
then b,a '||' b,c by PARSP_1:23;
then b,a,c are_collinear;
then
A5: a,b,c are_collinear by Th10;
A6: not a,q '||' b,p by A2,Th36;
p,b '||' q,c by A3;
then
A7: a<>c by A6,PARSP_1:23;
b<>c by A3,Th26;
hence thesis by A7,A5;
end;
theorem Th39:
parallelogram a,p,b,q & parallelogram a,p,c,r implies b,c '||' q ,r
proof
assume that
A1: parallelogram a,p,b,q and
A2: parallelogram a,p,c,r;
A3: a,p '||' c,r & a,c '||' p,r by A2;
not a,p,c are_collinear by A2;
then
A4: not a,p '||' a,c;
not a,p,b are_collinear by A1;
then
A5: not a,p '||' a,b;
a,p '||' b,q & a,b '||' p,q by A1;
hence thesis by A5,A4,A3,Def1;
end;
theorem Th40:
not b,q,c are_collinear & parallelogram a,p,b,q & parallelogram a
,p,c,r implies parallelogram b,q,c,r
proof
assume that
A1: not b,q,c are_collinear and
A2: parallelogram a,p,b,q and
A3: parallelogram a,p,c,r;
A4: a,p '||' c,r by A3;
a<>p & a,p '||' b,q by A2,Th26;
then
A5: b,q '||' c,r by A4,PARSP_1:def 12;
b,c '||' q,r by A2,A3,Th39;
hence thesis by A1,A5;
end;
theorem Th41:
a,b,c are_collinear & b<>c & parallelogram a,p,b,q &
parallelogram a,p,c,r implies parallelogram b,q,c,r
proof
assume that
A1: a,b,c are_collinear and
A2: b<>c and
A3: parallelogram a,p,b,q and
A4: parallelogram a,p,c,r;
A5: b<>q by A3,Th26;
a,b '||'a,c by A1;
then
A6: a,b '||' b,c by PARSP_1:24;
thus thesis by A2,A3,A4,A5,A6,Th11,Th40;
end;
theorem Th42:
parallelogram a,p,b,q & parallelogram a,p,c,r & parallelogram b,
q,d,s implies c,d '||' r,s
proof
assume that
A1: parallelogram a,p,b,q and
A2: parallelogram a,p,c,r and
A3: parallelogram b,q,d,s;
A4: now
assume
A5: not a,p,d are_collinear;
parallelogram b,q,a,p by A1,Th33;
then parallelogram a,p,d,s by A3,A5,Th40;
hence thesis by A2,Th39;
end;
A6: now
A7: a<>p by A1,Th26;
A8: ( not a,p,b are_collinear)& a,p '||' a,p by A1,PARSP_1:25;
assume that
A9: b,q,c are_collinear and
A10: a,p,d are_collinear;
a<>b by A1,Th26;
then consider x such that
A11: a,b,x are_collinear and
A12: x<>a and
A13: x<>b by Th38;
a,b '||' a,x by A11;
then consider y such that
A14: parallelogram a,p,x,y by A12,A8,A7,Th11,Th34;
A15: not x,y,d are_collinear by A10,A14,Th29;
parallelogram b,q,x,y by A1,A11,A13,A14,Th41;
then
A16: parallelogram x,y,d,s by A3,A15,Th40;
not x,y,c are_collinear by A1,A9,A11,A13,A14,Th29,Th41;
then parallelogram x,y,c,r by A2,A14,Th40;
hence thesis by A16,Th39;
end;
now
assume not b,q,c are_collinear;
then parallelogram b,q,c,r by A1,A2,Th40;
hence thesis by A3,Th39;
end;
hence thesis by A4,A6;
end;
theorem Th43:
a<>b implies ex c,d st parallelogram a,b,c,d
proof
assume a<>b;
then consider c such that
A1: not a,b,c are_collinear by Th14;
ex d st parallelogram a,b,c,d by A1,Th34;
hence thesis;
end;
theorem
a<>d implies ex b,c st parallelogram a,b,c,d
proof
assume a<>d;
then consider b such that
A1: not a,d,b are_collinear by Th14;
not b,a,d are_collinear by A1,Th10;
then consider c such that
A2: parallelogram b,a,d,c by Th34;
parallelogram a,b,c,d by A2,Th33;
hence thesis;
end;
definition
let FdSp,a,b,r,s;
pred a,b congr r,s means
a=b & r=s or ex p,q st parallelogram p,q,a,b & parallelogram p,q,r,s;
end;
theorem Th45:
a,a congr b,c implies b=c
by Th26;
theorem
a,b congr c,c implies a=b
by Th26;
theorem
a,b congr b,a implies a=b
by Th37;
theorem Th48:
a,b congr c,d implies a,b '||' c,d
proof
assume
A1: a,b congr c,d;
now
assume a<>b;
then consider p,q such that
A2: parallelogram p,q,a,b and
A3: parallelogram p,q,c,d by A1;
A4: p,q '||' c,d by A3;
p<>q & p,q '||' a,b by A2,Th26;
hence thesis by A4,PARSP_1:def 12;
end;
hence thesis by PARSP_1:20;
end;
theorem Th49:
a,b congr c,d implies a,c '||' b,d
proof
assume
A1: a,b congr c,d;
A2: now
assume
A3: a=b;
then c =d by A1,Th45;
hence thesis by A3,PARSP_1:25;
end;
a<>b implies thesis by A1,Th39;
hence thesis by A2;
end;
theorem Th50:
a,b congr c,d & not a,b,c are_collinear implies parallelogram a,b ,c,d
by Th48,Th49;
theorem Th51:
parallelogram a,b,c,d implies a,b congr c,d
proof
A1: a,b '||' a,b by PARSP_1:25;
assume
A2: parallelogram a,b,c,d;
then
A3: ( not a,c,b are_collinear)& a<>b by Th26,Th28;
a<>c by A2,Th26;
then consider p such that
A4: a,c,p are_collinear and
A5: a<>p and
A6: c <>p by Th38;
a,c '||' a,p by A4;
then consider q such that
A7: parallelogram a,p,b,q by A5,A1,A3,Th11,Th34;
parallelogram a,b,p,q by A7,Th33;
then parallelogram c,d,p,q by A2,A4,A6,Th41;
then
A8: parallelogram p,q,c,d by Th33;
parallelogram p,q,a,b by A7,Th33;
hence thesis by A8;
end;
theorem Th52:
a,b congr c,d & a,b,c are_collinear & parallelogram r,s,a,b
implies parallelogram r,s,c,d
proof
assume that
A1: a,b congr c,d and
A2: a,b,c are_collinear and
A3: parallelogram r,s,a,b;
now
assume
A4: a<>b;
then consider p,q such that
A5: parallelogram p,q,a,b and
A6: parallelogram p,q,c,d by A1;
r,s '||' a,b & a,b '||' c,d by A1,A3,Th48;
then
A7: r,s '||' c,d by A4,PARSP_1:26;
A8: parallelogram a,b,r,s by A3,Th33;
parallelogram a,b,p,q by A5,Th33;
then
A9: r,c '||' s,d by A6,A8,Th42;
not r,s,c are_collinear by A2,A3,Th29;
hence thesis by A7,A9;
end;
hence thesis by A3,Th26;
end;
theorem
a,b congr c,x & a,b congr c,y implies x=y
proof
assume that
A1: a,b congr c,x and
A2: a,b congr c,y;
A3: now
assume that
a<>b and
A4: not a,b,c are_collinear;
parallelogram a,b,c,x & parallelogram a,b,c,y by A1,A2,A4,Th50;
hence thesis by Th35;
end;
A5: now
assume that
A6: a<>b and
A7: a,b,c are_collinear;
consider p,q such that
A8: parallelogram a,b,p,q by A6,Th43;
parallelogram p,q,a,b by A8,Th33;
then parallelogram p,q,c,x & parallelogram p,q,c,y by A1,A2,A7,Th52;
hence thesis by Th35;
end;
now
assume
A9: a=b;
then c =x by A1,Th45;
hence thesis by A2,A9,Th45;
end;
hence thesis by A5,A3;
end;
theorem
ex d st a,b congr c,d
proof
A1: now
assume a=b;
then a,b congr c,c;
hence thesis;
end;
A2: now
assume that
A3: a<>b and
A4: a,b,c are_collinear;
consider p,q such that
A5: parallelogram a,b,p,q by A3,Th43;
not p,q,c are_collinear by A4,A5,Th29;
then consider d such that
A6: parallelogram p,q,c,d by Th34;
parallelogram p,q,a,b by A5,Th33;
then a,b congr c,d by A6;
hence thesis;
end;
now
assume that
a<>b and
A7: not a,b,c are_collinear;
ex d st parallelogram a,b,c,d by A7,Th34;
hence thesis by Th51;
end;
hence thesis by A1,A2;
end;
theorem
a,b congr a,b
proof
now
assume a<>b;
then consider p,q such that
A1: parallelogram a,b,p,q by Th43;
parallelogram p,q,a,b by A1,Th33;
hence thesis;
end;
hence thesis;
end;
theorem
r,s congr a,b & r,s congr c,d implies a,b congr c,d
proof
assume that
A1: r,s congr a,b and
A2: r,s congr c,d;
A3: now
assume that
r<>s and
A4: ( not r,s,a are_collinear)& not r,s,c are_collinear;
parallelogram r,s,a,b & parallelogram r,s,c,d by A1,A2,A4,Th50;
hence thesis;
end;
A5: now
assume that
A6: r<>s and
A7: r,s,c are_collinear;
consider p,q such that
A8: parallelogram p,q,r,s and
A9: parallelogram p,q,a,b by A1,A6;
parallelogram p,q,c,d by A2,A7,A8,Th52;
hence thesis by A9;
end;
A10: now
assume that
A11: r<>s and
A12: r,s,a are_collinear;
consider p,q such that
A13: parallelogram p,q,r,s and
A14: parallelogram p,q,c,d by A2,A11;
parallelogram p,q,a,b by A1,A12,A13,Th52;
hence thesis by A14;
end;
r=s implies thesis by A1,A2,Th45;
hence thesis by A10,A5,A3;
end;
theorem
a,b congr c,d implies c,d congr a,b;
theorem
a,b congr c,d implies b,a congr d,c
proof
assume
A1: a,b congr c,d;
A2: now
assume a<>b;
then consider p,q such that
A3: parallelogram p,q,a,b & parallelogram p,q,c,d by A1;
parallelogram q,p,b,a & parallelogram q,p,d,c by A3,Th33;
hence thesis;
end;
a=b implies thesis by A1,Th45;
hence thesis by A2;
end;