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

Theorem dalem24 33263
Description: Lemma for dath 33302. Show that auxiliary atom  G is outside of plane  Y. (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
) ) ) )
dalem23.m  |-  ./\  =  ( meet `  K )
dalem23.o  |-  O  =  ( LPlanes `  K )
dalem23.y  |-  Y  =  ( ( P  .\/  Q )  .\/  R )
dalem23.z  |-  Z  =  ( ( S  .\/  T )  .\/  U )
dalem23.g  |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )
Assertion
Ref Expression
dalem24  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  -.  G  .<_  Y )

Proof of Theorem dalem24
StepHypRef Expression
1 dalem23.g . . . . 5  |-  G  =  ( ( c  .\/  P )  ./\  ( d  .\/  S ) )
21oveq1i 6285 . . . 4  |-  ( G 
./\  Y )  =  ( ( ( c 
.\/  P )  ./\  ( d  .\/  S
) )  ./\  Y
)
3 dalem.ph . . . . . . . 8  |-  ( 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 ) ) ) ) )
43dalemkehl 33189 . . . . . . 7  |-  ( ph  ->  K  e.  HL )
5 hlol 32928 . . . . . . 7  |-  ( K  e.  HL  ->  K  e.  OL )
64, 5syl 17 . . . . . 6  |-  ( ph  ->  K  e.  OL )
763ad2ant1 1030 . . . . 5  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  K  e.  OL )
843ad2ant1 1030 . . . . . 6  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  K  e.  HL )
9 dalem.ps . . . . . . . 8  |-  ( ps  <->  ( ( c  e.  A  /\  d  e.  A
)  /\  -.  c  .<_  Y  /\  ( d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
) ) ) )
109dalemccea 33249 . . . . . . 7  |-  ( ps 
->  c  e.  A
)
11103ad2ant3 1032 . . . . . 6  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
c  e.  A )
123dalempea 33192 . . . . . . 7  |-  ( ph  ->  P  e.  A )
13123ad2ant1 1030 . . . . . 6  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  P  e.  A )
14 eqid 2451 . . . . . . 7  |-  ( Base `  K )  =  (
Base `  K )
15 dalem.j . . . . . . 7  |-  .\/  =  ( join `  K )
16 dalem.a . . . . . . 7  |-  A  =  ( Atoms `  K )
1714, 15, 16hlatjcl 32933 . . . . . 6  |-  ( ( K  e.  HL  /\  c  e.  A  /\  P  e.  A )  ->  ( c  .\/  P
)  e.  ( Base `  K ) )
188, 11, 13, 17syl3anc 1271 . . . . 5  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( c  .\/  P
)  e.  ( Base `  K ) )
199dalemddea 33250 . . . . . . 7  |-  ( ps 
->  d  e.  A
)
20193ad2ant3 1032 . . . . . 6  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
d  e.  A )
213dalemsea 33195 . . . . . . 7  |-  ( ph  ->  S  e.  A )
22213ad2ant1 1030 . . . . . 6  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  S  e.  A )
2314, 15, 16hlatjcl 32933 . . . . . 6  |-  ( ( K  e.  HL  /\  d  e.  A  /\  S  e.  A )  ->  ( d  .\/  S
)  e.  ( Base `  K ) )
248, 20, 22, 23syl3anc 1271 . . . . 5  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( d  .\/  S
)  e.  ( Base `  K ) )
25 dalem23.o . . . . . . 7  |-  O  =  ( LPlanes `  K )
263, 25dalemyeb 33215 . . . . . 6  |-  ( ph  ->  Y  e.  ( Base `  K ) )
27263ad2ant1 1030 . . . . 5  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  Y  e.  ( Base `  K ) )
28 dalem23.m . . . . . 6  |-  ./\  =  ( meet `  K )
2914, 28latmmdir 32802 . . . . 5  |-  ( ( K  e.  OL  /\  ( ( c  .\/  P )  e.  ( Base `  K )  /\  (
d  .\/  S )  e.  ( Base `  K
)  /\  Y  e.  ( Base `  K )
) )  ->  (
( ( c  .\/  P )  ./\  ( d  .\/  S ) )  ./\  Y )  =  ( ( ( c  .\/  P
)  ./\  Y )  ./\  ( ( d  .\/  S )  ./\  Y )
) )
307, 18, 24, 27, 29syl13anc 1273 . . . 4  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( ( c 
.\/  P )  ./\  ( d  .\/  S
) )  ./\  Y
)  =  ( ( ( c  .\/  P
)  ./\  Y )  ./\  ( ( d  .\/  S )  ./\  Y )
) )
312, 30syl5eq 2497 . . 3  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( G  ./\  Y
)  =  ( ( ( c  .\/  P
)  ./\  Y )  ./\  ( ( d  .\/  S )  ./\  Y )
) )
3215, 16hlatjcom 32934 . . . . . . 7  |-  ( ( K  e.  HL  /\  c  e.  A  /\  P  e.  A )  ->  ( c  .\/  P
)  =  ( P 
.\/  c ) )
338, 11, 13, 32syl3anc 1271 . . . . . 6  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( c  .\/  P
)  =  ( P 
.\/  c ) )
3433oveq1d 6290 . . . . 5  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( c  .\/  P )  ./\  Y )  =  ( ( P 
.\/  c )  ./\  Y ) )
35 dalem.l . . . . . . . 8  |-  .<_  =  ( le `  K )
36 dalem23.y . . . . . . . 8  |-  Y  =  ( ( P  .\/  Q )  .\/  R )
373, 35, 15, 16, 25, 36dalemply 33220 . . . . . . 7  |-  ( ph  ->  P  .<_  Y )
38373ad2ant1 1030 . . . . . 6  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  P  .<_  Y )
399dalem-ccly 33251 . . . . . . 7  |-  ( ps 
->  -.  c  .<_  Y )
40393ad2ant3 1032 . . . . . 6  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  -.  c  .<_  Y )
4114, 35, 15, 28, 162atjm 33011 . . . . . 6  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  c  e.  A  /\  Y  e.  ( Base `  K ) )  /\  ( P  .<_  Y  /\  -.  c  .<_  Y ) )  -> 
( ( P  .\/  c )  ./\  Y
)  =  P )
428, 13, 11, 27, 38, 40, 41syl132anc 1289 . . . . 5  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( P  .\/  c )  ./\  Y
)  =  P )
4334, 42eqtrd 2485 . . . 4  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( c  .\/  P )  ./\  Y )  =  P )
4415, 16hlatjcom 32934 . . . . . . 7  |-  ( ( K  e.  HL  /\  d  e.  A  /\  S  e.  A )  ->  ( d  .\/  S
)  =  ( S 
.\/  d ) )
458, 20, 22, 44syl3anc 1271 . . . . . 6  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( d  .\/  S
)  =  ( S 
.\/  d ) )
4645oveq1d 6290 . . . . 5  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( d  .\/  S )  ./\  Y )  =  ( ( S 
.\/  d )  ./\  Y ) )
47 dalem23.z . . . . . . . 8  |-  Z  =  ( ( S  .\/  T )  .\/  U )
483, 35, 15, 16, 47dalemsly 33221 . . . . . . 7  |-  ( (
ph  /\  Y  =  Z )  ->  S  .<_  Y )
49483adant3 1029 . . . . . 6  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  S  .<_  Y )
509dalem-ddly 33252 . . . . . . 7  |-  ( ps 
->  -.  d  .<_  Y )
51503ad2ant3 1032 . . . . . 6  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  -.  d  .<_  Y )
5214, 35, 15, 28, 162atjm 33011 . . . . . 6  |-  ( ( K  e.  HL  /\  ( S  e.  A  /\  d  e.  A  /\  Y  e.  ( Base `  K ) )  /\  ( S  .<_  Y  /\  -.  d  .<_  Y ) )  -> 
( ( S  .\/  d )  ./\  Y
)  =  S )
538, 22, 20, 27, 49, 51, 52syl132anc 1289 . . . . 5  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( S  .\/  d )  ./\  Y
)  =  S )
5446, 53eqtrd 2485 . . . 4  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( d  .\/  S )  ./\  Y )  =  S )
5543, 54oveq12d 6293 . . 3  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( ( ( c 
.\/  P )  ./\  Y )  ./\  ( (
d  .\/  S )  ./\  Y ) )  =  ( P  ./\  S
) )
563, 35, 15, 16, 25, 36dalempnes 33217 . . . . 5  |-  ( ph  ->  P  =/=  S )
57 hlatl 32927 . . . . . . 7  |-  ( K  e.  HL  ->  K  e.  AtLat )
584, 57syl 17 . . . . . 6  |-  ( ph  ->  K  e.  AtLat )
59 eqid 2451 . . . . . . 7  |-  ( 0.
`  K )  =  ( 0. `  K
)
6028, 59, 16atnem0 32885 . . . . . 6  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  S  e.  A )  ->  ( P  =/=  S  <->  ( P  ./\ 
S )  =  ( 0. `  K ) ) )
6158, 12, 21, 60syl3anc 1271 . . . . 5  |-  ( ph  ->  ( P  =/=  S  <->  ( P  ./\  S )  =  ( 0. `  K ) ) )
6256, 61mpbid 215 . . . 4  |-  ( ph  ->  ( P  ./\  S
)  =  ( 0.
`  K ) )
63623ad2ant1 1030 . . 3  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( P  ./\  S
)  =  ( 0.
`  K ) )
6431, 55, 633eqtrd 2489 . 2  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( G  ./\  Y
)  =  ( 0.
`  K ) )
65583ad2ant1 1030 . . 3  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  K  e.  AtLat )
663, 35, 15, 16, 9, 28, 25, 36, 47, 1dalem23 33262 . . 3  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  G  e.  A )
6714, 35, 28, 59, 16atnle 32884 . . 3  |-  ( ( K  e.  AtLat  /\  G  e.  A  /\  Y  e.  ( Base `  K
) )  ->  ( -.  G  .<_  Y  <->  ( G  ./\ 
Y )  =  ( 0. `  K ) ) )
6865, 66, 27, 67syl3anc 1271 . 2  |-  ( (
ph  /\  Y  =  Z  /\  ps )  -> 
( -.  G  .<_  Y  <-> 
( G  ./\  Y
)  =  ( 0.
`  K ) ) )
6964, 68mpbird 240 1  |-  ( (
ph  /\  Y  =  Z  /\  ps )  ->  -.  G  .<_  Y )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 986    = wceq 1447    e. wcel 1890    =/= wne 2621   class class class wbr 4373   ` cfv 5560  (class class class)co 6275   Basecbs 15131   lecple 15207   joincjn 16199   meetcmee 16200   0.cp0 16293   OLcol 32741   Atomscatm 32830   AtLatcal 32831   HLchlt 32917   LPlanesclpl 33058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-rep 4486  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-op 3942  df-uni 4168  df-iun 4249  df-br 4374  df-opab 4433  df-mpt 4434  df-id 4726  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-riota 6237  df-ov 6278  df-oprab 6279  df-preset 16183  df-poset 16201  df-plt 16214  df-lub 16230  df-glb 16231  df-join 16232  df-meet 16233  df-p0 16295  df-lat 16302  df-clat 16364  df-oposet 32743  df-ol 32745  df-oml 32746  df-covers 32833  df-ats 32834  df-atl 32865  df-cvlat 32889  df-hlat 32918  df-llines 33064  df-lplanes 33065
This theorem is referenced by:  dalem27  33265  dalem30  33268  dalem54  33292
  Copyright terms: Public domain W3C validator