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

Theorem dalemkehl 33606
Description: Lemma for dath 33719. 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 1099 . 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 965    e. wcel 1758   class class class wbr 4401   ` cfv 5527  (class class class)co 6201   Basecbs 14293   HLchlt 33334
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 967
This theorem is referenced by:  dalemkelat  33607  dalemkeop  33608  dalempjqeb  33628  dalemsjteb  33629  dalemtjueb  33630  dalemqrprot  33631  dalempnes  33634  dalemqnet  33635  dalempjsen  33636  dalemply  33637  dalemsly  33638  dalemswapyz  33639  dalemrot  33640  dalemrotyz  33641  dalem1  33642  dalemcea  33643  dalem2  33644  dalemdea  33645  dalem3  33647  dalem4  33648  dalem5  33650  dalem-cly  33654  dalem9  33655  dalem11  33657  dalem12  33658  dalem13  33659  dalem15  33661  dalem16  33662  dalem17  33663  dalem18  33664  dalem19  33665  dalemswapyzps  33673  dalemcjden  33675  dalem21  33677  dalem22  33678  dalem23  33679  dalem24  33680  dalem25  33681  dalem27  33682  dalem28  33683  dalem38  33693  dalem39  33694  dalem41  33696  dalem42  33697  dalem43  33698  dalem44  33699  dalem45  33700  dalem51  33706  dalem52  33707  dalem54  33709  dalem55  33710  dalem56  33711  dalem57  33712  dalem58  33713  dalem59  33714  dalem60  33715
  Copyright terms: Public domain W3C validator