Metamath Proof Explorer

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 = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ LDual ⁡ DVecH ⁡ k ⁡ w ↾ 𝑠 f ∈ LFnl ⁡ DVecH ⁡ k ⁡ w | ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f = LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f

Detailed syntax breakdown

Step Hyp Ref Expression
0 clcd class LCDual
1 vk setvar k
2 cvv class V
3 vw setvar w
4 clh class LHyp
5 1 cv setvar k
6 5 4 cfv class LHyp ⁡ k
7 cld class LDual
8 cdvh class DVecH
9 5 8 cfv class DVecH ⁡ k
10 3 cv setvar w
11 10 9 cfv class DVecH ⁡ k ⁡ w
12 11 7 cfv class LDual ⁡ DVecH ⁡ k ⁡ w
13 cress class ↾ 𝑠
14 vf setvar f
15 clfn class LFnl
16 11 15 cfv class LFnl ⁡ DVecH ⁡ k ⁡ w
17 coch class ocH
18 5 17 cfv class ocH ⁡ k
19 10 18 cfv class ocH ⁡ k ⁡ w
20 clk class LKer
21 11 20 cfv class LKer ⁡ DVecH ⁡ k ⁡ w
22 14 cv setvar f
23 22 21 cfv class LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f
24 23 19 cfv class ocH ⁡ k ⁡ w ⁡ LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f
25 24 19 cfv class ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f
26 25 23 wceq wff ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f = LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f
27 26 14 16 crab class f ∈ LFnl ⁡ DVecH ⁡ k ⁡ w | ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f = LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f
28 12 27 13 co class LDual ⁡ DVecH ⁡ k ⁡ w ↾ 𝑠 f ∈ LFnl ⁡ DVecH ⁡ k ⁡ w | ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f = LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f
29 3 6 28 cmpt class w ∈ LHyp ⁡ k ⟼ LDual ⁡ DVecH ⁡ k ⁡ w ↾ 𝑠 f ∈ LFnl ⁡ DVecH ⁡ k ⁡ w | ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f = LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f
30 1 2 29 cmpt class k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ LDual ⁡ DVecH ⁡ k ⁡ w ↾ 𝑠 f ∈ LFnl ⁡ DVecH ⁡ k ⁡ w | ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f = LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f
31 0 30 wceq wff LCDual = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ LDual ⁡ DVecH ⁡ k ⁡ w ↾ 𝑠 f ∈ LFnl ⁡ DVecH ⁡ k ⁡ w | ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f = LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f