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	⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝑈 ∈ 𝐴 ) → ∃ 𝑣 ∈ 𝑉 𝑈 = ( 𝑁 ‘ { 𝑣 } ) )