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

Theorem cvlsupr3 34097
 Description: Two equivalent ways of expressing that 𝑅 is a superposition of 𝑃 and 𝑄, which can replace the superposition part of ishlat1 34105, (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦)) ), with the simpler ∃𝑧 ∈ 𝐴(𝑥 ∨ 𝑧) = (𝑦 ∨ 𝑧) as shown in ishlat3N 34107. (Contributed by NM, 5-Nov-2012.)
Hypotheses
Ref Expression
cvlsupr2.a 𝐴 = (Atoms‘𝐾)
cvlsupr2.l = (le‘𝐾)
cvlsupr2.j = (join‘𝐾)
Assertion
Ref Expression
cvlsupr3 ((𝐾 ∈ CvLat ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → ((𝑃 𝑅) = (𝑄 𝑅) ↔ (𝑃𝑄 → (𝑅𝑃𝑅𝑄𝑅 (𝑃 𝑄)))))

Proof of Theorem cvlsupr3
StepHypRef Expression
1 df-ne 2797 . . . 4 (𝑃𝑄 ↔ ¬ 𝑃 = 𝑄)
21imbi1i 339 . . 3 ((𝑃𝑄 → (𝑃 𝑅) = (𝑄 𝑅)) ↔ (¬ 𝑃 = 𝑄 → (𝑃 𝑅) = (𝑄 𝑅)))
3 oveq1 6612 . . . 4 (𝑃 = 𝑄 → (𝑃 𝑅) = (𝑄 𝑅))
43biantrur 527 . . 3 ((¬ 𝑃 = 𝑄 → (𝑃 𝑅) = (𝑄 𝑅)) ↔ ((𝑃 = 𝑄 → (𝑃 𝑅) = (𝑄 𝑅)) ∧ (¬ 𝑃 = 𝑄 → (𝑃 𝑅) = (𝑄 𝑅))))
5 pm4.83 969 . . 3 (((𝑃 = 𝑄 → (𝑃 𝑅) = (𝑄 𝑅)) ∧ (¬ 𝑃 = 𝑄 → (𝑃 𝑅) = (𝑄 𝑅))) ↔ (𝑃 𝑅) = (𝑄 𝑅))
62, 4, 53bitrri 287 . 2 ((𝑃 𝑅) = (𝑄 𝑅) ↔ (𝑃𝑄 → (𝑃 𝑅) = (𝑄 𝑅)))
7 cvlsupr2.a . . . . 5 𝐴 = (Atoms‘𝐾)
8 cvlsupr2.l . . . . 5 = (le‘𝐾)
9 cvlsupr2.j . . . . 5 = (join‘𝐾)
107, 8, 9cvlsupr2 34096 . . . 4 ((𝐾 ∈ CvLat ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ 𝑃𝑄) → ((𝑃 𝑅) = (𝑄 𝑅) ↔ (𝑅𝑃𝑅𝑄𝑅 (𝑃 𝑄))))
11103expia 1264 . . 3 ((𝐾 ∈ CvLat ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → (𝑃𝑄 → ((𝑃 𝑅) = (𝑄 𝑅) ↔ (𝑅𝑃𝑅𝑄𝑅 (𝑃 𝑄)))))
1211pm5.74d 262 . 2 ((𝐾 ∈ CvLat ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → ((𝑃𝑄 → (𝑃 𝑅) = (𝑄 𝑅)) ↔ (𝑃𝑄 → (𝑅𝑃𝑅𝑄𝑅 (𝑃 𝑄)))))
136, 12syl5bb 272 1 ((𝐾 ∈ CvLat ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → ((𝑃 𝑅) = (𝑄 𝑅) ↔ (𝑃𝑄 → (𝑅𝑃𝑅𝑄𝑅 (𝑃 𝑄)))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1992   ≠ wne 2796   class class class wbr 4618  ‘cfv 5850  (class class class)co 6605  lecple 15864  joincjn 16860  Atomscatm 34016  CvLatclc 34018 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-riota 6566  df-ov 6608  df-oprab 6609  df-preset 16844  df-poset 16862  df-plt 16874  df-lub 16890  df-glb 16891  df-join 16892  df-meet 16893  df-p0 16955  df-lat 16962  df-covers 34019  df-ats 34020  df-atl 34051  df-cvlat 34075 This theorem is referenced by:  ishlat3N  34107  hlsupr2  34139
 Copyright terms: Public domain W3C validator