Metamath Proof Explorer


Theorem dalem61

Description: Lemma for dath . Show that atoms D , E , and F lie on the same line (axis of perspectivity). Eliminate hypotheses containing dummy atoms c and d . (Contributed by NM, 11-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
dalem61.m ˙ = meet K
dalem61.o O = LPlanes K
dalem61.y Y = P ˙ Q ˙ R
dalem61.z Z = S ˙ T ˙ U
dalem61.d D = P ˙ Q ˙ S ˙ T
dalem61.e E = Q ˙ R ˙ T ˙ U
dalem61.f F = R ˙ P ˙ U ˙ S
Assertion dalem61 φ Y = Z ψ F ˙ D ˙ E

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 dalem61.m ˙ = meet K
7 dalem61.o O = LPlanes K
8 dalem61.y Y = P ˙ Q ˙ R
9 dalem61.z Z = S ˙ T ˙ U
10 dalem61.d D = P ˙ Q ˙ S ˙ T
11 dalem61.e E = Q ˙ R ˙ T ˙ U
12 dalem61.f F = R ˙ P ˙ U ˙ S
13 eqid c ˙ P ˙ d ˙ S = c ˙ P ˙ d ˙ S
14 eqid c ˙ Q ˙ d ˙ T = c ˙ Q ˙ d ˙ T
15 eqid c ˙ R ˙ d ˙ U = c ˙ R ˙ d ˙ U
16 eqid c ˙ P ˙ d ˙ S ˙ c ˙ Q ˙ d ˙ T ˙ c ˙ R ˙ d ˙ U ˙ Y = c ˙ P ˙ d ˙ S ˙ c ˙ Q ˙ d ˙ T ˙ c ˙ R ˙ d ˙ U ˙ Y
17 1 2 3 4 5 6 7 8 9 12 13 14 15 16 dalem59 φ Y = Z ψ F ˙ c ˙ P ˙ d ˙ S ˙ c ˙ Q ˙ d ˙ T ˙ c ˙ R ˙ d ˙ U ˙ Y
18 1 2 3 4 5 6 7 8 9 10 11 13 14 15 16 dalem60 φ Y = Z ψ D ˙ E = c ˙ P ˙ d ˙ S ˙ c ˙ Q ˙ d ˙ T ˙ c ˙ R ˙ d ˙ U ˙ Y
19 17 18 breqtrrd φ Y = Z ψ F ˙ D ˙ E