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

Theorem cdlemg7fvbwN 37228
Description: Properties of a translation of an element not under 𝑊. TODO: Fix comment. Can this be simplified? Perhaps derived from cdleme48bw 37123? Done with a *ltrn* theorem? (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
cdlemg4.l = (le‘𝐾)
cdlemg4.a 𝐴 = (Atoms‘𝐾)
cdlemg4.h 𝐻 = (LHyp‘𝐾)
cdlemg4.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemg4.b 𝐵 = (Base‘𝐾)
Assertion
Ref Expression
cdlemg7fvbwN (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) → ((𝐹𝑋) ∈ 𝐵 ∧ ¬ (𝐹𝑋) 𝑊))

Proof of Theorem cdlemg7fvbwN
Dummy variable 𝑟 is distinct from all other variables.
StepHypRef Expression
1 cdlemg4.b . . . 4 𝐵 = (Base‘𝐾)
2 cdlemg4.l . . . 4 = (le‘𝐾)
3 eqid 2780 . . . 4 (join‘𝐾) = (join‘𝐾)
4 eqid 2780 . . . 4 (meet‘𝐾) = (meet‘𝐾)
5 cdlemg4.a . . . 4 𝐴 = (Atoms‘𝐾)
6 cdlemg4.h . . . 4 𝐻 = (LHyp‘𝐾)
71, 2, 3, 4, 5, 6lhpmcvr2 36645 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊)) → ∃𝑟𝐴𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋))
873adant3 1113 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) → ∃𝑟𝐴𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋))
9 simp11 1184 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
10 simp2 1118 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → 𝑟𝐴)
11 simp3l 1182 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → ¬ 𝑟 𝑊)
1210, 11jca 504 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝑟𝐴 ∧ ¬ 𝑟 𝑊))
13 simp12 1185 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝑋𝐵 ∧ ¬ 𝑋 𝑊))
14 simp13 1186 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → 𝐹𝑇)
15 simp3r 1183 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)
16 cdlemg4.t . . . . . . 7 𝑇 = ((LTrn‘𝐾)‘𝑊)
176, 16, 2, 3, 5, 4, 1cdlemg2fv 37220 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊)) ∧ (𝐹𝑇 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝐹𝑋) = ((𝐹𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)))
189, 12, 13, 14, 15, 17syl122anc 1360 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝐹𝑋) = ((𝐹𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)))
19 simp11l 1265 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → 𝐾 ∈ HL)
2019hllatd 35985 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → 𝐾 ∈ Lat)
212, 5, 6, 16ltrnel 36760 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑟𝐴 ∧ ¬ 𝑟 𝑊)) → ((𝐹𝑟) ∈ 𝐴 ∧ ¬ (𝐹𝑟) 𝑊))
2221simpld 487 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑟𝐴 ∧ ¬ 𝑟 𝑊)) → (𝐹𝑟) ∈ 𝐴)
239, 14, 12, 22syl3anc 1352 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝐹𝑟) ∈ 𝐴)
241, 5atbase 35910 . . . . . . 7 ((𝐹𝑟) ∈ 𝐴 → (𝐹𝑟) ∈ 𝐵)
2523, 24syl 17 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝐹𝑟) ∈ 𝐵)
26 simp12l 1267 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → 𝑋𝐵)
27 simp11r 1266 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → 𝑊𝐻)
281, 6lhpbase 36619 . . . . . . . 8 (𝑊𝐻𝑊𝐵)
2927, 28syl 17 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → 𝑊𝐵)
301, 4latmcl 17532 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑊𝐵) → (𝑋(meet‘𝐾)𝑊) ∈ 𝐵)
3120, 26, 29, 30syl3anc 1352 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝑋(meet‘𝐾)𝑊) ∈ 𝐵)
321, 3latjcl 17531 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝐹𝑟) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)𝑊) ∈ 𝐵) → ((𝐹𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) ∈ 𝐵)
3320, 25, 31, 32syl3anc 1352 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → ((𝐹𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) ∈ 𝐵)
3418, 33eqeltrd 2868 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝐹𝑋) ∈ 𝐵)
3521simprd 488 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑟𝐴 ∧ ¬ 𝑟 𝑊)) → ¬ (𝐹𝑟) 𝑊)
369, 14, 12, 35syl3anc 1352 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → ¬ (𝐹𝑟) 𝑊)
371, 2, 3latlej1 17540 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝐹𝑟) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)𝑊) ∈ 𝐵) → (𝐹𝑟) ((𝐹𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)))
3820, 25, 31, 37syl3anc 1352 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝐹𝑟) ((𝐹𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)))
391, 2lattr 17536 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((𝐹𝑟) ∈ 𝐵 ∧ ((𝐹𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) ∈ 𝐵𝑊𝐵)) → (((𝐹𝑟) ((𝐹𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) ∧ ((𝐹𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) 𝑊) → (𝐹𝑟) 𝑊))
4020, 25, 33, 29, 39syl13anc 1353 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (((𝐹𝑟) ((𝐹𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) ∧ ((𝐹𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) 𝑊) → (𝐹𝑟) 𝑊))
4138, 40mpand 683 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (((𝐹𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) 𝑊 → (𝐹𝑟) 𝑊))
4236, 41mtod 190 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → ¬ ((𝐹𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) 𝑊)
4318breq1d 4944 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → ((𝐹𝑋) 𝑊 ↔ ((𝐹𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) 𝑊))
4442, 43mtbird 317 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → ¬ (𝐹𝑋) 𝑊)
4534, 44jca 504 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) ∧ 𝑟𝐴 ∧ (¬ 𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → ((𝐹𝑋) ∈ 𝐵 ∧ ¬ (𝐹𝑋) 𝑊))
4645rexlimdv3a 3233 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) → (∃𝑟𝐴𝑟 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋) → ((𝐹𝑋) ∈ 𝐵 ∧ ¬ (𝐹𝑋) 𝑊)))
478, 46mpd 15 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ 𝐹𝑇) → ((𝐹𝑋) ∈ 𝐵 ∧ ¬ (𝐹𝑋) 𝑊))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 387  w3a 1069   = wceq 1508  wcel 2051  wrex 3091   class class class wbr 4934  cfv 6193  (class class class)co 6982  Basecbs 16345  lecple 16434  joincjn 17424  meetcmee 17425  Latclat 17525  Atomscatm 35884  HLchlt 35971  LHypclh 36605  LTrncltrn 36722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2752  ax-rep 5053  ax-sep 5064  ax-nul 5071  ax-pow 5123  ax-pr 5190  ax-un 7285  ax-riotaBAD 35574
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2551  df-eu 2589  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3419  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4182  df-if 4354  df-pw 4427  df-sn 4445  df-pr 4447  df-op 4451  df-uni 4718  df-iun 4799  df-iin 4800  df-br 4935  df-opab 4997  df-mpt 5014  df-id 5316  df-xp 5417  df-rel 5418  df-cnv 5419  df-co 5420  df-dm 5421  df-rn 5422  df-res 5423  df-ima 5424  df-iota 6157  df-fun 6195  df-fn 6196  df-f 6197  df-f1 6198  df-fo 6199  df-f1o 6200  df-fv 6201  df-riota 6943  df-ov 6985  df-oprab 6986  df-mpo 6987  df-1st 7507  df-2nd 7508  df-undef 7748  df-map 8214  df-proset 17408  df-poset 17426  df-plt 17438  df-lub 17454  df-glb 17455  df-join 17456  df-meet 17457  df-p0 17519  df-p1 17520  df-lat 17526  df-clat 17588  df-oposet 35797  df-ol 35799  df-oml 35800  df-covers 35887  df-ats 35888  df-atl 35919  df-cvlat 35943  df-hlat 35972  df-llines 36119  df-lplanes 36120  df-lvols 36121  df-lines 36122  df-psubsp 36124  df-pmap 36125  df-padd 36417  df-lhyp 36609  df-laut 36610  df-ldil 36725  df-ltrn 36726  df-trl 36780
This theorem is referenced by:  cdlemg7fvN  37245
  Copyright terms: Public domain W3C validator