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

Theorem dalem21 29810
Description: Lemma for dath 29852. Show that lines  c d and  P S intersect at an atom. (Contributed by NM, 2-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
) ) ) )
dalem21.m  |-  ./\  =  ( meet `  K )
dalem21.o  |-  O  =  ( LPlanes `  K )
dalem21.y  |-  Y  =  ( ( P  .\/  Q )  .\/  R )
dalem21.z  |-  Z  =  ( ( S  .\/  T )  .\/  U )
Assertion
Ref Expression
dalem21  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( c  .\/  d )  ./\  ( P  .\/  S ) )  e.  A )

Proof of Theorem dalem21
StepHypRef Expression
1 dalem.ph . . . 4  |-  ( 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 ) ) ) ) )
21dalemkehl 29739 . . 3  |-  ( ph  ->  K  e.  HL )
323ad2ant1 978 . 2  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  K  e.  HL )
4 dalem.l . . . 4  |-  .<_  =  ( le `  K )
5 dalem.j . . . 4  |-  .\/  =  ( join `  K )
6 dalem.a . . . 4  |-  A  =  ( Atoms `  K )
7 dalem.ps . . . 4  |-  ( ps  <->  ( ( c  e.  A  /\  d  e.  A
)  /\  -.  c  .<_  Y  /\  ( d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
) ) ) )
81, 4, 5, 6, 7dalemcjden 29808 . . 3  |-  ( (
ph  /\  ps )  ->  ( c  .\/  d
)  e.  ( LLines `  K ) )
983adant2 976 . 2  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( c  .\/  d
)  e.  ( LLines `  K ) )
10 dalem21.o . . . 4  |-  O  =  ( LPlanes `  K )
11 dalem21.y . . . 4  |-  Y  =  ( ( P  .\/  Q )  .\/  R )
121, 4, 5, 6, 10, 11dalempjsen 29769 . . 3  |-  ( ph  ->  ( P  .\/  S
)  e.  ( LLines `  K ) )
13123ad2ant1 978 . 2  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( P  .\/  S
)  e.  ( LLines `  K ) )
141, 4, 5, 6, 10, 11dalemply 29770 . . . . . . 7  |-  ( ph  ->  P  .<_  Y )
1514adantr 452 . . . . . 6  |-  ( (
ph  /\  Y  =  Z )  ->  P  .<_  Y )
16 dalem21.z . . . . . . 7  |-  Z  =  ( ( S  .\/  T )  .\/  U )
171, 4, 5, 6, 16dalemsly 29771 . . . . . 6  |-  ( (
ph  /\  Y  =  Z )  ->  S  .<_  Y )
181dalemkelat 29740 . . . . . . . 8  |-  ( ph  ->  K  e.  Lat )
191, 6dalempeb 29755 . . . . . . . 8  |-  ( ph  ->  P  e.  ( Base `  K ) )
201, 6dalemseb 29758 . . . . . . . 8  |-  ( ph  ->  S  e.  ( Base `  K ) )
211, 10dalemyeb 29765 . . . . . . . 8  |-  ( ph  ->  Y  e.  ( Base `  K ) )
22 eqid 2389 . . . . . . . . 9  |-  ( Base `  K )  =  (
Base `  K )
2322, 4, 5latjle12 14420 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  ( P  e.  ( Base `  K )  /\  S  e.  ( Base `  K )  /\  Y  e.  ( Base `  K
) ) )  -> 
( ( P  .<_  Y  /\  S  .<_  Y )  <-> 
( P  .\/  S
)  .<_  Y ) )
2418, 19, 20, 21, 23syl13anc 1186 . . . . . . 7  |-  ( ph  ->  ( ( P  .<_  Y  /\  S  .<_  Y )  <-> 
( P  .\/  S
)  .<_  Y ) )
2524adantr 452 . . . . . 6  |-  ( (
ph  /\  Y  =  Z )  ->  (
( P  .<_  Y  /\  S  .<_  Y )  <->  ( P  .\/  S )  .<_  Y ) )
2615, 17, 25mpbi2and 888 . . . . 5  |-  ( (
ph  /\  Y  =  Z )  ->  ( P  .\/  S )  .<_  Y )
27263adant3 977 . . . 4  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( P  .\/  S
)  .<_  Y )
287dalem-ccly 29801 . . . . . . 7  |-  ( ps 
->  -.  c  .<_  Y )
2928adantl 453 . . . . . 6  |-  ( (
ph  /\  ps )  ->  -.  c  .<_  Y )
3018adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  K  e.  Lat )
317, 6dalemcceb 29805 . . . . . . . . 9  |-  ( ps 
->  c  e.  ( Base `  K ) )
3231adantl 453 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  c  e.  ( Base `  K ) )
337dalemddea 29800 . . . . . . . . . 10  |-  ( ps 
->  d  e.  A
)
3422, 6atbase 29406 . . . . . . . . . 10  |-  ( d  e.  A  ->  d  e.  ( Base `  K
) )
3533, 34syl 16 . . . . . . . . 9  |-  ( ps 
->  d  e.  ( Base `  K ) )
3635adantl 453 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  d  e.  ( Base `  K ) )
3722, 4, 5latlej1 14418 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  c  e.  ( Base `  K )  /\  d  e.  ( Base `  K
) )  ->  c  .<_  ( c  .\/  d
) )
3830, 32, 36, 37syl3anc 1184 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  c  .<_  ( c  .\/  d ) )
39 eqid 2389 . . . . . . . . . 10  |-  ( LLines `  K )  =  (
LLines `  K )
4022, 39llnbase 29625 . . . . . . . . 9  |-  ( ( c  .\/  d )  e.  ( LLines `  K
)  ->  ( c  .\/  d )  e.  (
Base `  K )
)
418, 40syl 16 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( c  .\/  d
)  e.  ( Base `  K ) )
4221adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  Y  e.  ( Base `  K ) )
4322, 4lattr 14414 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  ( c  e.  (
Base `  K )  /\  ( c  .\/  d
)  e.  ( Base `  K )  /\  Y  e.  ( Base `  K
) ) )  -> 
( ( c  .<_  ( c  .\/  d
)  /\  ( c  .\/  d )  .<_  Y )  ->  c  .<_  Y ) )
4430, 32, 41, 42, 43syl13anc 1186 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ( ( c  .<_  ( c  .\/  d
)  /\  ( c  .\/  d )  .<_  Y )  ->  c  .<_  Y ) )
4538, 44mpand 657 . . . . . 6  |-  ( (
ph  /\  ps )  ->  ( ( c  .\/  d )  .<_  Y  -> 
c  .<_  Y ) )
4629, 45mtod 170 . . . . 5  |-  ( (
ph  /\  ps )  ->  -.  ( c  .\/  d )  .<_  Y )
47463adant2 976 . . . 4  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  -.  ( c  .\/  d
)  .<_  Y )
48 nbrne2 4173 . . . 4  |-  ( ( ( P  .\/  S
)  .<_  Y  /\  -.  ( c  .\/  d
)  .<_  Y )  -> 
( P  .\/  S
)  =/=  ( c 
.\/  d ) )
4927, 47, 48syl2anc 643 . . 3  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( P  .\/  S
)  =/=  ( c 
.\/  d ) )
5049necomd 2635 . 2  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( c  .\/  d
)  =/=  ( P 
.\/  S ) )
51 hlatl 29477 . . . . . 6  |-  ( K  e.  HL  ->  K  e.  AtLat )
522, 51syl 16 . . . . 5  |-  ( ph  ->  K  e.  AtLat )
5352adantr 452 . . . 4  |-  ( (
ph  /\  ps )  ->  K  e.  AtLat )
541dalempea 29742 . . . . . . 7  |-  ( ph  ->  P  e.  A )
551dalemsea 29745 . . . . . . 7  |-  ( ph  ->  S  e.  A )
5622, 5, 6hlatjcl 29483 . . . . . . 7  |-  ( ( K  e.  HL  /\  P  e.  A  /\  S  e.  A )  ->  ( P  .\/  S
)  e.  ( Base `  K ) )
572, 54, 55, 56syl3anc 1184 . . . . . 6  |-  ( ph  ->  ( P  .\/  S
)  e.  ( Base `  K ) )
5857adantr 452 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( P  .\/  S
)  e.  ( Base `  K ) )
59 dalem21.m . . . . . 6  |-  ./\  =  ( meet `  K )
6022, 59latmcl 14409 . . . . 5  |-  ( ( K  e.  Lat  /\  ( c  .\/  d
)  e.  ( Base `  K )  /\  ( P  .\/  S )  e.  ( Base `  K
) )  ->  (
( c  .\/  d
)  ./\  ( P  .\/  S ) )  e.  ( Base `  K
) )
6130, 41, 58, 60syl3anc 1184 . . . 4  |-  ( (
ph  /\  ps )  ->  ( ( c  .\/  d )  ./\  ( P  .\/  S ) )  e.  ( Base `  K
) )
621, 4, 5, 6, 10, 11dalemcea 29776 . . . . 5  |-  ( ph  ->  C  e.  A )
6362adantr 452 . . . 4  |-  ( (
ph  /\  ps )  ->  C  e.  A )
647dalemclccjdd 29804 . . . . . 6  |-  ( ps 
->  C  .<_  ( c 
.\/  d ) )
6564adantl 453 . . . . 5  |-  ( (
ph  /\  ps )  ->  C  .<_  ( c  .\/  d ) )
661dalemclpjs 29750 . . . . . 6  |-  ( ph  ->  C  .<_  ( P  .\/  S ) )
6766adantr 452 . . . . 5  |-  ( (
ph  /\  ps )  ->  C  .<_  ( P  .\/  S ) )
681, 6dalemceb 29754 . . . . . . 7  |-  ( ph  ->  C  e.  ( Base `  K ) )
6968adantr 452 . . . . . 6  |-  ( (
ph  /\  ps )  ->  C  e.  ( Base `  K ) )
7022, 4, 59latlem12 14436 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( C  e.  ( Base `  K )  /\  ( c  .\/  d
)  e.  ( Base `  K )  /\  ( P  .\/  S )  e.  ( Base `  K
) ) )  -> 
( ( C  .<_  ( c  .\/  d )  /\  C  .<_  ( P 
.\/  S ) )  <-> 
C  .<_  ( ( c 
.\/  d )  ./\  ( P  .\/  S ) ) ) )
7130, 69, 41, 58, 70syl13anc 1186 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( ( C  .<_  ( c  .\/  d )  /\  C  .<_  ( P 
.\/  S ) )  <-> 
C  .<_  ( ( c 
.\/  d )  ./\  ( P  .\/  S ) ) ) )
7265, 67, 71mpbi2and 888 . . . 4  |-  ( (
ph  /\  ps )  ->  C  .<_  ( (
c  .\/  d )  ./\  ( P  .\/  S
) ) )
73 eqid 2389 . . . . 5  |-  ( 0.
`  K )  =  ( 0. `  K
)
7422, 4, 73, 6atlen0 29427 . . . 4  |-  ( ( ( K  e.  AtLat  /\  ( ( c  .\/  d )  ./\  ( P  .\/  S ) )  e.  ( Base `  K
)  /\  C  e.  A )  /\  C  .<_  ( ( c  .\/  d )  ./\  ( P  .\/  S ) ) )  ->  ( (
c  .\/  d )  ./\  ( P  .\/  S
) )  =/=  ( 0. `  K ) )
7553, 61, 63, 72, 74syl31anc 1187 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( c  .\/  d )  ./\  ( P  .\/  S ) )  =/=  ( 0. `  K ) )
76753adant2 976 . 2  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( c  .\/  d )  ./\  ( P  .\/  S ) )  =/=  ( 0. `  K ) )
7759, 73, 6, 392llnmat 29640 . 2  |-  ( ( ( K  e.  HL  /\  ( c  .\/  d
)  e.  ( LLines `  K )  /\  ( P  .\/  S )  e.  ( LLines `  K )
)  /\  ( (
c  .\/  d )  =/=  ( P  .\/  S
)  /\  ( (
c  .\/  d )  ./\  ( P  .\/  S
) )  =/=  ( 0. `  K ) ) )  ->  ( (
c  .\/  d )  ./\  ( P  .\/  S
) )  e.  A
)
783, 9, 13, 50, 76, 77syl32anc 1192 1  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( c  .\/  d )  ./\  ( P  .\/  S ) )  e.  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1717    =/= wne 2552   class class class wbr 4155   ` cfv 5396  (class class class)co 6022   Basecbs 13398   lecple 13465   joincjn 14330   meetcmee 14331   0.cp0 14395   Latclat 14403   Atomscatm 29380   AtLatcal 29381   HLchlt 29467   LLinesclln 29607   LPlanesclpl 29608
This theorem is referenced by:  dalem22  29811
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-rep 4263  ax-sep 4273  ax-nul 4281  ax-pow 4320  ax-pr 4346  ax-un 4643
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-nel 2555  df-ral 2656  df-rex 2657  df-reu 2658  df-rab 2660  df-v 2903  df-sbc 3107  df-csb 3197  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-iun 4039  df-br 4156  df-opab 4210  df-mpt 4211  df-id 4441  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-iota 5360  df-fun 5398  df-fn 5399  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403  df-fv 5404  df-ov 6025  df-oprab 6026  df-mpt2 6027  df-1st 6290  df-2nd 6291  df-undef 6481  df-riota 6487  df-poset 14332  df-plt 14344  df-lub 14360  df-glb 14361  df-join 14362  df-meet 14363  df-p0 14397  df-lat 14404  df-clat 14466  df-oposet 29293  df-ol 29295  df-oml 29296  df-covers 29383  df-ats 29384  df-atl 29415  df-cvlat 29439  df-hlat 29468  df-llines 29614  df-lplanes 29615
  Copyright terms: Public domain W3C validator