let V be non trivial RealLinearSpace; :: thesis: ProjectiveSpace V is transitive
let p be Element of (ProjectiveSpace V); :: according to ANPROJ_2:def 8 :: thesis: for q, r, r1, r2 being Element of (ProjectiveSpace V) st p <> q & p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear holds
r,r1,r2 is_collinear
let q, r, r1, r2 be Element of (ProjectiveSpace V); :: thesis: ( p <> q & p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear implies r,r1,r2 is_collinear )
assume that
A1: p <> q and
A2: ( p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear ) ; :: thesis: r,r1,r2 is_collinear
consider u being Element of V such that
A3: ( not u is zero & p = Dir u ) by ANPROJ_1:42;
consider v being Element of V such that
A4: ( not v is zero & q = Dir v ) by ANPROJ_1:42;
consider u1, v1, w1 being Element of V such that
A5: ( p = Dir u1 & q = Dir v1 & r = Dir w1 & not u1 is zero & not v1 is zero & not w1 is zero & u1,v1,w1 are_LinDep ) by A2, Th24;
consider u2, v2, w2 being Element of V such that
A6: ( p = Dir u2 & q = Dir v2 & r1 = Dir w2 & not u2 is zero & not v2 is zero & not w2 is zero & u2,v2,w2 are_LinDep ) by A2, Th24;
consider u3, v3, w3 being Element of V such that
A7: ( p = Dir u3 & q = Dir v3 & r2 = Dir w3 & not u3 is zero & not v3 is zero & not w3 is zero & u3,v3,w3 are_LinDep ) by A2, Th24;
A8: not are_Prop u,v by A1, A3, A4, ANPROJ_1:35;
( are_Prop u1,u & are_Prop u2,u & are_Prop u3,u & are_Prop v1,v & are_Prop v2,v & are_Prop v3,v & are_Prop w1,w1 & are_Prop w2,w2 & are_Prop w3,w3 ) by A3, A4, A5, A6, A7, ANPROJ_1:35;
then ( u,v,w1 are_LinDep & u,v,w2 are_LinDep & u,v,w3 are_LinDep ) by A5, A6, A7, ANPROJ_1:9;
then w1,w2,w3 are_LinDep by A3, A4, A8, ANPROJ_1:19;
hence r,r1,r2 is_collinear by A5, A6, A7, Th24; :: thesis: verum