Theorem spansna

Description: The span of the singleton of a vector is an atom. (Contributed by NM, 18-Dec-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	spansna	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( span ‘ { 𝐴 } ) ∈ HAtoms )

Proof

Step	Hyp	Ref	Expression
1		spansn	⊢ ( 𝐴 ∈ ℋ → ( span ‘ { 𝐴 } ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( span ‘ { 𝐴 } ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) )
3		h1da	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) ∈ HAtoms )
4	2 3	eqeltrd	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( span ‘ { 𝐴 } ) ∈ HAtoms )