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

Metamath Proof Explorer

Theorem dalem18

Description: Lemma for dath . Show that a dummy atom c exists outside of the Y and Z planes (when those planes are equal). This requires that the projective space be 3-dimensional. (Desargues's theorem does not always hold in 2 dimensions.) (Contributed by NM, 29-Jul-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
dalem18.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
Assertion dalem18 ⊢ φ → ∃ c ∈ A ¬ c ≤ ˙ Y

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 dalem18.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
6 1 dalemkehl ⊢ φ → K ∈ HL
7 1 dalempea ⊢ φ → P ∈ A
8 1 dalemqea ⊢ φ → Q ∈ A
9 1 dalemrea ⊢ φ → R ∈ A
10 3 2 4 3dim3 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → ∃ c ∈ A ¬ c ≤ ˙ P ∨ ˙ Q ∨ ˙ R
11 6 7 8 9 10 syl13anc ⊢ φ → ∃ c ∈ A ¬ c ≤ ˙ P ∨ ˙ Q ∨ ˙ R
12 5 breq2i ⊢ c ≤ ˙ Y ↔ c ≤ ˙ P ∨ ˙ Q ∨ ˙ R
13 12 notbii ⊢ ¬ c ≤ ˙ Y ↔ ¬ c ≤ ˙ P ∨ ˙ Q ∨ ˙ R
14 13 rexbii ⊢ ∃ c ∈ A ¬ c ≤ ˙ Y ↔ ∃ c ∈ A ¬ c ≤ ˙ P ∨ ˙ Q ∨ ˙ R
15 11 14 sylibr ⊢ φ → ∃ c ∈ A ¬ c ≤ ˙ Y