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 e. HL /\ W e. H ) /\ F e. T ) -> F e. ( 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 e. HL /\ W e. H ) -> ( ( DVecA ` K ) ` W ) e. LVec )
7		lveclmod	|- ( ( ( DVecA ` K ) ` W ) e. LVec -> ( ( DVecA ` K ) ` W ) e. LMod )
8	6 7	syl	|- ( ( K e. HL /\ W e. H ) -> ( ( DVecA ` K ) ` W ) e. LMod )
9	8	adantr	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( DVecA ` K ) ` W ) e. LMod )
10		eqid	|- ( Base ` ( ( DVecA ` K ) ` W ) ) = ( Base ` ( ( DVecA ` K ) ` W ) )
11	1 2 5 10	dvavbase	|- ( ( K e. HL /\ W e. H ) -> ( Base ` ( ( DVecA ` K ) ` W ) ) = T )
12	11	eleq2d	|- ( ( K e. HL /\ W e. H ) -> ( F e. ( Base ` ( ( DVecA ` K ) ` W ) ) <-> F e. T ) )
13	12	biimpar	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F e. ( Base ` ( ( DVecA ` K ) ` W ) ) )
14		eqid	|- ( LSpan ` ( ( DVecA ` K ) ` W ) ) = ( LSpan ` ( ( DVecA ` K ) ` W ) )
15	10 14	lspsnid	|- ( ( ( ( DVecA ` K ) ` W ) e. LMod /\ F e. ( Base ` ( ( DVecA ` K ) ` W ) ) ) -> F e. ( ( LSpan ` ( ( DVecA ` K ) ` W ) ) ` { F } ) )
16	9 13 15	syl2anc	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F e. ( ( LSpan ` ( ( DVecA ` K ) ` W ) ) ` { F } ) )
17	1 2 3 5 4 14	dia1dim2	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = ( ( LSpan ` ( ( DVecA ` K ) ` W ) ) ` { F } ) )
18	16 17	eleqtrrd	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F e. ( I ` ( R ` F ) ) )