# Metamath Proof Explorer

## Theorem cdlemk51

Description: Part of proof of Lemma K of Crawley p. 118. Line 6, p. 120. G , I stand for g, h. X represents tau. TODO: Combine into cdlemk52 ? (Contributed by NM, 23-Jul-2013)

Ref Expression
Hypotheses cdlemk5.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdlemk5.l
cdlemk5.j
cdlemk5.m
cdlemk5.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemk5.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemk5.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemk5.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
cdlemk5.z
cdlemk5.y
cdlemk5.x ${⊢}{X}=\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({g}\right)\right)\to {z}\left({P}\right)={Y}\right)\right)$
Assertion cdlemk51

### Proof

Step Hyp Ref Expression
1 cdlemk5.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdlemk5.l
3 cdlemk5.j
4 cdlemk5.m
5 cdlemk5.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 cdlemk5.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 cdlemk5.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
8 cdlemk5.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
9 cdlemk5.z
10 cdlemk5.y
11 cdlemk5.x ${⊢}{X}=\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({g}\right)\right)\to {z}\left({P}\right)={Y}\right)\right)$
12 simp11
13 simp12
14 simp3
15 simp21
16 simp22
17 simp23
18 1 2 3 4 5 6 7 8 9 10 11 cdlemk39s
19 12 13 14 15 16 17 18 syl132anc
20 simp11l
21 20 hllatd
22 1 2 3 4 5 6 7 8 9 10 11 cdlemk35s
23 12 13 14 15 16 17 22 syl132anc
24 1 6 7 8 trlcl
25 12 23 24 syl2anc
26 simp3l
27 simp3r
28 1 5 6 7 8 trlnidat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {I}\in {T}\wedge {I}\ne {\mathrm{I}↾}_{{B}}\right)\to {R}\left({I}\right)\in {A}$
29 12 26 27 28 syl3anc
30 1 5 atbase ${⊢}{R}\left({I}\right)\in {A}\to {R}\left({I}\right)\in {B}$
31 29 30 syl
32 simp13
33 1 2 3 4 5 6 7 8 9 10 11 cdlemk35s
34 12 13 32 15 16 17 33 syl132anc
35 simp22l
36 2 5 6 7 ltrnat
37 12 34 35 36 syl3anc
38 1 5 atbase
39 37 38 syl
40 1 2 3 latjlej2
41 21 25 31 39 40 syl13anc
42 19 41 mpd
43 1 2 3 4 5 6 7 8 9 10 11 cdlemk39s
44 12 13 32 15 16 17 43 syl132anc
45 1 6 7 8 trlcl
46 12 34 45 syl2anc
47 simp13l
48 simp13r
49 1 5 6 7 8 trlnidat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {G}\in {T}\wedge {G}\ne {\mathrm{I}↾}_{{B}}\right)\to {R}\left({G}\right)\in {A}$
50 12 47 48 49 syl3anc
51 1 5 atbase ${⊢}{R}\left({G}\right)\in {A}\to {R}\left({G}\right)\in {B}$
52 50 51 syl
53 2 5 6 7 ltrnat
54 12 23 35 53 syl3anc
55 1 5 atbase
56 54 55 syl
57 1 2 3 latjlej2
58 21 46 52 56 57 syl13anc
59 44 58 mpd
60 1 3 latjcl
61 21 39 25 60 syl3anc
62 1 3 5 hlatjcl
63 20 37 29 62 syl3anc
64 1 3 latjcl
65 21 56 46 64 syl3anc
66 1 3 5 hlatjcl
67 20 54 50 66 syl3anc
68 1 2 4 latmlem12
69 21 61 63 65 67 68 syl122anc
70 42 59 69 mp2and