dochflcl

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

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

Proof

Step	Hyp	Ref	Expression
1		dochflcl.h	\|- H = ( LHyp ` K )
2		dochflcl.o	\|- ._\|_ = ( ( ocH ` K ) ` W )
3		dochflcl.u	\|- U = ( ( DVecH ` K ) ` W )
4		dochflcl.v	\|- V = ( Base ` U )
5		dochflcl.z	\|- .0. = ( 0g ` U )
6		dochflcl.a	\|- .+ = ( +g ` U )
7		dochflcl.t	\|- .x. = ( .s ` U )
8		dochflcl.f	\|- F = ( LFnl ` U )
9		dochflcl.d	\|- D = ( Scalar ` U )
10		dochflcl.r	\|- R = ( Base ` D )
11		dochflcl.g	\|- G = ( v e. V \|-> ( iota_ k e. R E. w e. ( ._\|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) )
12		dochflcl.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
13		dochflcl.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	lshpkrcl	\|- ( ph -> G e. F )

Metamath Proof Explorer

Theorem dochflcl

Proof