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

Theorem dalemkehl 30494
Description: Lemma for dath 30607. 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 1069 . 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 189 1  |-  ( ph  ->  K  e.  HL )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360    /\ w3a 937    e. wcel 1726   class class class wbr 4215   ` cfv 5457  (class class class)co 6084   Basecbs 13474   HLchlt 30222
This theorem is referenced by:  dalemkelat  30495  dalemkeop  30496  dalempjqeb  30516  dalemsjteb  30517  dalemtjueb  30518  dalemqrprot  30519  dalempnes  30522  dalemqnet  30523  dalempjsen  30524  dalemply  30525  dalemsly  30526  dalemswapyz  30527  dalemrot  30528  dalemrotyz  30529  dalem1  30530  dalemcea  30531  dalem2  30532  dalemdea  30533  dalem3  30535  dalem4  30536  dalem5  30538  dalem-cly  30542  dalem9  30543  dalem11  30545  dalem12  30546  dalem13  30547  dalem15  30549  dalem16  30550  dalem17  30551  dalem18  30552  dalem19  30553  dalemswapyzps  30561  dalemcjden  30563  dalem21  30565  dalem22  30566  dalem23  30567  dalem24  30568  dalem25  30569  dalem27  30570  dalem28  30571  dalem38  30581  dalem39  30582  dalem41  30584  dalem42  30585  dalem43  30586  dalem44  30587  dalem45  30588  dalem51  30594  dalem52  30595  dalem54  30597  dalem55  30598  dalem56  30599  dalem57  30600  dalem58  30601  dalem59  30602  dalem60  30603
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator