Metamath Proof Explorer

Theorem lcdvbasess

Description: The vector base set of the closed kernel dual space is a set of functionals. (Contributed by NM, 15-Mar-2015)

Ref Expression
Hypotheses lcdvbasess.h ⊢ H = LHyp ⁡ K
lcdvbasess.c ⊢ C = LCDual ⁡ K ⁡ W
lcdvbasess.v ⊢ V = Base C
lcdvbasess.u ⊢ U = DVecH ⁡ K ⁡ W
lcdvbasess.f ⊢ F = LFnl ⁡ U
lcdvbasess.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion lcdvbasess ⊢ φ → V ⊆ F

Proof

Step Hyp Ref Expression
1 lcdvbasess.h ⊢ H = LHyp ⁡ K
2 lcdvbasess.c ⊢ C = LCDual ⁡ K ⁡ W
3 lcdvbasess.v ⊢ V = Base C
4 lcdvbasess.u ⊢ U = DVecH ⁡ K ⁡ W
5 lcdvbasess.f ⊢ F = LFnl ⁡ U
6 lcdvbasess.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 eqid ⊢ ocH ⁡ K ⁡ W = ocH ⁡ K ⁡ W
8 eqid ⊢ LKer ⁡ U = LKer ⁡ U
9 eqid ⊢ f ∈ F | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f = f ∈ F | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f
10 1 7 2 3 4 5 8 9 6 lcdvbase ⊢ φ → V = f ∈ F | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f
11 ssrab2 ⊢ f ∈ F | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f ⊆ F
12 10 11 eqsstrdi ⊢ φ → V ⊆ F