# Metamath Proof Explorer

## Theorem cdlemk17-2N

Description: Part of proof of Lemma K of Crawley p. 118. Line 21 on p. 119. Q , C are k_2, f_2. (Contributed by NM, 1-Jul-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemk2.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdlemk2.l
cdlemk2.j
cdlemk2.m
cdlemk2.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemk2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemk2.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemk2.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
cdlemk2.s
cdlemk2.q ${⊢}{Q}={S}\left({C}\right)$
Assertion cdlemk17-2N

### Proof

Step Hyp Ref Expression
1 cdlemk2.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdlemk2.l
3 cdlemk2.j
4 cdlemk2.m
5 cdlemk2.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 cdlemk2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 cdlemk2.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
8 cdlemk2.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
9 cdlemk2.s
10 cdlemk2.q ${⊢}{Q}={S}\left({C}\right)$
11 simp11
12 simp12
13 11 12 jca
14 simp21
15 simp22
16 simp23
17 simp33
18 simp13
19 simp32l
20 simp32r
21 simp31
22 1 2 3 4 5 6 7 8 9 10 cdlemk17
23 13 14 15 16 17 18 19 20 21 22 syl333anc