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 } ) )