# Metamath Proof Explorer

## Theorem cdleme5

Description: Part of proof of Lemma E in Crawley p. 113. G represents f_s(r). We show r \/ f_s(r)) = p \/ q at the top of p. 114. (Contributed by NM, 7-Jun-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 cdleme5

### 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 8 oveq2i
10 simp1l
11 simp23l
12 simp21
13 simp22
14 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
15 14 2 4 hlatjcl
16 10 12 13 15 syl3anc
17 10 hllatd
18 simp1
19 simp3ll
20 1 2 3 4 5 6 7 14 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}}$
21 18 12 13 19 20 syl13anc
22 14 2 4 hlatjcl
23 10 11 19 22 syl3anc
24 simp1r
25 14 5 lhpbase ${⊢}{W}\in {H}\to {W}\in {\mathrm{Base}}_{{K}}$
26 24 25 syl
27 14 3 latmcl
28 17 23 26 27 syl3anc
29 14 2 latjcl
30 17 21 28 29 syl3anc
31 simp3r
32 14 1 2 3 4 atmod3i1
33 10 11 16 30 31 32 syl131anc
34 14 4 atbase ${⊢}{S}\in {A}\to {S}\in {\mathrm{Base}}_{{K}}$
35 19 34 syl
36 14 1 2 latlej2
37 17 35 16 36 syl3anc
38 14 4 atbase ${⊢}{R}\in {A}\to {R}\in {\mathrm{Base}}_{{K}}$
39 11 38 syl
40 14 2 latj12
41 17 39 21 35 40 syl13anc
42 1 2 3 4 5 6 14 cdleme0aa ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {P}\in {A}\wedge {Q}\in {A}\right)\to {U}\in {\mathrm{Base}}_{{K}}$
43 18 12 13 42 syl3anc
44 14 2 latj12
45 17 35 39 43 44 syl13anc
46 1 2 3 4 5 6 cdleme4
48 47 oveq2d
49 14 2 latjcom
50 17 21 35 49 syl3anc
51 simp3l
52 1 2 3 4 5 6 7 cdleme1
53 18 12 13 51 52 syl13anc
54 50 53 eqtrd
55 54 oveq2d
56 45 48 55 3eqtr4d
57 1 2 4 hlatlej1
58 10 11 19 57 syl3anc
59 14 1 2 3 4 atmod3i1
60 10 11 23 26 58 59 syl131anc
61 simp23r
62 eqid ${⊢}\mathrm{1.}\left({K}\right)=\mathrm{1.}\left({K}\right)$
63 1 2 62 4 5 lhpjat2
64 18 11 61 63 syl12anc
65 64 oveq2d
66 hlol ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OL}$
67 10 66 syl
68 14 3 62 olm11
69 67 23 68 syl2anc
70 65 69 eqtrd
71 60 70 eqtrd
72 71 oveq2d
73 41 56 72 3eqtr4d
74 14 2 latj12
75 17 21 39 28 74 syl13anc
76 73 75 eqtrd
77 37 76 breqtrd
78 14 2 latjcl
79 17 39 30 78 syl3anc
80 14 1 3 latleeqm1
81 17 16 79 80 syl3anc
82 77 81 mpbid
83 33 82 eqtrd
84 9 83 syl5eq