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