Metamath Proof Explorer

Theorem dalem44

Description: Lemma for dath . Dummy center of perspectivity c lies outside of plane G H I . (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 dalem44 ⊢ φ ∧ Y = Z ∧ ψ → ¬ c ≤ ˙ G ∨ ˙ H ∨ ˙ I

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 2 3 4 5 6 7 8 9 10 11 12 dalem43 ⊢ φ ∧ Y = Z ∧ ψ → G ∨ ˙ H ∨ ˙ I ≠ Y
14 13 necomd ⊢ φ ∧ Y = Z ∧ ψ → Y ≠ G ∨ ˙ H ∨ ˙ I
15 1 dalemkelat ⊢ φ → K ∈ Lat
16 15 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → K ∈ Lat
17 5 4 dalemcceb ⊢ ψ → c ∈ Base K
18 17 3ad2ant3 ⊢ φ ∧ Y = Z ∧ ψ → c ∈ Base K
19 1 2 3 4 5 6 7 8 9 10 11 12 dalem42 ⊢ φ ∧ Y = Z ∧ ψ → G ∨ ˙ H ∨ ˙ I ∈ O
20 eqid ⊢ Base K = Base K
21 20 7 lplnbase ⊢ G ∨ ˙ H ∨ ˙ I ∈ O → G ∨ ˙ H ∨ ˙ I ∈ Base K
22 19 21 syl ⊢ φ ∧ Y = Z ∧ ψ → G ∨ ˙ H ∨ ˙ I ∈ Base K
23 20 2 3 latleeqj1 ⊢ K ∈ Lat ∧ c ∈ Base K ∧ G ∨ ˙ H ∨ ˙ I ∈ Base K → c ≤ ˙ G ∨ ˙ H ∨ ˙ I ↔ c ∨ ˙ G ∨ ˙ H ∨ ˙ I = G ∨ ˙ H ∨ ˙ I
24 16 18 22 23 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → c ≤ ˙ G ∨ ˙ H ∨ ˙ I ↔ c ∨ ˙ G ∨ ˙ H ∨ ˙ I = G ∨ ˙ H ∨ ˙ I
25 1 2 3 4 5 6 7 8 9 10 dalem28 ⊢ φ ∧ Y = Z ∧ ψ → P ≤ ˙ G ∨ ˙ c
26 1 dalemkehl ⊢ φ → K ∈ HL
27 26 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → K ∈ HL
28 5 dalemccea ⊢ ψ → c ∈ A
29 28 3ad2ant3 ⊢ φ ∧ Y = Z ∧ ψ → c ∈ A
30 1 2 3 4 5 6 7 8 9 10 dalem23 ⊢ φ ∧ Y = Z ∧ ψ → G ∈ A
31 3 4 hlatjcom ⊢ K ∈ HL ∧ c ∈ A ∧ G ∈ A → c ∨ ˙ G = G ∨ ˙ c
32 27 29 30 31 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ G = G ∨ ˙ c
33 25 32 breqtrrd ⊢ φ ∧ Y = Z ∧ ψ → P ≤ ˙ c ∨ ˙ G
34 1 2 3 4 5 6 7 8 9 11 dalem33 ⊢ φ ∧ Y = Z ∧ ψ → Q ≤ ˙ H ∨ ˙ c
35 1 2 3 4 5 6 7 8 9 11 dalem29 ⊢ φ ∧ Y = Z ∧ ψ → H ∈ A
36 3 4 hlatjcom ⊢ K ∈ HL ∧ c ∈ A ∧ H ∈ A → c ∨ ˙ H = H ∨ ˙ c
37 27 29 35 36 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ H = H ∨ ˙ c
38 34 37 breqtrrd ⊢ φ ∧ Y = Z ∧ ψ → Q ≤ ˙ c ∨ ˙ H
39 1 4 dalempeb ⊢ φ → P ∈ Base K
40 39 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → P ∈ Base K
41 20 3 4 hlatjcl ⊢ K ∈ HL ∧ c ∈ A ∧ G ∈ A → c ∨ ˙ G ∈ Base K
42 27 29 30 41 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ G ∈ Base K
43 1 4 dalemqeb ⊢ φ → Q ∈ Base K
44 43 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → Q ∈ Base K
45 20 3 4 hlatjcl ⊢ K ∈ HL ∧ c ∈ A ∧ H ∈ A → c ∨ ˙ H ∈ Base K
46 27 29 35 45 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ H ∈ Base K
47 20 2 3 latjlej12 ⊢ K ∈ Lat ∧ P ∈ Base K ∧ c ∨ ˙ G ∈ Base K ∧ Q ∈ Base K ∧ c ∨ ˙ H ∈ Base K → P ≤ ˙ c ∨ ˙ G ∧ Q ≤ ˙ c ∨ ˙ H → P ∨ ˙ Q ≤ ˙ c ∨ ˙ G ∨ ˙ c ∨ ˙ H
48 16 40 42 44 46 47 syl122anc ⊢ φ ∧ Y = Z ∧ ψ → P ≤ ˙ c ∨ ˙ G ∧ Q ≤ ˙ c ∨ ˙ H → P ∨ ˙ Q ≤ ˙ c ∨ ˙ G ∨ ˙ c ∨ ˙ H
49 33 38 48 mp2and ⊢ φ ∧ Y = Z ∧ ψ → P ∨ ˙ Q ≤ ˙ c ∨ ˙ G ∨ ˙ c ∨ ˙ H
50 20 4 atbase ⊢ G ∈ A → G ∈ Base K
51 30 50 syl ⊢ φ ∧ Y = Z ∧ ψ → G ∈ Base K
52 20 4 atbase ⊢ H ∈ A → H ∈ Base K
53 35 52 syl ⊢ φ ∧ Y = Z ∧ ψ → H ∈ Base K
54 20 3 latjjdi ⊢ K ∈ Lat ∧ c ∈ Base K ∧ G ∈ Base K ∧ H ∈ Base K → c ∨ ˙ G ∨ ˙ H = c ∨ ˙ G ∨ ˙ c ∨ ˙ H
55 16 18 51 53 54 syl13anc ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ G ∨ ˙ H = c ∨ ˙ G ∨ ˙ c ∨ ˙ H
56 49 55 breqtrrd ⊢ φ ∧ Y = Z ∧ ψ → P ∨ ˙ Q ≤ ˙ c ∨ ˙ G ∨ ˙ H
57 1 2 3 4 5 6 7 8 9 12 dalem37 ⊢ φ ∧ Y = Z ∧ ψ → R ≤ ˙ I ∨ ˙ c
58 1 2 3 4 5 6 7 8 9 12 dalem34 ⊢ φ ∧ Y = Z ∧ ψ → I ∈ A
59 3 4 hlatjcom ⊢ K ∈ HL ∧ c ∈ A ∧ I ∈ A → c ∨ ˙ I = I ∨ ˙ c
60 27 29 58 59 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ I = I ∨ ˙ c
61 57 60 breqtrrd ⊢ φ ∧ Y = Z ∧ ψ → R ≤ ˙ c ∨ ˙ I
62 1 3 4 dalempjqeb ⊢ φ → P ∨ ˙ Q ∈ Base K
63 62 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → P ∨ ˙ Q ∈ Base K
64 20 3 4 hlatjcl ⊢ K ∈ HL ∧ G ∈ A ∧ H ∈ A → G ∨ ˙ H ∈ Base K
65 27 30 35 64 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → G ∨ ˙ H ∈ Base K
66 20 3 latjcl ⊢ K ∈ Lat ∧ c ∈ Base K ∧ G ∨ ˙ H ∈ Base K → c ∨ ˙ G ∨ ˙ H ∈ Base K
67 16 18 65 66 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ G ∨ ˙ H ∈ Base K
68 1 4 dalemreb ⊢ φ → R ∈ Base K
69 68 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → R ∈ Base K
70 20 3 4 hlatjcl ⊢ K ∈ HL ∧ c ∈ A ∧ I ∈ A → c ∨ ˙ I ∈ Base K
71 27 29 58 70 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ I ∈ Base K
72 20 2 3 latjlej12 ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ Base K ∧ c ∨ ˙ G ∨ ˙ H ∈ Base K ∧ R ∈ Base K ∧ c ∨ ˙ I ∈ Base K → P ∨ ˙ Q ≤ ˙ c ∨ ˙ G ∨ ˙ H ∧ R ≤ ˙ c ∨ ˙ I → P ∨ ˙ Q ∨ ˙ R ≤ ˙ c ∨ ˙ G ∨ ˙ H ∨ ˙ c ∨ ˙ I
73 16 63 67 69 71 72 syl122anc ⊢ φ ∧ Y = Z ∧ ψ → P ∨ ˙ Q ≤ ˙ c ∨ ˙ G ∨ ˙ H ∧ R ≤ ˙ c ∨ ˙ I → P ∨ ˙ Q ∨ ˙ R ≤ ˙ c ∨ ˙ G ∨ ˙ H ∨ ˙ c ∨ ˙ I
74 56 61 73 mp2and ⊢ φ ∧ Y = Z ∧ ψ → P ∨ ˙ Q ∨ ˙ R ≤ ˙ c ∨ ˙ G ∨ ˙ H ∨ ˙ c ∨ ˙ I
75 20 4 atbase ⊢ I ∈ A → I ∈ Base K
76 58 75 syl ⊢ φ ∧ Y = Z ∧ ψ → I ∈ Base K
77 20 3 latjjdi ⊢ K ∈ Lat ∧ c ∈ Base K ∧ G ∨ ˙ H ∈ Base K ∧ I ∈ Base K → c ∨ ˙ G ∨ ˙ H ∨ ˙ I = c ∨ ˙ G ∨ ˙ H ∨ ˙ c ∨ ˙ I
78 16 18 65 76 77 syl13anc ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ G ∨ ˙ H ∨ ˙ I = c ∨ ˙ G ∨ ˙ H ∨ ˙ c ∨ ˙ I
79 74 78 breqtrrd ⊢ φ ∧ Y = Z ∧ ψ → P ∨ ˙ Q ∨ ˙ R ≤ ˙ c ∨ ˙ G ∨ ˙ H ∨ ˙ I
80 8 79 eqbrtrid ⊢ φ ∧ Y = Z ∧ ψ → Y ≤ ˙ c ∨ ˙ G ∨ ˙ H ∨ ˙ I
81 breq2 ⊢ c ∨ ˙ G ∨ ˙ H ∨ ˙ I = G ∨ ˙ H ∨ ˙ I → Y ≤ ˙ c ∨ ˙ G ∨ ˙ H ∨ ˙ I ↔ Y ≤ ˙ G ∨ ˙ H ∨ ˙ I
82 80 81 syl5ibcom ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ G ∨ ˙ H ∨ ˙ I = G ∨ ˙ H ∨ ˙ I → Y ≤ ˙ G ∨ ˙ H ∨ ˙ I
83 24 82 sylbid ⊢ φ ∧ Y = Z ∧ ψ → c ≤ ˙ G ∨ ˙ H ∨ ˙ I → Y ≤ ˙ G ∨ ˙ H ∨ ˙ I
84 1 dalemyeo ⊢ φ → Y ∈ O
85 84 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → Y ∈ O
86 2 7 lplncmp ⊢ K ∈ HL ∧ Y ∈ O ∧ G ∨ ˙ H ∨ ˙ I ∈ O → Y ≤ ˙ G ∨ ˙ H ∨ ˙ I ↔ Y = G ∨ ˙ H ∨ ˙ I
87 27 85 19 86 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → Y ≤ ˙ G ∨ ˙ H ∨ ˙ I ↔ Y = G ∨ ˙ H ∨ ˙ I
88 83 87 sylibd ⊢ φ ∧ Y = Z ∧ ψ → c ≤ ˙ G ∨ ˙ H ∨ ˙ I → Y = G ∨ ˙ H ∨ ˙ I
89 88 necon3ad ⊢ φ ∧ Y = Z ∧ ψ → Y ≠ G ∨ ˙ H ∨ ˙ I → ¬ c ≤ ˙ G ∨ ˙ H ∨ ˙ I
90 14 89 mpd ⊢ φ ∧ Y = Z ∧ ψ → ¬ c ≤ ˙ G ∨ ˙ H ∨ ˙ I