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

Theorem dalemrot 37283
Description: Lemma for dath 37362. Rotate triangles 𝑌 = 𝑃𝑄𝑅 and 𝑍 = 𝑆𝑇𝑈 to allow reuse of analogous proofs. (Contributed by NM, 14-Aug-2012.)
Hypotheses
Ref Expression
dalema.ph (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))))
dalemc.l = (le‘𝐾)
dalemc.j = (join‘𝐾)
dalemc.a 𝐴 = (Atoms‘𝐾)
dalemrot.y 𝑌 = ((𝑃 𝑄) 𝑅)
dalemrot.z 𝑍 = ((𝑆 𝑇) 𝑈)
Assertion
Ref Expression
dalemrot (𝜑 → (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑄𝐴𝑅𝐴𝑃𝐴) ∧ (𝑇𝐴𝑈𝐴𝑆𝐴)) ∧ (((𝑄 𝑅) 𝑃) ∈ 𝑂 ∧ ((𝑇 𝑈) 𝑆) ∈ 𝑂) ∧ ((¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃) ∧ ¬ 𝐶 (𝑃 𝑄)) ∧ (¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆) ∧ ¬ 𝐶 (𝑆 𝑇)) ∧ (𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈) ∧ 𝐶 (𝑃 𝑆)))))

