Metamath Proof Explorer

Theorem elspansn

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

Ref Expression
Assertion elspansn ⊢ A ∈ ℋ → B ∈ span ⁡ A ↔ ∃ x ∈ ℂ B = x ⋅ ℎ A

Proof

Step Hyp Ref Expression
1 sneq ⊢ A = if A ∈ ℋ A 0 ℎ → A = if A ∈ ℋ A 0 ℎ
2 1 fveq2d ⊢ A = if A ∈ ℋ A 0 ℎ → span ⁡ A = span ⁡ if A ∈ ℋ A 0 ℎ
3 2 eleq2d ⊢ A = if A ∈ ℋ A 0 ℎ → B ∈ span ⁡ A ↔ B ∈ span ⁡ if A ∈ ℋ A 0 ℎ
4 oveq2 ⊢ A = if A ∈ ℋ A 0 ℎ → x ⋅ ℎ A = x ⋅ ℎ if A ∈ ℋ A 0 ℎ
5 4 eqeq2d ⊢ A = if A ∈ ℋ A 0 ℎ → B = x ⋅ ℎ A ↔ B = x ⋅ ℎ if A ∈ ℋ A 0 ℎ
6 5 rexbidv ⊢ A = if A ∈ ℋ A 0 ℎ → ∃ x ∈ ℂ B = x ⋅ ℎ A ↔ ∃ x ∈ ℂ B = x ⋅ ℎ if A ∈ ℋ A 0 ℎ
7 3 6 bibi12d ⊢ A = if A ∈ ℋ A 0 ℎ → B ∈ span ⁡ A ↔ ∃ x ∈ ℂ B = x ⋅ ℎ A ↔ B ∈ span ⁡ if A ∈ ℋ A 0 ℎ ↔ ∃ x ∈ ℂ B = x ⋅ ℎ if A ∈ ℋ A 0 ℎ
8 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
9 8 elspansni ⊢ B ∈ span ⁡ if A ∈ ℋ A 0 ℎ ↔ ∃ x ∈ ℂ B = x ⋅ ℎ if A ∈ ℋ A 0 ℎ
10 7 9 dedth ⊢ A ∈ ℋ → B ∈ span ⁡ A ↔ ∃ x ∈ ℂ B = x ⋅ ℎ A