Metamath Proof Explorer


Theorem dalem27

Description: Lemma for dath . Show that the line G P intersects the dummy center of perspectivity c . (Contributed by NM, 8-Aug-2012)

Ref Expression
Hypotheses dalem.ph φ K HL C Base K P A Q A R A S A T A U A Y O Z O ¬ C ˙ P ˙ Q ¬ C ˙ Q ˙ R ¬ C ˙ R ˙ P ¬ C ˙ S ˙ T ¬ C ˙ T ˙ U ¬ C ˙ U ˙ S C ˙ P ˙ S C ˙ Q ˙ T C ˙ R ˙ U
dalem.l ˙ = K
dalem.j ˙ = join K
dalem.a A = Atoms K
dalem.ps ψ c A d A ¬ c ˙ Y d c ¬ d ˙ Y C ˙ c ˙ d
dalem23.m ˙ = meet K
dalem23.o O = LPlanes K
dalem23.y Y = P ˙ Q ˙ R
dalem23.z Z = S ˙ T ˙ U
dalem23.g G = c ˙ P ˙ d ˙ S
Assertion dalem27 φ Y = Z ψ c ˙ G ˙ P

Proof

Step Hyp Ref Expression
1 dalem.ph φ K HL C Base K P A Q A R A S A T A U A Y O Z O ¬ C ˙ P ˙ Q ¬ C ˙ Q ˙ R ¬ C ˙ R ˙ P ¬ C ˙ S ˙ T ¬ C ˙ T ˙ U ¬ C ˙ U ˙ S C ˙ P ˙ S C ˙ Q ˙ T C ˙ R ˙ U
2 dalem.l ˙ = K
3 dalem.j ˙ = join K
4 dalem.a A = Atoms K
5 dalem.ps ψ c A d A ¬ c ˙ Y d c ¬ d ˙ Y C ˙ c ˙ d
6 dalem23.m ˙ = meet K
7 dalem23.o O = LPlanes K
8 dalem23.y Y = P ˙ Q ˙ R
9 dalem23.z Z = S ˙ T ˙ U
10 dalem23.g G = c ˙ P ˙ d ˙ S
11 1 dalemkelat φ K Lat
12 11 3ad2ant1 φ Y = Z ψ K Lat
13 1 dalemkehl φ K HL
14 13 3ad2ant1 φ Y = Z ψ K HL
15 5 dalemccea ψ c A
16 15 3ad2ant3 φ Y = Z ψ c A
17 1 dalempea φ P A
18 17 3ad2ant1 φ Y = Z ψ P A
19 eqid Base K = Base K
20 19 3 4 hlatjcl K HL c A P A c ˙ P Base K
21 14 16 18 20 syl3anc φ Y = Z ψ c ˙ P Base K
22 5 dalemddea ψ d A
23 22 3ad2ant3 φ Y = Z ψ d A
24 1 dalemsea φ S A
25 24 3ad2ant1 φ Y = Z ψ S A
26 19 3 4 hlatjcl K HL d A S A d ˙ S Base K
27 14 23 25 26 syl3anc φ Y = Z ψ d ˙ S Base K
28 19 2 6 latmle1 K Lat c ˙ P Base K d ˙ S Base K c ˙ P ˙ d ˙ S ˙ c ˙ P
29 12 21 27 28 syl3anc φ Y = Z ψ c ˙ P ˙ d ˙ S ˙ c ˙ P
30 10 29 eqbrtrid φ Y = Z ψ G ˙ c ˙ P
31 1 2 3 4 5 6 7 8 9 10 dalem23 φ Y = Z ψ G A
32 1 2 3 4 7 8 dalemply φ P ˙ Y
33 32 3ad2ant1 φ Y = Z ψ P ˙ Y
34 1 2 3 4 5 6 7 8 9 10 dalem24 φ Y = Z ψ ¬ G ˙ Y
35 nbrne2 P ˙ Y ¬ G ˙ Y P G
36 35 necomd P ˙ Y ¬ G ˙ Y G P
37 33 34 36 syl2anc φ Y = Z ψ G P
38 2 3 4 hlatexch2 K HL G A c A P A G P G ˙ c ˙ P c ˙ G ˙ P
39 14 31 16 18 37 38 syl131anc φ Y = Z ψ G ˙ c ˙ P c ˙ G ˙ P
40 30 39 mpd φ Y = Z ψ c ˙ G ˙ P