# Metamath Proof Explorer

## Theorem cdlemg17

Description: Part of Lemma G of Crawley p. 117, lines 7 and 8. We show an argument whose value at G equals itself. TODO: fix comment. (Contributed by NM, 12-May-2013)

Ref Expression
Hypotheses cdlemg12.l
cdlemg12.j
cdlemg12.m
cdlemg12.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemg12.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemg12.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemg12b.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
Assertion cdlemg17

### Proof

Step Hyp Ref Expression
1 cdlemg12.l
2 cdlemg12.j
3 cdlemg12.m
4 cdlemg12.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 cdlemg12.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 cdlemg12.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
7 cdlemg12b.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
8 simp11
9 simp22
10 simp12l
11 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
12 11 4 atbase ${⊢}{P}\in {A}\to {P}\in {\mathrm{Base}}_{{K}}$
13 10 12 syl
14 simp21
15 1 4 5 6 ltrncoat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({F}\in {T}\wedge {G}\in {T}\right)\wedge {P}\in {A}\right)\to {F}\left({G}\left({P}\right)\right)\in {A}$
16 8 14 9 10 15 syl121anc
17 11 4 atbase ${⊢}{F}\left({G}\left({P}\right)\right)\in {A}\to {F}\left({G}\left({P}\right)\right)\in {\mathrm{Base}}_{{K}}$
18 16 17 syl
19 11 2 5 6 ltrnj
20 8 9 13 18 19 syl112anc
21 simp1
22 simp23
23 simp3
24 1 2 3 4 5 6 7 cdlemg17b
25 21 9 22 23 24 syl121anc
26 25 fveq2d
27 26 fveq2d
28 1 2 3 4 5 6 7 cdlemg17jq
29 27 28 eqtrd
30 25 29 oveq12d
31 20 30 eqtrd
32 simp13l
33 11 4 atbase ${⊢}{Q}\in {A}\to {Q}\in {\mathrm{Base}}_{{K}}$
34 32 33 syl
35 1 4 5 6 ltrncoat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({F}\in {T}\wedge {G}\in {T}\right)\wedge {Q}\in {A}\right)\to {F}\left({G}\left({Q}\right)\right)\in {A}$
36 8 14 9 32 35 syl121anc
37 11 4 atbase ${⊢}{F}\left({G}\left({Q}\right)\right)\in {A}\to {F}\left({G}\left({Q}\right)\right)\in {\mathrm{Base}}_{{K}}$
38 36 37 syl
39 11 2 5 6 ltrnj
40 8 9 34 38 39 syl112anc
41 1 2 3 4 5 6 7 cdlemg17bq
42 41 fveq2d
43 42 fveq2d
44 1 2 3 4 5 6 7 cdlemg17j
45 43 44 eqtrd
46 41 45 oveq12d
47 40 46 eqtrd
48 31 47 oveq12d
49 simp11l
50 11 2 4 hlatjcl
51 49 10 16 50 syl3anc
52 11 2 4 hlatjcl
53 49 32 36 52 syl3anc
54 11 3 5 6 ltrnm
55 8 9 51 53 54 syl112anc
56 49 hllatd
57 11 3 latmcom
58 56 51 53 57 syl3anc
59 48 55 58 3eqtr4d