Theorem lcdlmod

Description: The dual vector space of functionals with closed kernels is a left module. (Contributed by NM, 13-Mar-2015)

	Ref	Expression
Hypotheses	lcdlmod.h	|- H = ( LHyp ` K )
	lcdlmod.c	|- C = ( ( LCDual ` K ) ` W )
	lcdlmod.k	|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion	lcdlmod	|- ( ph -> C e. LMod )

Proof

Step	Hyp	Ref	Expression
1		lcdlmod.h	|- H = ( LHyp ` K )
2		lcdlmod.c	|- C = ( ( LCDual ` K ) ` W )
3		lcdlmod.k	|- ( ph -> ( K e. HL /\ W e. H ) )
4	1 2 3	lcdlvec	|- ( ph -> C e. LVec )
5		lveclmod	|- ( C e. LVec -> C e. LMod )
6	4 5	syl	|- ( ph -> C e. LMod )