# Metamath Proof Explorer

## Theorem lcfrlem22

Description: Lemma for lcfr . (Contributed by NM, 24-Feb-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
Assertion lcfrlem22 ${⊢}{\phi }\to {B}\in {A}$

### 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 1 2 3 4 5 6 7 8 9 10 11 12 lcfrlem21
15 13 14 eqeltrid ${⊢}{\phi }\to {B}\in {A}$