Metamath Proof Explorer


Theorem dalemdnee

Description: Lemma for dath . Axis of perspectivity points D and E are different. (Contributed by NM, 10-Aug-2012)

Ref Expression
Hypotheses dalema.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
dalemc.l ˙ = K
dalemc.j ˙ = join K
dalemc.a A = Atoms K
dalem3.m ˙ = meet K
dalem3.o O = LPlanes K
dalem3.y Y = P ˙ Q ˙ R
dalem3.z Z = S ˙ T ˙ U
dalem3.d D = P ˙ Q ˙ S ˙ T
dalem3.e E = Q ˙ R ˙ T ˙ U
Assertion dalemdnee φ D E

Proof

Step Hyp Ref Expression
1 dalema.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 dalemc.l ˙ = K
3 dalemc.j ˙ = join K
4 dalemc.a A = Atoms K
5 dalem3.m ˙ = meet K
6 dalem3.o O = LPlanes K
7 dalem3.y Y = P ˙ Q ˙ R
8 dalem3.z Z = S ˙ T ˙ U
9 dalem3.d D = P ˙ Q ˙ S ˙ T
10 dalem3.e E = Q ˙ R ˙ T ˙ U
11 simpr φ D = Q D = Q
12 1 2 3 4 6 7 dalemqnet φ Q T
13 12 adantr φ D = Q Q T
14 11 13 eqnetrd φ D = Q D T
15 1 2 3 4 5 6 7 8 9 10 dalem4 φ D T D E
16 14 15 syldan φ D = Q D E
17 1 2 3 4 5 6 7 8 9 10 dalem3 φ D Q D E
18 16 17 pm2.61dane φ D E