This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem islsat

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)

Ref Expression
Hypotheses lsatset.v 
|- V = ( Base ` W )
lsatset.n 
|- N = ( LSpan ` W )
lsatset.z 
|- .0. = ( 0g ` W )
lsatset.a 
|- A = ( LSAtoms ` W )
Assertion islsat 
|- ( W e. X -> ( U e. A <-> E. x e. ( V \ { .0. } ) U = ( N ` { x } ) ) )

Proof

Step Hyp Ref Expression
1 lsatset.v 
 |-  V = ( Base ` W )
2 lsatset.n 
 |-  N = ( LSpan ` W )
3 lsatset.z 
 |-  .0. = ( 0g ` W )
4 lsatset.a 
 |-  A = ( LSAtoms ` W )
5 1 2 3 4 lsatset 
 |-  ( W e. X -> A = ran ( x e. ( V \ { .0. } ) |-> ( N ` { x } ) ) )
6 5 eleq2d 
 |-  ( W e. X -> ( U e. A <-> U e. ran ( x e. ( V \ { .0. } ) |-> ( N ` { x } ) ) ) )
7 eqid 
 |-  ( x e. ( V \ { .0. } ) |-> ( N ` { x } ) ) = ( x e. ( V \ { .0. } ) |-> ( N ` { x } ) )
8 fvex 
 |-  ( N ` { x } ) e. _V
9 7 8 elrnmpti 
 |-  ( U e. ran ( x e. ( V \ { .0. } ) |-> ( N ` { x } ) ) <-> E. x e. ( V \ { .0. } ) U = ( N ` { x } ) )
10 6 9 bitrdi 
 |-  ( W e. X -> ( U e. A <-> E. x e. ( V \ { .0. } ) U = ( N ` { x } ) ) )