![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > dalem15 | Structured version Visualization version GIF version |
Description: Lemma for dath 38544. The axis of perspectivity 𝑋 is a line. (Contributed by NM, 21-Jul-2012.) |
Ref | Expression |
---|---|
dalema.ph | ⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) |
dalemc.l | ⊢ ≤ = (le‘𝐾) |
dalemc.j | ⊢ ∨ = (join‘𝐾) |
dalemc.a | ⊢ 𝐴 = (Atoms‘𝐾) |
dalem15.m | ⊢ ∧ = (meet‘𝐾) |
dalem15.n | ⊢ 𝑁 = (LLines‘𝐾) |
dalem15.o | ⊢ 𝑂 = (LPlanes‘𝐾) |
dalem15.y | ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) |
dalem15.z | ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) |
dalem15.x | ⊢ 𝑋 = (𝑌 ∧ 𝑍) |
Ref | Expression |
---|---|
dalem15 | ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑋 ∈ 𝑁) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dalem15.x | . 2 ⊢ 𝑋 = (𝑌 ∧ 𝑍) | |
2 | dalema.ph | . . . 4 ⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) | |
3 | dalemc.l | . . . 4 ⊢ ≤ = (le‘𝐾) | |
4 | dalemc.j | . . . 4 ⊢ ∨ = (join‘𝐾) | |
5 | dalemc.a | . . . 4 ⊢ 𝐴 = (Atoms‘𝐾) | |
6 | dalem15.o | . . . 4 ⊢ 𝑂 = (LPlanes‘𝐾) | |
7 | eqid 2733 | . . . 4 ⊢ (LVols‘𝐾) = (LVols‘𝐾) | |
8 | dalem15.y | . . . 4 ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) | |
9 | dalem15.z | . . . 4 ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) | |
10 | eqid 2733 | . . . 4 ⊢ (𝑌 ∨ 𝐶) = (𝑌 ∨ 𝐶) | |
11 | 2, 3, 4, 5, 6, 7, 8, 9, 10 | dalem14 38485 | . . 3 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → (𝑌 ∨ 𝑍) ∈ (LVols‘𝐾)) |
12 | 2 | dalemkehl 38431 | . . . . 5 ⊢ (𝜑 → 𝐾 ∈ HL) |
13 | 2 | dalemyeo 38440 | . . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑂) |
14 | 2 | dalemzeo 38441 | . . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑂) |
15 | dalem15.m | . . . . . 6 ⊢ ∧ = (meet‘𝐾) | |
16 | dalem15.n | . . . . . 6 ⊢ 𝑁 = (LLines‘𝐾) | |
17 | 4, 15, 16, 6, 7 | 2lplnmj 38430 | . . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) → ((𝑌 ∧ 𝑍) ∈ 𝑁 ↔ (𝑌 ∨ 𝑍) ∈ (LVols‘𝐾))) |
18 | 12, 13, 14, 17 | syl3anc 1372 | . . . 4 ⊢ (𝜑 → ((𝑌 ∧ 𝑍) ∈ 𝑁 ↔ (𝑌 ∨ 𝑍) ∈ (LVols‘𝐾))) |
19 | 18 | adantr 482 | . . 3 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → ((𝑌 ∧ 𝑍) ∈ 𝑁 ↔ (𝑌 ∨ 𝑍) ∈ (LVols‘𝐾))) |
20 | 11, 19 | mpbird 257 | . 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → (𝑌 ∧ 𝑍) ∈ 𝑁) |
21 | 1, 20 | eqeltrid 2838 | 1 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑋 ∈ 𝑁) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 class class class wbr 5146 ‘cfv 6539 (class class class)co 7403 Basecbs 17139 lecple 17199 joincjn 18259 meetcmee 18260 Atomscatm 38070 HLchlt 38157 LLinesclln 38299 LPlanesclpl 38300 LVolsclvol 38301 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5283 ax-sep 5297 ax-nul 5304 ax-pow 5361 ax-pr 5425 ax-un 7719 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3776 df-csb 3892 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4321 df-if 4527 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4907 df-iun 4997 df-br 5147 df-opab 5209 df-mpt 5230 df-id 5572 df-xp 5680 df-rel 5681 df-cnv 5682 df-co 5683 df-dm 5684 df-rn 5685 df-res 5686 df-ima 5687 df-iota 6491 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7359 df-ov 7406 df-oprab 7407 df-proset 18243 df-poset 18261 df-plt 18278 df-lub 18294 df-glb 18295 df-join 18296 df-meet 18297 df-p0 18373 df-lat 18380 df-clat 18447 df-oposet 37983 df-ol 37985 df-oml 37986 df-covers 38073 df-ats 38074 df-atl 38105 df-cvlat 38129 df-hlat 38158 df-llines 38306 df-lplanes 38307 df-lvols 38308 |
This theorem is referenced by: dalem16 38487 dalem53 38533 |
Copyright terms: Public domain | W3C validator |