dochsnkr2

Description: Kernel of the explicit functional G determined by a nonzero vector X . Compare the more general lshpkr . (Contributed by NM, 27-Oct-2014)

	Ref	Expression
Hypotheses	dochsnkr2.h	\|- H = ( LHyp ` K )
	dochsnkr2.o	\|- ._\|_ = ( ( ocH ` K ) ` W )
	dochsnkr2.u	\|- U = ( ( DVecH ` K ) ` W )
	dochsnkr2.v	\|- V = ( Base ` U )
	dochsnkr2.z	\|- .0. = ( 0g ` U )
	dochsnkr2.a	\|- .+ = ( +g ` U )
	dochsnkr2.t	\|- .x. = ( .s ` U )
	dochsnkr2.l	\|- L = ( LKer ` U )
	dochsnkr2.d	\|- D = ( Scalar ` U )
	dochsnkr2.r	\|- R = ( Base ` D )
	dochsnkr2.g	\|- G = ( v e. V \|-> ( iota_ k e. R E. w e. ( ._\|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) )
	dochsnkr2.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
	dochsnkr2.x	\|- ( ph -> X e. ( V \ { .0. } ) )
Assertion	dochsnkr2	\|- ( ph -> ( L ` G ) = ( ._\|_ ` { X } ) )

Proof

Step	Hyp	Ref	Expression
1		dochsnkr2.h	\|- H = ( LHyp ` K )
2		dochsnkr2.o	\|- ._\|_ = ( ( ocH ` K ) ` W )
3		dochsnkr2.u	\|- U = ( ( DVecH ` K ) ` W )
4		dochsnkr2.v	\|- V = ( Base ` U )
5		dochsnkr2.z	\|- .0. = ( 0g ` U )
6		dochsnkr2.a	\|- .+ = ( +g ` U )
7		dochsnkr2.t	\|- .x. = ( .s ` U )
8		dochsnkr2.l	\|- L = ( LKer ` U )
9		dochsnkr2.d	\|- D = ( Scalar ` U )
10		dochsnkr2.r	\|- R = ( Base ` D )
11		dochsnkr2.g	\|- G = ( v e. V \|-> ( iota_ k e. R E. w e. ( ._\|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) )
12		dochsnkr2.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
13		dochsnkr2.x	\|- ( ph -> X e. ( V \ { .0. } ) )
14		eqid	\|- ( LSpan ` U ) = ( LSpan ` U )
15		eqid	\|- ( LSSum ` U ) = ( LSSum ` U )
16		eqid	\|- ( LSHyp ` U ) = ( LSHyp ` U )
17	1 3 12	dvhlvec	\|- ( ph -> U e. LVec )
18	1 2 3 4 5 16 12 13	dochsnshp	\|- ( ph -> ( ._\|_ ` { X } ) e. ( LSHyp ` U ) )
19	13	eldifad	\|- ( ph -> X e. V )
20	1 2 3 4 5 14 15 12 13	dochexmidat	\|- ( ph -> ( ( ._\|_ ` { X } ) ( LSSum ` U ) ( ( LSpan ` U ) ` { X } ) ) = V )
21	4 6 14 15 16 17 18 19 20 9 10 7 11 8	lshpkr	\|- ( ph -> ( L ` G ) = ( ._\|_ ` { X } ) )

Metamath Proof Explorer

Theorem dochsnkr2

Proof