Theorem islsat

Description: The predicate "is a 1-dim subspace (atom)" (of a left module or left vector space). (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	islsat	⊢ ( 𝑊 ∈ 𝑋 → ( 𝑈 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝑈 = ( 𝑁 ‘ { 𝑥 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lsatset.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lsatset.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		lsatset.z	⊢ 0 = ( 0g ‘ 𝑊 )
4		lsatset.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
5	1 2 3 4	lsatset	⊢ ( 𝑊 ∈ 𝑋 → 𝐴 = ran ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑥 } ) ) )
6	5	eleq2d	⊢ ( 𝑊 ∈ 𝑋 → ( 𝑈 ∈ 𝐴 ↔ 𝑈 ∈ ran ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑥 } ) ) ) )
7		eqid	⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑥 } ) ) = ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑥 } ) )
8		fvex	⊢ ( 𝑁 ‘ { 𝑥 } ) ∈ V
9	7 8	elrnmpti	⊢ ( 𝑈 ∈ ran ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑁 ‘ { 𝑥 } ) ) ↔ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝑈 = ( 𝑁 ‘ { 𝑥 } ) )
10	6 9	bitrdi	⊢ ( 𝑊 ∈ 𝑋 → ( 𝑈 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝑈 = ( 𝑁 ‘ { 𝑥 } ) ) )