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

Theorem islsat 32473
Description: The predicate "is a 1-dim subspace (atom)" (of a left module or left vector space). (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
Hypotheses
Ref Expression
lsatset.v  |-  V  =  ( Base `  W
)
lsatset.n  |-  N  =  ( LSpan `  W )
lsatset.z  |-  .0.  =  ( 0g `  W )
lsatset.a  |-  A  =  (LSAtoms `  W )
Assertion
Ref Expression
islsat  |-  ( W  e.  X  ->  ( U  e.  A  <->  E. x  e.  ( V  \  {  .0.  } ) U  =  ( N `  {
x } ) ) )
Distinct variable groups:    x, W    x, X    x, N    x, U    x, V    x,  .0.
Allowed substitution hint:    A( x)

Proof of Theorem islsat
StepHypRef Expression
1 lsatset.v . . . 4  |-  V  =  ( Base `  W
)
2 lsatset.n . . . 4  |-  N  =  ( LSpan `  W )
3 lsatset.z . . . 4  |-  .0.  =  ( 0g `  W )
4 lsatset.a . . . 4  |-  A  =  (LSAtoms `  W )
51, 2, 3, 4lsatset 32472 . . 3  |-  ( W  e.  X  ->  A  =  ran  ( x  e.  ( V  \  {  .0.  } )  |->  ( N `
 { x }
) ) )
65eleq2d 2492 . 2  |-  ( W  e.  X  ->  ( U  e.  A  <->  U  e.  ran  ( x  e.  ( V  \  {  .0.  } )  |->  ( N `  { x } ) ) ) )
7 eqid 2422 . . 3  |-  ( x  e.  ( V  \  {  .0.  } )  |->  ( N `  { x } ) )  =  ( x  e.  ( V  \  {  .0.  } )  |->  ( N `  { x } ) )
8 fvex 5887 . . 3  |-  ( N `
 { x }
)  e.  _V
97, 8elrnmpti 5100 . 2  |-  ( U  e.  ran  ( x  e.  ( V  \  {  .0.  } )  |->  ( N `  { x } ) )  <->  E. x  e.  ( V  \  {  .0.  } ) U  =  ( N `  {
x } ) )
106, 9syl6bb 264 1  |-  ( W  e.  X  ->  ( U  e.  A  <->  E. x  e.  ( V  \  {  .0.  } ) U  =  ( N `  {
x } ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437    e. wcel 1868   E.wrex 2776    \ cdif 3433   {csn 3996    |-> cmpt 4479   ran crn 4850   ` cfv 5597   Basecbs 15106   0gc0g 15323   LSpanclspn 18179  LSAtomsclsa 32456
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-fv 5605  df-lsatoms 32458
This theorem is referenced by:  lsatlspsn2  32474  lsatlspsn  32475  islsati  32476  lsateln0  32477  lsatn0  32481  lsatcmp  32485  lsmsat  32490  lsatfixedN  32491  islshpat  32499  lsatcv0  32513  lsat0cv  32515  lcv1  32523  l1cvpat  32536  dih1dimatlem  34813  dihlatat  34821  dochsatshp  34935
  Copyright terms: Public domain W3C validator