Metamath Proof Explorer


Theorem dia1dim2

Description: Two expressions for a 1-dimensional subspace of partial vector space A (when F is a nonzero vector i.e. non-identity translation). (Contributed by NM, 15-Jan-2014) (Revised by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses dia1dim2.h H = LHyp K
dia1dim2.t T = LTrn K W
dia1dim2.r R = trL K W
dva1dim2.u U = DVecA K W
dia1dim2.i I = DIsoA K W
dva1dim2.n N = LSpan U
Assertion dia1dim2 K HL W H F T I R F = N F

Proof

Step Hyp Ref Expression
1 dia1dim2.h H = LHyp K
2 dia1dim2.t T = LTrn K W
3 dia1dim2.r R = trL K W
4 dva1dim2.u U = DVecA K W
5 dia1dim2.i I = DIsoA K W
6 dva1dim2.n N = LSpan U
7 eqid TEndo K W = TEndo K W
8 eqid Scalar U = Scalar U
9 eqid Base Scalar U = Base Scalar U
10 1 7 4 8 9 dvabase K HL W H Base Scalar U = TEndo K W
11 10 adantr K HL W H F T Base Scalar U = TEndo K W
12 11 rexeqdv K HL W H F T s Base Scalar U g = s U F s TEndo K W g = s U F
13 eqid U = U
14 1 2 7 4 13 dvavsca K HL W H s TEndo K W F T s U F = s F
15 14 anass1rs K HL W H F T s TEndo K W s U F = s F
16 15 eqeq2d K HL W H F T s TEndo K W g = s U F g = s F
17 16 rexbidva K HL W H F T s TEndo K W g = s U F s TEndo K W g = s F
18 12 17 bitrd K HL W H F T s Base Scalar U g = s U F s TEndo K W g = s F
19 18 abbidv K HL W H F T g | s Base Scalar U g = s U F = g | s TEndo K W g = s F
20 1 4 dvalvec K HL W H U LVec
21 20 adantr K HL W H F T U LVec
22 lveclmod U LVec U LMod
23 21 22 syl K HL W H F T U LMod
24 simpr K HL W H F T F T
25 eqid Base U = Base U
26 1 2 4 25 dvavbase K HL W H Base U = T
27 26 adantr K HL W H F T Base U = T
28 24 27 eleqtrrd K HL W H F T F Base U
29 8 9 25 13 6 lspsn U LMod F Base U N F = g | s Base Scalar U g = s U F
30 23 28 29 syl2anc K HL W H F T N F = g | s Base Scalar U g = s U F
31 1 2 3 7 5 dia1dim K HL W H F T I R F = g | s TEndo K W g = s F
32 19 30 31 3eqtr4rd K HL W H F T I R F = N F