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=BaseC
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=BaseC
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