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

Theorem dalem39 38030
Description: Lemma for dath 38055. Auxiliary atoms 𝐺, 𝐻, and 𝐼 are not colinear. (Contributed by NM, 4-Aug-2012.)
Hypotheses
Ref Expression
dalem.ph (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))))
dalem.l = (le‘𝐾)
dalem.j = (join‘𝐾)
dalem.a 𝐴 = (Atoms‘𝐾)
dalem.ps (𝜓 ↔ ((𝑐𝐴𝑑𝐴) ∧ ¬ 𝑐 𝑌 ∧ (𝑑𝑐 ∧ ¬ 𝑑 𝑌𝐶 (𝑐 𝑑))))
dalem38.m = (meet‘𝐾)
dalem38.o 𝑂 = (LPlanes‘𝐾)
dalem38.y 𝑌 = ((𝑃 𝑄) 𝑅)
dalem38.z 𝑍 = ((𝑆 𝑇) 𝑈)
dalem38.g 𝐺 = ((𝑐 𝑃) (𝑑 𝑆))
dalem38.h 𝐻 = ((𝑐 𝑄) (𝑑 𝑇))
dalem38.i 𝐼 = ((𝑐 𝑅) (𝑑 𝑈))
Assertion
Ref Expression
dalem39 ((𝜑𝑌 = 𝑍𝜓) → ¬ 𝐻 (𝐼 𝐺))

