This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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