HomeHome Metamath Proof Explorer
Theorem List (p. 306 of 328)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-22421)
  Hilbert Space Explorer  Hilbert Space Explorer
(22422-23944)
  Users' Mathboxes  Users' Mathboxes
(23945-32762)
 

Theorem List for Metamath Proof Explorer - 30501-30600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremdalem32 30501 Lemma for dath 30533. Analog of dalem27 30496 for  H. (Contributed by NM, 8-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  c  .<_  ( H  .\/  Q )
 )
 
Theoremdalem33 30502 Lemma for dath 30533. Analog of dalem28 30497 for  H. (Contributed by NM, 4-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  Q  .<_  ( H  .\/  c )
 )
 
Theoremdalem34 30503 Lemma for dath 30533. Analog of dalem23 30493 for  I. (Contributed by NM, 2-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  I  e.  A )
 
Theoremdalem35 30504 Lemma for dath 30533. Analog of dalem24 30494 for  I. (Contributed by NM, 3-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  -.  I  .<_  Y )
 
Theoremdalem36 30505 Lemma for dath 30533. Analog of dalem27 30496 for  I. (Contributed by NM, 8-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  c  .<_  ( I  .\/  R )
 )
 
Theoremdalem37 30506 Lemma for dath 30533. Analog of dalem28 30497 for  I. (Contributed by NM, 4-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  R  .<_  ( I  .\/  c )
 )
 
Theoremdalem38 30507 Lemma for dath 30533. Plane  Y belongs to the 3-dimensional volume  G H I c. (Contributed by NM, 5-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  Y  .<_  ( ( ( G  .\/  H )  .\/  I )  .\/  c ) )
 
Theoremdalem39 30508 Lemma for dath 30533. Auxiliary atoms  G,  H, and  I are not colinear. (Contributed by NM, 4-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  -.  H  .<_  ( I  .\/  G )
 )
 
Theoremdalem40 30509 Lemma for dath 30533. Analog of dalem39 30508 for  I. (Contributed by NM, 4-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  -.  I  .<_  ( G  .\/  H )
 )
 
Theoremdalem41 30510 Lemma for dath 30533. (Contributed by NM, 4-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  G  =/=  H )
 
Theoremdalem42 30511 Lemma for dath 30533. Auxiliary atoms  G H I form a plane. (Contributed by NM, 4-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  ( ( G  .\/  H )  .\/  I )  e.  O )
 
Theoremdalem43 30512 Lemma for dath 30533. Planes  G H I and  Y are different. (Contributed by NM, 8-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  ( ( G  .\/  H )  .\/  I )  =/=  Y )
 
Theoremdalem44 30513 Lemma for dath 30533. Dummy center of perspectivity  c lies outside of plane  G H I. (Contributed by NM, 16-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  -.  c  .<_  ( ( G  .\/  H )  .\/  I )
 )
 
Theoremdalem45 30514 Lemma for dath 30533. Dummy center of perspectivity  c is not on the line  G H. (Contributed by NM, 16-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  -.  c  .<_  ( G  .\/  H ) )
 
Theoremdalem46 30515 Lemma for dath 30533. Analog of dalem45 30514 for  H I. (Contributed by NM, 16-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  -.  c  .<_  ( H  .\/  I
 ) )
 
Theoremdalem47 30516 Lemma for dath 30533. Analog of dalem45 30514 for  I G. (Contributed by NM, 16-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  -.  c  .<_  ( I  .\/  G ) )
 
Theoremdalem48 30517 Lemma for dath 30533. Analog of dalem45 30514 for  P Q. (Contributed by NM, 16-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\ 
 ps )  ->  -.  c  .<_  ( P  .\/  Q ) )
 
Theoremdalem49 30518 Lemma for dath 30533. Analog of dalem45 30514 for  Q R. (Contributed by NM, 16-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\ 
 ps )  ->  -.  c  .<_  ( Q  .\/  R ) )
 
Theoremdalem50 30519 Lemma for dath 30533. Analog of dalem45 30514 for  R P. (Contributed by NM, 16-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\ 
 ps )  ->  -.  c  .<_  ( R  .\/  P ) )
 
Theoremdalem51 30520 Lemma for dath 30533. Construct the condition  ph with  c,  G H I, and 
Y in place of  C,  Y, and  Z respectively. This lets us reuse the special case of Desargues' Theorem where  Y  =/=  Z, to eventually prove the case where  Y  =  Z. (Contributed by NM, 16-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  ( (
 ( ( K  e.  HL  /\  c  e.  A )  /\  ( G  e.  A  /\  H  e.  A  /\  I  e.  A )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A ) )  /\  ( ( ( G  .\/  H )  .\/  I )  e.  O  /\  Y  e.  O )  /\  ( ( -.  c  .<_  ( G 
 .\/  H )  /\  -.  c  .<_  ( H  .\/  I )  /\  -.  c  .<_  ( I  .\/  G ) )  /\  ( -.  c  .<_  ( P  .\/  Q )  /\  -.  c  .<_  ( Q  .\/  R )  /\  -.  c  .<_  ( R  .\/  P )
 )  /\  ( c  .<_  ( G  .\/  P )  /\  c  .<_  ( H 
 .\/  Q )  /\  c  .<_  ( I  .\/  R ) ) ) ) 
 /\  ( ( G 
 .\/  H )  .\/  I
 )  =/=  Y )
 )
 
