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

Theorem dalem52 38300
Description: Lemma for dath 38312. Lines 𝐺𝐻 and 𝑃𝑄 intersect at an atom. (Contributed by NM, 8-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
dalem52 ((𝜑𝑌 = 𝑍𝜓) → ((𝐺 𝐻) (𝑃 𝑄)) ∈ 𝐴)

Proof of Theorem dalem52
StepHypRef Expression
1 dalem.ph . . . . 5 (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))))
21dalemkehl 38199 . . . 4 (𝜑𝐾 ∈ HL)
323ad2ant1 1133 . . 3 ((𝜑𝑌 = 𝑍𝜓) → 𝐾 ∈ HL)
4 dalem.ps . . . . 5 (𝜓 ↔ ((𝑐𝐴𝑑𝐴) ∧ ¬ 𝑐 𝑌 ∧ (𝑑𝑐 ∧ ¬ 𝑑 𝑌𝐶 (𝑐 𝑑))))
5 dalem.a . . . . 5 𝐴 = (Atoms‘𝐾)
64, 5dalemcceb 38265 . . . 4 (𝜓𝑐 ∈ (Base‘𝐾))
763ad2ant3 1135 . . 3 ((𝜑𝑌 = 𝑍𝜓) → 𝑐 ∈ (Base‘𝐾))
83, 7jca 512 . 2 ((𝜑𝑌 = 𝑍𝜓) → (𝐾 ∈ HL ∧ 𝑐 ∈ (Base‘𝐾)))
9 dalem.l . . . 4 = (le‘𝐾)
10 dalem.j . . . 4 = (join‘𝐾)
11 dalem44.m . . . 4 = (meet‘𝐾)
12 dalem44.o . . . 4 𝑂 = (LPlanes‘𝐾)
13 dalem44.y . . . 4 𝑌 = ((𝑃 𝑄) 𝑅)
14 dalem44.z . . . 4 𝑍 = ((𝑆 𝑇) 𝑈)
15 dalem44.g . . . 4 𝐺 = ((𝑐 𝑃) (𝑑 𝑆))
161, 9, 10, 5, 4, 11, 12, 13, 14, 15dalem23 38272 . . 3 ((𝜑𝑌 = 𝑍𝜓) → 𝐺𝐴)
17 dalem44.h . . . 4 𝐻 = ((𝑐 𝑄) (𝑑 𝑇))
181, 9, 10, 5, 4, 11, 12, 13, 14, 17dalem29 38277 . . 3 ((𝜑𝑌 = 𝑍𝜓) → 𝐻𝐴)
19 dalem44.i . . . 4 𝐼 = ((𝑐 𝑅) (𝑑 𝑈))
201, 9, 10, 5, 4, 11, 12, 13, 14, 19dalem34 38282 . . 3 ((𝜑𝑌 = 𝑍𝜓) → 𝐼𝐴)
2116, 18, 203jca 1128 . 2 ((𝜑𝑌 = 𝑍𝜓) → (𝐺𝐴𝐻𝐴𝐼𝐴))
221dalempea 38202 . . . 4 (𝜑𝑃𝐴)
231dalemqea 38203 . . . 4 (𝜑𝑄𝐴)
241dalemrea 38204 . . . 4 (𝜑𝑅𝐴)
2522, 23, 243jca 1128 . . 3 (𝜑 → (𝑃𝐴𝑄𝐴𝑅𝐴))
26253ad2ant1 1133 . 2 ((𝜑𝑌 = 𝑍𝜓) → (𝑃𝐴𝑄𝐴𝑅𝐴))
271, 9, 10, 5, 4, 11, 12, 13, 14, 15, 17, 19dalem42 38290 . 2 ((𝜑𝑌 = 𝑍𝜓) → ((𝐺 𝐻) 𝐼) ∈ 𝑂)
281dalemyeo 38208 . . 3 (𝜑𝑌𝑂)
29283ad2ant1 1133 . 2 ((𝜑𝑌 = 𝑍𝜓) → 𝑌𝑂)
301, 9, 10, 5, 4, 11, 12, 13, 14, 15, 17, 19dalem45 38293 . . 3 ((𝜑𝑌 = 𝑍𝜓) → ¬ 𝑐 (𝐺 𝐻))
311, 9, 10, 5, 4, 11, 12, 13, 14, 15, 17, 19dalem46 38294 . . 3 ((𝜑𝑌 = 𝑍𝜓) → ¬ 𝑐 (𝐻 𝐼))
321, 9, 10, 5, 4, 11, 12, 13, 14, 15, 17, 19dalem47 38295 . . 3 ((𝜑𝑌 = 𝑍𝜓) → ¬ 𝑐 (𝐼 𝐺))
3330, 31, 323jca 1128 . 2 ((𝜑𝑌 = 𝑍𝜓) → (¬ 𝑐 (𝐺 𝐻) ∧ ¬ 𝑐 (𝐻 𝐼) ∧ ¬ 𝑐 (𝐼 𝐺)))
341, 9, 10, 5, 4, 11, 12, 13, 14, 15, 17, 19dalem48 38296 . . . 4 ((𝜑𝜓) → ¬ 𝑐 (𝑃 𝑄))
351, 9, 10, 5, 4, 11, 12, 13, 14, 15, 17, 19dalem49 38297 . . . 4 ((𝜑𝜓) → ¬ 𝑐 (𝑄 𝑅))
361, 9, 10, 5, 4, 11, 12, 13, 14, 15, 17, 19dalem50 38298 . . . 4 ((𝜑𝜓) → ¬ 𝑐 (𝑅 𝑃))
3734, 35, 363jca 1128 . . 3 ((𝜑𝜓) → (¬ 𝑐 (𝑃 𝑄) ∧ ¬ 𝑐 (𝑄 𝑅) ∧ ¬ 𝑐 (𝑅 𝑃)))
38373adant2 1131 . 2 ((𝜑𝑌 = 𝑍𝜓) → (¬ 𝑐 (𝑃 𝑄) ∧ ¬ 𝑐 (𝑄 𝑅) ∧ ¬ 𝑐 (𝑅 𝑃)))
391, 9, 10, 5, 4, 11, 12, 13, 14, 15dalem27 38275 . . 3 ((𝜑𝑌 = 𝑍𝜓) → 𝑐 (𝐺 𝑃))
401, 9, 10, 5, 4, 11, 12, 13, 14, 17dalem32 38280 . . 3 ((𝜑𝑌 = 𝑍𝜓) → 𝑐 (𝐻 𝑄))
411, 9, 10, 5, 4, 11, 12, 13, 14, 19dalem36 38284 . . 3 ((𝜑𝑌 = 𝑍𝜓) → 𝑐 (𝐼 𝑅))
4239, 40, 413jca 1128 . 2 ((𝜑𝑌 = 𝑍𝜓) → (𝑐 (𝐺 𝑃) ∧ 𝑐 (𝐻 𝑄) ∧ 𝑐 (𝐼 𝑅)))
43 biid 260 . . 3 ((((𝐾 ∈ HL ∧ 𝑐 ∈ (Base‘𝐾)) ∧ (𝐺𝐴𝐻𝐴𝐼𝐴) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) ∧ (((𝐺 𝐻) 𝐼) ∈ 𝑂𝑌𝑂) ∧ ((¬ 𝑐 (𝐺 𝐻) ∧ ¬ 𝑐 (𝐻 𝐼) ∧ ¬ 𝑐 (𝐼 𝐺)) ∧ (¬ 𝑐 (𝑃 𝑄) ∧ ¬ 𝑐 (𝑄 𝑅) ∧ ¬ 𝑐 (𝑅 𝑃)) ∧ (𝑐 (𝐺 𝑃) ∧ 𝑐 (𝐻 𝑄) ∧ 𝑐 (𝐼 𝑅)))) ↔ (((𝐾 ∈ HL ∧ 𝑐 ∈ (Base‘𝐾)) ∧ (𝐺𝐴𝐻𝐴𝐼𝐴) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) ∧ (((𝐺 𝐻) 𝐼) ∈ 𝑂𝑌𝑂) ∧ ((¬ 𝑐 (𝐺 𝐻) ∧ ¬ 𝑐 (𝐻 𝐼) ∧ ¬ 𝑐 (𝐼 𝐺)) ∧ (¬ 𝑐 (𝑃 𝑄) ∧ ¬ 𝑐 (𝑄 𝑅) ∧ ¬ 𝑐 (𝑅 𝑃)) ∧ (𝑐 (𝐺 𝑃) ∧ 𝑐 (𝐻 𝑄) ∧ 𝑐 (𝐼 𝑅)))))
44 eqid 2731 . . 3 ((𝐺 𝐻) 𝐼) = ((𝐺 𝐻) 𝐼)
45 eqid 2731 . . 3 ((𝐺 𝐻) (𝑃 𝑄)) = ((𝐺 𝐻) (𝑃 𝑄))
4643, 9, 10, 5, 11, 12, 44, 13, 45dalemdea 38238 . 2 ((((𝐾 ∈ HL ∧ 𝑐 ∈ (Base‘𝐾)) ∧ (𝐺𝐴𝐻𝐴𝐼𝐴) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) ∧ (((𝐺 𝐻) 𝐼) ∈ 𝑂𝑌𝑂) ∧ ((¬ 𝑐 (𝐺 𝐻) ∧ ¬ 𝑐 (𝐻 𝐼) ∧ ¬ 𝑐 (𝐼 𝐺)) ∧ (¬ 𝑐 (𝑃 𝑄) ∧ ¬ 𝑐 (𝑄 𝑅) ∧ ¬ 𝑐 (𝑅 𝑃)) ∧ (𝑐 (𝐺 𝑃) ∧ 𝑐 (𝐻 𝑄) ∧ 𝑐 (𝐼 𝑅)))) → ((𝐺 𝐻) (𝑃 𝑄)) ∈ 𝐴)
478, 21, 26, 27, 29, 33, 38, 42, 46syl323anc 1400 1 ((𝜑𝑌 = 𝑍𝜓) → ((𝐺 𝐻) (𝑃 𝑄)) ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2939   class class class wbr 5132  cfv 6523  (class class class)co 7384  Basecbs 17116  lecple 17176  joincjn 18236  meetcmee 18237  Atomscatm 37838  HLchlt 37925  LPlanesclpl 38068
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 2702  ax-rep 5269  ax-sep 5283  ax-nul 5290  ax-pow 5347  ax-pr 5411  ax-un 7699
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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3372  df-rab 3426  df-v 3468  df-sbc 3765  df-csb 3881  df-dif 3938  df-un 3940  df-in 3942  df-ss 3952  df-nul 4310  df-if 4514  df-pw 4589  df-sn 4614  df-pr 4616  df-op 4620  df-uni 4893  df-iun 4983  df-br 5133  df-opab 5195  df-mpt 5216  df-id 5558  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-iota 6475  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-riota 7340  df-ov 7387  df-oprab 7388  df-proset 18220  df-poset 18238  df-plt 18255  df-lub 18271  df-glb 18272  df-join 18273  df-meet 18274  df-p0 18350  df-lat 18357  df-clat 18424  df-oposet 37751  df-ol 37753  df-oml 37754  df-covers 37841  df-ats 37842  df-atl 37873  df-cvlat 37897  df-hlat 37926  df-llines 38074  df-lplanes 38075  df-lvols 38076
This theorem is referenced by:  dalem54  38302  dalem55  38303
  Copyright terms: Public domain W3C validator