# Metamath Proof Explorer

## Theorem cdlemg18a

Description: Show two lines are different. TODO: fix comment. (Contributed by NM, 14-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 cdlemg18a

### 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 simp3r
9 simpl1l
10 simpl21
11 simpl1
12 simpl23
13 simpl22
14 1 4 5 6 ltrnat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {Q}\in {A}\right)\to {F}\left({Q}\right)\in {A}$
15 11 12 13 14 syl3anc
16 1 4 5 6 ltrnat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {P}\in {A}\right)\to {F}\left({P}\right)\in {A}$
17 11 12 10 16 syl3anc
18 simpl3l
19 4 5 6 ltrn11at ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {P}\ne {Q}\right)\right)\to {F}\left({P}\right)\ne {F}\left({Q}\right)$
20 11 12 10 13 18 19 syl113anc
21 20 necomd
22 simpr
23 2 4 hlatexch4
24 9 10 15 13 17 18 21 22 23 syl323anc
25 24 eqcomd
26 25 ex
27 26 necon3d
28 8 27 mpd