# Metamath Proof Explorer

## Theorem lcdsbase

Description: Base set of scalar ring for the closed kernel dual of a vector space. (Contributed by NM, 18-Mar-2015)

Ref Expression
Hypotheses lcdsbase.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
lcdsbase.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
lcdsbase.f ${⊢}{F}=\mathrm{Scalar}\left({U}\right)$
lcdsbase.l ${⊢}{L}={\mathrm{Base}}_{{F}}$
lcdsbase.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
lcdsbase.s ${⊢}{S}=\mathrm{Scalar}\left({C}\right)$
lcdsbase.r ${⊢}{R}={\mathrm{Base}}_{{S}}$
lcdsbase.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
Assertion lcdsbase ${⊢}{\phi }\to {R}={L}$

### Proof

Step Hyp Ref Expression
1 lcdsbase.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 lcdsbase.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 lcdsbase.f ${⊢}{F}=\mathrm{Scalar}\left({U}\right)$
4 lcdsbase.l ${⊢}{L}={\mathrm{Base}}_{{F}}$
5 lcdsbase.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
6 lcdsbase.s ${⊢}{S}=\mathrm{Scalar}\left({C}\right)$
7 lcdsbase.r ${⊢}{R}={\mathrm{Base}}_{{S}}$
8 lcdsbase.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
9 eqid ${⊢}{opp}_{r}\left({F}\right)={opp}_{r}\left({F}\right)$
10 1 2 3 9 5 6 8 lcdsca ${⊢}{\phi }\to {S}={opp}_{r}\left({F}\right)$
11 10 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{opp}_{r}\left({F}\right)}$
12 9 4 opprbas ${⊢}{L}={\mathrm{Base}}_{{opp}_{r}\left({F}\right)}$
13 11 7 12 3eqtr4g ${⊢}{\phi }\to {R}={L}$