Proof of Theorem dalemrot
StepHypRef Expression
1 dalema.ph . . . . 5 (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))))
21dalemkehl 37249 . . . 4 (𝜑𝐾 ∈ HL)
3 dalemc.a . . . . 5 𝐴 = (Atoms‘𝐾)
41, 3dalemceb 37264 . . . 4 (𝜑𝐶 ∈ (Base‘𝐾))
52, 4jca 515 . . 3 (𝜑 → (𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)))
61dalemqea 37253 . . . 4 (𝜑𝑄𝐴)
71dalemrea 37254 . . . 4 (𝜑𝑅𝐴)
81dalempea 37252 . . . 4 (𝜑𝑃𝐴)
96, 7, 83jca 1129 . . 3 (𝜑 → (𝑄𝐴𝑅𝐴𝑃𝐴))
101dalemtea 37256 . . . 4 (𝜑𝑇𝐴)
111dalemuea 37257 . . . 4 (𝜑𝑈𝐴)
121dalemsea 37255 . . . 4 (𝜑𝑆𝐴)
1310, 11, 123jca 1129 . . 3 (𝜑 → (𝑇𝐴𝑈𝐴𝑆𝐴))
145, 9, 133jca 1129 . 2 (𝜑 → ((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑄𝐴𝑅𝐴𝑃𝐴) ∧ (𝑇𝐴𝑈𝐴𝑆𝐴)))
15 dalemc.j . . . . 5 = (join‘𝐾)
161, 15, 3dalemqrprot 37274 . . . 4 (𝜑 → ((𝑄 𝑅) 𝑃) = ((𝑃 𝑄) 𝑅))
17 dalemrot.y . . . . 5 𝑌 = ((𝑃 𝑄) 𝑅)
181dalemyeo 37258 . . . . 5 (𝜑𝑌𝑂)
1917, 18eqeltrrid 2838 . . . 4 (𝜑 → ((𝑃 𝑄) 𝑅) ∈ 𝑂)
2016, 19eqeltrd 2833 . . 3 (𝜑 → ((𝑄 𝑅) 𝑃) ∈ 𝑂)
2115, 3hlatjrot 36999 . . . . 5 ((𝐾 ∈ HL ∧ (𝑇𝐴𝑈𝐴𝑆𝐴)) → ((𝑇 𝑈) 𝑆) = ((𝑆 𝑇) 𝑈))
222, 10, 11, 12, 21syl13anc 1373 . . . 4 (𝜑 → ((𝑇 𝑈) 𝑆) = ((𝑆 𝑇) 𝑈))
23 dalemrot.z . . . . 5 𝑍 = ((𝑆 𝑇) 𝑈)
241dalemzeo 37259 . . . . 5 (𝜑𝑍𝑂)
2523, 24eqeltrrid 2838 . . . 4 (𝜑 → ((𝑆 𝑇) 𝑈) ∈ 𝑂)
2622, 25eqeltrd 2833 . . 3 (𝜑 → ((𝑇 𝑈) 𝑆) ∈ 𝑂)
2720, 26jca 515 . 2 (𝜑 → (((𝑄 𝑅) 𝑃) ∈ 𝑂 ∧ ((𝑇 𝑈) 𝑆) ∈ 𝑂))
28 simp312 1322 . . . . 5 ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))) → ¬ 𝐶 (𝑄 𝑅))
291, 28sylbi 220 . . . 4 (𝜑 → ¬ 𝐶 (𝑄 𝑅))
30 simp313 1323 . . . . 5 ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))) → ¬ 𝐶 (𝑅 𝑃))
311, 30sylbi 220 . . . 4 (𝜑 → ¬ 𝐶 (𝑅 𝑃))
321dalem-clpjq 37263 . . . 4 (𝜑 → ¬ 𝐶 (𝑃 𝑄))
3329, 31, 323jca 1129 . . 3 (𝜑 → (¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃) ∧ ¬ 𝐶 (𝑃 𝑄)))
34 simp322 1325 . . . . 5 ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))) → ¬ 𝐶 (𝑇 𝑈))
351, 34sylbi 220 . . . 4 (𝜑 → ¬ 𝐶 (𝑇 𝑈))
36 simp323 1326 . . . . 5 ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))) → ¬ 𝐶 (𝑈 𝑆))
371, 36sylbi 220 . . . 4 (𝜑 → ¬ 𝐶 (𝑈 𝑆))
38 simp321 1324 . . . . 5 ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))) → ¬ 𝐶 (𝑆 𝑇))
391, 38sylbi 220 . . . 4 (𝜑 → ¬ 𝐶 (𝑆 𝑇))
4035, 37, 393jca 1129 . . 3 (𝜑 → (¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆) ∧ ¬ 𝐶 (𝑆 𝑇)))
411dalemclqjt 37261 . . . 4 (𝜑𝐶 (𝑄 𝑇))
421dalemclrju 37262 . . . 4 (𝜑𝐶 (𝑅 𝑈))
431dalemclpjs 37260 . . . 4 (𝜑𝐶 (𝑃 𝑆))
4441, 42, 433jca 1129 . . 3 (𝜑 → (𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈) ∧ 𝐶 (𝑃 𝑆)))
4533, 40, 443jca 1129 . 2 (𝜑 → ((¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃) ∧ ¬ 𝐶 (𝑃 𝑄)) ∧ (¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆) ∧ ¬ 𝐶 (𝑆 𝑇)) ∧ (𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈) ∧ 𝐶 (𝑃 𝑆))))
4614, 27, 453jca 1129 1 (𝜑 → (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑄𝐴𝑅𝐴𝑃𝐴) ∧ (𝑇𝐴𝑈𝐴𝑆𝐴)) ∧ (((𝑄 𝑅) 𝑃) ∈ 𝑂 ∧ ((𝑇 𝑈) 𝑆) ∈ 𝑂) ∧ ((¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃) ∧ ¬ 𝐶 (𝑃 𝑄)) ∧ (¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆) ∧ ¬ 𝐶 (𝑆 𝑇)) ∧ (𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈) ∧ 𝐶 (𝑃 𝑆)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1088   = wceq 1542  wcel 2113   class class class wbr 5027  cfv 6333  (class class class)co 7164  Basecbs 16579  lecple 16668  joincjn 17663  Atomscatm 36889  HLchlt 36976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5151  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7121  df-ov 7167  df-oprab 7168  df-proset 17647  df-poset 17665  df-lub 17693  df-glb 17694  df-join 17695  df-meet 17696  df-lat 17765  df-ats 36893  df-atl 36924  df-cvlat 36948  df-hlat 36977
This theorem is referenced by:  dalemeea  37289  dalem6  37294  dalem7  37295  dalem11  37300  dalem12  37301  dalem29  37327  dalem30  37328  dalem31N  37329  dalem32  37330  dalem33  37331  dalem34  37332  dalem35  37333  dalem36  37334  dalem37  37335  dalem40  37338  dalem46  37344  dalem47  37345  dalem49  37347  dalem50  37348  dalem58  37356  dalem59  37357
  Copyright terms: Public domain W3C validator