# Metamath Proof Explorer

## Theorem cdleml5N

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 cdleml5N

### 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 simpl1
8 1 2 3 5 6 tendo0cl
9 7 8 syl
10 simpl2l
11 1 2 3 5 6 tendo0mul
12 7 10 11 syl2anc
13 simpr
14 12 13 eqtr4d
15 coeq1
16 15 eqeq1d
17 16 rspcev
18 9 14 17 syl2anc
19 simpl1
20 simpl2
21 simpl3
22 simpr
23 1 2 3 4 5 6 cdleml4N
24 19 20 21 22 23 syl112anc
25 18 24 pm2.61dane