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

Metamath Proof Explorer

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 } ) 𝑈 = ( 𝑁 ‘ { 𝑥 } ) ) )