Theorem hvmaplkr

Description: Kernel of the vector to functional map. TODO: make this become lcfrlem11 . (Contributed by NM, 29-Mar-2015)

	Ref	Expression
Hypotheses	hvmaplkr.h	|- H = ( LHyp ` K )
	hvmaplkr.o	|- O = ( ( ocH ` K ) ` W )
	hvmaplkr.u	|- U = ( ( DVecH ` K ) ` W )
	hvmaplkr.v	|- V = ( Base ` U )
	hvmaplkr.z	|- .0. = ( 0g ` U )
	hvmaplkr.l	|- L = ( LKer ` U )
	hvmaplkr.m	|- M = ( ( HVMap ` K ) ` W )
	hvmaplkr.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hvmaplkr.x	|- ( ph -> X e. ( V \ { .0. } ) )
Assertion	hvmaplkr	|- ( ph -> ( L ` ( M ` X ) ) = ( O ` { X } ) )

Proof

Step	Hyp	Ref	Expression
1		hvmaplkr.h	|- H = ( LHyp ` K )
2		hvmaplkr.o	|- O = ( ( ocH ` K ) ` W )
3		hvmaplkr.u	|- U = ( ( DVecH ` K ) ` W )
4		hvmaplkr.v	|- V = ( Base ` U )
5		hvmaplkr.z	|- .0. = ( 0g ` U )
6		hvmaplkr.l	|- L = ( LKer ` U )
7		hvmaplkr.m	|- M = ( ( HVMap ` K ) ` W )
8		hvmaplkr.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		hvmaplkr.x	|- ( ph -> X e. ( V \ { .0. } ) )
10		eqid	|- ( +g ` U ) = ( +g ` U )
11		eqid	|- ( .s ` U ) = ( .s ` U )
12		eqid	|- ( Scalar ` U ) = ( Scalar ` U )
13		eqid	|- ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
14	1 3 2 4 10 11 5 12 13 7 8	hvmapfval	|- ( ph -> M = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. ( Base ` ( Scalar ` U ) ) E. t e. ( O ` { x } ) v = ( t ( +g ` U ) ( j ( .s ` U ) x ) ) ) ) ) )
15	14	fveq1d	|- ( ph -> ( M ` X ) = ( ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. ( Base ` ( Scalar ` U ) ) E. t e. ( O ` { x } ) v = ( t ( +g ` U ) ( j ( .s ` U ) x ) ) ) ) ) ` X ) )
16	15	fveq2d	|- ( ph -> ( L ` ( M ` X ) ) = ( L ` ( ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. ( Base ` ( Scalar ` U ) ) E. t e. ( O ` { x } ) v = ( t ( +g ` U ) ( j ( .s ` U ) x ) ) ) ) ) ` X ) ) )
17		eqid	|- ( LFnl ` U ) = ( LFnl ` U )
18		eqid	|- ( LDual ` U ) = ( LDual ` U )
19		eqid	|- ( 0g ` ( LDual ` U ) ) = ( 0g ` ( LDual ` U ) )
20		eqid	|- { f e. ( LFnl ` U ) | ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) } = { f e. ( LFnl ` U ) | ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) }
21		eqid	|- ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. ( Base ` ( Scalar ` U ) ) E. t e. ( O ` { x } ) v = ( t ( +g ` U ) ( j ( .s ` U ) x ) ) ) ) ) = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. ( Base ` ( Scalar ` U ) ) E. t e. ( O ` { x } ) v = ( t ( +g ` U ) ( j ( .s ` U ) x ) ) ) ) )
22	1 2 3 4 10 11 12 13 5 17 6 18 19 20 21 8 9	lcfrlem11	|- ( ph -> ( L ` ( ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. ( Base ` ( Scalar ` U ) ) E. t e. ( O ` { x } ) v = ( t ( +g ` U ) ( j ( .s ` U ) x ) ) ) ) ) ` X ) ) = ( O ` { X } ) )
23	16 22	eqtrd	|- ( ph -> ( L ` ( M ` X ) ) = ( O ` { X } ) )