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 ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 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 )