Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dalem44 Structured version   Visualization version   GIF version

Theorem dalem44 38179
Description: Lemma for dath 38199. Dummy center of perspectivity 𝑐 lies outside of plane 𝐺𝐻𝐼. (Contributed by NM, 16-Aug-2012.)
Hypotheses
Ref Expression
dalem.ph (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))))
dalem.l = (le‘𝐾)
dalem.j = (join‘𝐾)
dalem.a 𝐴 = (Atoms‘𝐾)
dalem.ps (𝜓 ↔ ((𝑐𝐴𝑑𝐴) ∧ ¬ 𝑐 𝑌 ∧ (𝑑𝑐 ∧ ¬ 𝑑 𝑌𝐶 (𝑐 𝑑))))
dalem44.m = (meet‘𝐾)
dalem44.o 𝑂 = (LPlanes‘𝐾)
dalem44.y 𝑌 = ((𝑃 𝑄) 𝑅)
dalem44.z 𝑍 = ((𝑆 𝑇) 𝑈)
dalem44.g 𝐺 = ((𝑐 𝑃) (𝑑 𝑆))
dalem44.h 𝐻 = ((𝑐 𝑄) (𝑑 𝑇))
dalem44.i 𝐼 = ((𝑐 𝑅) (𝑑 𝑈))
Assertion
Ref Expression
dalem44 ((𝜑𝑌 = 𝑍𝜓) → ¬ 𝑐 ((𝐺 𝐻) 𝐼))

