# Metamath Proof Explorer

## Theorem cdlemg19

Description: Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-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 cdlemg19

### 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 simp11l
9 8 hllatd
10 simp12l
11 simp11
12 simp21
13 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}$
14 11 12 10 13 syl3anc
15 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
16 15 2 4 hlatjcl
17 8 10 14 16 syl3anc
18 simp13l
19 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}$
20 11 12 18 19 syl3anc
21 15 2 4 hlatjcl
22 8 18 20 21 syl3anc
23 15 3 latmcom
24 9 17 22 23 syl3anc
25 1 2 3 4 5 6 7 cdlemg19a
26 simp13
27 simp12
28 simp22
29 28 necomd
30 simp21r
31 simp23
32 1 4 5 6 ltrnatneq
33 11 30 27 26 31 32 syl131anc
34 simp31
35 2 4 hlatjcom
36 8 10 18 35 syl3anc
37 34 36 breqtrd
38 simp32
39 2 4 hlatjcom
40 8 14 20 39 syl3anc
41 38 40 36 3netr3d
42 simp33
43 eqcom
44 43 anbi2i
45 44 rexbii
46 42 45 sylnib
47 1 2 3 4 5 6 7 cdlemg19a
48 11 26 27 12 29 33 37 41 46 47 syl333anc
49 24 25 48 3eqtr3d