Theorem lcdlvec

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

	Ref	Expression
Hypotheses	lcdlmod.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcdlmod.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcdlmod.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	lcdlvec	⊢ ( 𝜑 → 𝐶 ∈ LVec )

Proof

Step	Hyp	Ref	Expression
1		lcdlmod.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcdlmod.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
3		lcdlmod.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
4		eqid	⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
5		eqid	⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
6		eqid	⊢ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
7		eqid	⊢ ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
8		eqid	⊢ ( LDual ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LDual ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
9	1 4 2 5 6 7 8 3	lcdval	⊢ ( 𝜑 → 𝐶 = ( ( LDual ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ↾s { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) } ) )
10	1 5 3	dvhlvec	⊢ ( 𝜑 → ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∈ LVec )
11	8 10	lduallvec	⊢ ( 𝜑 → ( LDual ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ LVec )
12		eqid	⊢ ( LSubSp ‘ ( LDual ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( LSubSp ‘ ( LDual ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
13		eqid	⊢ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) } = { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) }
14	1 5 4 6 7 8 12 13 3	lclkr	⊢ ( 𝜑 → { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) } ∈ ( LSubSp ‘ ( LDual ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
15		eqid	⊢ ( ( LDual ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ↾s { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) } ) = ( ( LDual ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ↾s { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) } )
16	15 12	lsslvec	⊢ ( ( ( LDual ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ LVec ∧ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) } ∈ ( LSubSp ‘ ( LDual ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → ( ( LDual ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ↾s { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) } ) ∈ LVec )
17	11 14 16	syl2anc	⊢ ( 𝜑 → ( ( LDual ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ↾s { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ 𝑓 ) } ) ∈ LVec )
18	9 17	eqeltrd	⊢ ( 𝜑 → 𝐶 ∈ LVec )