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

Metamath Proof Explorer

Theorem lsatlspsn2

Description: The span of a nonzero singleton is an atom. TODO: make this obsolete and use lsatlspsn instead? (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 lsatlspsn2 
|- ( ( W e. LMod /\ X e. V /\ X =/= .0. ) -> ( N ` { X } ) e. A )

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 3simpc 
 |-  ( ( W e. LMod /\ X e. V /\ X =/= .0. ) -> ( X e. V /\ X =/= .0. ) )
6 eldifsn 
 |-  ( X e. ( V \ { .0. } ) <-> ( X e. V /\ X =/= .0. ) )
7 5 6 sylibr 
 |-  ( ( W e. LMod /\ X e. V /\ X =/= .0. ) -> X e. ( V \ { .0. } ) )
8 eqid 
 |-  ( N ` { X } ) = ( N ` { X } )
9 sneq 
 |-  ( v = X -> { v } = { X } )
10 9 fveq2d 
 |-  ( v = X -> ( N ` { v } ) = ( N ` { X } ) )
11 10 rspceeqv 
 |-  ( ( X e. ( V \ { .0. } ) /\ ( N ` { X } ) = ( N ` { X } ) ) -> E. v e. ( V \ { .0. } ) ( N ` { X } ) = ( N ` { v } ) )
12 7 8 11 sylancl 
 |-  ( ( W e. LMod /\ X e. V /\ X =/= .0. ) -> E. v e. ( V \ { .0. } ) ( N ` { X } ) = ( N ` { v } ) )
13 1 2 3 4 islsat 
 |-  ( W e. LMod -> ( ( N ` { X } ) e. A <-> E. v e. ( V \ { .0. } ) ( N ` { X } ) = ( N ` { v } ) ) )
14 13 3ad2ant1 
 |-  ( ( W e. LMod /\ X e. V /\ X =/= .0. ) -> ( ( N ` { X } ) e. A <-> E. v e. ( V \ { .0. } ) ( N ` { X } ) = ( N ` { v } ) ) )
15 12 14 mpbird 
 |-  ( ( W e. LMod /\ X e. V /\ X =/= .0. ) -> ( N ` { X } ) e. A )