Metamath Proof Explorer

Theorem cdleme16e

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph on p. 114, 3rd part of 3rd sentence. F and G represent f(s) and f(t) respectively. We show, in their notation, (s \/ t) /\ (f(s) \/ f(t))=(s \/ t) /\ w. (Contributed by NM, 11-Oct-2012)

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

Proof

Step Hyp Ref Expression
1 cdleme12.l
2 cdleme12.j
3 cdleme12.m
4 cdleme12.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 cdleme12.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 cdleme12.u
7 cdleme12.f
8 cdleme12.g
9 simp11l
10 9 hllatd
11 simp21l
12 simp22l
13 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
14 13 2 4 hlatjcl
15 9 11 12 14 syl3anc
16 simp11
17 simp12
18 simp13
19 simp21
20 simp23l
21 simp31
22 1 2 3 4 5 6 7 cdleme3fa
23 16 17 18 19 20 21 22 syl132anc
24 simp22
25 simp32
26 1 2 3 4 5 6 8 cdleme3fa
27 16 17 18 24 20 25 26 syl132anc
28 13 2 4 hlatjcl
29 9 23 27 28 syl3anc
30 13 1 3 latmle1
31 10 15 29 30 syl3anc
32 1 2 3 4 5 6 7 8 cdleme15
33 13 3 latmcl
34 10 15 29 33 syl3anc
35 simp11r
36 13 5 lhpbase ${⊢}{W}\in {H}\to {W}\in {\mathrm{Base}}_{{K}}$
37 35 36 syl
38 13 1 3 latlem12
39 10 34 15 37 38 syl13anc
40 31 32 39 mpbi2and
41 hlatl ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{AtLat}$
42 9 41 syl
43 1 2 3 4 5 6 7 8 cdleme16d
44 simp21r
45 simp23r
46 1 2 3 4 5 lhpat
47 9 35 11 44 12 45 46 syl222anc
48 1 4 atcmp
49 42 43 47 48 syl3anc
50 40 49 mpbid