let V be up-3-dimensional RealLinearSpace; ProjectiveSpace V is Desarguesian
let o, p1, p2, p3, q1, q2, q3, r1, r2, r3 be Element of ; ANPROJ_2:def 12 ( o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not o,p1,p2 is_collinear & not o,p1,p3 is_collinear & not o,p2,p3 is_collinear & p1,p2,r3 is_collinear & q1,q2,r3 is_collinear & p2,p3,r1 is_collinear & q2,q3,r1 is_collinear & p1,p3,r2 is_collinear & q1,q3,r2 is_collinear & o,p1,q1 is_collinear & o,p2,q2 is_collinear & o,p3,q3 is_collinear implies r1,r2,r3 is_collinear )
assume that
A1:
o <> q1
and
A2:
p1 <> q1
and
A3:
o <> q2
and
A4:
p2 <> q2
and
A5:
o <> q3
and
A6:
p3 <> q3
and
A7:
not o,p1,p2 is_collinear
and
A8:
( not o,p1,p3 is_collinear & not o,p2,p3 is_collinear )
and
A9:
p1,p2,r3 is_collinear
and
A10:
q1,q2,r3 is_collinear
and
A11:
p2,p3,r1 is_collinear
and
A12:
q2,q3,r1 is_collinear
and
A13:
p1,p3,r2 is_collinear
and
A14:
q1,q3,r2 is_collinear
and
A15:
o,p1,q1 is_collinear
and
A16:
o,p2,q2 is_collinear
and
A17:
o,p3,q3 is_collinear
; r1,r2,r3 is_collinear
consider q1', q2', r3'' being Element of such that
A18:
q1 = Dir q1'
and
A19:
q2 = Dir q2'
and
A20:
r3 = Dir r3''
and
A21:
not q1' is zero
and
A22:
not q2' is zero
and
A23:
not r3'' is zero
and
A24:
q1',q2',r3'' are_LinDep
by A10, Th24;
consider q2'', q3', r1'' being Element of such that
A25:
q2 = Dir q2''
and
A26:
q3 = Dir q3'
and
A27:
r1 = Dir r1''
and
A28:
not q2'' is zero
and
A29:
not q3' is zero
and
A30:
not r1'' is zero
and
A31:
q2'',q3',r1'' are_LinDep
by A12, Th24;
A32:
are_Prop q2'',q2'
by A19, A22, A25, A28, ANPROJ_1:35;
consider p2'', p3', r1' being Element of such that
A33:
p2 = Dir p2''
and
A34:
p3 = Dir p3'
and
A35:
r1 = Dir r1'
and
A36:
not p2'' is zero
and
A37:
not p3' is zero
and
A38:
not r1' is zero
and
A39:
p2'',p3',r1' are_LinDep
by A11, Th24;
A40:
not are_Prop p3',q3'
by A6, A34, A37, A26, A29, ANPROJ_1:35;
are_Prop r1'',r1'
by A35, A38, A27, A30, ANPROJ_1:35;
then A41:
q2',q3',r1' are_LinDep
by A31, A32, ANPROJ_1:9;
consider p1'', p3'', r2' being Element of such that
A42:
p1 = Dir p1''
and
A43:
p3 = Dir p3''
and
A44:
r2 = Dir r2'
and
A45:
not p1'' is zero
and
A46:
not p3'' is zero
and
A47:
not r2' is zero
and
A48:
p1'',p3'',r2' are_LinDep
by A13, Th24;
A49:
are_Prop p3'',p3'
by A34, A37, A43, A46, ANPROJ_1:35;
consider o' being Element of such that
A50:
not o' is zero
and
A51:
o = Dir o'
by ANPROJ_1:42;
A52:
not are_Prop o',q3'
by A5, A50, A51, A26, A29, ANPROJ_1:35;
consider p1', p2', r3' being Element of such that
A53:
p1 = Dir p1'
and
A54:
p2 = Dir p2'
and
A55:
r3 = Dir r3'
and
A56:
not p1' is zero
and
A57:
not p2' is zero
and
A58:
not r3' is zero
and
A59:
p1',p2',r3' are_LinDep
by A9, Th24;
A60:
( not are_Prop p1',q1' & not are_Prop p2',q2' )
by A2, A4, A53, A54, A56, A57, A18, A19, A21, A22, ANPROJ_1:35;
A61:
( not are_Prop o',q1' & not are_Prop o',q2' )
by A1, A3, A50, A51, A18, A19, A21, A22, ANPROJ_1:35;
consider o''', p2''', q2''' being Element of such that
A62:
o = Dir o'''
and
A63:
p2 = Dir p2'''
and
A64:
q2 = Dir q2'''
and
A65:
not o''' is zero
and
A66:
not p2''' is zero
and
A67:
not q2''' is zero
and
A68:
o''',p2''',q2''' are_LinDep
by A16, Th24;
A69:
are_Prop q2''',q2'
by A19, A22, A64, A67, ANPROJ_1:35;
A70:
are_Prop o''',o'
by A50, A51, A62, A65, ANPROJ_1:35;
are_Prop p2''',p2'
by A54, A57, A63, A66, ANPROJ_1:35;
then A71:
o',p2',q2' are_LinDep
by A68, A70, A69, ANPROJ_1:9;
consider q1'', q3'', r2'' being Element of such that
A72:
q1 = Dir q1''
and
A73:
q3 = Dir q3''
and
A74:
r2 = Dir r2''
and
A75:
not q1'' is zero
and
A76:
not q3'' is zero
and
A77:
not r2'' is zero
and
A78:
q1'',q3'',r2'' are_LinDep
by A14, Th24;
A79:
are_Prop q1'',q1'
by A18, A21, A72, A75, ANPROJ_1:35;
A80:
not o',p1',p2' are_LinDep
by A7, A50, A51, A53, A54, A56, A57, Th24;
are_Prop r3'',r3'
by A55, A58, A20, A23, ANPROJ_1:35;
then A81:
q1',q2',r3' are_LinDep
by A24, ANPROJ_1:9;
A82:
are_Prop q3'',q3'
by A26, A29, A73, A76, ANPROJ_1:35;
consider o'''', p3''', q3''' being Element of such that
A83:
o = Dir o''''
and
A84:
p3 = Dir p3'''
and
A85:
q3 = Dir q3'''
and
A86:
not o'''' is zero
and
A87:
not p3''' is zero
and
A88:
not q3''' is zero
and
A89:
o'''',p3''',q3''' are_LinDep
by A17, Th24;
A90:
are_Prop q3''',q3'
by A26, A29, A85, A88, ANPROJ_1:35;
are_Prop p2'',p2'
by A54, A57, A33, A36, ANPROJ_1:35;
then A91:
p2',p3',r1' are_LinDep
by A39, ANPROJ_1:9;
are_Prop p1'',p1'
by A53, A56, A42, A45, ANPROJ_1:35;
then
p1',p3',r2' are_LinDep
by A48, A49, ANPROJ_1:9;
then A92:
p1',p2',p3',r1',r2',r3' lie_on_a_triangle
by A59, A91, Def2;
A93:
q1',q2',q3' are_Prop_Vect
by A21, A22, A29, Def1;
consider o'', p1''', q1''' being Element of such that
A94:
o = Dir o''
and
A95:
p1 = Dir p1'''
and
A96:
q1 = Dir q1'''
and
A97:
not o'' is zero
and
A98:
not p1''' is zero
and
A99:
not q1''' is zero
and
A100:
o'',p1''',q1''' are_LinDep
by A15, Th24;
A101:
are_Prop q1''',q1'
by A18, A21, A96, A99, ANPROJ_1:35;
A102:
( not o',p1',p3' are_LinDep & not o',p2',p3' are_LinDep )
by A8, A50, A51, A53, A54, A56, A57, A34, A37, Th24;
A103:
p1',p2',p3' are_Prop_Vect
by A56, A57, A37, Def1;
A104:
are_Prop o'''',o'
by A50, A51, A83, A86, ANPROJ_1:35;
are_Prop p3''',p3'
by A34, A37, A84, A87, ANPROJ_1:35;
then A105:
o',p3',q3' are_LinDep
by A89, A104, A90, ANPROJ_1:9;
A106:
are_Prop o'',o'
by A50, A51, A94, A97, ANPROJ_1:35;
are_Prop p1''',p1'
by A53, A56, A95, A98, ANPROJ_1:35;
then
o',p1',q1' are_LinDep
by A100, A106, A101, ANPROJ_1:9;
then A107:
o',p1',p2',p3',q1',q2',q3' are_perspective
by A71, A105, Def3;
are_Prop r2'',r2'
by A44, A47, A74, A77, ANPROJ_1:35;
then
q1',q3',r2' are_LinDep
by A78, A79, A82, ANPROJ_1:9;
then A108:
q1',q2',q3',r1',r2',r3' lie_on_a_triangle
by A81, A41, Def2;
r1',r2',r3' are_Prop_Vect
by A58, A38, A47, Def1;
then
r1',r2',r3' are_LinDep
by A50, A61, A52, A60, A40, A103, A93, A107, A80, A102, A92, A108, Th8;
hence
r1,r2,r3 is_collinear
by A55, A58, A35, A38, A44, A47, Th24; verum