set PTR3 = ProjectiveSpace (TOP-REAL 3);
ex u, v, w1 being Element of (TOP-REAL 3) st
for a, b, c being Real st ((a * u) + (b * v)) + (c * w1) = 0. (TOP-REAL 3) holds
( a = 0 & b = 0 & c = 0 )
proof
reconsider u = <e1> , v = <e2> , w = <e3> as Element of (TOP-REAL 3) by EUCLID:22;
take u ; :: thesis: ex v, w1 being Element of (TOP-REAL 3) st
for a, b, c being Real st ((a * u) + (b * v)) + (c * w1) = 0. (TOP-REAL 3) holds
( a = 0 & b = 0 & c = 0 )
take v ; :: thesis: ex w1 being Element of (TOP-REAL 3) st
for a, b, c being Real st ((a * u) + (b * v)) + (c * w1) = 0. (TOP-REAL 3) holds
( a = 0 & b = 0 & c = 0 )
take w ; :: thesis: for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. (TOP-REAL 3) holds
( a = 0 & b = 0 & c = 0 )
now :: thesis: for a, b, c being Real st ((a * <e1>) + (b * <e2>)) + (c * <e3>) = 0. (TOP-REAL 3) holds
( a = 0 & b = 0 & c = 0 )
let a, b, c be Real; :: thesis: ( ((a * <e1>) + (b * <e2>)) + (c * <e3>) = 0. (TOP-REAL 3) implies ( a = 0 & b = 0 & c = 0 ) )
assume ((a * <e1>) + (b * <e2>)) + (c * <e3>) = 0. (TOP-REAL 3) ; :: thesis: ( a = 0 & b = 0 & c = 0 )
then A1: |[a,b,c]| = |[0,0,0]| by EUCLID_5:4, EUCLID_8:39;
( |[a,b,c]| `1 = a & |[a,b,c]| `2 = b & |[a,b,c]| `3 = c ) by EUCLID_5:2;
hence ( a = 0 & b = 0 & c = 0 ) by A1, EUCLID_5:2; :: thesis: verum
end;
hence for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. (TOP-REAL 3) holds
( a = 0 & b = 0 & c = 0 ) ; :: thesis: verum
end;
then TOP-REAL 3 is up-3-dimensional by ANPROJ_2:def 6;
then reconsider PTR3 = ProjectiveSpace (TOP-REAL 3) as CollProjectiveSpace ;
for p, p1, q, q1 being Element of PTR3 ex r being Element of PTR3 st
( p,p1,r are_collinear & q,q1,r are_collinear )
proof
let p, p1, q, q1 be Element of PTR3; :: thesis: ex r being Element of PTR3 st
( p,p1,r are_collinear & q,q1,r are_collinear )
consider up being Element of (TOP-REAL 3) such that
A2: not up is zero and
A3: p = Dir up by ANPROJ_1:26;
consider up1 being Element of (TOP-REAL 3) such that
A4: not up1 is zero and
A5: p1 = Dir up1 by ANPROJ_1:26;
consider uq being Element of (TOP-REAL 3) such that
A6: not uq is zero and
A7: q = Dir uq by ANPROJ_1:26;
consider uq1 being Element of (TOP-REAL 3) such that
A8: not uq1 is zero and
A9: q1 = Dir uq1 by ANPROJ_1:26;
ex r being Element of PTR3 st
( p,p1,r are_collinear & q,q1,r are_collinear )
proof
set w = (up <X> up1) <X> (uq <X> uq1);
per cases ( (up <X> up1) <X> (uq <X> uq1) is zero or not (up <X> up1) <X> (uq <X> uq1) is zero ) ;
suppose (up <X> up1) <X> (uq <X> uq1) is zero ; :: thesis: ex r being Element of PTR3 st
( p,p1,r are_collinear & q,q1,r are_collinear )
per cases then ( are_Prop up,up1 or are_Prop uq,uq1 or are_Prop up <X> up1,uq <X> uq1 ) by A4, A6, A8, A2, Th44;
suppose A12: are_Prop up <X> up1,uq <X> uq1 ; :: thesis: ex r being Element of PTR3 st
( p,p1,r are_collinear & q,q1,r are_collinear )
then consider a being Real such that
a <> 0 and
A13: uq <X> uq1 = a * (up <X> up1) by ANPROJ_1:1;
per cases ( up <X> up1 is zero or not up <X> up1 is zero ) ;
suppose A15: not up <X> up1 is zero ; :: thesis: ex r being Element of PTR3 st
( p,p1,r are_collinear & q,q1,r are_collinear )
A16: not uq <X> uq1 is zero
proof
assume A17: uq <X> uq1 is zero ; :: thesis: contradiction
consider a being Real such that
A18: a <> 0 and
A19: uq <X> uq1 = a * (up <X> up1) by A12, ANPROJ_1:1;
set r1 = (up <X> up1) `1 ;
set r2 = (up <X> up1) `2 ;
set r3 = (up <X> up1) `3 ;
|[(a * ((up <X> up1) `1)),(a * ((up <X> up1) `2)),(a * ((up <X> up1) `3))]| = a * |[((up <X> up1) `1),((up <X> up1) `2),((up <X> up1) `3)]| by EUCLID_5:8
.= |[0,0,0]| by A19, A17, EUCLID_5:3, EUCLID_5:4 ;
then ( a * ((up <X> up1) `1) = 0 & a * ((up <X> up1) `2) = 0 & a * ((up <X> up1) `3) = 0 ) by FINSEQ_1:78;
then ( (up <X> up1) `1 = 0 & (up <X> up1) `2 = 0 & (up <X> up1) `3 = 0 ) by A18, XCMPLX_1:6;
hence contradiction by A15, EUCLID_5:3, EUCLID_5:4; :: thesis: verum
end;
reconsider r = Dir up as Element of PTR3 by A2, ANPROJ_1:26;
take r ; :: thesis: ( p,p1,r are_collinear & q,q1,r are_collinear )
|{up,up1,up}| = 0 by EUCLID_5:31;
hence p,p1,r are_collinear by A2, A3, A4, A5, Th37, ANPROJ_2:23; :: thesis: q,q1,r are_collinear
now :: thesis: ( not uq <X> uq1 is zero & |((uq <X> uq1),uq)| = 0 & |((uq <X> uq1),uq1)| = 0 & |((uq <X> uq1),up)| = 0 )
thus not uq <X> uq1 is zero by A16; :: thesis: ( |((uq <X> uq1),uq)| = 0 & |((uq <X> uq1),uq1)| = 0 & |((uq <X> uq1),up)| = 0 )
thus |((uq <X> uq1),uq)| = |{uq,uq,uq1}| by EUCLID_5:def 5
.= 0 by EUCLID_5:31 ; :: thesis: ( |((uq <X> uq1),uq1)| = 0 & |((uq <X> uq1),up)| = 0 )
thus |((uq <X> uq1),uq1)| = |{uq1,uq,uq1}| by EUCLID_5:def 5
.= 0 by EUCLID_5:31 ; :: thesis: |((uq <X> uq1),up)| = 0
reconsider rp1 = up <X> up1, rp = up as Element of REAL 3 by EUCLID:22;
A20: a * |((up <X> up1),up)| = |((a * rp1),rp)| by EUCLID_8:68
.= |((a * (up <X> up1)),up)| ;
|((up <X> up1),up)| = |{up,up,up1}| by EUCLID_5:def 5
.= 0 by EUCLID_5:31 ;
hence |((uq <X> uq1),up)| = 0 by A20, A13; :: thesis: verum
end;
then |{uq,uq1,up}| = 0 by Th47;
hence q,q1,r are_collinear by A2, A6, A7, A8, A9, Th37, ANPROJ_2:23; :: thesis: verum
end;
end;
end;
end;
end;
suppose A21: not (up <X> up1) <X> (uq <X> uq1) is zero ; :: thesis: ex r being Element of PTR3 st
( p,p1,r are_collinear & q,q1,r are_collinear )
then reconsider r = Dir ((up <X> up1) <X> (uq <X> uq1)) as Element of PTR3 by ANPROJ_1:26;
take r ; :: thesis: ( p,p1,r are_collinear & q,q1,r are_collinear )
thus p,p1,r are_collinear by A2, A3, A4, A5, A21, Th41, ANPROJ_2:23; :: thesis: q,q1,r are_collinear
thus q,q1,r are_collinear by A6, A7, A8, A9, A21, Th41, ANPROJ_2:23; :: thesis: verum
end;
end;
end;
hence ex r being Element of PTR3 st
( p,p1,r are_collinear & q,q1,r are_collinear ) ; :: thesis: verum
end;
hence ProjectiveSpace (TOP-REAL 3) is CollProjectivePlane by ANPROJ_2:def 14; :: thesis: verum