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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
islsati.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
islsati.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
Assertion islsati ( ( 𝑊 ∈ 𝑋 ∧ 𝑈 ∈ 𝐴 ) → ∃ 𝑣 ∈ 𝑉 𝑈 = ( 𝑁 ‘ { 𝑣 } ) )

Proof

Step Hyp Ref Expression
1 islsati.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 islsati.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 islsati.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
4 difss ⊢ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ⊆ 𝑉
5 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
6 1 2 5 3 islsat ⊢ ( 𝑊 ∈ 𝑋 → ( 𝑈 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) 𝑈 = ( 𝑁 ‘ { 𝑣 } ) ) )
7 6 biimpa ⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝑈 ∈ 𝐴 ) → ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) 𝑈 = ( 𝑁 ‘ { 𝑣 } ) )
8 ssrexv ⊢ ( ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ⊆ 𝑉 → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) 𝑈 = ( 𝑁 ‘ { 𝑣 } ) → ∃ 𝑣 ∈ 𝑉 𝑈 = ( 𝑁 ‘ { 𝑣 } ) ) )
9 4 7 8 mpsyl ⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝑈 ∈ 𝐴 ) → ∃ 𝑣 ∈ 𝑉 𝑈 = ( 𝑁 ‘ { 𝑣 } ) )