Metamath Proof Explorer


Theorem lsatlspsn

Description: The span of a nonzero singleton is an atom. (Contributed by NM, 16-Jan-2015)

Ref Expression
Hypotheses lsatset.v
|- V = ( Base ` W )
lsatset.n
|- N = ( LSpan ` W )
lsatset.z
|- .0. = ( 0g ` W )
lsatset.a
|- A = ( LSAtoms ` W )
lsatlspsn.w
|- ( ph -> W e. LMod )
lsatlspsn.x
|- ( ph -> X e. ( V \ { .0. } ) )
Assertion lsatlspsn
|- ( ph -> ( 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 lsatlspsn.w
 |-  ( ph -> W e. LMod )
6 lsatlspsn.x
 |-  ( ph -> X e. ( V \ { .0. } ) )
7 eqid
 |-  ( N ` { X } ) = ( N ` { X } )
8 sneq
 |-  ( v = X -> { v } = { X } )
9 8 fveq2d
 |-  ( v = X -> ( N ` { v } ) = ( N ` { X } ) )
10 9 rspceeqv
 |-  ( ( X e. ( V \ { .0. } ) /\ ( N ` { X } ) = ( N ` { X } ) ) -> E. v e. ( V \ { .0. } ) ( N ` { X } ) = ( N ` { v } ) )
11 6 7 10 sylancl
 |-  ( ph -> E. v e. ( V \ { .0. } ) ( N ` { X } ) = ( N ` { v } ) )
12 1 2 3 4 islsat
 |-  ( W e. LMod -> ( ( N ` { X } ) e. A <-> E. v e. ( V \ { .0. } ) ( N ` { X } ) = ( N ` { v } ) ) )
13 5 12 syl
 |-  ( ph -> ( ( N ` { X } ) e. A <-> E. v e. ( V \ { .0. } ) ( N ` { X } ) = ( N ` { v } ) ) )
14 11 13 mpbird
 |-  ( ph -> ( N ` { X } ) e. A )