# 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}=\mathrm{LHyp}\left({K}\right)$
lcdvbase.o
lcdvbase.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
lcdvbase.v ${⊢}{V}={\mathrm{Base}}_{{C}}$
lcdvbase.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
lcdvbase.f ${⊢}{F}=\mathrm{LFnl}\left({U}\right)$
lcdvbase.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
lcdvbase.b
lcdvbase.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
Assertion lcdvbase ${⊢}{\phi }\to {V}={B}$

### Proof

Step Hyp Ref Expression
1 lcdvbase.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 lcdvbase.o
3 lcdvbase.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
4 lcdvbase.v ${⊢}{V}={\mathrm{Base}}_{{C}}$
5 lcdvbase.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
6 lcdvbase.f ${⊢}{F}=\mathrm{LFnl}\left({U}\right)$
7 lcdvbase.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
8 lcdvbase.b
9 lcdvbase.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
10 eqid ${⊢}\mathrm{LDual}\left({U}\right)=\mathrm{LDual}\left({U}\right)$
11 1 2 3 5 6 7 10 9 8 lcdval2 ${⊢}{\phi }\to {C}=\mathrm{LDual}\left({U}\right){↾}_{𝑠}{B}$
12 11 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{C}}={\mathrm{Base}}_{\left(\mathrm{LDual}\left({U}\right){↾}_{𝑠}{B}\right)}$
13 4 12 syl5eq ${⊢}{\phi }\to {V}={\mathrm{Base}}_{\left(\mathrm{LDual}\left({U}\right){↾}_{𝑠}{B}\right)}$
14 ssrab2
15 8 14 eqsstri ${⊢}{B}\subseteq {F}$
16 eqid ${⊢}{\mathrm{Base}}_{\mathrm{LDual}\left({U}\right)}={\mathrm{Base}}_{\mathrm{LDual}\left({U}\right)}$
17 1 5 9 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
18 6 10 16 17 ldualvbase ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{LDual}\left({U}\right)}={F}$
19 15 18 sseqtrrid ${⊢}{\phi }\to {B}\subseteq {\mathrm{Base}}_{\mathrm{LDual}\left({U}\right)}$
20 eqid ${⊢}\mathrm{LDual}\left({U}\right){↾}_{𝑠}{B}=\mathrm{LDual}\left({U}\right){↾}_{𝑠}{B}$
21 20 16 ressbas2 ${⊢}{B}\subseteq {\mathrm{Base}}_{\mathrm{LDual}\left({U}\right)}\to {B}={\mathrm{Base}}_{\left(\mathrm{LDual}\left({U}\right){↾}_{𝑠}{B}\right)}$
22 19 21 syl ${⊢}{\phi }\to {B}={\mathrm{Base}}_{\left(\mathrm{LDual}\left({U}\right){↾}_{𝑠}{B}\right)}$
23 13 22 eqtr4d ${⊢}{\phi }\to {V}={B}$