Metamath Proof Explorer

Theorem cdleme4a

Description: Part of proof of Lemma E in Crawley p. 114 top. G represents f_s(r). Auxiliary lemma derived from cdleme5 . We show f_s(r) <_ p \/ q. (Contributed by NM, 10-Nov-2012)

Ref Expression
Hypotheses cdleme4.l
cdleme4.j
cdleme4.m
cdleme4.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdleme4.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdleme4.u
cdleme4.f
cdleme4.g
Assertion cdleme4a

Proof

Step Hyp Ref Expression
1 cdleme4.l
2 cdleme4.j
3 cdleme4.m
4 cdleme4.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 cdleme4.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 cdleme4.u
7 cdleme4.f
8 cdleme4.g
9 simp1l ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {R}\in {A}\right)\wedge {S}\in {A}\right)\to {K}\in \mathrm{HL}$
10 9 hllatd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {R}\in {A}\right)\wedge {S}\in {A}\right)\to {K}\in \mathrm{Lat}$
11 simp21 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {R}\in {A}\right)\wedge {S}\in {A}\right)\to {P}\in {A}$
12 simp22 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {R}\in {A}\right)\wedge {S}\in {A}\right)\to {Q}\in {A}$
13 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
14 13 2 4 hlatjcl
15 9 11 12 14 syl3anc
16 simp1r ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {R}\in {A}\right)\wedge {S}\in {A}\right)\to {W}\in {H}$
17 simp3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {R}\in {A}\right)\wedge {S}\in {A}\right)\to {S}\in {A}$
18 1 2 3 4 5 6 7 13 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}}$
19 9 16 11 12 17 18 syl23anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {R}\in {A}\right)\wedge {S}\in {A}\right)\to {F}\in {\mathrm{Base}}_{{K}}$
20 simp23 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {R}\in {A}\right)\wedge {S}\in {A}\right)\to {R}\in {A}$
21 13 2 4 hlatjcl
22 9 20 17 21 syl3anc
23 13 5 lhpbase ${⊢}{W}\in {H}\to {W}\in {\mathrm{Base}}_{{K}}$
24 16 23 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {R}\in {A}\right)\wedge {S}\in {A}\right)\to {W}\in {\mathrm{Base}}_{{K}}$
25 13 3 latmcl
26 10 22 24 25 syl3anc
27 13 2 latjcl
28 10 19 26 27 syl3anc
29 13 1 3 latmle1
30 10 15 28 29 syl3anc
31 8 30 eqbrtrid