Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  4atex2-0cOLDN Structured version   Visualization version   GIF version

Theorem 4atex2-0cOLDN 35881
Description: Same as 4atex2 35878 except that 𝑆 and 𝑇 are zero. TODO: do we need this one or 4atex2-0aOLDN 35879 or 4atex2-0bOLDN 35880? (Contributed by NM, 27-May-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
4that.l = (le‘𝐾)
4that.j = (join‘𝐾)
4that.a 𝐴 = (Atoms‘𝐾)
4that.h 𝐻 = (LHyp‘𝐾)
Assertion
Ref Expression
4atex2-0cOLDN (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑆 = (0.‘𝐾)) ∧ (𝑃𝑄𝑇 = (0.‘𝐾) ∧ ∃𝑟𝐴𝑟 𝑊 ∧ (𝑃 𝑟) = (𝑄 𝑟)))) → ∃𝑧𝐴𝑧 𝑊 ∧ (𝑆 𝑧) = (𝑇 𝑧)))
Distinct variable groups:   𝑧,𝑟,𝐴   𝐻,𝑟   ,𝑟,𝑧   𝐾,𝑟,𝑧   ,𝑟,𝑧   𝑃,𝑟,𝑧   𝑄,𝑟,𝑧   𝑆,𝑟,𝑧   𝑊,𝑟,𝑧   𝑇,𝑟,𝑧   𝑧,𝐻

Proof of Theorem 4atex2-0cOLDN
StepHypRef Expression
1 simp21l 1374 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑆 = (0.‘𝐾)) ∧ (𝑃𝑄𝑇 = (0.‘𝐾) ∧ ∃𝑟𝐴𝑟 𝑊 ∧ (𝑃 𝑟) = (𝑄 𝑟)))) → 𝑃𝐴)
2 simp21r 1375 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑆 = (0.‘𝐾)) ∧ (𝑃𝑄𝑇 = (0.‘𝐾) ∧ ∃𝑟𝐴𝑟 𝑊 ∧ (𝑃 𝑟) = (𝑄 𝑟)))) → ¬ 𝑃 𝑊)
3 simp23 1250 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑆 = (0.‘𝐾)) ∧ (𝑃𝑄𝑇 = (0.‘𝐾) ∧ ∃𝑟𝐴𝑟 𝑊 ∧ (𝑃 𝑟) = (𝑄 𝑟)))) → 𝑆 = (0.‘𝐾))
43oveq1d 6806 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑆 = (0.‘𝐾)) ∧ (𝑃𝑄𝑇 = (0.‘𝐾) ∧ ∃𝑟𝐴𝑟 𝑊 ∧ (𝑃 𝑟) = (𝑄 𝑟)))) → (𝑆 𝑃) = ((0.‘𝐾) 𝑃))
5 simp32 1252 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑆 = (0.‘𝐾)) ∧ (𝑃𝑄𝑇 = (0.‘𝐾) ∧ ∃𝑟𝐴𝑟 𝑊 ∧ (𝑃 𝑟) = (𝑄 𝑟)))) → 𝑇 = (0.‘𝐾))
65oveq1d 6806 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑆 = (0.‘𝐾)) ∧ (𝑃𝑄𝑇 = (0.‘𝐾) ∧ ∃𝑟𝐴𝑟 𝑊 ∧ (𝑃 𝑟) = (𝑄 𝑟)))) → (𝑇 𝑃) = ((0.‘𝐾) 𝑃))
74, 6eqtr4d 2808 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑆 = (0.‘𝐾)) ∧ (𝑃𝑄𝑇 = (0.‘𝐾) ∧ ∃𝑟𝐴𝑟 𝑊 ∧ (𝑃 𝑟) = (𝑄 𝑟)))) → (𝑆 𝑃) = (𝑇 𝑃))
8 breq1 4789 . . . . 5 (𝑧 = 𝑃 → (𝑧 𝑊𝑃 𝑊))
98notbid 307 . . . 4 (𝑧 = 𝑃 → (¬ 𝑧 𝑊 ↔ ¬ 𝑃 𝑊))
10 oveq2 6799 . . . . 5 (𝑧 = 𝑃 → (𝑆 𝑧) = (𝑆 𝑃))
11 oveq2 6799 . . . . 5 (𝑧 = 𝑃 → (𝑇 𝑧) = (𝑇 𝑃))
1210, 11eqeq12d 2786 . . . 4 (𝑧 = 𝑃 → ((𝑆 𝑧) = (𝑇 𝑧) ↔ (𝑆 𝑃) = (𝑇 𝑃)))
139, 12anbi12d 616 . . 3 (𝑧 = 𝑃 → ((¬ 𝑧 𝑊 ∧ (𝑆 𝑧) = (𝑇 𝑧)) ↔ (¬ 𝑃 𝑊 ∧ (𝑆 𝑃) = (𝑇 𝑃))))
1413rspcev 3460 . 2 ((𝑃𝐴 ∧ (¬ 𝑃 𝑊 ∧ (𝑆 𝑃) = (𝑇 𝑃))) → ∃𝑧𝐴𝑧 𝑊 ∧ (𝑆 𝑧) = (𝑇 𝑧)))
151, 2, 7, 14syl12anc 1474 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝑆 = (0.‘𝐾)) ∧ (𝑃𝑄𝑇 = (0.‘𝐾) ∧ ∃𝑟𝐴𝑟 𝑊 ∧ (𝑃 𝑟) = (𝑄 𝑟)))) → ∃𝑧𝐴𝑧 𝑊 ∧ (𝑆 𝑧) = (𝑇 𝑧)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wrex 3062   class class class wbr 4786  cfv 6029  (class class class)co 6791  lecple 16149  joincjn 17145  0.cp0 17238  Atomscatm 35065  HLchlt 35152  LHypclh 35785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-iota 5992  df-fv 6037  df-ov 6794
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator