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 𝐴 ∈ ℋ
Assertion elspansni ( 𝐵 ∈ ( span ‘ { 𝐴 } ) ↔ ∃ 𝑥 ∈ ℂ 𝐵 = ( 𝑥 · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 spansn.1 𝐴 ∈ ℋ
2 1 spansni ( span ‘ { 𝐴 } ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) )
3 2 eleq2i ( 𝐵 ∈ ( span ‘ { 𝐴 } ) ↔ 𝐵 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) )
4 1 h1de2ci ( 𝐵 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) ↔ ∃ 𝑥 ∈ ℂ 𝐵 = ( 𝑥 · 𝐴 ) )
5 3 4 bitri ( 𝐵 ∈ ( span ‘ { 𝐴 } ) ↔ ∃ 𝑥 ∈ ℂ 𝐵 = ( 𝑥 · 𝐴 ) )