Metamath Proof Explorer

Theorem elspansni

Description: Membership in the span of a singleton. (Contributed by NM, 3-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypothesis spansn.1 ⊢ A ∈ ℋ
Assertion elspansni ⊢ B ∈ span ⁡ A ↔ ∃ x ∈ ℂ B = x ⋅ ℎ A

Proof

Step Hyp Ref Expression
1 spansn.1 ⊢ A ∈ ℋ
2 1 spansni ⊢ span ⁡ A = ⊥ ⁡ ⊥ ⁡ A
3 2 eleq2i ⊢ B ∈ span ⁡ A ↔ B ∈ ⊥ ⁡ ⊥ ⁡ A
4 1 h1de2ci ⊢ B ∈ ⊥ ⁡ ⊥ ⁡ A ↔ ∃ x ∈ ℂ B = x ⋅ ℎ A
5 3 4 bitri ⊢ B ∈ span ⁡ A ↔ ∃ x ∈ ℂ B = x ⋅ ℎ A