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

Theorem dihmeetlem17N 37882
Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
dihmeetlem14.b 𝐵 = (Base‘𝐾)
dihmeetlem14.l = (le‘𝐾)
dihmeetlem14.h 𝐻 = (LHyp‘𝐾)
dihmeetlem14.j = (join‘𝐾)
dihmeetlem14.m = (meet‘𝐾)
dihmeetlem14.a 𝐴 = (Atoms‘𝐾)
dihmeetlem14.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
dihmeetlem14.s = (LSSum‘𝑈)
dihmeetlem14.i 𝐼 = ((DIsoH‘𝐾)‘𝑊)
dihmeetlem17.o 0 = (0.‘𝐾)
Assertion
Ref Expression
dihmeetlem17N ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → (𝑌 𝑝) = 0 )

Proof of Theorem dihmeetlem17N
StepHypRef Expression
1 simpl1l 1204 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → 𝐾 ∈ HL)
21hllatd 35923 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → 𝐾 ∈ Lat)
3 simpl3l 1208 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → 𝑝𝐴)
4 dihmeetlem14.b . . . . 5 𝐵 = (Base‘𝐾)
5 dihmeetlem14.a . . . . 5 𝐴 = (Atoms‘𝐾)
64, 5atbase 35848 . . . 4 (𝑝𝐴𝑝𝐵)
73, 6syl 17 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → 𝑝𝐵)
8 simpr1 1174 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → 𝑌𝐵)
9 dihmeetlem14.m . . . 4 = (meet‘𝐾)
104, 9latmcom 17537 . . 3 ((𝐾 ∈ Lat ∧ 𝑝𝐵𝑌𝐵) → (𝑝 𝑌) = (𝑌 𝑝))
112, 7, 8, 10syl3anc 1351 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → (𝑝 𝑌) = (𝑌 𝑝))
12 simpl1 1171 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
13 simpl2 1172 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → (𝑋𝐵 ∧ ¬ 𝑋 𝑊))
14 simpl3 1173 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → (𝑝𝐴 ∧ ¬ 𝑝 𝑊))
15 simpr2 1175 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → (𝑋 𝑌) 𝑊)
16 simpr3 1176 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → 𝑝 𝑋)
17 dihmeetlem14.l . . . . 5 = (le‘𝐾)
18 dihmeetlem14.j . . . . 5 = (join‘𝐾)
19 dihmeetlem14.h . . . . 5 𝐻 = (LHyp‘𝐾)
204, 17, 18, 9, 5, 19lhpmcvr4N 36585 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → ¬ 𝑝 𝑌)
2112, 13, 14, 8, 15, 16, 20syl123anc 1367 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → ¬ 𝑝 𝑌)
22 hlatl 35919 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
231, 22syl 17 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → 𝐾 ∈ AtLat)
24 dihmeetlem17.o . . . . 5 0 = (0.‘𝐾)
254, 17, 9, 24, 5atnle 35876 . . . 4 ((𝐾 ∈ AtLat ∧ 𝑝𝐴𝑌𝐵) → (¬ 𝑝 𝑌 ↔ (𝑝 𝑌) = 0 ))
2623, 3, 8, 25syl3anc 1351 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → (¬ 𝑝 𝑌 ↔ (𝑝 𝑌) = 0 ))
2721, 26mpbid 224 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → (𝑝 𝑌) = 0 )
2811, 27eqtr3d 2813 1 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ (𝑝𝐴 ∧ ¬ 𝑝 𝑊)) ∧ (𝑌𝐵 ∧ (𝑋 𝑌) 𝑊𝑝 𝑋)) → (𝑌 𝑝) = 0 )
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wcel 2048   class class class wbr 4927  cfv 6186  (class class class)co 6974  Basecbs 16333  lecple 16422  joincjn 17406  meetcmee 17407  0.cp0 17499  Latclat 17507  LSSumclsm 18514  Atomscatm 35822  AtLatcal 35823  HLchlt 35909  LHypclh 36543  DVecHcdvh 37637  DIsoHcdih 37787
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-rep 5047  ax-sep 5058  ax-nul 5065  ax-pow 5117  ax-pr 5184  ax-un 7277
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-ral 3090  df-rex 3091  df-reu 3092  df-rab 3094  df-v 3414  df-sbc 3681  df-csb 3786  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-nul 4178  df-if 4349  df-pw 4422  df-sn 4440  df-pr 4442  df-op 4446  df-uni 4711  df-iun 4792  df-br 4928  df-opab 4990  df-mpt 5007  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6935  df-ov 6977  df-oprab 6978  df-proset 17390  df-poset 17408  df-plt 17420  df-lub 17436  df-glb 17437  df-join 17438  df-meet 17439  df-p0 17501  df-lat 17508  df-covers 35825  df-ats 35826  df-atl 35857  df-cvlat 35881  df-hlat 35910  df-lhyp 36547
This theorem is referenced by:  dihmeetlem18N  37883
  Copyright terms: Public domain W3C validator