Metamath Proof Explorer


Theorem lcdvbase

Description: Vector base set of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015)

Ref Expression
Hypotheses lcdvbase.h H = LHyp K
lcdvbase.o ˙ = ocH K W
lcdvbase.c C = LCDual K W
lcdvbase.v V = Base C
lcdvbase.u U = DVecH K W
lcdvbase.f F = LFnl U
lcdvbase.l L = LKer U
lcdvbase.b B = f F | ˙ ˙ L f = L f
lcdvbase.k φ K HL W H
Assertion lcdvbase φ V = B

Proof

Step Hyp Ref Expression
1 lcdvbase.h H = LHyp K
2 lcdvbase.o ˙ = ocH K W
3 lcdvbase.c C = LCDual K W
4 lcdvbase.v V = Base C
5 lcdvbase.u U = DVecH K W
6 lcdvbase.f F = LFnl U
7 lcdvbase.l L = LKer U
8 lcdvbase.b B = f F | ˙ ˙ L f = L f
9 lcdvbase.k φ K HL W H
10 eqid LDual U = LDual U
11 1 2 3 5 6 7 10 9 8 lcdval2 φ C = LDual U 𝑠 B
12 11 fveq2d φ Base C = Base LDual U 𝑠 B
13 4 12 syl5eq φ V = Base LDual U 𝑠 B
14 ssrab2 f F | ˙ ˙ L f = L f F
15 8 14 eqsstri B F
16 eqid Base LDual U = Base LDual U
17 1 5 9 dvhlmod φ U LMod
18 6 10 16 17 ldualvbase φ Base LDual U = F
19 15 18 sseqtrrid φ B Base LDual U
20 eqid LDual U 𝑠 B = LDual U 𝑠 B
21 20 16 ressbas2 B Base LDual U B = Base LDual U 𝑠 B
22 19 21 syl φ B = Base LDual U 𝑠 B
23 13 22 eqtr4d φ V = B