# Metamath Proof Explorer

## Theorem dalem55

Description: Lemma for dath . Lines G H and P Q intersect at the auxiliary line B (later shown to be an axis of perspectivity; see dalem60 ). (Contributed by NM, 8-Aug-2012)

Ref Expression
Hypotheses dalem.ph
dalem.l
dalem.j
dalem.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
dalem.ps
dalem54.m
dalem54.o ${⊢}{O}=\mathrm{LPlanes}\left({K}\right)$
dalem54.y
dalem54.z
dalem54.g
dalem54.h
dalem54.i
dalem54.b1
Assertion dalem55

### Proof

Step Hyp Ref Expression
1 dalem.ph
2 dalem.l
3 dalem.j
4 dalem.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 dalem.ps
6 dalem54.m
7 dalem54.o ${⊢}{O}=\mathrm{LPlanes}\left({K}\right)$
8 dalem54.y
9 dalem54.z
10 dalem54.g
11 dalem54.h
12 dalem54.i
13 dalem54.b1
14 1 dalemkelat ${⊢}{\phi }\to {K}\in \mathrm{Lat}$
15 14 3ad2ant1 ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {K}\in \mathrm{Lat}$
16 1 dalemkehl ${⊢}{\phi }\to {K}\in \mathrm{HL}$
17 16 3ad2ant1 ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {K}\in \mathrm{HL}$
18 1 2 3 4 5 6 7 8 9 10 dalem23 ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {G}\in {A}$
19 1 2 3 4 5 6 7 8 9 11 dalem29 ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {H}\in {A}$
20 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
21 20 3 4 hlatjcl
22 17 18 19 21 syl3anc
23 1 3 4 dalempjqeb
25 20 2 6 latmle1
26 15 22 24 25 syl3anc
27 1 2 3 4 5 6 7 8 9 12 dalem34 ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {I}\in {A}$
28 20 4 atbase ${⊢}{I}\in {A}\to {I}\in {\mathrm{Base}}_{{K}}$
29 27 28 syl ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {I}\in {\mathrm{Base}}_{{K}}$
30 20 2 3 latlej1
31 15 22 29 30 syl3anc
32 1 4 dalemreb ${⊢}{\phi }\to {R}\in {\mathrm{Base}}_{{K}}$
33 20 2 3 latlej1
34 14 23 32 33 syl3anc
35 34 8 breqtrrdi
37 1 2 3 4 5 6 7 8 9 10 11 12 dalem42
38 20 7 lplnbase
39 37 38 syl
40 1 7 dalemyeb ${⊢}{\phi }\to {Y}\in {\mathrm{Base}}_{{K}}$
41 40 3ad2ant1 ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {Y}\in {\mathrm{Base}}_{{K}}$
42 20 2 6 latmlem12
43 15 22 39 24 41 42 syl122anc
44 31 36 43 mp2and
45 44 13 breqtrrdi
46 20 6 latmcl
47 15 22 24 46 syl3anc
48 eqid ${⊢}\mathrm{LLines}\left({K}\right)=\mathrm{LLines}\left({K}\right)$
49 1 2 3 4 5 6 48 7 8 9 10 11 12 13 dalem53 ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {B}\in \mathrm{LLines}\left({K}\right)$
50 20 48 llnbase ${⊢}{B}\in \mathrm{LLines}\left({K}\right)\to {B}\in {\mathrm{Base}}_{{K}}$
51 49 50 syl ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {B}\in {\mathrm{Base}}_{{K}}$
52 20 2 6 latlem12
53 15 47 22 51 52 syl13anc
54 26 45 53 mpbi2and
55 hlatl ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{AtLat}$
56 17 55 syl ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {K}\in \mathrm{AtLat}$
57 1 2 3 4 5 6 7 8 9 10 11 12 dalem52
58 1 2 3 4 5 6 7 8 9 10 11 12 13 dalem54
59 2 4 atcmp
60 56 57 58 59 syl3anc
61 54 60 mpbid