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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
lsatset.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lsatset.z ⊢ 0 = ( 0g ‘ 𝑊 )
lsatset.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
Assertion lsatlspsn2 ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 )

Proof

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