Proof of Theorem dalem39
StepHypRef Expression
1 dalem.ph . . . . 5 (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))))
21dalemkehl 37942 . . . 4 (𝜑𝐾 ∈ HL)
323ad2ant1 1132 . . 3 ((𝜑𝑌 = 𝑍𝜓) → 𝐾 ∈ HL)
41dalemyeo 37951 . . . . 5 (𝜑𝑌𝑂)
543ad2ant1 1132 . . . 4 ((𝜑𝑌 = 𝑍𝜓) → 𝑌𝑂)
6 dalem.ps . . . . . 6 (𝜓 ↔ ((𝑐𝐴𝑑𝐴) ∧ ¬ 𝑐 𝑌 ∧ (𝑑𝑐 ∧ ¬ 𝑑 𝑌𝐶 (𝑐 𝑑))))
76dalemccea 38002 . . . . 5 (𝜓𝑐𝐴)
873ad2ant3 1134 . . . 4 ((𝜑𝑌 = 𝑍𝜓) → 𝑐𝐴)
96dalem-ccly 38004 . . . . 5 (𝜓 → ¬ 𝑐 𝑌)
1093ad2ant3 1134 . . . 4 ((𝜑𝑌 = 𝑍𝜓) → ¬ 𝑐 𝑌)
11 dalem.l . . . . 5 = (le‘𝐾)
12 dalem.j . . . . 5 = (join‘𝐾)
13 dalem.a . . . . 5 𝐴 = (Atoms‘𝐾)
14 dalem38.o . . . . 5 𝑂 = (LPlanes‘𝐾)
15 eqid 2736 . . . . 5 (LVols‘𝐾) = (LVols‘𝐾)
1611, 12, 13, 14, 15lvoli3 37896 . . . 4 (((𝐾 ∈ HL ∧ 𝑌𝑂𝑐𝐴) ∧ ¬ 𝑐 𝑌) → (𝑌 𝑐) ∈ (LVols‘𝐾))
173, 5, 8, 10, 16syl31anc 1372 . . 3 ((𝜑𝑌 = 𝑍𝜓) → (𝑌 𝑐) ∈ (LVols‘𝐾))
18 dalem38.m . . . 4 = (meet‘𝐾)
19 dalem38.y . . . 4 𝑌 = ((𝑃 𝑄) 𝑅)
20 dalem38.z . . . 4 𝑍 = ((𝑆 𝑇) 𝑈)
21 dalem38.i . . . 4 𝐼 = ((𝑐 𝑅) (𝑑 𝑈))
221, 11, 12, 13, 6, 18, 14, 19, 20, 21dalem34 38025 . . 3 ((𝜑𝑌 = 𝑍𝜓) → 𝐼𝐴)
23 dalem38.g . . . 4 𝐺 = ((𝑐 𝑃) (𝑑 𝑆))
241, 11, 12, 13, 6, 18, 14, 19, 20, 23dalem23 38015 . . 3 ((𝜑𝑌 = 𝑍𝜓) → 𝐺𝐴)
2511, 12, 13, 15lvolnle3at 37901 . . 3 (((𝐾 ∈ HL ∧ (𝑌 𝑐) ∈ (LVols‘𝐾)) ∧ (𝐼𝐴𝐺𝐴𝑐𝐴)) → ¬ (𝑌 𝑐) ((𝐼 𝐺) 𝑐))
263, 17, 22, 24, 8, 25syl23anc 1376 . 2 ((𝜑𝑌 = 𝑍𝜓) → ¬ (𝑌 𝑐) ((𝐼 𝐺) 𝑐))
27 dalem38.h . . . . . . 7 𝐻 = ((𝑐 𝑄) (𝑑 𝑇))
281, 11, 12, 13, 6, 18, 14, 19, 20, 23, 27, 21dalem38 38029 . . . . . 6 ((𝜑𝑌 = 𝑍𝜓) → 𝑌 (((𝐺 𝐻) 𝐼) 𝑐))
291dalemkelat 37943 . . . . . . . 8 (𝜑𝐾 ∈ Lat)
30293ad2ant1 1132 . . . . . . 7 ((𝜑𝑌 = 𝑍𝜓) → 𝐾 ∈ Lat)
311, 11, 12, 13, 6, 18, 14, 19, 20, 27dalem29 38020 . . . . . . . . 9 ((𝜑𝑌 = 𝑍𝜓) → 𝐻𝐴)
32 eqid 2736 . . . . . . . . . 10 (Base‘𝐾) = (Base‘𝐾)
3332, 12, 13hlatjcl 37685 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝐺𝐴𝐻𝐴) → (𝐺 𝐻) ∈ (Base‘𝐾))
343, 24, 31, 33syl3anc 1370 . . . . . . . 8 ((𝜑𝑌 = 𝑍𝜓) → (𝐺 𝐻) ∈ (Base‘𝐾))
3532, 13atbase 37607 . . . . . . . . 9 (𝐼𝐴𝐼 ∈ (Base‘𝐾))
3622, 35syl 17 . . . . . . . 8 ((𝜑𝑌 = 𝑍𝜓) → 𝐼 ∈ (Base‘𝐾))
3732, 12latjcl 18255 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝐺 𝐻) ∈ (Base‘𝐾) ∧ 𝐼 ∈ (Base‘𝐾)) → ((𝐺 𝐻) 𝐼) ∈ (Base‘𝐾))
3830, 34, 36, 37syl3anc 1370 . . . . . . 7 ((𝜑𝑌 = 𝑍𝜓) → ((𝐺 𝐻) 𝐼) ∈ (Base‘𝐾))
396, 13dalemcceb 38008 . . . . . . . 8 (𝜓𝑐 ∈ (Base‘𝐾))
40393ad2ant3 1134 . . . . . . 7 ((𝜑𝑌 = 𝑍𝜓) → 𝑐 ∈ (Base‘𝐾))
4132, 11, 12latlej2 18265 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((𝐺 𝐻) 𝐼) ∈ (Base‘𝐾) ∧ 𝑐 ∈ (Base‘𝐾)) → 𝑐 (((𝐺 𝐻) 𝐼) 𝑐))
4230, 38, 40, 41syl3anc 1370 . . . . . 6 ((𝜑𝑌 = 𝑍𝜓) → 𝑐 (((𝐺 𝐻) 𝐼) 𝑐))
431, 14dalemyeb 37968 . . . . . . . 8 (𝜑𝑌 ∈ (Base‘𝐾))
44433ad2ant1 1132 . . . . . . 7 ((𝜑𝑌 = 𝑍𝜓) → 𝑌 ∈ (Base‘𝐾))
4532, 12latjcl 18255 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((𝐺 𝐻) 𝐼) ∈ (Base‘𝐾) ∧ 𝑐 ∈ (Base‘𝐾)) → (((𝐺 𝐻) 𝐼) 𝑐) ∈ (Base‘𝐾))
4630, 38, 40, 45syl3anc 1370 . . . . . . 7 ((𝜑𝑌 = 𝑍𝜓) → (((𝐺 𝐻) 𝐼) 𝑐) ∈ (Base‘𝐾))
4732, 11, 12latjle12 18266 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑌 ∈ (Base‘𝐾) ∧ 𝑐 ∈ (Base‘𝐾) ∧ (((𝐺 𝐻) 𝐼) 𝑐) ∈ (Base‘𝐾))) → ((𝑌 (((𝐺 𝐻) 𝐼) 𝑐) ∧ 𝑐 (((𝐺 𝐻) 𝐼) 𝑐)) ↔ (𝑌 𝑐) (((𝐺 𝐻) 𝐼) 𝑐)))
4830, 44, 40, 46, 47syl13anc 1371 . . . . . 6 ((𝜑𝑌 = 𝑍𝜓) → ((𝑌 (((𝐺 𝐻) 𝐼) 𝑐) ∧ 𝑐 (((𝐺 𝐻) 𝐼) 𝑐)) ↔ (𝑌 𝑐) (((𝐺 𝐻) 𝐼) 𝑐)))
4928, 42, 48mpbi2and 709 . . . . 5 ((𝜑𝑌 = 𝑍𝜓) → (𝑌 𝑐) (((𝐺 𝐻) 𝐼) 𝑐))
5012, 13hlatjrot 37691 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝐺𝐴𝐻𝐴𝐼𝐴)) → ((𝐺 𝐻) 𝐼) = ((𝐼 𝐺) 𝐻))
513, 24, 31, 22, 50syl13anc 1371 . . . . . 6 ((𝜑𝑌 = 𝑍𝜓) → ((𝐺 𝐻) 𝐼) = ((𝐼 𝐺) 𝐻))
5251oveq1d 7353 . . . . 5 ((𝜑𝑌 = 𝑍𝜓) → (((𝐺 𝐻) 𝐼) 𝑐) = (((𝐼 𝐺) 𝐻) 𝑐))
5349, 52breqtrd 5119 . . . 4 ((𝜑𝑌 = 𝑍𝜓) → (𝑌 𝑐) (((𝐼 𝐺) 𝐻) 𝑐))
5453adantr 481 . . 3 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝐻 (𝐼 𝐺)) → (𝑌 𝑐) (((𝐼 𝐺) 𝐻) 𝑐))
5532, 13atbase 37607 . . . . . . 7 (𝐻𝐴𝐻 ∈ (Base‘𝐾))
5631, 55syl 17 . . . . . 6 ((𝜑𝑌 = 𝑍𝜓) → 𝐻 ∈ (Base‘𝐾))
5732, 12, 13hlatjcl 37685 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝐼𝐴𝐺𝐴) → (𝐼 𝐺) ∈ (Base‘𝐾))
583, 22, 24, 57syl3anc 1370 . . . . . 6 ((𝜑𝑌 = 𝑍𝜓) → (𝐼 𝐺) ∈ (Base‘𝐾))
5932, 11, 12latleeqj2 18268 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝐻 ∈ (Base‘𝐾) ∧ (𝐼 𝐺) ∈ (Base‘𝐾)) → (𝐻 (𝐼 𝐺) ↔ ((𝐼 𝐺) 𝐻) = (𝐼 𝐺)))
6030, 56, 58, 59syl3anc 1370 . . . . 5 ((𝜑𝑌 = 𝑍𝜓) → (𝐻 (𝐼 𝐺) ↔ ((𝐼 𝐺) 𝐻) = (𝐼 𝐺)))
6160biimpa 477 . . . 4 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝐻 (𝐼 𝐺)) → ((𝐼 𝐺) 𝐻) = (𝐼 𝐺))
6261oveq1d 7353 . . 3 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝐻 (𝐼 𝐺)) → (((𝐼 𝐺) 𝐻) 𝑐) = ((𝐼 𝐺) 𝑐))
6354, 62breqtrd 5119 . 2 (((𝜑𝑌 = 𝑍𝜓) ∧ 𝐻 (𝐼 𝐺)) → (𝑌 𝑐) ((𝐼 𝐺) 𝑐))
6426, 63mtand 813 1 ((𝜑𝑌 = 𝑍𝜓) → ¬ 𝐻 (𝐼 𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wcel 2105  wne 2940   class class class wbr 5093  cfv 6480  (class class class)co 7338  Basecbs 17010  lecple 17067  joincjn 18127  meetcmee 18128  Latclat 18247  Atomscatm 37581  HLchlt 37668  LPlanesclpl 37811  LVolsclvol 37812
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-iun 4944  df-br 5094  df-opab 5156  df-mpt 5177  df-id 5519  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-riota 7294  df-ov 7341  df-oprab 7342  df-proset 18111  df-poset 18129  df-plt 18146  df-lub 18162  df-glb 18163  df-join 18164  df-meet 18165  df-p0 18241  df-lat 18248  df-clat 18315  df-oposet 37494  df-ol 37496  df-oml 37497  df-covers 37584  df-ats 37585  df-atl 37616  df-cvlat 37640  df-hlat 37669  df-llines 37817  df-lplanes 37818  df-lvols 37819
This theorem is referenced by:  dalem40  38031  dalem41  38032
  Copyright terms: Public domain W3C validator