Metamath Proof Explorer


Theorem lspsnel

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 lspsnel 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