# Metamath Proof Explorer

## Theorem cdlemk6u

Description: Part of proof of Lemma K of Crawley p. 118. Apply dalaw . (Contributed by NM, 4-Jul-2013)

Ref Expression
Hypotheses cdlemk1.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdlemk1.l
cdlemk1.j
cdlemk1.m
cdlemk1.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemk1.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemk1.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemk1.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
cdlemk1.s
cdlemk1.o ${⊢}{O}={S}\left({D}\right)$
Assertion cdlemk6u

### Proof

Step Hyp Ref Expression
1 cdlemk1.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdlemk1.l
3 cdlemk1.j
4 cdlemk1.m
5 cdlemk1.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 cdlemk1.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 cdlemk1.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
8 cdlemk1.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
9 cdlemk1.s
10 cdlemk1.o ${⊢}{O}={S}\left({D}\right)$
11 1 2 3 4 5 6 7 8 9 10 cdlemk5u
12 simp11l
13 simp22l
14 simp11
15 simp212
16 2 5 6 7 ltrnat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {G}\in {T}\wedge {P}\in {A}\right)\to {G}\left({P}\right)\in {A}$
17 14 15 13 16 syl3anc
18 simp213
19 2 5 6 7 ltrnat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {T}\wedge {P}\in {A}\right)\to {X}\left({P}\right)\in {A}$
20 14 18 13 19 syl3anc
21 simp1
22 simp211
23 simp22
24 simp23
25 simp3l1
26 simp3l2
27 simp3r1
28 1 2 3 4 5 6 7 8 9 10 cdlemkoatnle
29 28 simpld
30 21 22 23 24 25 26 27 29 syl133anc
31 simp13
32 simp3r2
33 5 6 7 8 trlcocnvat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({G}\in {T}\wedge {D}\in {T}\right)\wedge {R}\left({G}\right)\ne {R}\left({D}\right)\right)\to {R}\left({G}\circ {{D}}^{-1}\right)\in {A}$
34 14 15 31 32 33 syl121anc
35 simp3r3
36 5 6 7 8 trlcocnvat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {T}\wedge {D}\in {T}\right)\wedge {R}\left({X}\right)\ne {R}\left({D}\right)\right)\to {R}\left({X}\circ {{D}}^{-1}\right)\in {A}$
37 14 18 31 35 36 syl121anc
38 2 3 4 5 dalaw
39 12 13 17 20 30 34 37 38 syl133anc
40 11 39 mpd