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

Theorem dalemkehl 34294
Description: Lemma for dath 34407. 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 1102 . 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 195 1  |-  ( ph  ->  K  e.  HL )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 968    e. wcel 1762   class class class wbr 4440   ` cfv 5579  (class class class)co 6275   Basecbs 14479   HLchlt 34022
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 970
This theorem is referenced by:  dalemkelat  34295  dalemkeop  34296  dalempjqeb  34316  dalemsjteb  34317  dalemtjueb  34318  dalemqrprot  34319  dalempnes  34322  dalemqnet  34323  dalempjsen  34324  dalemply  34325  dalemsly  34326  dalemswapyz  34327  dalemrot  34328  dalemrotyz  34329  dalem1  34330  dalemcea  34331  dalem2  34332  dalemdea  34333  dalem3  34335  dalem4  34336  dalem5  34338  dalem-cly  34342  dalem9  34343  dalem11  34345  dalem12  34346  dalem13  34347  dalem15  34349  dalem16  34350  dalem17  34351  dalem18  34352  dalem19  34353  dalemswapyzps  34361  dalemcjden  34363  dalem21  34365  dalem22  34366  dalem23  34367  dalem24  34368  dalem25  34369  dalem27  34370  dalem28  34371  dalem38  34381  dalem39  34382  dalem41  34384  dalem42  34385  dalem43  34386  dalem44  34387  dalem45  34388  dalem51  34394  dalem52  34395  dalem54  34397  dalem55  34398  dalem56  34399  dalem57  34400  dalem58  34401  dalem59  34402  dalem60  34403
  Copyright terms: Public domain W3C validator