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 classLCDual
1 vk setvark
2 cvv classV
3 vw setvarw
4 clh classLHyp
5 1 cv setvark
6 5 4 cfv classLHyp⁡k
7 cld classLDual
8 cdvh classDVecH
9 5 8 cfv classDVecH⁡k
10 3 cv setvarw
11 10 9 cfv classDVecH⁡k⁡w
12 11 7 cfv classLDual⁡DVecH⁡k⁡w
13 cress class↾𝑠
14 vf setvarf
15 clfn classLFnl
16 11 15 cfv classLFnl⁡DVecH⁡k⁡w
17 coch classocH
18 5 17 cfv classocH⁡k
19 10 18 cfv classocH⁡k⁡w
20 clk classLKer
21 11 20 cfv classLKer⁡DVecH⁡k⁡w
22 14 cv setvarf
23 22 21 cfv classLKer⁡DVecH⁡k⁡w⁡f
24 23 19 cfv classocH⁡k⁡w⁡LKer⁡DVecH⁡k⁡w⁡f
25 24 19 cfv classocH⁡k⁡w⁡ocH⁡k⁡w⁡LKer⁡DVecH⁡k⁡w⁡f
26 25 23 wceq wffocH⁡k⁡w⁡ocH⁡k⁡w⁡LKer⁡DVecH⁡k⁡w⁡f=LKer⁡DVecH⁡k⁡w⁡f
27 26 14 16 crab classf∈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 classLDual⁡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 classw∈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 classk∈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 wffLCDual=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