Theoremdalem52 30521 Lemma for dath 30533. Lines  G H and  P Q intersect at an atom. (Contributed by NM, 8-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  ( ( G  .\/  H )  ./\  ( P  .\/  Q ) )  e.  A )
 
Theoremdalem53 30522 Lemma for dath 30533. The auxliary axis of perspectivity  B is a line (analogous to the actual axis of perspectivity  X in dalem15 30475. (Contributed by NM, 8-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  N  =  ( LLines `  K )   &    |-  O  =  (
 LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   &    |-  B  =  ( ( ( G 
 .\/  H )  .\/  I
 )  ./\  Y )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  B  e.  N )
 
Theoremdalem54 30523 Lemma for dath 30533. Line  G H intersects the auxiliary axis of perspectivity  B. (Contributed by NM, 8-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   &    |-  B  =  ( ( ( G 
 .\/  H )  .\/  I
 )  ./\  Y )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  ( ( G  .\/  H )  ./\  B )  e.  A )
 
Theoremdalem55 30524 Lemma for dath 30533. Lines  G H and  P Q intersect at the auxiliary line  B (later shown to be an axis of perspectivity; see dalem60 30529). (Contributed by NM, 8-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   &    |-  B  =  ( ( ( G 
 .\/  H )  .\/  I
 )  ./\  Y )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  ( ( G  .\/  H )  ./\  ( P  .\/  Q ) )  =  ( ( G  .\/  H )  ./\ 
 B ) )
 
Theoremdalem56 30525 Lemma for dath 30533. Analog of dalem55 30524 for line  S T. (Contributed by NM, 8-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   &    |-  B  =  ( ( ( G 
 .\/  H )  .\/  I
 )  ./\  Y )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  ( ( G  .\/  H )  ./\  ( S  .\/  T ) )  =  ( ( G  .\/  H )  ./\ 
 B ) )
 
Theoremdalem57 30526 Lemma for dath 30533. Axis of perspectivity point  D is on the auxiliary line  B. (Contributed by NM, 9-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   &    |-  B  =  ( ( ( G 
 .\/  H )  .\/  I
 )  ./\  Y )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  D  .<_  B )
 
Theoremdalem58 30527 Lemma for dath 30533. Analog of dalem57 30526 for  E. (Contributed by NM, 10-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   &    |-  B  =  ( ( ( G 
 .\/  H )  .\/  I
 )  ./\  Y )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  E  .<_  B )
 
Theoremdalem59 30528 Lemma for dath 30533. Analog of dalem57 30526 for  F. (Contributed by NM, 10-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  F  =  ( ( R  .\/  P )  ./\  ( U  .\/  S ) )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   &    |-  B  =  ( ( ( G 
 .\/  H )  .\/  I
 )  ./\  Y )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  F  .<_  B )
 
Theoremdalem60 30529 Lemma for dath 30533. 
B is an axis of perspectivity (almost). (Contributed by NM, 11-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   &    |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )   &    |-  H  =  ( ( c  .\/  Q )  ./\  ( d  .\/  T ) )   &    |-  I  =  ( ( c  .\/  R )  ./\  ( d  .\/  U ) )   &    |-  B  =  ( ( ( G 
 .\/  H )  .\/  I
 )  ./\  Y )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  ( D  .\/  E )  =  B )
 
Theoremdalem61 30530 Lemma for dath 30533. Show that atoms  D,  E, and  F lie on the same line (axis of perspectivity). Eliminate hypotheses containing dummy atoms  c and  d. (Contributed by NM, 11-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ( ps 
 <->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  Y  /\  (
 d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
 ) ) ) )   &    |-  ./\ 
 =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   &    |-  F  =  ( ( R  .\/  P )  ./\  ( U  .\/  S ) )   =>    |-  ( ( ph  /\  Y  =  Z  /\  ps )  ->  F  .<_  ( D  .\/  E )
 )
 
Theoremdalem62 30531 Lemma for dath 30533. Eliminate the condition  ps containing dummy variables  c and  d. (Contributed by NM, 11-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   &    |-  F  =  ( ( R  .\/  P )  ./\  ( U  .\/  S ) )   =>    |-  ( ( ph  /\  Y  =  Z ) 
 ->  F  .<_  ( D  .\/  E ) )
 
Theoremdalem63 30532 Lemma for dath 30533. Combine the cases where  Y and  Z are different planes with the case where  Y and 
Z are the same plane. (Contributed by NM, 11-Aug-2012.)
 |-  ( ph 
 <->  ( ( ( 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 ) )  /\  ( Y  e.  O  /\  Z  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 ) ) ) ) )   &    |-  .<_  =  ( le `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  Y  =  ( ( P  .\/  Q )  .\/  R )   &    |-  Z  =  ( ( S  .\/  T )  .\/  U )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   &    |-  F  =  ( ( R  .\/  P )  ./\  ( U  .\/  S ) )   =>    |-  ( ph  ->  F 
 .<_  ( D  .\/  E ) )
 
Theoremdath 30533 Desargues' 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 don't assume  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 30457.

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

See theorem dalaw 30683 for Desargues Law, which eliminates all of the preconditions on the atoms except for central perspectivity. (Contributed by NM, 20-Aug-2012.)

 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   &    |-  F  =  ( ( R  .\/  P )  ./\  ( U  .\/  S ) )   =>    |-  ( ( ( ( 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 ) )
 
Theoremdath2 30534 Version of Desargues' Theorem dath 30533 with a different variable ordering. (Contributed by NM, 7-Oct-2012.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  O  =  ( LPlanes `  K )   &    |-  D  =  ( ( P  .\/  Q )  ./\  ( S  .\/  T ) )   &    |-  E  =  ( ( Q  .\/  R )  ./\  ( T  .\/  U ) )   &    |-  F  =  ( ( R  .\/  P )  ./\  ( U  .\/  S ) )   =>    |-  ( ( ( ( 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 ) ) ) ) 
 ->  D  .<_  ( E  .\/  F ) )
 
Theoremlineset 30535* The set of lines in a Hilbert lattice. (Contributed by NM, 19-Sep-2011.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  N  =  ( Lines `  K )   =>    |-  ( K  e.  B  ->  N  =  { s  | 
 E. q  e.  A  E. r  e.  A  ( q  =/=  r  /\  s  =  { p  e.  A  |  p  .<_  ( q  .\/  r ) } ) } )
 
Theoremisline 30536* The predicate "is a line". (Contributed by NM, 19-Sep-2011.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  N  =  ( Lines `  K )   =>    |-  ( K  e.  D  ->  ( X  e.  N  <->  E. q  e.  A  E. r  e.  A  ( q  =/=  r  /\  X  =  { p  e.  A  |  p  .<_  ( q  .\/  r ) } ) ) )
 
Theoremislinei 30537* Condition implying "is a line". (Contributed by NM, 3-Feb-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  N  =  ( Lines `  K )   =>    |-  (
 ( ( K  e.  D  /\  Q  e.  A  /\  R  e.  A ) 
 /\  ( Q  =/=  R 
 /\  X  =  { p  e.  A  |  p  .<_  ( Q  .\/  R ) } ) ) 
 ->  X  e.  N )
 
TheorempointsetN 30538* The set of points in a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) (New usage is discouraged.)
 |-  A  =  ( Atoms `  K )   &    |-  P  =  ( Points `  K )   =>    |-  ( K  e.  B  ->  P  =  { p  |  E. a  e.  A  p  =  { a } } )
 
TheoremispointN 30539* The predicate "is a point". (Contributed by NM, 2-Oct-2011.) (New usage is discouraged.)
 |-  A  =  ( Atoms `  K )   &    |-  P  =  ( Points `  K )   =>    |-  ( K  e.  D  ->  ( X  e.  P  <->  E. a  e.  A  X  =  { a } ) )
 
TheorematpointN 30540 The singleton of an atom is a point. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.)
 |-  A  =  ( Atoms `  K )   &    |-  P  =  ( Points `  K )   =>    |-  (
 ( K  e.  D  /\  X  e.  A ) 
 ->  { X }  e.  P )
 
Theorempsubspset 30541* The set of projective subspaces in a Hilbert lattice. (Contributed by NM, 2-Oct-2011.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  S  =  ( PSubSp `  K )   =>    |-  ( K  e.  B  ->  S  =  { s  |  ( s  C_  A  /\  A. p  e.  s  A. q  e.  s  A. r  e.  A  ( r  .<_  ( p 
 .\/  q )  ->  r  e.  s )
 ) } )
 
Theoremispsubsp 30542* The predicate "is a projective subspace". (Contributed by NM, 2-Oct-2011.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  S  =  ( PSubSp `  K )   =>    |-  ( K  e.  D  ->  ( X  e.  S  <->  ( X  C_  A  /\  A. p  e.  X  A. q  e.  X  A. r  e.  A  ( r  .<_  ( p  .\/  q )  ->  r  e.  X ) ) ) )
 
Theoremispsubsp2 30543* The predicate "is a projective subspace". (Contributed by NM, 13-Jan-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  S  =  ( PSubSp `  K )   =>    |-  ( K  e.  D  ->  ( X  e.  S  <->  ( X  C_  A  /\  A. p  e.  A  ( E. q  e.  X  E. r  e.  X  p  .<_  ( q 
 .\/  r )  ->  p  e.  X )
 ) ) )
 
Theorempsubspi 30544* Property of a projective subspace. (Contributed by NM, 13-Jan-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  S  =  ( PSubSp `  K )   =>    |-  (
 ( ( K  e.  D  /\  X  e.  S  /\  P  e.  A ) 
 /\  E. q  e.  X  E. r  e.  X  P  .<_  ( q  .\/  r ) )  ->  P  e.  X )
 
Theorempsubspi2N 30545 Property of a projective subspace. (Contributed by NM, 13-Jan-2012.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  S  =  ( PSubSp `  K )   =>    |-  (
 ( ( K  e.  D  /\  X  e.  S  /\  P  e.  A ) 
 /\  ( Q  e.  X  /\  R  e.  X  /\  P  .<_  ( Q  .\/  R ) ) )  ->  P  e.  X )
 
Theorem0psubN 30546 The empty set is a projective subspace. Remark below Definition 15.1 of [MaedaMaeda] p. 61. (Contributed by NM, 13-Oct-2011.) (New usage is discouraged.)
 |-  S  =  ( PSubSp `  K )   =>    |-  ( K  e.  V  ->  (/)  e.  S )
 
TheoremsnatpsubN 30547 The singleton of an atom is a projective subspace. (Contributed by NM, 9-Sep-2013.) (New usage is discouraged.)
 |-  A  =  ( Atoms `  K )   &    |-  S  =  ( PSubSp `  K )   =>    |-  (
 ( K  e.  AtLat  /\  P  e.  A ) 
 ->  { P }  e.  S )
 
TheorempointpsubN 30548 A point (singleton of an atom) is a projective subspace. Remark below Definition 15.1 of [MaedaMaeda] p. 61. (Contributed by NM, 13-Oct-2011.) (New usage is discouraged.)
 |-  P  =  ( Points `  K )   &    |-  S  =  ( PSubSp `  K )   =>    |-  (
 ( K  e.  AtLat  /\  X  e.  P ) 
 ->  X  e.  S )
 
TheoremlinepsubN 30549 A line is a projective subspace. (Contributed by NM, 16-Oct-2011.) (New usage is discouraged.)
 |-  N  =  ( Lines `  K )   &    |-  S  =  ( PSubSp `  K )   =>    |-  (
 ( K  e.  Lat  /\  X  e.  N ) 
 ->  X  e.  S )
 
TheorematpsubN 30550 The set of all atoms is a projective subspace. Remark below Definition 15.1 of [MaedaMaeda] p. 61. (Contributed by NM, 13-Oct-2011.) (New usage is discouraged.)
 |-  A  =  ( Atoms `  K )   &    |-  S  =  ( PSubSp `  K )   =>    |-  ( K  e.  V  ->  A  e.  S )
 
Theorempsubssat 30551 A projective subspace consists of atoms. (Contributed by NM, 4-Nov-2011.)
 |-  A  =  ( Atoms `  K )   &    |-  S  =  ( PSubSp `  K )   =>    |-  (
 ( K  e.  B  /\  X  e.  S ) 
 ->  X  C_  A )
 
TheorempsubatN 30552 A member of a projective subspace is an atom. (Contributed by NM, 4-Nov-2011.) (New usage is discouraged.)
 |-  A  =  ( Atoms `  K )   &    |-  S  =  ( PSubSp `  K )   =>    |-  (
 ( K  e.  B  /\  X  e.  S  /\  Y  e.  X )  ->  Y  e.  A )
 
Theorempmapfval 30553* The projective map of a Hilbert lattice. (Contributed by NM, 2-Oct-2011.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  M  =  (
 pmap `  K )   =>    |-  ( K  e.  C  ->  M  =  ( x  e.  B  |->  { a  e.  A  |  a  .<_  x } )
 )
 
Theorempmapval 30554* Value of the projective map of a Hilbert lattice. Definition in Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 2-Oct-2011.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  M  =  (
 pmap `  K )   =>    |-  ( ( K  e.  C  /\  X  e.  B )  ->  ( M `  X )  =  { a  e.  A  |  a  .<_  X }
 )
 
Theoremelpmap 30555 Member of a projective map. (Contributed by NM, 27-Jan-2012.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  M  =  (
 pmap `  K )   =>    |-  ( ( K  e.  C  /\  X  e.  B )  ->  ( P  e.  ( M `  X )  <->  ( P  e.  A  /\  P  .<_  X ) ) )
 
Theorempmapssat 30556 The projective map of a Hilbert lattice is a set of atoms. (Contributed by NM, 14-Jan-2012.)
 |-  B  =  ( Base `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  (
 ( K  e.  C  /\  X  e.  B ) 
 ->  ( M `  X )  C_  A )
 
TheorempmapssbaN 30557 A weakening of pmapssat 30556 to shorten some proofs. (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  (
 ( K  e.  C  /\  X  e.  B ) 
 ->  ( M `  X )  C_  B )
 
Theorempmaple 30558 The projective map of a Hilbert lattice preserves ordering. Part of Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 22-Oct-2011.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  ( ( K  e.  HL  /\  X  e.  B  /\  Y  e.  B ) 
 ->  ( X  .<_  Y  <->  ( M `  X )  C_  ( M `
  Y ) ) )
 
Theorempmap11 30559 The projective map of a Hilbert lattice is one-to-one. Part of Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 22-Oct-2011.)
 |-  B  =  ( Base `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  (
 ( K  e.  HL  /\  X  e.  B  /\  Y  e.  B )  ->  ( ( M `  X )  =  ( M `  Y )  <->  X  =  Y ) )
 
Theorempmapat 30560 The projective map of an atom. (Contributed by NM, 25-Jan-2012.)
 |-  A  =  ( Atoms `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  (
 ( K  e.  HL  /\  P  e.  A ) 
 ->  ( M `  P )  =  { P } )
 
Theoremelpmapat 30561 Member of the projective map of an atom. (Contributed by NM, 27-Jan-2012.)
 |-  A  =  ( Atoms `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  (
 ( K  e.  HL  /\  P  e.  A ) 
 ->  ( X  e.  ( M `  P )  <->  X  =  P ) )
 
Theorempmap0 30562 Value of the projective map of a Hilbert lattice at lattice zero. Part of Theorem 15.5.1 of [MaedaMaeda] p. 62. (Contributed by NM, 17-Oct-2011.)
 |-  .0.  =  ( 0. `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  ( K  e.  AtLat  ->  ( M `  .0.  )  =  (/) )
 
Theorempmapeq0 30563 A projective map value is zero iff its argument is lattice zero. (Contributed by NM, 27-Jan-2012.)
 |-  B  =  ( Base `  K )   &    |-  .0.  =  ( 0. `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  ( ( K  e.  HL  /\  X  e.  B )  ->  ( ( M `
  X )  =  (/) 
 <->  X  =  .0.  )
 )
 
Theorempmap1N 30564 Value of the projective map of a Hilbert lattice at lattice unit. Part of Theorem 15.5.1 of [MaedaMaeda] p. 62. (Contributed by NM, 22-Oct-2011.) (New usage is discouraged.)
 |-  .1.  =  ( 1. `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  M  =  (
 pmap `  K )   =>    |-  ( K  e.  OP  ->  ( M `  .1.  )  =  A )
 
Theorempmapsub 30565 The projective map of a Hilbert lattice maps to projective subspaces. Part of Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 17-Oct-2011.)
 |-  B  =  ( Base `  K )   &    |-  S  =  ( PSubSp `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  (
 ( K  e.  Lat  /\  X  e.  B ) 
 ->  ( M `  X )  e.  S )
 
Theorempmapglbx 30566* The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb 30567, where we read  S as  S ( i ). Theorem 15.5.2 of [MaedaMaeda] p. 62. (Contributed by NM, 5-Dec-2011.)
 |-  B  =  ( Base `  K )   &    |-  G  =  ( glb `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  ( ( K  e.  HL  /\  A. i  e.  I  S  e.  B  /\  I  =/=  (/) )  ->  ( M `  ( G `
  { y  | 
 E. i  e.  I  y  =  S }
 ) )  =  |^|_ i  e.  I  ( M `
  S ) )
 
Theorempmapglb 30567* The projective map of the GLB of a set of lattice elements  S. Variant of Theorem 15.5.2 of [MaedaMaeda] p. 62. (Contributed by NM, 5-Dec-2011.)
 |-  B  =  ( Base `  K )   &    |-  G  =  ( glb `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  ( ( K  e.  HL  /\  S  C_  B  /\  S  =/=  (/) )  ->  ( M `  ( G `
  S ) )  =  |^|_ x  e.  S  ( M `  x ) )
 
Theorempmapglb2N 30568* The projective map of the GLB of a set of lattice elements  S. Variant of Theorem 15.5.2 of [MaedaMaeda] p. 62. Allows  S  =  (/). (Contributed by NM, 21-Jan-2012.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  G  =  ( glb `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  M  =  (
 pmap `  K )   =>    |-  ( ( K  e.  HL  /\  S  C_  B )  ->  ( M `  ( G `  S ) )  =  ( A  i^i  |^|_ x  e.  S  ( M `  x ) ) )
 
Theorempmapglb2xN 30569* The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb2N 30568, where we read  S as  S ( i ). Extension of Theorem 15.5.2 of [MaedaMaeda] p. 62 that allows  I  =  (/). (Contributed by NM, 21-Jan-2012.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  G  =  ( glb `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  M  =  (
 pmap `  K )   =>    |-  ( ( K  e.  HL  /\  A. i  e.  I  S  e.  B )  ->  ( M `  ( G `  { y  |  E. i  e.  I  y  =  S } ) )  =  ( A  i^i  |^|_ i  e.  I  ( M `  S ) ) )
 
Theorempmapmeet 30570 The projective map of a meet. (Contributed by NM, 25-Jan-2012.)
 |-  B  =  ( Base `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  P  =  ( pmap `  K )   =>    |-  (
 ( K  e.  HL  /\  X  e.  B  /\  Y  e.  B )  ->  ( P `  ( X  ./\  Y ) )  =  ( ( P `
  X )  i^i  ( P `  Y ) ) )
 
Theoremisline2 30571* Definition of line in terms of projective map. (Contributed by NM, 25-Jan-2012.)
 |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  N  =  ( Lines `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  ( K  e.  Lat  ->  ( X  e.  N  <->  E. p  e.  A  E. q  e.  A  ( p  =/=  q  /\  X  =  ( M `
  ( p  .\/  q ) ) ) ) )
 
Theoremlinepmap 30572 A line described with a projective map. (Contributed by NM, 3-Feb-2012.)
 |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  N  =  ( Lines `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  (
 ( ( K  e.  Lat  /\  P  e.  A  /\  Q  e.  A )  /\  P  =/=  Q ) 
 ->  ( M `  ( P  .\/  Q ) )  e.  N )
 
Theoremisline3 30573* Definition of line in terms of original lattice elements. (Contributed by NM, 29-Apr-2012.)
 |-  B  =  ( Base `  K )   &    |-  .\/  =  ( join `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  N  =  ( Lines `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  (
 ( K  e.  HL  /\  X  e.  B ) 
 ->  ( ( M `  X )  e.  N  <->  E. p  e.  A  E. q  e.  A  ( p  =/=  q  /\  X  =  ( p  .\/  q
 ) ) ) )
 
Theoremisline4N 30574* Definition of line in terms of original lattice elements. (Contributed by NM, 16-Jun-2012.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  C  =  (  <o  `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  N  =  (
 Lines `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  (
 ( K  e.  HL  /\  X  e.  B ) 
 ->  ( ( M `  X )  e.  N  <->  E. p  e.  A  p C X ) )
 
Theoremlneq2at 30575 A line equals the join of any two of its distinct points (atoms). (Contributed by NM, 29-Apr-2012.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  N  =  ( Lines `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  (
 ( ( K  e.  HL  /\  X  e.  B  /\  ( M `  X )  e.  N )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( P  .<_  X  /\  Q  .<_  X ) ) 
 ->  X  =  ( P 
 .\/  Q ) )
 
TheoremlnatexN 30576* There is an atom in a line different from any other. (Contributed by NM, 30-Apr-2012.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  N  =  (
 Lines `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  (
 ( K  e.  HL  /\  X  e.  B  /\  ( M `  X )  e.  N )  ->  E. q  e.  A  ( q  =/=  P  /\  q  .<_  X ) )
 
TheoremlnjatN 30577* Given an atom in a line, there is another atom which when joined equals the line. (Contributed by NM, 30-Apr-2012.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  N  =  ( Lines `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  (
 ( ( K  e.  HL  /\  X  e.  B  /\  P  e.  A ) 
 /\  ( ( M `
  X )  e.  N  /\  P  .<_  X ) )  ->  E. q  e.  A  ( q  =/= 
 P  /\  X  =  ( P  .\/  q ) ) )
 
TheoremlncvrelatN 30578 A lattice element covered by a line is an atom. (Contributed by NM, 28-Apr-2012.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  C  =  (  <o  `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  N  =  (
 Lines `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  (
 ( ( K  e.  HL  /\  X  e.  B  /\  P  e.  B ) 
 /\  ( ( M `
  X )  e.  N  /\  P C X ) )  ->  P  e.  A )
 
Theoremlncvrat 30579 A line covers the atoms it contains. (Contributed by NM, 30-Apr-2012.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |-  C  =  (  <o  `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  N  =  ( Lines `  K )   &    |-  M  =  ( pmap `  K )   =>    |-  (
 ( ( K  e.  HL  /\  X  e.  B  /\  P  e.  A ) 
 /\  ( ( M `
  X )  e.  N  /\  P  .<_  X ) )  ->  P C X )
 
Theoremlncmp 30580 If two lines are comparable, they are equal. (Contributed by NM, 30-Apr-2012.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |-  N  =  ( Lines `  K )   &    |-  M  =  (
 pmap `  K )   =>    |-  ( ( ( K  e.  HL  /\  X  e.  B  /\  Y  e.  B )  /\  ( ( M `  X )  e.  N  /\  ( M `  Y )  e.  N )
 )  ->  ( X  .<_  Y  <->  X  =  Y ) )
 
Theorem2lnat 30581 Two intersecting lines intersect at an atom. (Contributed by NM, 30-Apr-2012.)
 |-  B  =  ( Base `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  .0.  =  ( 0. `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  N  =  (
 Lines `  K )   &    |-  F  =  ( pmap `  K )   =>    |-  (
 ( ( K  e.  HL  /\  X  e.  B  /\  Y  e.  B ) 
 /\  ( ( F `
  X )  e.  N  /\  ( F `
  Y )  e.  N )  /\  ( X  =/=  Y  /\  ( X  ./\  Y )  =/= 
 .0.  ) )  ->  ( X  ./\  Y )  e.  A )
 
Theorem2atm2atN 30582 Two joins with a common atom have a nonzero meet. (Contributed by NM, 4-Jul-2012.) (New usage is discouraged.)
 |-  .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  .0.  =  ( 0. `  K )   &    |-  A  =  ( Atoms `  K )   =>    |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A ) )  ->  ( ( R  .\/  P )  ./\  ( R  .\/  Q ) )  =/=  .0.  )
 
Theorem2llnma1b 30583 Generalization of 2llnma1 30584. (Contributed by NM, 26-Apr-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   =>    |-  (
 ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A )  /\  -.  Q  .<_  ( P 
 .\/  X ) )  ->  ( ( P  .\/  X )  ./\  ( P  .\/  Q ) )  =  P )
 
Theorem2llnma1 30584 Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 11-Oct-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   =>    |-  (
 ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  -.  R  .<_  ( P 
 .\/  Q ) )  ->  ( ( Q  .\/  P )  ./\  ( Q  .\/  R ) )  =  Q )
 
Theorem2llnma3r 30585 Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 30-Apr-2013.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   =>    |-  (
 ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( P  .\/  R )  =/=  ( Q  .\/  R ) )  ->  (
 ( P  .\/  R )  ./\  ( Q  .\/  R ) )  =  R )
 
Theorem2llnma2 30586 Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 28-May-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   =>    |-  (
 ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( P  =/=  Q  /\  -.  R  .<_  ( P 
 .\/  Q ) ) ) 
 ->  ( ( R  .\/  P )  ./\  ( R  .\/  Q ) )  =  R )
 
Theorem2llnma2rN 30587 Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 2-May-2013.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   =>    |-  (
 ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( P  =/=  Q  /\  -.  R  .<_  ( P 
 .\/  Q ) ) ) 
 ->  ( ( P  .\/  R )  ./\  ( Q  .\/  R ) )  =  R )
 
19.26.10  Construction of a vector space from a Hilbert lattice
 
Theoremcdlema1N 30588 A condition for required for proof of Lemma A in [Crawley] p. 112. (Contributed by NM, 29-Apr-2012.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  N  =  ( Lines `  K )   &    |-  F  =  ( pmap `  K )   =>    |-  (
 ( ( K  e.  HL  /\  X  e.  B  /\  Y  e.  B ) 
 /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A ) 
 /\  ( ( R  =/=  P  /\  R  .<_  ( P  .\/  Q ) )  /\  ( P 
 .<_  X  /\  Q  .<_  Y )  /\  ( ( F `  Y )  e.  N  /\  ( X  ./\  Y )  e.  A  /\  -.  Q  .<_  X ) ) ) 
 ->  ( X  .\/  R )  =  ( X  .\/  Y ) )
 
Theoremcdlema2N 30589 A condition for required for proof of Lemma A in [Crawley] p. 112. (Contributed by NM, 9-May-2012.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  .0.  =  ( 0. `  K )   &    |-  A  =  ( Atoms `  K )   =>    |-  ( ( ( K  e.  HL  /\  X  e.  B )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( ( R  =/=  P 
 /\  R  .<_  ( P 
 .\/  Q ) )  /\  ( P  .<_  X  /\  -.  Q  .<_  X ) ) )  ->  ( R  ./\ 
 X )  =  .0.  )
 
Theoremcdlemblem 30590 Lemma for cdlemb 30591. (Contributed by NM, 8-May-2012.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  .1.  =  ( 1. `  K )   &    |-  C  =  (  <o  `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  .<  =  ( lt `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  V  =  ( ( P  .\/  Q )  ./\ 
 X )   =>    |-  ( ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( X  e.  B  /\  P  =/=  Q ) 
 /\  ( X C  .1.  /\  -.  P  .<_  X 
 /\  -.  Q  .<_  X ) )  /\  ( u  e.  A  /\  ( u  =/=  V  /\  u  .<  X ) ) 
 /\  ( r  e.  A  /\  ( r  =/=  P  /\  r  =/=  u  /\  r  .<_  ( P  .\/  u )
 ) ) )  ->  ( -.  r  .<_  X  /\  -.  r  .<_  ( P  .\/  Q ) ) )
 
Theoremcdlemb 30591* Given two atoms not less than or equal to an element covered by 1, there is a third. Lemma B in [Crawley] p. 112. (Contributed by NM, 8-May-2012.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  .1.  =  ( 1. `  K )   &    |-  C  =  (  <o  `  K )   &    |-  A  =  (
 Atoms `  K )   =>    |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( X  e.  B  /\  P  =/=  Q ) 
 /\  ( X C  .1.  /\  -.  P  .<_  X 
 /\  -.  Q  .<_  X ) )  ->  E. r  e.  A  ( -.  r  .<_  X  /\  -.  r  .<_  ( P  .\/  Q ) ) )
 
Syntaxcpadd 30592 Extend class notation with projective subspace sum.
 class  + P
 
Definitiondf-padd 30593* Define projective sum of two subspaces (or more generally two sets of atoms), which is the union of all lines generated by pairs of atoms from each subspace. Lemma 16.2 of [MaedaMaeda] p. 68. For convenience, our definition is generalized to apply to empty sets. (Contributed by NM, 29-Dec-2011.)
 |-  + P  =  ( l  e.  _V  |->  ( m  e. 
 ~P ( Atoms `  l
 ) ,  n  e. 
 ~P ( Atoms `  l
 )  |->  ( ( m  u.  n )  u. 
 { p  e.  ( Atoms `  l )  | 
 E. q  e.  m  E. r  e.  n  p ( le `  l
 ) ( q (
 join `  l ) r ) } ) ) )
 
Theorempaddfval 30594* Projective subspace sum operation. (Contributed by NM, 29-Dec-2011.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  .+  =  ( + P `  K )   =>    |-  ( K  e.  B  ->  .+  =  ( m  e.  ~P A ,  n  e.  ~P A  |->  ( ( m  u.  n )  u.  { p  e.  A  |  E. q  e.  m  E. r  e.  n  p  .<_  ( q  .\/  r ) } ) ) )
 
Theorempaddval 30595* Projective subspace sum operation value. (Contributed by NM, 29-Dec-2011.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  .+  =  ( + P `  K )   =>    |-  ( ( K  e.  B  /\  X  C_  A  /\  Y  C_  A )  ->  ( X  .+  Y )  =  ( ( X  u.  Y )  u. 
 { p  e.  A  |  E. q  e.  X  E. r  e.  Y  p  .<_  ( q  .\/  r ) } )
 )
 
Theoremelpadd 30596* Member of a projective subspace sum. (Contributed by NM, 29-Dec-2011.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  .+  =  ( + P `  K )   =>    |-  ( ( K  e.  B  /\  X  C_  A  /\  Y  C_  A )  ->  ( S  e.  ( X  .+  Y )  <->  ( ( S  e.  X  \/  S  e.  Y )  \/  ( S  e.  A  /\  E. q  e.  X  E. r  e.  Y  S  .<_  ( q  .\/  r
 ) ) ) ) )
 
Theoremelpaddn0 30597* Member of projective subspace sum of non-empty sets. (Contributed by NM, 3-Jan-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  .+  =  ( + P `  K )   =>    |-  ( ( ( K  e.  Lat  /\  X  C_  A  /\  Y  C_  A )  /\  ( X  =/=  (/)  /\  Y  =/=  (/) ) ) 
 ->  ( S  e.  ( X  .+  Y )  <->  ( S  e.  A  /\  E. q  e.  X  E. r  e.  Y  S  .<_  ( q 
 .\/  r ) ) ) )
 
Theorempaddvaln0N 30598* Projective subspace sum operation value for non-empty sets. (Contributed by NM, 27-Jan-2012.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  .+  =  ( + P `  K )   =>    |-  ( ( ( K  e.  Lat  /\  X  C_  A  /\  Y  C_  A )  /\  ( X  =/=  (/)  /\  Y  =/=  (/) ) ) 
 ->  ( X  .+  Y )  =  { p  e.  A  |  E. q  e.  X  E. r  e.  Y  p  .<_  ( q 
 .\/  r ) }
 )
 
Theoremelpaddri 30599 Condition implying membership in a projective subspace sum. (Contributed by NM, 8-Jan-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  .+  =  ( + P `  K )   =>    |-  ( ( ( K  e.  Lat  /\  X  C_  A  /\  Y  C_  A )  /\  ( Q  e.  X  /\  R  e.  Y )  /\  ( S  e.  A  /\  S  .<_  ( Q 
 .\/  R ) ) ) 
 ->  S  e.  ( X 
 .+  Y ) )
 
TheoremelpaddatriN 30600 Condition implying membership in a projective subspace sum with a point. (Contributed by NM, 1-Feb-2012.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  A  =  (
 Atoms `  K )   &    |-  .+  =  ( + P `  K )   =>    |-  ( ( ( K  e.  Lat  /\  X  C_  A  /\  Q  e.  A )  /\  ( R  e.  X  /\  S  e.  A  /\  S  .<_  ( R  .\/  Q ) ) )  ->  S  e.  ( X  .+ 
 { Q } )
 )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20&n