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

Metamath Proof Explorer

Theorem islsati

Description: A 1-dim subspace (atom) (of a left module or left vector space) equals the span of some vector. (Contributed by NM, 1-Oct-2014)

Ref Expression
Hypotheses islsati.v ⊢ V = Base W
islsati.n ⊢ N = LSpan ⁡ W
islsati.a ⊢ A = LSAtoms ⁡ W
Assertion islsati ⊢ W ∈ X ∧ U ∈ A → ∃ v ∈ V U = N ⁡ v

Proof

Step Hyp Ref Expression
1 islsati.v ⊢ V = Base W
2 islsati.n ⊢ N = LSpan ⁡ W
3 islsati.a ⊢ A = LSAtoms ⁡ W
4 difss ⊢ V ∖ 0 W ⊆ V
5 eqid ⊢ 0 W = 0 W
6 1 2 5 3 islsat ⊢ W ∈ X → U ∈ A ↔ ∃ v ∈ V ∖ 0 W U = N ⁡ v
7 6 biimpa ⊢ W ∈ X ∧ U ∈ A → ∃ v ∈ V ∖ 0 W U = N ⁡ v
8 ssrexv ⊢ V ∖ 0 W ⊆ V → ∃ v ∈ V ∖ 0 W U = N ⁡ v → ∃ v ∈ V U = N ⁡ v
9 4 7 8 mpsyl ⊢ W ∈ X ∧ U ∈ A → ∃ v ∈ V U = N ⁡ v