Proof of Theorem dalem44
StepHypRef Expression
1 dalem.ph . . . 4 (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))))
2 dalem.l . . . 4 = (le‘𝐾)
3 dalem.j . . . 4 = (join‘𝐾)
4 dalem.a . . . 4 𝐴 = (Atoms‘𝐾)
5 dalem.ps . . . 4 (𝜓 ↔ ((𝑐𝐴𝑑𝐴) ∧ ¬ 𝑐 𝑌 ∧ (𝑑𝑐 ∧ ¬ 𝑑 𝑌𝐶 (𝑐 𝑑))))
6 dalem44.m . . . 4 = (meet‘𝐾)
7 dalem44.o . . . 4 𝑂 = (LPlanes‘𝐾)
8 dalem44.y . . . 4 𝑌 = ((𝑃 𝑄) 𝑅)
9 dalem44.z . . . 4 𝑍 = ((𝑆 𝑇) 𝑈)
10 dalem44.g . . . 4 𝐺 = ((𝑐 𝑃) (𝑑 𝑆))
11 dalem44.h . . . 4 𝐻 = ((𝑐 𝑄) (𝑑 𝑇))
12 dalem44.i . . . 4 𝐼 = ((𝑐 𝑅) (𝑑 𝑈))
131, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12dalem43 38178 . . 3 ((𝜑𝑌 = 𝑍𝜓) → ((𝐺 𝐻) 𝐼) ≠ 𝑌)
1413necomd 2999 . 2 ((𝜑𝑌 = 𝑍𝜓) → 𝑌 ≠ ((𝐺 𝐻) 𝐼))
151dalemkelat 38087 . . . . . . 7 (𝜑𝐾 ∈ Lat)
16153ad2ant1 1133 . . . . . 6 ((𝜑𝑌 = 𝑍𝜓) → 𝐾 ∈ Lat)
175, 4dalemcceb 38152 . . . . . . 7 (𝜓𝑐 ∈ (Base‘𝐾))
18173ad2ant3 1135 . . . . . 6 ((𝜑𝑌 = 𝑍𝜓) → 𝑐 ∈ (Base‘𝐾))
191, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12dalem42 38177 . . . . . . 7 ((𝜑𝑌 = 𝑍𝜓) → ((𝐺 𝐻) 𝐼) ∈ 𝑂)
20 eqid 2736 . . . . . . . 8 (Base‘𝐾) = (Base‘𝐾)
2120, 7lplnbase 37997 . . . . . . 7 (((𝐺 𝐻) 𝐼) ∈ 𝑂 → ((𝐺 𝐻) 𝐼) ∈ (Base‘𝐾))
2219, 21syl 17 . . . . . 6 ((𝜑𝑌 = 𝑍𝜓) → ((𝐺 𝐻) 𝐼) ∈ (Base‘𝐾))
2320, 2, 3latleeqj1 18340 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑐 ∈ (Base‘𝐾) ∧ ((𝐺 𝐻) 𝐼) ∈ (Base‘𝐾)) → (𝑐 ((𝐺 𝐻) 𝐼) ↔ (𝑐 ((𝐺 𝐻) 𝐼)) = ((𝐺 𝐻) 𝐼)))
2416, 18, 22, 23syl3anc 1371 . . . . 5 ((𝜑𝑌 = 𝑍𝜓) → (𝑐 ((𝐺 𝐻) 𝐼) ↔ (𝑐 ((𝐺 𝐻) 𝐼)) = ((𝐺 𝐻) 𝐼)))
251, 2, 3, 4, 5, 6, 7, 8, 9, 10dalem28 38163 . . . . . . . . . . . 12 ((𝜑𝑌 = 𝑍𝜓) → 𝑃 (𝐺 𝑐))
261dalemkehl 38086 . . . . . . . . . . . . . 14 (𝜑𝐾 ∈ HL)
27263ad2ant1 1133 . . . . . . . . . . . . 13 ((𝜑𝑌 = 𝑍𝜓) → 𝐾 ∈ HL)
285dalemccea 38146 . . . . . . . . . . . . . 14 (𝜓𝑐𝐴)
29283ad2ant3 1135 . . . . . . . . . . . . 13 ((𝜑𝑌 = 𝑍𝜓) → 𝑐𝐴)
301, 2, 3, 4, 5, 6, 7, 8, 9, 10dalem23 38159 . . . . . . . . . . . . 13 ((𝜑𝑌 = 𝑍𝜓) → 𝐺𝐴)
313, 4hlatjcom 37830 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑐𝐴𝐺𝐴) → (𝑐 𝐺) = (𝐺 𝑐))
3227, 29, 30, 31syl3anc 1371 . . . . . . . . . . . 12 ((𝜑𝑌 = 𝑍𝜓) → (𝑐 𝐺) = (𝐺 𝑐))
3325, 32breqtrrd 5133 . . . . . . . . . . 11 ((𝜑𝑌 = 𝑍𝜓) → 𝑃 (𝑐 𝐺))
341, 2, 3, 4, 5, 6, 7, 8, 9, 11dalem33 38168 . . . . . . . . . . . 12 ((𝜑𝑌 = 𝑍𝜓) → 𝑄 (𝐻 𝑐))
351, 2, 3, 4, 5, 6, 7, 8, 9, 11dalem29 38164 . . . . . . . . . . . . 13 ((𝜑𝑌 = 𝑍𝜓) → 𝐻𝐴)
363, 4hlatjcom 37830 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑐𝐴𝐻𝐴) → (𝑐 𝐻) = (𝐻 𝑐))
3727, 29, 35, 36syl3anc 1371 . . . . . . . . . . . 12 ((𝜑𝑌 = 𝑍𝜓) → (𝑐 𝐻) = (𝐻 𝑐))
3834, 37breqtrrd 5133 . . . . . . . . . . 11 ((𝜑𝑌 = 𝑍𝜓) → 𝑄 (𝑐 𝐻))
391, 4dalempeb 38102 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ (Base‘𝐾))
40393ad2ant1 1133 . . . . . . . . . . . 12 ((𝜑𝑌 = 𝑍𝜓) → 𝑃 ∈ (Base‘𝐾))
4120, 3, 4hlatjcl 37829 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑐𝐴𝐺𝐴) → (𝑐 𝐺) ∈ (Base‘𝐾))
4227, 29, 30, 41syl3anc 1371 . . . . . . . . . . . 12 ((𝜑𝑌 = 𝑍𝜓) → (𝑐 𝐺) ∈ (Base‘𝐾))
431, 4dalemqeb 38103 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ (Base‘𝐾))
44433ad2ant1 1133 . . . . . . . . . . . 12 ((𝜑𝑌 = 𝑍𝜓) → 𝑄 ∈ (Base‘𝐾))
4520, 3, 4hlatjcl 37829 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑐𝐴𝐻𝐴) → (𝑐 𝐻) ∈ (Base‘𝐾))
4627, 29, 35, 45syl3anc 1371 . . . . . . . . . . . 12 ((𝜑𝑌 = 𝑍𝜓) → (𝑐 𝐻) ∈ (Base‘𝐾))
4720, 2, 3latjlej12 18344 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ (𝑐 𝐺) ∈ (Base‘𝐾)) ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑐 𝐻) ∈ (Base‘𝐾))) → ((𝑃 (𝑐 𝐺) ∧ 𝑄 (𝑐 𝐻)) → (𝑃 𝑄) ((𝑐 𝐺) (𝑐 𝐻))))
4816, 40, 42, 44, 46, 47syl122anc 1379 . . . . . . . . . . 11 ((𝜑𝑌 = 𝑍𝜓) → ((𝑃 (𝑐 𝐺) ∧ 𝑄 (𝑐 𝐻)) → (𝑃 𝑄) ((𝑐 𝐺) (𝑐 𝐻))))
4933, 38, 48mp2and 697 . . . . . . . . . 10 ((𝜑𝑌 = 𝑍𝜓) → (𝑃 𝑄) ((𝑐 𝐺) (𝑐 𝐻)))
5020, 4atbase 37751 . . . . . . . . . . . 12 (𝐺𝐴𝐺 ∈ (Base‘𝐾))
5130, 50syl 17 . . . . . . . . . . 11 ((𝜑𝑌 = 𝑍𝜓) → 𝐺 ∈ (Base‘𝐾))
5220, 4atbase 37751 . . . . . . . . . . . 12 (𝐻𝐴𝐻 ∈ (Base‘𝐾))
5335, 52syl 17 . . . . . . . . . . 11 ((𝜑𝑌 = 𝑍𝜓) → 𝐻 ∈ (Base‘𝐾))
5420, 3latjjdi 18380 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑐 ∈ (Base‘𝐾) ∧ 𝐺 ∈ (Base‘𝐾) ∧ 𝐻 ∈ (Base‘𝐾))) → (𝑐 (𝐺 𝐻)) = ((𝑐 𝐺) (𝑐 𝐻)))
5516, 18, 51, 53, 54syl13anc 1372 . . . . . . . . . 10 ((𝜑𝑌 = 𝑍𝜓) → (𝑐 (𝐺 𝐻)) = ((𝑐 𝐺) (𝑐 𝐻)))
5649, 55breqtrrd 5133 . . . . . . . . 9 ((𝜑𝑌 = 𝑍𝜓) → (𝑃 𝑄) (𝑐 (𝐺 𝐻)))
571, 2, 3, 4, 5, 6, 7, 8, 9, 12dalem37 38172 . . . . . . . . . 10 ((𝜑𝑌 = 𝑍𝜓) → 𝑅 (𝐼 𝑐))
581, 2, 3, 4, 5, 6, 7, 8, 9, 12dalem34 38169 . . . . . . . . . . 11 ((𝜑𝑌 = 𝑍𝜓) → 𝐼𝐴)
593, 4hlatjcom 37830 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑐𝐴𝐼𝐴) → (𝑐 𝐼) = (𝐼 𝑐))
6027, 29, 58, 59syl3anc 1371 . . . . . . . . . 10 ((𝜑𝑌 = 𝑍𝜓) → (𝑐 𝐼) = (𝐼 𝑐))
6157, 60breqtrrd 5133 . . . . . . . . 9 ((𝜑𝑌 = 𝑍𝜓) → 𝑅 (𝑐 𝐼))
621, 3, 4dalempjqeb 38108 . . . . . . . . . . 11 (𝜑 → (𝑃 𝑄) ∈ (Base‘𝐾))
63623ad2ant1 1133 . . . . . . . . . 10 ((𝜑𝑌 = 𝑍𝜓) → (𝑃 𝑄) ∈ (Base‘𝐾))
6420, 3, 4hlatjcl 37829 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝐺𝐴𝐻𝐴) → (𝐺 𝐻) ∈ (Base‘𝐾))
6527, 30, 35, 64syl3anc 1371 . . . . . . . . . . 11 ((𝜑𝑌 = 𝑍𝜓) → (𝐺 𝐻) ∈ (Base‘𝐾))
6620, 3latjcl 18328 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ 𝑐 ∈ (Base‘𝐾) ∧ (𝐺 𝐻) ∈ (Base‘𝐾)) → (𝑐 (𝐺 𝐻)) ∈ (Base‘𝐾))
6716, 18, 65, 66syl3anc 1371 . . . . . . . . . 10 ((𝜑𝑌 = 𝑍𝜓) → (𝑐 (𝐺 𝐻)) ∈ (Base‘𝐾))
681, 4dalemreb 38104 . . . . . . . . . . 11 (𝜑𝑅 ∈ (Base‘𝐾))
69683ad2ant1 1133 . . . . . . . . . 10 ((𝜑𝑌 = 𝑍𝜓) → 𝑅 ∈ (Base‘𝐾))
7020, 3, 4hlatjcl 37829 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑐𝐴𝐼𝐴) → (𝑐 𝐼) ∈ (Base‘𝐾))
7127, 29, 58, 70syl3anc 1371 . . . . . . . . . 10 ((𝜑𝑌 = 𝑍𝜓) → (𝑐 𝐼) ∈ (Base‘𝐾))
7220, 2, 3latjlej12 18344 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝑐 (𝐺 𝐻)) ∈ (Base‘𝐾)) ∧ (𝑅 ∈ (Base‘𝐾) ∧ (𝑐 𝐼) ∈ (Base‘𝐾))) → (((𝑃 𝑄) (𝑐 (𝐺 𝐻)) ∧ 𝑅 (𝑐 𝐼)) → ((𝑃 𝑄) 𝑅) ((𝑐 (𝐺 𝐻)) (𝑐 𝐼))))
7316, 63, 67, 69, 71, 72syl122anc 1379 . . . . . . . . 9 ((𝜑𝑌 = 𝑍𝜓) → (((𝑃 𝑄) (𝑐 (𝐺 𝐻)) ∧ 𝑅 (𝑐 𝐼)) → ((𝑃 𝑄) 𝑅) ((𝑐 (𝐺 𝐻)) (𝑐 𝐼))))
7456, 61, 73mp2and 697 . . . . . . . 8 ((𝜑𝑌 = 𝑍𝜓) → ((𝑃 𝑄) 𝑅) ((𝑐 (𝐺 𝐻)) (𝑐 𝐼)))
7520, 4atbase 37751 . . . . . . . . . 10 (𝐼𝐴𝐼 ∈ (Base‘𝐾))
7658, 75syl 17 . . . . . . . . 9 ((𝜑𝑌 = 𝑍𝜓) → 𝐼 ∈ (Base‘𝐾))
7720, 3latjjdi 18380 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑐 ∈ (Base‘𝐾) ∧ (𝐺 𝐻) ∈ (Base‘𝐾) ∧ 𝐼 ∈ (Base‘𝐾))) → (𝑐 ((𝐺 𝐻) 𝐼)) = ((𝑐 (𝐺 𝐻)) (𝑐 𝐼)))
7816, 18, 65, 76, 77syl13anc 1372 . . . . . . . 8 ((𝜑𝑌 = 𝑍𝜓) → (𝑐 ((𝐺 𝐻) 𝐼)) = ((𝑐 (𝐺 𝐻)) (𝑐 𝐼)))
7974, 78breqtrrd 5133 . . . . . . 7 ((𝜑𝑌 = 𝑍𝜓) → ((𝑃 𝑄) 𝑅) (𝑐 ((𝐺 𝐻) 𝐼)))
808, 79eqbrtrid 5140 . . . . . 6 ((𝜑𝑌 = 𝑍𝜓) → 𝑌 (𝑐 ((𝐺 𝐻) 𝐼)))
81 breq2 5109 . . . . . 6 ((𝑐 ((𝐺 𝐻) 𝐼)) = ((𝐺 𝐻) 𝐼) → (𝑌 (𝑐 ((𝐺 𝐻) 𝐼)) ↔ 𝑌 ((𝐺 𝐻) 𝐼)))
8280, 81syl5ibcom 244 . . . . 5 ((𝜑𝑌 = 𝑍𝜓) → ((𝑐 ((𝐺 𝐻) 𝐼)) = ((𝐺 𝐻) 𝐼) → 𝑌 ((𝐺 𝐻) 𝐼)))
8324, 82sylbid 239 . . . 4 ((𝜑𝑌 = 𝑍𝜓) → (𝑐 ((𝐺 𝐻) 𝐼) → 𝑌 ((𝐺 𝐻) 𝐼)))
841dalemyeo 38095 . . . . . 6 (𝜑𝑌𝑂)
85843ad2ant1 1133 . . . . 5 ((𝜑𝑌 = 𝑍𝜓) → 𝑌𝑂)
862, 7lplncmp 38025 . . . . 5 ((𝐾 ∈ HL ∧ 𝑌𝑂 ∧ ((𝐺 𝐻) 𝐼) ∈ 𝑂) → (𝑌 ((𝐺 𝐻) 𝐼) ↔ 𝑌 = ((𝐺 𝐻) 𝐼)))
8727, 85, 19, 86syl3anc 1371 . . . 4 ((𝜑𝑌 = 𝑍𝜓) → (𝑌 ((𝐺 𝐻) 𝐼) ↔ 𝑌 = ((𝐺 𝐻) 𝐼)))
8883, 87sylibd 238 . . 3 ((𝜑𝑌 = 𝑍𝜓) → (𝑐 ((𝐺 𝐻) 𝐼) → 𝑌 = ((𝐺 𝐻) 𝐼)))
8988necon3ad 2956 . 2 ((𝜑𝑌 = 𝑍𝜓) → (𝑌 ≠ ((𝐺 𝐻) 𝐼) → ¬ 𝑐 ((𝐺 𝐻) 𝐼)))
9014, 89mpd 15 1 ((𝜑𝑌 = 𝑍𝜓) → ¬ 𝑐 ((𝐺 𝐻) 𝐼))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2943   class class class wbr 5105  cfv 6496  (class class class)co 7357  Basecbs 17083  lecple 17140  joincjn 18200  meetcmee 18201  Latclat 18320  Atomscatm 37725  HLchlt 37812  LPlanesclpl 37955
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-proset 18184  df-poset 18202  df-plt 18219  df-lub 18235  df-glb 18236  df-join 18237  df-meet 18238  df-p0 18314  df-lat 18321  df-clat 18388  df-oposet 37638  df-ol 37640  df-oml 37641  df-covers 37728  df-ats 37729  df-atl 37760  df-cvlat 37784  df-hlat 37813  df-llines 37961  df-lplanes 37962  df-lvols 37963
This theorem is referenced by:  dalem45  38180
  Copyright terms: Public domain W3C validator