Metamath Proof Explorer


Theorem dia1dim

Description: Two expressions for the 1-dimensional subspaces of partial vector space A (when F is a nonzero vector i.e. non-identity translation). Remark after Lemma L in Crawley p. 120 line 21. (Contributed by NM, 15-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses dia1dim.h H=LHypK
dia1dim.t T=LTrnKW
dia1dim.r R=trLKW
dia1dim.e E=TEndoKW
dia1dim.i I=DIsoAKW
Assertion dia1dim KHLWHFTIRF=g|sEg=sF

Proof

Step Hyp Ref Expression
1 dia1dim.h H=LHypK
2 dia1dim.t T=LTrnKW
3 dia1dim.r R=trLKW
4 dia1dim.e E=TEndoKW
5 dia1dim.i I=DIsoAKW
6 simpl KHLWHFTKHLWH
7 eqid BaseK=BaseK
8 7 1 2 3 trlcl KHLWHFTRFBaseK
9 eqid K=K
10 9 1 2 3 trlle KHLWHFTRFKW
11 7 9 1 2 3 5 diaval KHLWHRFBaseKRFKWIRF=gT|RgKRF
12 6 8 10 11 syl12anc KHLWHFTIRF=gT|RgKRF
13 9 1 2 3 4 dva1dim KHLWHFTg|sEg=sF=gT|RgKRF
14 12 13 eqtr4d KHLWHFTIRF=g|sEg=sF