Metamath Proof Explorer


Theorem dath

Description: Desargues's theorem of projective geometry (proved for a Hilbert lattice). Assume each triple of atoms (points) P Q R and S T U forms a triangle (i.e. determines a plane). Assume that lines P S , Q T , and R U meet at a "center of perspectivity" C . (We also assume that C is not on any of the 6 lines forming the two triangles.) Then the atoms D = ( P .\/ Q ) ./\ ( S .\/ T ) , E = ( Q .\/ R ) ./\ ( T .\/ U ) , F = ( R .\/ P ) ./\ ( U .\/ S ) are colinear, forming an "axis of perspectivity".

Our proof roughly follows Theorem 2.7.1, p. 78 in Beutelspacher and Rosenbaum,Projective Geometry: From Foundations to Applications, Cambridge University Press (1988). Unlike them, we do not assume that C is an atom to make this theorem slightly more general for easier future use. However, we prove that C must be an atom in dalemcea .

For a visual demonstration, see the "Desargues's theorem" applet at http://www.dynamicgeometry.com/JavaSketchpad/Gallery.html . The points I, J, and K there define the axis of perspectivity.

See Theorems dalaw for Desargues's law, which eliminates all of the preconditions on the atoms except for central perspectivity. This is Metamath 100 proof #87. (Contributed by NM, 20-Aug-2012)

Ref Expression
Hypotheses dath.b
|- B = ( Base ` K )
dath.l
|- .<_ = ( le ` K )
dath.j
|- .\/ = ( join ` K )
dath.a
|- A = ( Atoms ` K )
dath.m
|- ./\ = ( meet ` K )
dath.o
|- O = ( LPlanes ` K )
dath.d
|- D = ( ( P .\/ Q ) ./\ ( S .\/ T ) )
dath.e
|- E = ( ( Q .\/ R ) ./\ ( T .\/ U ) )
dath.f
|- F = ( ( R .\/ P ) ./\ ( U .\/ S ) )
Assertion dath
|- ( ( ( ( K e. HL /\ C e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) /\ ( ( ( P .\/ Q ) .\/ R ) e. O /\ ( ( S .\/ T ) .\/ U ) e. O ) /\ ( ( -. C .<_ ( P .\/ Q ) /\ -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) ) /\ ( -. C .<_ ( S .\/ T ) /\ -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) ) /\ ( C .<_ ( P .\/ S ) /\ C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) ) ) ) -> F .<_ ( D .\/ E ) )

Proof

Step Hyp Ref Expression
1 dath.b
 |-  B = ( Base ` K )
2 dath.l
 |-  .<_ = ( le ` K )
3 dath.j
 |-  .\/ = ( join ` K )
4 dath.a
 |-  A = ( Atoms ` K )
5 dath.m
 |-  ./\ = ( meet ` K )
6 dath.o
 |-  O = ( LPlanes ` K )
7 dath.d
 |-  D = ( ( P .\/ Q ) ./\ ( S .\/ T ) )
8 dath.e
 |-  E = ( ( Q .\/ R ) ./\ ( T .\/ U ) )
9 dath.f
 |-  F = ( ( R .\/ P ) ./\ ( U .\/ S ) )
10 1 eleq2i
 |-  ( C e. B <-> C e. ( Base ` K ) )
11 10 anbi2i
 |-  ( ( K e. HL /\ C e. B ) <-> ( K e. HL /\ C e. ( Base ` K ) ) )
12 11 3anbi1i
 |-  ( ( ( K e. HL /\ C e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) <-> ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) )
13 12 3anbi1i
 |-  ( ( ( ( K e. HL /\ C e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) /\ ( ( ( P .\/ Q ) .\/ R ) e. O /\ ( ( S .\/ T ) .\/ U ) e. O ) /\ ( ( -. C .<_ ( P .\/ Q ) /\ -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) ) /\ ( -. C .<_ ( S .\/ T ) /\ -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) ) /\ ( C .<_ ( P .\/ S ) /\ C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) ) ) ) <-> ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) /\ ( ( ( P .\/ Q ) .\/ R ) e. O /\ ( ( S .\/ T ) .\/ U ) e. O ) /\ ( ( -. C .<_ ( P .\/ Q ) /\ -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) ) /\ ( -. C .<_ ( S .\/ T ) /\ -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) ) /\ ( C .<_ ( P .\/ S ) /\ C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) ) ) ) )
14 eqid
 |-  ( ( P .\/ Q ) .\/ R ) = ( ( P .\/ Q ) .\/ R )
15 eqid
 |-  ( ( S .\/ T ) .\/ U ) = ( ( S .\/ T ) .\/ U )
16 13 2 3 4 5 6 14 15 7 8 9 dalem63
 |-  ( ( ( ( K e. HL /\ C e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) /\ ( ( ( P .\/ Q ) .\/ R ) e. O /\ ( ( S .\/ T ) .\/ U ) e. O ) /\ ( ( -. C .<_ ( P .\/ Q ) /\ -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) ) /\ ( -. C .<_ ( S .\/ T ) /\ -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) ) /\ ( C .<_ ( P .\/ S ) /\ C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) ) ) ) -> F .<_ ( D .\/ E ) )