# Metamath Proof Explorer

## Theorem atbtwn

Description: Property of a 3rd atom R on a line P .\/ Q intersecting element X at P . (Contributed by NM, 30-Jul-2012)

Ref Expression
Hypotheses atbtwn.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
atbtwn.l
atbtwn.j
atbtwn.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
Assertion atbtwn

### Proof

Step Hyp Ref Expression
1 atbtwn.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 atbtwn.l
3 atbtwn.j
4 atbtwn.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 simpl33
6 simpr
7 simpl11
8 7 hllatd
9 simpl2l
10 1 4 atbase ${⊢}{R}\in {A}\to {R}\in {B}$
11 9 10 syl
12 simpl1
13 1 3 4 hlatjcl
14 12 13 syl
15 simpl2r
16 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
17 1 2 16 latlem12
18 8 11 14 15 17 syl13anc
19 5 6 18 mpbi2and
20 simpl12
21 simpl13
22 simpl31
23 simpl32
24 1 2 3 16 4 2atjm
25 7 20 21 15 22 23 24 syl132anc
26 19 25 breqtrd
27 hlatl ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{AtLat}$
28 7 27 syl
29 2 4 atcmp
30 28 9 20 29 syl3anc
31 26 30 mpbid
32 31 ex