Metamath Proof Explorer


Theorem lcdval2

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

Ref Expression
Hypotheses lcdval.h H = LHyp K
lcdval.o ˙ = ocH K W
lcdval.c C = LCDual K W
lcdval.u U = DVecH K W
lcdval.f F = LFnl U
lcdval.l L = LKer U
lcdval.d D = LDual U
lcdval.k φ K X W H
lcdval2.b B = f F | ˙ ˙ L f = L f
Assertion lcdval2 φ C = D 𝑠 B

Proof

Step Hyp Ref Expression
1 lcdval.h H = LHyp K
2 lcdval.o ˙ = ocH K W
3 lcdval.c C = LCDual K W
4 lcdval.u U = DVecH K W
5 lcdval.f F = LFnl U
6 lcdval.l L = LKer U
7 lcdval.d D = LDual U
8 lcdval.k φ K X W H
9 lcdval2.b B = f F | ˙ ˙ L f = L f
10 1 2 3 4 5 6 7 8 lcdval φ C = D 𝑠 f F | ˙ ˙ L f = L f
11 9 oveq2i D 𝑠 B = D 𝑠 f F | ˙ ˙ L f = L f
12 10 11 eqtr4di φ C = D 𝑠 B