Theorem elspansn

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

	Ref	Expression
Assertion	elspansn	⊢ ( 𝐴 ∈ ℋ → ( 𝐵 ∈ ( span ‘ { 𝐴 } ) ↔ ∃ 𝑥 ∈ ℂ 𝐵 = ( 𝑥 ·ℎ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sneq	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → { 𝐴 } = { if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) } )
2	1	fveq2d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( span ‘ { 𝐴 } ) = ( span ‘ { if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) } ) )
3	2	eleq2d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( 𝐵 ∈ ( span ‘ { 𝐴 } ) ↔ 𝐵 ∈ ( span ‘ { if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) } ) ) )
4		oveq2	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( 𝑥 ·ℎ 𝐴 ) = ( 𝑥 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) )
5	4	eqeq2d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( 𝐵 = ( 𝑥 ·ℎ 𝐴 ) ↔ 𝐵 = ( 𝑥 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ) )
6	5	rexbidv	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ∃ 𝑥 ∈ ℂ 𝐵 = ( 𝑥 ·ℎ 𝐴 ) ↔ ∃ 𝑥 ∈ ℂ 𝐵 = ( 𝑥 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ) )
7	3 6	bibi12d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( 𝐵 ∈ ( span ‘ { 𝐴 } ) ↔ ∃ 𝑥 ∈ ℂ 𝐵 = ( 𝑥 ·ℎ 𝐴 ) ) ↔ ( 𝐵 ∈ ( span ‘ { if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) } ) ↔ ∃ 𝑥 ∈ ℂ 𝐵 = ( 𝑥 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ) ) )
8		ifhvhv0	⊢ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ℋ
9	8	elspansni	⊢ ( 𝐵 ∈ ( span ‘ { if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) } ) ↔ ∃ 𝑥 ∈ ℂ 𝐵 = ( 𝑥 ·ℎ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) )
10	7 9	dedth	⊢ ( 𝐴 ∈ ℋ → ( 𝐵 ∈ ( span ‘ { 𝐴 } ) ↔ ∃ 𝑥 ∈ ℂ 𝐵 = ( 𝑥 ·ℎ 𝐴 ) ) )