# Metamath Proof Explorer

## Theorem cdleml4N

Description: Part of proof of Lemma L of Crawley p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdleml1.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdleml1.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdleml1.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdleml1.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
cdleml1.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
cdleml3.o
Assertion cdleml4N

### Proof

Step Hyp Ref Expression
1 cdleml1.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdleml1.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 cdleml1.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
4 cdleml1.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
5 cdleml1.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
6 cdleml3.o
7 1 2 3 cdlemftr0 ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \exists {f}\in {T}\phantom{\rule{.4em}{0ex}}{f}\ne {\mathrm{I}↾}_{{B}}$