Theorem lcdval2

Description: Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015)

	Ref	Expression
Hypotheses	lcdval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcdval.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lcdval.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcdval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcdval.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lcdval.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcdval.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lcdval.k	⊢ ( 𝜑 → ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) )
	lcdval2.b	⊢ 𝐵 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
Assertion	lcdval2	⊢ ( 𝜑 → 𝐶 = ( 𝐷 ↾s 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		lcdval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcdval.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcdval.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
4		lcdval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		lcdval.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6		lcdval.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
7		lcdval.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
8		lcdval.k	⊢ ( 𝜑 → ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) )
9		lcdval2.b	⊢ 𝐵 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
10	1 2 3 4 5 6 7 8	lcdval	⊢ ( 𝜑 → 𝐶 = ( 𝐷 ↾s { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } ) )
11	9	oveq2i	⊢ ( 𝐷 ↾s 𝐵 ) = ( 𝐷 ↾s { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } )
12	10 11	eqtr4di	⊢ ( 𝜑 → 𝐶 = ( 𝐷 ↾s 𝐵 ) )