# Metamath Proof Explorer

## Theorem lcfrlem30

Description: Lemma for lcfr . (Contributed by NM, 6-Mar-2015)

Ref Expression
Hypotheses lcfrlem17.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
lcfrlem17.o
lcfrlem17.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
lcfrlem17.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
lcfrlem17.p
lcfrlem17.z
lcfrlem17.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
lcfrlem17.a ${⊢}{A}=\mathrm{LSAtoms}\left({U}\right)$
lcfrlem17.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
lcfrlem17.x
lcfrlem17.y
lcfrlem17.ne ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
lcfrlem22.b
lcfrlem24.t
lcfrlem24.s ${⊢}{S}=\mathrm{Scalar}\left({U}\right)$
lcfrlem24.q ${⊢}{Q}={0}_{{S}}$
lcfrlem24.r ${⊢}{R}={\mathrm{Base}}_{{S}}$
lcfrlem24.j
lcfrlem24.ib ${⊢}{\phi }\to {I}\in {B}$
lcfrlem24.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
lcfrlem25.d ${⊢}{D}=\mathrm{LDual}\left({U}\right)$
lcfrlem28.jn ${⊢}{\phi }\to {J}\left({Y}\right)\left({I}\right)\ne {Q}$
lcfrlem29.i ${⊢}{F}={inv}_{r}\left({S}\right)$
lcfrlem30.m
lcfrlem30.c
Assertion lcfrlem30 ${⊢}{\phi }\to {C}\in \mathrm{LFnl}\left({U}\right)$

### Proof

Step Hyp Ref Expression
1 lcfrlem17.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 lcfrlem17.o
3 lcfrlem17.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 lcfrlem17.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 lcfrlem17.p
6 lcfrlem17.z
7 lcfrlem17.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
8 lcfrlem17.a ${⊢}{A}=\mathrm{LSAtoms}\left({U}\right)$
9 lcfrlem17.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
10 lcfrlem17.x
11 lcfrlem17.y
12 lcfrlem17.ne ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
13 lcfrlem22.b
14 lcfrlem24.t
15 lcfrlem24.s ${⊢}{S}=\mathrm{Scalar}\left({U}\right)$
16 lcfrlem24.q ${⊢}{Q}={0}_{{S}}$
17 lcfrlem24.r ${⊢}{R}={\mathrm{Base}}_{{S}}$
18 lcfrlem24.j
19 lcfrlem24.ib ${⊢}{\phi }\to {I}\in {B}$
20 lcfrlem24.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
21 lcfrlem25.d ${⊢}{D}=\mathrm{LDual}\left({U}\right)$
22 lcfrlem28.jn ${⊢}{\phi }\to {J}\left({Y}\right)\left({I}\right)\ne {Q}$
23 lcfrlem29.i ${⊢}{F}={inv}_{r}\left({S}\right)$
24 lcfrlem30.m
25 lcfrlem30.c
26 eqid ${⊢}\mathrm{LFnl}\left({U}\right)=\mathrm{LFnl}\left({U}\right)$
27 1 3 9 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
28 eqid ${⊢}{0}_{{D}}={0}_{{D}}$
29 eqid
30 1 2 3 4 5 14 15 17 6 26 20 21 28 29 18 9 10 lcfrlem10 ${⊢}{\phi }\to {J}\left({X}\right)\in \mathrm{LFnl}\left({U}\right)$
31 eqid ${⊢}{\cdot }_{{D}}={\cdot }_{{D}}$
32 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 lcfrlem29 ${⊢}{\phi }\to {F}\left({J}\left({Y}\right)\left({I}\right)\right){\cdot }_{{S}}{J}\left({X}\right)\left({I}\right)\in {R}$
33 1 2 3 4 5 14 15 17 6 26 20 21 28 29 18 9 11 lcfrlem10 ${⊢}{\phi }\to {J}\left({Y}\right)\in \mathrm{LFnl}\left({U}\right)$
34 26 15 17 21 31 27 32 33 ldualvscl ${⊢}{\phi }\to \left({F}\left({J}\left({Y}\right)\left({I}\right)\right){\cdot }_{{S}}{J}\left({X}\right)\left({I}\right)\right){\cdot }_{{D}}{J}\left({Y}\right)\in \mathrm{LFnl}\left({U}\right)$
35 26 21 24 27 30 34 ldualvsubcl
36 25 35 eqeltrid ${⊢}{\phi }\to {C}\in \mathrm{LFnl}\left({U}\right)$