# Metamath Proof Explorer

## Theorem cdlemd7

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 1-Jun-2012)

Ref Expression
Hypotheses cdlemd4.l
cdlemd4.j
cdlemd4.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemd4.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemd4.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
Assertion cdlemd7

### Proof

Step Hyp Ref Expression
1 cdlemd4.l
2 cdlemd4.j
3 cdlemd4.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
4 cdlemd4.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
5 cdlemd4.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
6 simp1
7 simp2l
8 simp2r
9 simp11l
10 9 hllatd
11 simp2rl
12 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
13 12 3 atbase ${⊢}{Q}\in {A}\to {Q}\in {\mathrm{Base}}_{{K}}$
14 11 13 syl
15 simp2ll
16 12 3 atbase ${⊢}{P}\in {A}\to {P}\in {\mathrm{Base}}_{{K}}$
17 15 16 syl
18 simp11
19 simp12l
20 12 4 5 ltrncl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {P}\in {\mathrm{Base}}_{{K}}\right)\to {F}\left({P}\right)\in {\mathrm{Base}}_{{K}}$
21 18 19 17 20 syl3anc
22 simp3r
23 12 1 2 latnlej1l
24 23 necomd
25 10 14 17 21 22 24 syl131anc
26 simp3l
27 simp12
28 1 2 3 4 5 cdlemd6
29 18 27 7 8 22 26 28 syl231anc
30 1 2 3 4 5 cdlemd5
31 6 7 8 25 26 29 30 syl132anc