Definition df-lcdual

Description: Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn . TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd using ( Base( ( LCDualK )W ) ) . (Contributed by NM, 13-Mar-2015)

	Ref	Expression
Assertion	df-lcdual	⊢ LCDual = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( ( LDual ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↾s { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∣ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clcd	⊢ LCDual
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vw	⊢ 𝑤
4		clh	⊢ LHyp
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( LHyp ‘ 𝑘 )
7		cld	⊢ LDual
8		cdvh	⊢ DVecH
9	5 8	cfv	⊢ ( DVecH ‘ 𝑘 )
10	3	cv	⊢ 𝑤
11	10 9	cfv	⊢ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 )
12	11 7	cfv	⊢ ( LDual ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) )
13		cress	⊢ ↾s
14		vf	⊢ 𝑓
15		clfn	⊢ LFnl
16	11 15	cfv	⊢ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) )
17		coch	⊢ ocH
18	5 17	cfv	⊢ ( ocH ‘ 𝑘 )
19	10 18	cfv	⊢ ( ( ocH ‘ 𝑘 ) ‘ 𝑤 )
20		clk	⊢ LKer
21	11 20	cfv	⊢ ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) )
22	14	cv	⊢ 𝑓
23	22 21	cfv	⊢ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 )
24	23 19	cfv	⊢ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) )
25	24 19	cfv	⊢ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) )
26	25 23	wceq	⊢ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 )
27	26 14 16	crab	⊢ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∣ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) }
28	12 27 13	co	⊢ ( ( LDual ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↾s { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∣ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) } )
29	3 6 28	cmpt	⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( ( LDual ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↾s { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∣ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) } ) )
30	1 2 29	cmpt	⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( ( LDual ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↾s { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∣ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) } ) ) )
31	0 30	wceq	⊢ LCDual = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( ( LDual ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↾s { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∣ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) } ) ) )