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

Metamath Proof Explorer

Theorem dalem42

Description: Lemma for dath . Auxiliary atoms G H I form a plane. (Contributed by NM, 4-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
dalem38.m ⊢ ∧ ˙ = meet ⁡ K
dalem38.o ⊢ O = LPlanes ⁡ K
dalem38.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
dalem38.z ⊢ Z = S ∨ ˙ T ∨ ˙ U
dalem38.g ⊢ G = c ∨ ˙ P ∧ ˙ d ∨ ˙ S
dalem38.h ⊢ H = c ∨ ˙ Q ∧ ˙ d ∨ ˙ T
dalem38.i ⊢ I = c ∨ ˙ R ∧ ˙ d ∨ ˙ U
Assertion dalem42 ⊢ φ ∧ Y = Z ∧ ψ → G ∨ ˙ H ∨ ˙ I ∈ O

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 dalem38.m ⊢ ∧ ˙ = meet ⁡ K
7 dalem38.o ⊢ O = LPlanes ⁡ K
8 dalem38.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
9 dalem38.z ⊢ Z = S ∨ ˙ T ∨ ˙ U
10 dalem38.g ⊢ G = c ∨ ˙ P ∧ ˙ d ∨ ˙ S
11 dalem38.h ⊢ H = c ∨ ˙ Q ∧ ˙ d ∨ ˙ T
12 dalem38.i ⊢ I = c ∨ ˙ R ∧ ˙ d ∨ ˙ U
13 1 dalemkehl ⊢ φ → K ∈ HL
14 13 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → K ∈ HL
15 1 2 3 4 5 6 7 8 9 10 dalem23 ⊢ φ ∧ Y = Z ∧ ψ → G ∈ A
16 1 2 3 4 5 6 7 8 9 11 dalem29 ⊢ φ ∧ Y = Z ∧ ψ → H ∈ A
17 1 2 3 4 5 6 7 8 9 12 dalem34 ⊢ φ ∧ Y = Z ∧ ψ → I ∈ A
18 1 2 3 4 5 6 7 8 9 10 11 12 dalem41 ⊢ φ ∧ Y = Z ∧ ψ → G ≠ H
19 1 2 3 4 5 6 7 8 9 10 11 12 dalem40 ⊢ φ ∧ Y = Z ∧ ψ → ¬ I ≤ ˙ G ∨ ˙ H
20 2 3 4 7 lplni2 ⊢ K ∈ HL ∧ G ∈ A ∧ H ∈ A ∧ I ∈ A ∧ G ≠ H ∧ ¬ I ≤ ˙ G ∨ ˙ H → G ∨ ˙ H ∨ ˙ I ∈ O
21 14 15 16 17 18 19 20 syl132anc ⊢ φ ∧ Y = Z ∧ ψ → G ∨ ˙ H ∨ ˙ I ∈ O