# Metamath Proof Explorer

## Theorem lcfrlem10

Description: Lemma for lcfr . (Contributed by NM, 23-Feb-2015)

Ref Expression
Hypotheses lcf1o.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
lcf1o.o
lcf1o.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
lcf1o.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
lcf1o.a
lcf1o.t
lcf1o.s ${⊢}{S}=\mathrm{Scalar}\left({U}\right)$
lcf1o.r ${⊢}{R}={\mathrm{Base}}_{{S}}$
lcf1o.z
lcf1o.f ${⊢}{F}=\mathrm{LFnl}\left({U}\right)$
lcf1o.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
lcf1o.d ${⊢}{D}=\mathrm{LDual}\left({U}\right)$
lcf1o.q ${⊢}{Q}={0}_{{D}}$
lcf1o.c
lcf1o.j
lcflo.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
lcfrlem10.x
Assertion lcfrlem10 ${⊢}{\phi }\to {J}\left({X}\right)\in {F}$

### Proof

Step Hyp Ref Expression
1 lcf1o.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 lcf1o.o
3 lcf1o.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 lcf1o.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 lcf1o.a
6 lcf1o.t
7 lcf1o.s ${⊢}{S}=\mathrm{Scalar}\left({U}\right)$
8 lcf1o.r ${⊢}{R}={\mathrm{Base}}_{{S}}$
9 lcf1o.z
10 lcf1o.f ${⊢}{F}=\mathrm{LFnl}\left({U}\right)$
11 lcf1o.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
12 lcf1o.d ${⊢}{D}=\mathrm{LDual}\left({U}\right)$
13 lcf1o.q ${⊢}{Q}={0}_{{D}}$
14 lcf1o.c
15 lcf1o.j
16 lcflo.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
17 lcfrlem10.x
18 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 lcfrlem8
19 eqid
20 1 2 3 4 9 5 6 10 7 8 19 16 17 dochflcl
21 18 20 eqeltrd ${⊢}{\phi }\to {J}\left({X}\right)\in {F}$