Theorem hvmapidN

Description: The value of the vector to functional map, at the vector, is one. (Contributed by NM, 23-Mar-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hvmapid.h	|- H = ( LHyp ` K )
	hvmapid.u	|- U = ( ( DVecH ` K ) ` W )
	hvmapid.v	|- V = ( Base ` U )
	hvmapid.z	|- .0. = ( 0g ` U )
	hvmapid.s	|- S = ( Scalar ` U )
	hvmapid.i	|- .1. = ( 1r ` S )
	hvmapid.m	|- M = ( ( HVMap ` K ) ` W )
	hvmapid.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hvmapid.x	|- ( ph -> X e. ( V \ { .0. } ) )
Assertion	hvmapidN	|- ( ph -> ( ( M ` X ) ` X ) = .1. )

Proof

Step	Hyp	Ref	Expression
1		hvmapid.h	|- H = ( LHyp ` K )
2		hvmapid.u	|- U = ( ( DVecH ` K ) ` W )
3		hvmapid.v	|- V = ( Base ` U )
4		hvmapid.z	|- .0. = ( 0g ` U )
5		hvmapid.s	|- S = ( Scalar ` U )
6		hvmapid.i	|- .1. = ( 1r ` S )
7		hvmapid.m	|- M = ( ( HVMap ` K ) ` W )
8		hvmapid.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		hvmapid.x	|- ( ph -> X e. ( V \ { .0. } ) )
10		eqid	|- ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
11		eqid	|- ( +g ` U ) = ( +g ` U )
12		eqid	|- ( .s ` U ) = ( .s ` U )
13		eqid	|- ( Base ` S ) = ( Base ` S )
14	1 2 10 3 11 12 4 5 13 7 8 9	hvmapval	|- ( ph -> ( M ` X ) = ( v e. V |-> ( iota_ j e. ( Base ` S ) E. t e. ( ( ( ocH ` K ) ` W ) ` { X } ) v = ( t ( +g ` U ) ( j ( .s ` U ) X ) ) ) ) )
15	14	fveq1d	|- ( ph -> ( ( M ` X ) ` X ) = ( ( v e. V |-> ( iota_ j e. ( Base ` S ) E. t e. ( ( ( ocH ` K ) ` W ) ` { X } ) v = ( t ( +g ` U ) ( j ( .s ` U ) X ) ) ) ) ` X ) )
16		eqid	|- ( v e. V |-> ( iota_ j e. ( Base ` S ) E. t e. ( ( ( ocH ` K ) ` W ) ` { X } ) v = ( t ( +g ` U ) ( j ( .s ` U ) X ) ) ) ) = ( v e. V |-> ( iota_ j e. ( Base ` S ) E. t e. ( ( ( ocH ` K ) ` W ) ` { X } ) v = ( t ( +g ` U ) ( j ( .s ` U ) X ) ) ) )
17	1 10 2 3 11 12 4 5 13 6 8 9 16	dochfl1	|- ( ph -> ( ( v e. V |-> ( iota_ j e. ( Base ` S ) E. t e. ( ( ( ocH ` K ) ` W ) ` { X } ) v = ( t ( +g ` U ) ( j ( .s ` U ) X ) ) ) ) ` X ) = .1. )
18	15 17	eqtrd	|- ( ph -> ( ( M ` X ) ` X ) = .1. )