Theorem dih1dimb

Description: Two expressions for a 1-dimensional subspace of vector space H (when F is a nonzero vector i.e. non-identity translation). (Contributed by NM, 27-Apr-2014)

	Ref	Expression
Hypotheses	dih1dimb.b	|- B = ( Base ` K )
	dih1dimb.h	|- H = ( LHyp ` K )
	dih1dimb.t	|- T = ( ( LTrn ` K ) ` W )
	dih1dimb.r	|- R = ( ( trL ` K ) ` W )
	dih1dimb.o	|- O = ( h e. T |-> ( _I |` B ) )
	dih1dimb.u	|- U = ( ( DVecH ` K ) ` W )
	dih1dimb.i	|- I = ( ( DIsoH ` K ) ` W )
	dih1dimb.n	|- N = ( LSpan ` U )
Assertion	dih1dimb	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = ( N ` { <. F , O >. } ) )

Proof

Step	Hyp	Ref	Expression
1		dih1dimb.b	|- B = ( Base ` K )
2		dih1dimb.h	|- H = ( LHyp ` K )
3		dih1dimb.t	|- T = ( ( LTrn ` K ) ` W )
4		dih1dimb.r	|- R = ( ( trL ` K ) ` W )
5		dih1dimb.o	|- O = ( h e. T |-> ( _I |` B ) )
6		dih1dimb.u	|- U = ( ( DVecH ` K ) ` W )
7		dih1dimb.i	|- I = ( ( DIsoH ` K ) ` W )
8		dih1dimb.n	|- N = ( LSpan ` U )
9		simpl	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( K e. HL /\ W e. H ) )
10	1 2 3 4	trlcl	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) e. B )
11		eqid	|- ( le ` K ) = ( le ` K )
12	11 2 3 4	trlle	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) ( le ` K ) W )
13		eqid	|- ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )
14	1 11 2 7 13	dihvalb	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( R ` F ) e. B /\ ( R ` F ) ( le ` K ) W ) ) -> ( I ` ( R ` F ) ) = ( ( ( DIsoB ` K ) ` W ) ` ( R ` F ) ) )
15	9 10 12 14	syl12anc	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = ( ( ( DIsoB ` K ) ` W ) ` ( R ` F ) ) )
16	1 2 3 4 5 6 13 8	dib1dim2	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( ( DIsoB ` K ) ` W ) ` ( R ` F ) ) = ( N ` { <. F , O >. } ) )
17	15 16	eqtrd	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = ( N ` { <. F , O >. } ) )