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

Theorem 2atmat 33120
Description: The meet of two intersecting lines (expressed as joins of atoms) is an atom. (Contributed by NM, 21-Nov-2012.)
Hypotheses
Ref Expression
2atmat.l  |-  .<_  =  ( le `  K )
2atmat.j  |-  .\/  =  ( join `  K )
2atmat.m  |-  ./\  =  ( meet `  K )
2atmat.a  |-  A  =  ( Atoms `  K )
Assertion
Ref Expression
2atmat  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  (
( P  .\/  Q
)  ./\  ( R  .\/  S ) )  e.  A )

Proof of Theorem 2atmat
StepHypRef Expression
1 simp11 1037 . . . . . 6  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  K  e.  HL )
2 hllat 32923 . . . . . 6  |-  ( K  e.  HL  ->  K  e.  Lat )
31, 2syl 17 . . . . 5  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  K  e.  Lat )
4 eqid 2450 . . . . . . 7  |-  ( Base `  K )  =  (
Base `  K )
5 2atmat.j . . . . . . 7  |-  .\/  =  ( join `  K )
6 2atmat.a . . . . . . 7  |-  A  =  ( Atoms `  K )
74, 5, 6hlatjcl 32926 . . . . . 6  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  ( P  .\/  Q
)  e.  ( Base `  K ) )
873ad2ant1 1028 . . . . 5  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  ( P  .\/  Q )  e.  ( Base `  K
) )
9 simp21 1040 . . . . . 6  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  R  e.  A )
104, 6atbase 32849 . . . . . 6  |-  ( R  e.  A  ->  R  e.  ( Base `  K
) )
119, 10syl 17 . . . . 5  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  R  e.  ( Base `  K
) )
12 simp22 1041 . . . . . 6  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  S  e.  A )
134, 6atbase 32849 . . . . . 6  |-  ( S  e.  A  ->  S  e.  ( Base `  K
) )
1412, 13syl 17 . . . . 5  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  S  e.  ( Base `  K
) )
154, 5latjass 16334 . . . . 5  |-  ( ( K  e.  Lat  /\  ( ( P  .\/  Q )  e.  ( Base `  K )  /\  R  e.  ( Base `  K
)  /\  S  e.  ( Base `  K )
) )  ->  (
( ( P  .\/  Q )  .\/  R ) 
.\/  S )  =  ( ( P  .\/  Q )  .\/  ( R 
.\/  S ) ) )
163, 8, 11, 14, 15syl13anc 1269 . . . 4  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  (
( ( P  .\/  Q )  .\/  R ) 
.\/  S )  =  ( ( P  .\/  Q )  .\/  ( R 
.\/  S ) ) )
17 simp33 1045 . . . . 5  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  S  .<_  ( ( P  .\/  Q )  .\/  R ) )
184, 5latjcl 16290 . . . . . . 7  |-  ( ( K  e.  Lat  /\  ( P  .\/  Q )  e.  ( Base `  K
)  /\  R  e.  ( Base `  K )
)  ->  ( ( P  .\/  Q )  .\/  R )  e.  ( Base `  K ) )
193, 8, 11, 18syl3anc 1267 . . . . . 6  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  (
( P  .\/  Q
)  .\/  R )  e.  ( Base `  K
) )
20 2atmat.l . . . . . . 7  |-  .<_  =  ( le `  K )
214, 20, 5latleeqj2 16303 . . . . . 6  |-  ( ( K  e.  Lat  /\  S  e.  ( Base `  K )  /\  (
( P  .\/  Q
)  .\/  R )  e.  ( Base `  K
) )  ->  ( S  .<_  ( ( P 
.\/  Q )  .\/  R )  <->  ( ( ( P  .\/  Q ) 
.\/  R )  .\/  S )  =  ( ( P  .\/  Q ) 
.\/  R ) ) )
223, 14, 19, 21syl3anc 1267 . . . . 5  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  ( S  .<_  ( ( P 
.\/  Q )  .\/  R )  <->  ( ( ( P  .\/  Q ) 
.\/  R )  .\/  S )  =  ( ( P  .\/  Q ) 
.\/  R ) ) )
2317, 22mpbid 214 . . . 4  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  (
( ( P  .\/  Q )  .\/  R ) 
.\/  S )  =  ( ( P  .\/  Q )  .\/  R ) )
2416, 23eqtr3d 2486 . . 3  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  (
( P  .\/  Q
)  .\/  ( R  .\/  S ) )  =  ( ( P  .\/  Q )  .\/  R ) )
25 simp23 1042 . . . 4  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  P  =/=  Q )
26 simp32 1044 . . . 4  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  -.  R  .<_  ( P  .\/  Q ) )
27 simp12 1038 . . . . 5  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  P  e.  A )
28 simp13 1039 . . . . 5  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  Q  e.  A )
29 eqid 2450 . . . . . 6  |-  ( LPlanes `  K )  =  (
LPlanes `  K )
3020, 5, 6, 29islpln2a 33107 . . . . 5  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A
) )  ->  (
( ( P  .\/  Q )  .\/  R )  e.  ( LPlanes `  K
)  <->  ( P  =/= 
Q  /\  -.  R  .<_  ( P  .\/  Q
) ) ) )
311, 27, 28, 9, 30syl13anc 1269 . . . 4  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  (
( ( P  .\/  Q )  .\/  R )  e.  ( LPlanes `  K
)  <->  ( P  =/= 
Q  /\  -.  R  .<_  ( P  .\/  Q
) ) ) )
3225, 26, 31mpbir2and 932 . . 3  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  (
( P  .\/  Q
)  .\/  R )  e.  ( LPlanes `  K )
)
3324, 32eqeltrd 2528 . 2  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  (
( P  .\/  Q
)  .\/  ( R  .\/  S ) )  e.  ( LPlanes `  K )
)
34 eqid 2450 . . . . 5  |-  ( LLines `  K )  =  (
LLines `  K )
355, 6, 34llni2 33071 . . . 4  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  P  =/=  Q
)  ->  ( P  .\/  Q )  e.  (
LLines `  K ) )
361, 27, 28, 25, 35syl31anc 1270 . . 3  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  ( P  .\/  Q )  e.  ( LLines `  K )
)
37 simp31 1043 . . . 4  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  R  =/=  S )
385, 6, 34llni2 33071 . . . 4  |-  ( ( ( K  e.  HL  /\  R  e.  A  /\  S  e.  A )  /\  R  =/=  S
)  ->  ( R  .\/  S )  e.  (
LLines `  K ) )
391, 9, 12, 37, 38syl31anc 1270 . . 3  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  ( R  .\/  S )  e.  ( LLines `  K )
)
40 2atmat.m . . . 4  |-  ./\  =  ( meet `  K )
415, 40, 6, 34, 292llnmj 33119 . . 3  |-  ( ( K  e.  HL  /\  ( P  .\/  Q )  e.  ( LLines `  K
)  /\  ( R  .\/  S )  e.  (
LLines `  K ) )  ->  ( ( ( P  .\/  Q ) 
./\  ( R  .\/  S ) )  e.  A  <->  ( ( P  .\/  Q
)  .\/  ( R  .\/  S ) )  e.  ( LPlanes `  K )
) )
421, 36, 39, 41syl3anc 1267 . 2  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  (
( ( P  .\/  Q )  ./\  ( R  .\/  S ) )  e.  A  <->  ( ( P 
.\/  Q )  .\/  ( R  .\/  S ) )  e.  ( LPlanes `  K ) ) )
4333, 42mpbird 236 1  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  /\  ( R  e.  A  /\  S  e.  A  /\  P  =/=  Q
)  /\  ( R  =/=  S  /\  -.  R  .<_  ( P  .\/  Q
)  /\  S  .<_  ( ( P  .\/  Q
)  .\/  R )
) )  ->  (
( P  .\/  Q
)  ./\  ( R  .\/  S ) )  e.  A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    /\ wa 371    /\ w3a 984    = wceq 1443    e. wcel 1886    =/= wne 2621   class class class wbr 4401   ` cfv 5581  (class class class)co 6288   Basecbs 15114   lecple 15190   joincjn 16182   meetcmee 16183   Latclat 16284   Atomscatm 32823   HLchlt 32910   LLinesclln 33050   LPlanesclpl 33051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250  df-ov 6291  df-oprab 6292  df-preset 16166  df-poset 16184  df-plt 16197  df-lub 16213  df-glb 16214  df-join 16215  df-meet 16216  df-p0 16278  df-lat 16285  df-clat 16347  df-oposet 32736  df-ol 32738  df-oml 32739  df-covers 32826  df-ats 32827  df-atl 32858  df-cvlat 32882  df-hlat 32911  df-llines 33057  df-lplanes 33058
This theorem is referenced by:  4atexlemc  33628
  Copyright terms: Public domain W3C validator