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

Theorem dalemrotps 33302
Description: Lemma for dath 33347. Rotate triangles  Y  =  P Q R and  Z  =  S T U to allow reuse of analogous proofs. (Contributed by NM, 15-Aug-2012.)
Hypotheses
Ref Expression
dalem.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 ) ) ) ) )
dalem.l  |-  .<_  =  ( le `  K )
dalem.j  |-  .\/  =  ( join `  K )
dalem.a  |-  A  =  ( Atoms `  K )
dalem.ps  |-  ( ps  <->  ( ( c  e.  A  /\  d  e.  A
)  /\  -.  c  .<_  Y  /\  ( d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
) ) ) )
dalemrotps.y  |-  Y  =  ( ( P  .\/  Q )  .\/  R )
Assertion
Ref Expression
dalemrotps  |-  ( (
ph  /\  ps )  ->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  ( ( Q 
.\/  R )  .\/  P )  /\  ( d  =/=  c  /\  -.  d  .<_  ( ( Q 
.\/  R )  .\/  P )  /\  C  .<_  ( c  .\/  d ) ) ) )

Proof of Theorem dalemrotps
StepHypRef Expression
1 dalem.ps . . . . 5  |-  ( ps  <->  ( ( c  e.  A  /\  d  e.  A
)  /\  -.  c  .<_  Y  /\  ( d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
) ) ) )
21dalemccea 33294 . . . 4  |-  ( ps 
->  c  e.  A
)
31dalemddea 33295 . . . 4  |-  ( ps 
->  d  e.  A
)
42, 3jca 539 . . 3  |-  ( ps 
->  ( c  e.  A  /\  d  e.  A
) )
54adantl 472 . 2  |-  ( (
ph  /\  ps )  ->  ( c  e.  A  /\  d  e.  A
) )
61dalem-ccly 33296 . . . 4  |-  ( ps 
->  -.  c  .<_  Y )
76adantl 472 . . 3  |-  ( (
ph  /\  ps )  ->  -.  c  .<_  Y )
8 dalem.ph . . . . . . 7  |-  ( 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 ) ) ) ) )
9 dalem.j . . . . . . 7  |-  .\/  =  ( join `  K )
10 dalem.a . . . . . . 7  |-  A  =  ( Atoms `  K )
118, 9, 10dalemqrprot 33259 . . . . . 6  |-  ( ph  ->  ( ( Q  .\/  R )  .\/  P )  =  ( ( P 
.\/  Q )  .\/  R ) )
12 dalemrotps.y . . . . . 6  |-  Y  =  ( ( P  .\/  Q )  .\/  R )
1311, 12syl6reqr 2515 . . . . 5  |-  ( ph  ->  Y  =  ( ( Q  .\/  R ) 
.\/  P ) )
1413breq2d 4430 . . . 4  |-  ( ph  ->  ( c  .<_  Y  <->  c  .<_  ( ( Q  .\/  R
)  .\/  P )
) )
1514adantr 471 . . 3  |-  ( (
ph  /\  ps )  ->  ( c  .<_  Y  <->  c  .<_  ( ( Q  .\/  R
)  .\/  P )
) )
167, 15mtbid 306 . 2  |-  ( (
ph  /\  ps )  ->  -.  c  .<_  ( ( Q  .\/  R ) 
.\/  P ) )
171dalemccnedd 33298 . . . . 5  |-  ( ps 
->  c  =/=  d
)
1817necomd 2691 . . . 4  |-  ( ps 
->  d  =/=  c
)
1918adantl 472 . . 3  |-  ( (
ph  /\  ps )  ->  d  =/=  c )
201dalem-ddly 33297 . . . . 5  |-  ( ps 
->  -.  d  .<_  Y )
2120adantl 472 . . . 4  |-  ( (
ph  /\  ps )  ->  -.  d  .<_  Y )
2213breq2d 4430 . . . . 5  |-  ( ph  ->  ( d  .<_  Y  <->  d  .<_  ( ( Q  .\/  R
)  .\/  P )
) )
2322adantr 471 . . . 4  |-  ( (
ph  /\  ps )  ->  ( d  .<_  Y  <->  d  .<_  ( ( Q  .\/  R
)  .\/  P )
) )
2421, 23mtbid 306 . . 3  |-  ( (
ph  /\  ps )  ->  -.  d  .<_  ( ( Q  .\/  R ) 
.\/  P ) )
251dalemclccjdd 33299 . . . 4  |-  ( ps 
->  C  .<_  ( c 
.\/  d ) )
2625adantl 472 . . 3  |-  ( (
ph  /\  ps )  ->  C  .<_  ( c  .\/  d ) )
2719, 24, 263jca 1194 . 2  |-  ( (
ph  /\  ps )  ->  ( d  =/=  c  /\  -.  d  .<_  ( ( Q  .\/  R ) 
.\/  P )  /\  C  .<_  ( c  .\/  d ) ) )
285, 16, 273jca 1194 1  |-  ( (
ph  /\  ps )  ->  ( ( c  e.  A  /\  d  e.  A )  /\  -.  c  .<_  ( ( Q 
.\/  R )  .\/  P )  /\  ( d  =/=  c  /\  -.  d  .<_  ( ( Q 
.\/  R )  .\/  P )  /\  C  .<_  ( c  .\/  d ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 991    = wceq 1455    e. wcel 1898    =/= wne 2633   class class class wbr 4418   ` cfv 5605  (class class class)co 6320   Basecbs 15176   lecple 15252   joincjn 16244   Atomscatm 32875   HLchlt 32962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-preset 16228  df-poset 16246  df-lub 16275  df-glb 16276  df-join 16277  df-meet 16278  df-lat 16347  df-ats 32879  df-atl 32910  df-cvlat 32934  df-hlat 32963
This theorem is referenced by:  dalem29  33312  dalem30  33313  dalem31N  33314  dalem32  33315  dalem33  33316  dalem34  33317  dalem35  33318  dalem36  33319  dalem37  33320  dalem40  33323  dalem46  33329  dalem47  33330  dalem49  33332  dalem50  33333  dalem58  33341  dalem59  33342
  Copyright terms: Public domain W3C validator