Metamath Proof Explorer


Theorem lspprel

Description: Member of the span of a pair of vectors. (Contributed by NM, 10-Apr-2015)

Ref Expression
Hypotheses lsppr.v V = Base W
lsppr.a + ˙ = + W
lsppr.f F = Scalar W
lsppr.k K = Base F
lsppr.t · ˙ = W
lsppr.n N = LSpan W
lsppr.w φ W LMod
lsppr.x φ X V
lsppr.y φ Y V
Assertion lspprel φ Z N X Y k K l K Z = k · ˙ X + ˙ l · ˙ Y

Proof

Step Hyp Ref Expression
1 lsppr.v V = Base W
2 lsppr.a + ˙ = + W
3 lsppr.f F = Scalar W
4 lsppr.k K = Base F
5 lsppr.t · ˙ = W
6 lsppr.n N = LSpan W
7 lsppr.w φ W LMod
8 lsppr.x φ X V
9 lsppr.y φ Y V
10 1 2 3 4 5 6 7 8 9 lsppr φ N X Y = v | k K l K v = k · ˙ X + ˙ l · ˙ Y
11 10 eleq2d φ Z N X Y Z v | k K l K v = k · ˙ X + ˙ l · ˙ Y
12 id Z = k · ˙ X + ˙ l · ˙ Y Z = k · ˙ X + ˙ l · ˙ Y
13 ovex k · ˙ X + ˙ l · ˙ Y V
14 12 13 eqeltrdi Z = k · ˙ X + ˙ l · ˙ Y Z V
15 14 rexlimivw l K Z = k · ˙ X + ˙ l · ˙ Y Z V
16 15 rexlimivw k K l K Z = k · ˙ X + ˙ l · ˙ Y Z V
17 eqeq1 v = Z v = k · ˙ X + ˙ l · ˙ Y Z = k · ˙ X + ˙ l · ˙ Y
18 17 2rexbidv v = Z k K l K v = k · ˙ X + ˙ l · ˙ Y k K l K Z = k · ˙ X + ˙ l · ˙ Y
19 16 18 elab3 Z v | k K l K v = k · ˙ X + ˙ l · ˙ Y k K l K Z = k · ˙ X + ˙ l · ˙ Y
20 11 19 bitrdi φ Z N X Y k K l K Z = k · ˙ X + ˙ l · ˙ Y