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 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spansn | ⊢ ( 𝐴 ∈ ℋ → ( span ‘ { 𝐴 } ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) ) | |
2 | 1 | adantr | ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( span ‘ { 𝐴 } ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) ) |
3 | h1da | ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) ∈ HAtoms ) | |
4 | 2 3 | eqeltrd | ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( span ‘ { 𝐴 } ) ∈ HAtoms ) |