Metamath Proof Explorer


Theorem dalemcjden

Description: Lemma for dath . Show that the dummy atoms form a line. (Contributed by NM, 15-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
Assertion dalemcjden φ ψ c ˙ d LLines K

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 1 dalemkehl φ K HL
7 6 adantr φ ψ K HL
8 5 dalemccea ψ c A
9 8 adantl φ ψ c A
10 5 dalemddea ψ d A
11 10 adantl φ ψ d A
12 5 dalemccnedd ψ c d
13 12 adantl φ ψ c d
14 eqid LLines K = LLines K
15 3 4 14 llni2 K HL c A d A c d c ˙ d LLines K
16 7 9 11 13 15 syl31anc φ ψ c ˙ d LLines K