Metamath Proof Explorer

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 ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → span ⁡ A ∈ HAtoms

Proof

Step Hyp Ref Expression
1 spansn ⊢ A ∈ ℋ → span ⁡ A = ⊥ ⁡ ⊥ ⁡ A
2 1 adantr ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → span ⁡ A = ⊥ ⁡ ⊥ ⁡ A
3 h1da ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → ⊥ ⁡ ⊥ ⁡ A ∈ HAtoms
4 2 3 eqeltrd ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → span ⁡ A ∈ HAtoms