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 𝐵 = ( Base ‘ 𝐾 )
dath.l = ( le ‘ 𝐾 )
dath.j = ( join ‘ 𝐾 )
dath.a 𝐴 = ( Atoms ‘ 𝐾 )
dath.m = ( meet ‘ 𝐾 )
dath.o 𝑂 = ( LPlanes ‘ 𝐾 )
dath.d 𝐷 = ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) )
dath.e 𝐸 = ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) )
dath.f 𝐹 = ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) )
Assertion dath ( ( ( ( 𝐾 ∈ HL ∧ 𝐶𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ( 𝑃 𝑄 ) ∧ ¬ 𝐶 ( 𝑄 𝑅 ) ∧ ¬ 𝐶 ( 𝑅 𝑃 ) ) ∧ ( ¬ 𝐶 ( 𝑆 𝑇 ) ∧ ¬ 𝐶 ( 𝑇 𝑈 ) ∧ ¬ 𝐶 ( 𝑈 𝑆 ) ) ∧ ( 𝐶 ( 𝑃 𝑆 ) ∧ 𝐶 ( 𝑄 𝑇 ) ∧ 𝐶 ( 𝑅 𝑈 ) ) ) ) → 𝐹 ( 𝐷 𝐸 ) )

Proof

Step Hyp Ref Expression
1 dath.b 𝐵 = ( Base ‘ 𝐾 )
2 dath.l = ( le ‘ 𝐾 )
3 dath.j = ( join ‘ 𝐾 )
4 dath.a 𝐴 = ( Atoms ‘ 𝐾 )
5 dath.m = ( meet ‘ 𝐾 )
6 dath.o 𝑂 = ( LPlanes ‘ 𝐾 )
7 dath.d 𝐷 = ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) )
8 dath.e 𝐸 = ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) )
9 dath.f 𝐹 = ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) )
10 1 eleq2i ( 𝐶𝐵𝐶 ∈ ( Base ‘ 𝐾 ) )
11 10 anbi2i ( ( 𝐾 ∈ HL ∧ 𝐶𝐵 ) ↔ ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) )
12 11 3anbi1i ( ( ( 𝐾 ∈ HL ∧ 𝐶𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ↔ ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) )
13 12 3anbi1i ( ( ( ( 𝐾 ∈ HL ∧ 𝐶𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ( 𝑃 𝑄 ) ∧ ¬ 𝐶 ( 𝑄 𝑅 ) ∧ ¬ 𝐶 ( 𝑅 𝑃 ) ) ∧ ( ¬ 𝐶 ( 𝑆 𝑇 ) ∧ ¬ 𝐶 ( 𝑇 𝑈 ) ∧ ¬ 𝐶 ( 𝑈 𝑆 ) ) ∧ ( 𝐶 ( 𝑃 𝑆 ) ∧ 𝐶 ( 𝑄 𝑇 ) ∧ 𝐶 ( 𝑅 𝑈 ) ) ) ) ↔ ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ( 𝑃 𝑄 ) ∧ ¬ 𝐶 ( 𝑄 𝑅 ) ∧ ¬ 𝐶 ( 𝑅 𝑃 ) ) ∧ ( ¬ 𝐶 ( 𝑆 𝑇 ) ∧ ¬ 𝐶 ( 𝑇 𝑈 ) ∧ ¬ 𝐶 ( 𝑈 𝑆 ) ) ∧ ( 𝐶 ( 𝑃 𝑆 ) ∧ 𝐶 ( 𝑄 𝑇 ) ∧ 𝐶 ( 𝑅 𝑈 ) ) ) ) )
14 eqid ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑃 𝑄 ) 𝑅 )
15 eqid ( ( 𝑆 𝑇 ) 𝑈 ) = ( ( 𝑆 𝑇 ) 𝑈 )
16 13 2 3 4 5 6 14 15 7 8 9 dalem63 ( ( ( ( 𝐾 ∈ HL ∧ 𝐶𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ( 𝑃 𝑄 ) ∧ ¬ 𝐶 ( 𝑄 𝑅 ) ∧ ¬ 𝐶 ( 𝑅 𝑃 ) ) ∧ ( ¬ 𝐶 ( 𝑆 𝑇 ) ∧ ¬ 𝐶 ( 𝑇 𝑈 ) ∧ ¬ 𝐶 ( 𝑈 𝑆 ) ) ∧ ( 𝐶 ( 𝑃 𝑆 ) ∧ 𝐶 ( 𝑄 𝑇 ) ∧ 𝐶 ( 𝑅 𝑈 ) ) ) ) → 𝐹 ( 𝐷 𝐸 ) )