Metamath Proof Explorer

Theorem ellspsn

Description: Member of span of the singleton of a vector. ( elspansn analog.) (Contributed by NM, 22-Feb-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lspsn.f ⊢ F = Scalar ⁡ W
lspsn.k ⊢ K = Base F
lspsn.v ⊢ V = Base W
lspsn.t ⊢ · ˙ = ⋅ W
lspsn.n ⊢ N = LSpan ⁡ W
Assertion ellspsn ⊢ W ∈ LMod ∧ X ∈ V → U ∈ N ⁡ X ↔ ∃ k ∈ K U = k · ˙ X

Proof

Step Hyp Ref Expression
1 lspsn.f ⊢ F = Scalar ⁡ W
2 lspsn.k ⊢ K = Base F
3 lspsn.v ⊢ V = Base W
4 lspsn.t ⊢ · ˙ = ⋅ W
5 lspsn.n ⊢ N = LSpan ⁡ W
6 1 2 3 4 5 lspsn ⊢ W ∈ LMod ∧ X ∈ V → N ⁡ X = v | ∃ k ∈ K v = k · ˙ X
7 6 eleq2d ⊢ W ∈ LMod ∧ X ∈ V → U ∈ N ⁡ X ↔ U ∈ v | ∃ k ∈ K v = k · ˙ X
8 id ⊢ U = k · ˙ X → U = k · ˙ X
9 ovex ⊢ k · ˙ X ∈ V
10 8 9 eqeltrdi ⊢ U = k · ˙ X → U ∈ V
11 10 rexlimivw ⊢ ∃ k ∈ K U = k · ˙ X → U ∈ V
12 eqeq1 ⊢ v = U → v = k · ˙ X ↔ U = k · ˙ X
13 12 rexbidv ⊢ v = U → ∃ k ∈ K v = k · ˙ X ↔ ∃ k ∈ K U = k · ˙ X
14 11 13 elab3 ⊢ U ∈ v | ∃ k ∈ K v = k · ˙ X ↔ ∃ k ∈ K U = k · ˙ X
15 7 14 bitrdi ⊢ W ∈ LMod ∧ X ∈ V → U ∈ N ⁡ X ↔ ∃ k ∈ K U = k · ˙ X