Theorem lsatlspsn

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

	Ref	Expression
Hypotheses	lsatset.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lsatset.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lsatset.z	⊢ 0 = ( 0g ‘ 𝑊 )
	lsatset.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	lsatlspsn.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lsatlspsn.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion	lsatlspsn	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		lsatset.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lsatset.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		lsatset.z	⊢ 0 = ( 0g ‘ 𝑊 )
4		lsatset.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
5		lsatlspsn.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
6		lsatlspsn.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
7		eqid	⊢ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑋 } )
8		sneq	⊢ ( 𝑣 = 𝑋 → { 𝑣 } = { 𝑋 } )
9	8	fveq2d	⊢ ( 𝑣 = 𝑋 → ( 𝑁 ‘ { 𝑣 } ) = ( 𝑁 ‘ { 𝑋 } ) )
10	9	rspceeqv	⊢ ( ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑋 } ) ) → ∃ 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑣 } ) )
11	6 7 10	sylancl	⊢ ( 𝜑 → ∃ 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑣 } ) )
12	1 2 3 4	islsat	⊢ ( 𝑊 ∈ LMod → ( ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑣 } ) ) )
13	5 12	syl	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑣 } ) ) )
14	11 13	mpbird	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 )