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 are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear holds

r,r1,r2 are_collinear

let q, r, r1, r2 be Element of (ProjectiveSpace V); :: thesis: ( p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear implies r,r1,r2 are_collinear )

assume that

A1: p <> q and

A2: p,q,r are_collinear and

A3: p,q,r1 are_collinear and

A4: p,q,r2 are_collinear ; :: thesis: r,r1,r2 are_collinear

consider u1, v1, w1 being Element of V such that

A5: p = Dir u1 and

A6: q = Dir v1 and

A7: r = Dir w1 and

A8: not u1 is zero and

A9: not v1 is zero and

A10: not w1 is zero and

A11: u1,v1,w1 are_LinDep by A2, Th23;

consider v being Element of V such that

A12: not v is zero and

A13: q = Dir v by ANPROJ_1:26;

A14: are_Prop v1,v by A12, A13, A6, A9, ANPROJ_1:22;

consider u3, v3, w3 being Element of V such that

A15: p = Dir u3 and

A16: q = Dir v3 and

A17: r2 = Dir w3 and

A18: not u3 is zero and

A19: not v3 is zero and

A20: not w3 is zero and

A21: u3,v3,w3 are_LinDep by A4, Th23;

A22: are_Prop v3,v by A12, A13, A16, A19, ANPROJ_1:22;

consider u2, v2, w2 being Element of V such that

A23: p = Dir u2 and

A24: q = Dir v2 and

A25: r1 = Dir w2 and

A26: not u2 is zero and

A27: not v2 is zero and

A28: not w2 is zero and

A29: u2,v2,w2 are_LinDep by A3, Th23;

A30: are_Prop v2,v by A12, A13, A24, A27, ANPROJ_1:22;

consider u being Element of V such that

A31: not u is zero and

A32: p = Dir u by ANPROJ_1:26;

are_Prop u1,u by A31, A32, A5, A8, ANPROJ_1:22;

then A33: u,v,w1 are_LinDep by A11, A14, ANPROJ_1:4;

are_Prop u3,u by A31, A32, A15, A18, ANPROJ_1:22;

then A34: u,v,w3 are_LinDep by A21, A22, ANPROJ_1:4;

are_Prop u2,u by A31, A32, A23, A26, ANPROJ_1:22;

then A35: u,v,w2 are_LinDep by A29, A30, ANPROJ_1:4;

not are_Prop u,v by A1, A31, A32, A12, A13, ANPROJ_1:22;

then w1,w2,w3 are_LinDep by A31, A12, A33, A35, A34, ANPROJ_1:14;

hence r,r1,r2 are_collinear by A7, A10, A25, A28, A17, A20, Th23; :: thesis: verum

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 are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear holds

r,r1,r2 are_collinear

let q, r, r1, r2 be Element of (ProjectiveSpace V); :: thesis: ( p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear implies r,r1,r2 are_collinear )

assume that

A1: p <> q and

A2: p,q,r are_collinear and

A3: p,q,r1 are_collinear and

A4: p,q,r2 are_collinear ; :: thesis: r,r1,r2 are_collinear

consider u1, v1, w1 being Element of V such that

A5: p = Dir u1 and

A6: q = Dir v1 and

A7: r = Dir w1 and

A8: not u1 is zero and

A9: not v1 is zero and

A10: not w1 is zero and

A11: u1,v1,w1 are_LinDep by A2, Th23;

consider v being Element of V such that

A12: not v is zero and

A13: q = Dir v by ANPROJ_1:26;

A14: are_Prop v1,v by A12, A13, A6, A9, ANPROJ_1:22;

consider u3, v3, w3 being Element of V such that

A15: p = Dir u3 and

A16: q = Dir v3 and

A17: r2 = Dir w3 and

A18: not u3 is zero and

A19: not v3 is zero and

A20: not w3 is zero and

A21: u3,v3,w3 are_LinDep by A4, Th23;

A22: are_Prop v3,v by A12, A13, A16, A19, ANPROJ_1:22;

consider u2, v2, w2 being Element of V such that

A23: p = Dir u2 and

A24: q = Dir v2 and

A25: r1 = Dir w2 and

A26: not u2 is zero and

A27: not v2 is zero and

A28: not w2 is zero and

A29: u2,v2,w2 are_LinDep by A3, Th23;

A30: are_Prop v2,v by A12, A13, A24, A27, ANPROJ_1:22;

consider u being Element of V such that

A31: not u is zero and

A32: p = Dir u by ANPROJ_1:26;

are_Prop u1,u by A31, A32, A5, A8, ANPROJ_1:22;

then A33: u,v,w1 are_LinDep by A11, A14, ANPROJ_1:4;

are_Prop u3,u by A31, A32, A15, A18, ANPROJ_1:22;

then A34: u,v,w3 are_LinDep by A21, A22, ANPROJ_1:4;

are_Prop u2,u by A31, A32, A23, A26, ANPROJ_1:22;

then A35: u,v,w2 are_LinDep by A29, A30, ANPROJ_1:4;

not are_Prop u,v by A1, A31, A32, A12, A13, ANPROJ_1:22;

then w1,w2,w3 are_LinDep by A31, A12, A33, A35, A34, ANPROJ_1:14;

hence r,r1,r2 are_collinear by A7, A10, A25, A28, A17, A20, Th23; :: thesis: verum