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

Metamath Proof Explorer

Theorem dalem45

Description: Lemma for dath . Dummy center of perspectivity c is not on the line G H . (Contributed by NM, 16-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
dalem44.m ⊢ ∧ ˙ = meet ⁡ K
dalem44.o ⊢ O = LPlanes ⁡ K
dalem44.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
dalem44.z ⊢ Z = S ∨ ˙ T ∨ ˙ U
dalem44.g ⊢ G = c ∨ ˙ P ∧ ˙ d ∨ ˙ S
dalem44.h ⊢ H = c ∨ ˙ Q ∧ ˙ d ∨ ˙ T
dalem44.i ⊢ I = c ∨ ˙ R ∧ ˙ d ∨ ˙ U
Assertion dalem45 ⊢ φ ∧ Y = Z ∧ ψ → ¬ c ≤ ˙ G ∨ ˙ H

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 dalem44.m ⊢ ∧ ˙ = meet ⁡ K
7 dalem44.o ⊢ O = LPlanes ⁡ K
8 dalem44.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
9 dalem44.z ⊢ Z = S ∨ ˙ T ∨ ˙ U
10 dalem44.g ⊢ G = c ∨ ˙ P ∧ ˙ d ∨ ˙ S
11 dalem44.h ⊢ H = c ∨ ˙ Q ∧ ˙ d ∨ ˙ T
12 dalem44.i ⊢ I = c ∨ ˙ R ∧ ˙ d ∨ ˙ U
13 1 dalemkelat ⊢ φ → K ∈ Lat
14 13 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → K ∈ Lat
15 5 4 dalemcceb ⊢ ψ → c ∈ Base K
16 15 3ad2ant3 ⊢ φ ∧ Y = Z ∧ ψ → c ∈ Base K
17 1 dalemkehl ⊢ φ → K ∈ HL
18 17 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → K ∈ HL
19 1 2 3 4 5 6 7 8 9 10 dalem23 ⊢ φ ∧ Y = Z ∧ ψ → G ∈ A
20 1 2 3 4 5 6 7 8 9 11 dalem29 ⊢ φ ∧ Y = Z ∧ ψ → H ∈ A
21 eqid ⊢ Base K = Base K
22 21 3 4 hlatjcl ⊢ K ∈ HL ∧ G ∈ A ∧ H ∈ A → G ∨ ˙ H ∈ Base K
23 18 19 20 22 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → G ∨ ˙ H ∈ Base K
24 1 2 3 4 5 6 7 8 9 12 dalem34 ⊢ φ ∧ Y = Z ∧ ψ → I ∈ A
25 21 4 atbase ⊢ I ∈ A → I ∈ Base K
26 24 25 syl ⊢ φ ∧ Y = Z ∧ ψ → I ∈ Base K
27 1 2 3 4 5 6 7 8 9 10 11 12 dalem44 ⊢ φ ∧ Y = Z ∧ ψ → ¬ c ≤ ˙ G ∨ ˙ H ∨ ˙ I
28 21 2 3 latnlej2l ⊢ K ∈ Lat ∧ c ∈ Base K ∧ G ∨ ˙ H ∈ Base K ∧ I ∈ Base K ∧ ¬ c ≤ ˙ G ∨ ˙ H ∨ ˙ I → ¬ c ≤ ˙ G ∨ ˙ H
29 14 16 23 26 27 28 syl131anc ⊢ φ ∧ Y = Z ∧ ψ → ¬ c ≤ ˙ G ∨ ˙ H