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

Metamath Proof Explorer

Theorem lsator0sp

Description: The span of a vector is either an atom or the zero subspace. (Contributed by NM, 15-Mar-2015)

Ref Expression
Hypotheses lsator0sp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lsator0sp.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lsator0sp.o ⊢ 0 = ( 0g ‘ 𝑊 )
lsator0sp.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
isator0sp.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
isator0sp.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion lsator0sp ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ∨ ( 𝑁 ‘ { 𝑋 } ) = { 0 } ) )

Proof

Step Hyp Ref Expression
1 lsator0sp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lsator0sp.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 lsator0sp.o ⊢ 0 = ( 0g ‘ 𝑊 )
4 lsator0sp.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
5 isator0sp.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
6 isator0sp.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
7 1 2 3 4 5 6 lsatspn0 ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ↔ 𝑋 ≠ 0 ) )
8 7 biimprd ⊢ ( 𝜑 → ( 𝑋 ≠ 0 → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ) )
9 8 necon1bd ⊢ ( 𝜑 → ( ¬ ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 → 𝑋 = 0 ) )
10 1 3 2 lspsneq0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) = { 0 } ↔ 𝑋 = 0 ) )
11 5 6 10 syl2anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = { 0 } ↔ 𝑋 = 0 ) )
12 9 11 sylibrd ⊢ ( 𝜑 → ( ¬ ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 → ( 𝑁 ‘ { 𝑋 } ) = { 0 } ) )
13 12 orrd ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ∨ ( 𝑁 ‘ { 𝑋 } ) = { 0 } ) )