Metamath Proof Explorer


Theorem dalem19

Description: Lemma for dath . Show that a second dummy atom d exists outside of the Y and Z planes (when those planes are equal). (Contributed by NM, 15-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
dalem19.o O = LPlanes K
dalem19.y Y = P ˙ Q ˙ R
dalem19.z Z = S ˙ T ˙ U
Assertion dalem19 φ Y = Z c A ¬ c ˙ Y d A d c ¬ d ˙ Y C ˙ c ˙ d

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 dalem19.o O = LPlanes K
6 dalem19.y Y = P ˙ Q ˙ R
7 dalem19.z Z = S ˙ T ˙ U
8 1 dalemkehl φ K HL
9 8 ad3antrrr φ Y = Z c A ¬ c ˙ Y K HL
10 1 2 3 4 5 6 dalemcea φ C A
11 10 ad3antrrr φ Y = Z c A ¬ c ˙ Y C A
12 simplr φ Y = Z c A ¬ c ˙ Y c A
13 1 5 dalemyeb φ Y Base K
14 13 ad3antrrr φ Y = Z c A ¬ c ˙ Y Y Base K
15 1 2 3 4 5 6 7 dalem17 φ Y = Z C ˙ Y
16 15 ad2antrr φ Y = Z c A ¬ c ˙ Y C ˙ Y
17 simpr φ Y = Z c A ¬ c ˙ Y ¬ c ˙ Y
18 eqid Base K = Base K
19 18 2 3 4 atbtwnex K HL C A c A Y Base K C ˙ Y ¬ c ˙ Y d A d c ¬ d ˙ Y C ˙ c ˙ d
20 9 11 12 14 16 17 19 syl33anc φ Y = Z c A ¬ c ˙ Y d A d c ¬ d ˙ Y C ˙ c ˙ d