Metamath Proof Explorer


Theorem dia1dimid

Description: A vector (translation) belongs to the 1-dim subspace it generates. (Contributed by NM, 8-Sep-2014)

Ref Expression
Hypotheses dia1dimid.h H = LHyp K
dia1dimid.t T = LTrn K W
dia1dimid.r R = trL K W
dia1dimid.i I = DIsoA K W
Assertion dia1dimid K HL W H F T F I R F

Proof

Step Hyp Ref Expression
1 dia1dimid.h H = LHyp K
2 dia1dimid.t T = LTrn K W
3 dia1dimid.r R = trL K W
4 dia1dimid.i I = DIsoA K W
5 eqid DVecA K W = DVecA K W
6 1 5 dvalvec K HL W H DVecA K W LVec
7 lveclmod DVecA K W LVec DVecA K W LMod
8 6 7 syl K HL W H DVecA K W LMod
9 8 adantr K HL W H F T DVecA K W LMod
10 eqid Base DVecA K W = Base DVecA K W
11 1 2 5 10 dvavbase K HL W H Base DVecA K W = T
12 11 eleq2d K HL W H F Base DVecA K W F T
13 12 biimpar K HL W H F T F Base DVecA K W
14 eqid LSpan DVecA K W = LSpan DVecA K W
15 10 14 lspsnid DVecA K W LMod F Base DVecA K W F LSpan DVecA K W F
16 9 13 15 syl2anc K HL W H F T F LSpan DVecA K W F
17 1 2 3 5 4 14 dia1dim2 K HL W H F T I R F = LSpan DVecA K W F
18 16 17 eleqtrrd K HL W H F T F I R F