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

Metamath Proof Explorer

Theorem dalem14

Description: Lemma for dath . Planes Y and Z form a 3-dimensional space (when they are different). (Contributed by NM, 22-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
dalem14.o ⊢ O = LPlanes ⁡ K
dalem14.v ⊢ V = LVols ⁡ K
dalem14.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
dalem14.z ⊢ Z = S ∨ ˙ T ∨ ˙ U
dalem14.w ⊢ W = Y ∨ ˙ C
Assertion dalem14 ⊢ φ ∧ Y ≠ Z → Y ∨ ˙ Z ∈ V

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 dalem14.o ⊢ O = LPlanes ⁡ K
6 dalem14.v ⊢ V = LVols ⁡ K
7 dalem14.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
8 dalem14.z ⊢ Z = S ∨ ˙ T ∨ ˙ U
9 dalem14.w ⊢ W = Y ∨ ˙ C
10 1 2 3 4 5 7 8 9 dalem13 ⊢ φ ∧ Y ≠ Z → Y ∨ ˙ Z = W
11 1 2 3 4 5 6 7 8 9 dalem9 ⊢ φ ∧ Y ≠ Z → W ∈ V
12 10 11 eqeltrd ⊢ φ ∧ Y ≠ Z → Y ∨ ˙ Z ∈ V