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