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

Metamath Proof Explorer

Theorem dalem9

Description: Lemma for dath . Since -. C .<_ Y , the join Y .\/ C forms a 3-dimensional space. (Contributed by NM, 20-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
dalem9.o ⊢ O = LPlanes ⁡ K
dalem9.v ⊢ V = LVols ⁡ K
dalem9.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
dalem9.z ⊢ Z = S ∨ ˙ T ∨ ˙ U
dalem9.w ⊢ W = Y ∨ ˙ C
Assertion dalem9 ⊢ φ ∧ Y ≠ Z → W ∈ 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 dalem9.o ⊢ O = LPlanes ⁡ K
6 dalem9.v ⊢ V = LVols ⁡ K
7 dalem9.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
8 dalem9.z ⊢ Z = S ∨ ˙ T ∨ ˙ U
9 dalem9.w ⊢ W = Y ∨ ˙ C
10 1 dalemkehl ⊢ φ → K ∈ HL
11 10 adantr ⊢ φ ∧ Y ≠ Z → K ∈ HL
12 1 dalemyeo ⊢ φ → Y ∈ O
13 12 adantr ⊢ φ ∧ Y ≠ Z → Y ∈ O
14 1 2 3 4 5 7 dalemcea ⊢ φ → C ∈ A
15 14 adantr ⊢ φ ∧ Y ≠ Z → C ∈ A
16 1 2 3 4 5 7 8 dalem-cly ⊢ φ ∧ Y ≠ Z → ¬ C ≤ ˙ Y
17 2 3 4 5 6 lvoli3 ⊢ K ∈ HL ∧ Y ∈ O ∧ C ∈ A ∧ ¬ C ≤ ˙ Y → Y ∨ ˙ C ∈ V
18 11 13 15 16 17 syl31anc ⊢ φ ∧ Y ≠ Z → Y ∨ ˙ C ∈ V
19 9 18 eqeltrid ⊢ φ ∧ Y ≠ Z → W ∈ V