Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dalemkehl Structured version   Unicode version

Theorem dalemkehl 30358
Description: Lemma for dath 30471. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.)
Hypothesis
Ref Expression
dalema.ph  |-  ( 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 ) ) ) ) )
Assertion
Ref Expression
dalemkehl  |-  ( ph  ->  K  e.  HL )

Proof of Theorem dalemkehl
StepHypRef Expression
1 dalema.ph . 2  |-  ( 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 ) ) ) ) )
2 simp11l 1068 . 2  |-  ( ( ( ( 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 ) ) ) )  ->  K  e.  HL )
31, 2sylbi 188 1  |-  ( ph  ->  K  e.  HL )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936    e. wcel 1725   class class class wbr 4205   ` cfv 5447  (class class class)co 6074   Basecbs 13462   HLchlt 30086
This theorem is referenced by:  dalemkelat  30359  dalemkeop  30360  dalempjqeb  30380  dalemsjteb  30381  dalemtjueb  30382  dalemqrprot  30383  dalempnes  30386  dalemqnet  30387  dalempjsen  30388  dalemply  30389  dalemsly  30390  dalemswapyz  30391  dalemrot  30392  dalemrotyz  30393  dalem1  30394  dalemcea  30395  dalem2  30396  dalemdea  30397  dalem3  30399  dalem4  30400  dalem5  30402  dalem-cly  30406  dalem9  30407  dalem11  30409  dalem12  30410  dalem13  30411  dalem15  30413  dalem16  30414  dalem17  30415  dalem18  30416  dalem19  30417  dalemswapyzps  30425  dalemcjden  30427  dalem21  30429  dalem22  30430  dalem23  30431  dalem24  30432  dalem25  30433  dalem27  30434  dalem28  30435  dalem38  30445  dalem39  30446  dalem41  30448  dalem42  30449  dalem43  30450  dalem44  30451  dalem45  30452  dalem51  30458  dalem52  30459  dalem54  30461  dalem55  30462  dalem56  30463  dalem57  30464  dalem58  30465  dalem59  30466  dalem60  30467
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator