# Metamath Proof Explorer

## Theorem cdlemi

Description: Lemma I of Crawley p. 118. (Contributed by NM, 19-Jun-2013)

Ref Expression
Hypotheses cdlemi.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdlemi.l
cdlemi.j
cdlemi.m
cdlemi.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemi.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemi.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemi.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
cdlemi.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
cdlemi.s
Assertion cdlemi

### Proof

Step Hyp Ref Expression
1 cdlemi.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdlemi.l
3 cdlemi.j
4 cdlemi.m
5 cdlemi.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 cdlemi.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 cdlemi.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
8 cdlemi.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
9 cdlemi.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
10 cdlemi.s
11 simp11l
12 simp11r
13 simp2l
14 simp13
15 simp2r
16 1 2 3 4 5 6 7 8 9 cdlemi1
17 11 12 13 14 15 16 syl221anc
18 simp12
19 1 2 3 4 5 6 7 8 9 cdlemi2
20 11 12 13 18 14 15 19 syl231anc
21 11 hllatd
22 simp11
23 6 7 9 tendocl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {U}\in {E}\wedge {G}\in {T}\right)\to {U}\left({G}\right)\in {T}$
24 22 13 14 23 syl3anc
25 simp2rl
26 1 5 atbase ${⊢}{P}\in {A}\to {P}\in {B}$
27 25 26 syl
28 1 6 7 ltrncl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {U}\left({G}\right)\in {T}\wedge {P}\in {B}\right)\to {U}\left({G}\right)\left({P}\right)\in {B}$
29 22 24 27 28 syl3anc
30 1 6 7 8 trlcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {G}\in {T}\right)\to {R}\left({G}\right)\in {B}$
31 22 14 30 syl2anc
32 1 3 latjcl
33 21 27 31 32 syl3anc
34 6 7 9 tendocl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {U}\in {E}\wedge {F}\in {T}\right)\to {U}\left({F}\right)\in {T}$
35 22 13 18 34 syl3anc
36 1 6 7 ltrncl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {U}\left({F}\right)\in {T}\wedge {P}\in {B}\right)\to {U}\left({F}\right)\left({P}\right)\in {B}$
37 22 35 27 36 syl3anc
38 6 7 ltrncnv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {{F}}^{-1}\in {T}$
39 22 18 38 syl2anc
40 6 7 ltrnco ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {G}\in {T}\wedge {{F}}^{-1}\in {T}\right)\to {G}\circ {{F}}^{-1}\in {T}$
41 22 14 39 40 syl3anc
42 1 6 7 8 trlcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {G}\circ {{F}}^{-1}\in {T}\right)\to {R}\left({G}\circ {{F}}^{-1}\right)\in {B}$
43 22 41 42 syl2anc
44 1 3 latjcl
45 21 37 43 44 syl3anc
46 1 2 4 latlem12
47 21 29 33 45 46 syl13anc
48 17 20 47 mpbi2and
49 hlatl ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{AtLat}$
50 11 49 syl
51 2 5 6 7 ltrnat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {U}\left({G}\right)\in {T}\wedge {P}\in {A}\right)\to {U}\left({G}\right)\left({P}\right)\in {A}$
52 22 24 25 51 syl3anc
53 2 5 6 7 ltrnel
54 22 35 15 53 syl3anc
55 1 2 3 4 5 6 7 8 9 cdlemi1
56 11 12 13 18 15 55 syl221anc
57 15 54 56 3jca
58 eqid
59 1 2 3 4 5 6 7 8 58 cdlemh
60 59 simpld
61 57 60 syld3an2
62 2 5 atcmp
63 50 52 61 62 syl3anc
64 48 63 mpbid
65 64 10 syl6eqr