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

Theorem dalemkehl 29812
Description: Lemma for dath 29925. 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 1066 . 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 187 1  |-  ( ph  ->  K  e.  HL )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    e. wcel 1684   class class class wbr 4023   ` cfv 5255  (class class class)co 5858   Basecbs 13148   HLchlt 29540
This theorem is referenced by:  dalemkelat  29813  dalemkeop  29814  dalempjqeb  29834  dalemsjteb  29835  dalemtjueb  29836  dalemqrprot  29837  dalempnes  29840  dalemqnet  29841  dalempjsen  29842  dalemply  29843  dalemsly  29844  dalemswapyz  29845  dalemrot  29846  dalemrotyz  29847  dalem1  29848  dalemcea  29849  dalem2  29850  dalemdea  29851  dalem3  29853  dalem4  29854  dalem5  29856  dalem-cly  29860  dalem9  29861  dalem11  29863  dalem12  29864  dalem13  29865  dalem15  29867  dalem16  29868  dalem17  29869  dalem18  29870  dalem19  29871  dalemswapyzps  29879  dalemcjden  29881  dalem21  29883  dalem22  29884  dalem23  29885  dalem24  29886  dalem25  29887  dalem27  29888  dalem28  29889  dalem38  29899  dalem39  29900  dalem41  29902  dalem42  29903  dalem43  29904  dalem44  29905  dalem45  29906  dalem51  29912  dalem52  29913  dalem54  29915  dalem55  29916  dalem56  29917  dalem57  29918  dalem58  29919  dalem59  29920  dalem60  29921
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator