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

Metamath Proof Explorer

Theorem dalempjsen

Description: Lemma for dath . Frequently-used utility lemma. (Contributed by NM, 13-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
dalempnes.o ⊢ O = LPlanes ⁡ K
dalempnes.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
Assertion dalempjsen ⊢ φ → P ∨ ˙ S ∈ LLines ⁡ K

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 dalempnes.o ⊢ O = LPlanes ⁡ K
6 dalempnes.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
7 1 dalemkehl ⊢ φ → K ∈ HL
8 1 dalempea ⊢ φ → P ∈ A
9 1 dalemsea ⊢ φ → S ∈ A
10 1 2 3 4 5 6 dalempnes ⊢ φ → P ≠ S
11 eqid ⊢ LLines ⁡ K = LLines ⁡ K
12 3 4 11 llni2 ⊢ K ∈ HL ∧ P ∈ A ∧ S ∈ A ∧ P ≠ S → P ∨ ˙ S ∈ LLines ⁡ K
13 7 8 9 10 12 syl31anc ⊢ φ → P ∨ ˙ S ∈ LLines ⁡ K