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 ˙ = 0 W
lsatset.a ⊢ A = LSAtoms ⁡ W
Assertion lsatlspsn2 ⊢ W ∈ LMod ∧ X ∈ V ∧ X ≠ 0 ˙ → N ⁡ X ∈ A

Proof

Step Hyp Ref Expression
1 lsatset.v ⊢ V = Base W
2 lsatset.n ⊢ N = LSpan ⁡ W
3 lsatset.z ⊢ 0 ˙ = 0 W
4 lsatset.a ⊢ A = LSAtoms ⁡ W
5 3simpc ⊢ W ∈ LMod ∧ X ∈ V ∧ X ≠ 0 ˙ → X ∈ V ∧ X ≠ 0 ˙
6 eldifsn ⊢ X ∈ V ∖ 0 ˙ ↔ X ∈ V ∧ X ≠ 0 ˙
7 5 6 sylibr ⊢ W ∈ LMod ∧ X ∈ V ∧ X ≠ 0 ˙ → X ∈ 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 ∈ V ∖ 0 ˙ ∧ N ⁡ X = N ⁡ X → ∃ v ∈ V ∖ 0 ˙ N ⁡ X = N ⁡ v
12 7 8 11 sylancl ⊢ W ∈ LMod ∧ X ∈ V ∧ X ≠ 0 ˙ → ∃ v ∈ V ∖ 0 ˙ N ⁡ X = N ⁡ v
13 1 2 3 4 islsat ⊢ W ∈ LMod → N ⁡ X ∈ A ↔ ∃ v ∈ V ∖ 0 ˙ N ⁡ X = N ⁡ v
14 13 3ad2ant1 ⊢ W ∈ LMod ∧ X ∈ V ∧ X ≠ 0 ˙ → N ⁡ X ∈ A ↔ ∃ v ∈ V ∖ 0 ˙ N ⁡ X = N ⁡ v
15 12 14 mpbird ⊢ W ∈ LMod ∧ X ∈ V ∧ X ≠ 0 ˙ → N ⁡ X ∈ A