# Metamath Proof Explorer

## Theorem cdleme20k

Description: Part of proof of Lemma E in Crawley p. 113, last paragraph on p. 114, antepenultimate line. D , F , Y , G represent s_2, f(s), t_2, f(t). (Contributed by NM, 20-Nov-2012)

Ref Expression
Hypotheses cdleme19.l
cdleme19.j
cdleme19.m
cdleme19.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdleme19.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdleme19.u
cdleme19.f
cdleme19.g
cdleme19.d
cdleme19.y
cdleme20.v
Assertion cdleme20k

### Proof

Step Hyp Ref Expression
1 cdleme19.l
2 cdleme19.j
3 cdleme19.m
4 cdleme19.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 cdleme19.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 cdleme19.u
7 cdleme19.f
8 cdleme19.g
9 cdleme19.d
10 cdleme19.y
11 cdleme20.v
12 simp11
13 simp12
14 simp13
15 simp2r
16 simp2l
17 simp3r
18 simp3l
19 1 2 3 4 5 9 cdlemednpq
20 12 13 14 15 16 17 18 19 syl133anc
21 simp11l
22 21 hllatd
23 simp11r
24 simp2ll
25 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
26 1 2 3 4 5 6 7 25 cdleme1b ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {S}\in {A}\right)\right)\to {F}\in {\mathrm{Base}}_{{K}}$
27 21 23 13 14 24 26 syl23anc
28 simp2rl
29 1 2 3 4 5 9 25 cdlemedb ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({R}\in {A}\wedge {S}\in {A}\right)\right)\to {D}\in {\mathrm{Base}}_{{K}}$
30 21 23 28 24 29 syl22anc
31 25 1 2 latlej2
32 22 27 30 31 syl3anc
33 breq2
34 32 33 syl5ibcom
35 34 necon3bd
36 20 35 mpd