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

Theorem atmod1i1m 37427
 Description: Version of modular law pmod1i 37417 that holds in a Hilbert lattice, when an element meets an atom. (Contributed by NM, 2-Sep-2012.) (Revised by Mario Carneiro, 10-May-2013.)
Hypotheses
Ref Expression
atmod.b 𝐵 = (Base‘𝐾)
atmod.l = (le‘𝐾)
atmod.j = (join‘𝐾)
atmod.m = (meet‘𝐾)
atmod.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
atmod1i1m (((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) → ((𝑋 𝑃) (𝑌 𝑍)) = (((𝑋 𝑃) 𝑌) 𝑍))

Proof of Theorem atmod1i1m
StepHypRef Expression
1 simpl1l 1222 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) ∈ 𝐴) → 𝐾 ∈ HL)
2 simpr 489 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) ∈ 𝐴) → (𝑋 𝑃) ∈ 𝐴)
3 simpl22 1250 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) ∈ 𝐴) → 𝑌𝐵)
4 simpl23 1251 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) ∈ 𝐴) → 𝑍𝐵)
5 simpl3 1191 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) ∈ 𝐴) → (𝑋 𝑃) 𝑍)
6 atmod.b . . . 4 𝐵 = (Base‘𝐾)
7 atmod.l . . . 4 = (le‘𝐾)
8 atmod.j . . . 4 = (join‘𝐾)
9 atmod.m . . . 4 = (meet‘𝐾)
10 atmod.a . . . 4 𝐴 = (Atoms‘𝐾)
116, 7, 8, 9, 10atmod1i1 37426 . . 3 ((𝐾 ∈ HL ∧ ((𝑋 𝑃) ∈ 𝐴𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) → ((𝑋 𝑃) (𝑌 𝑍)) = (((𝑋 𝑃) 𝑌) 𝑍))
121, 2, 3, 4, 5, 11syl131anc 1381 . 2 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) ∈ 𝐴) → ((𝑋 𝑃) (𝑌 𝑍)) = (((𝑋 𝑃) 𝑌) 𝑍))
13 simp1l 1195 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) → 𝐾 ∈ HL)
14 hlol 36930 . . . . . 6 (𝐾 ∈ HL → 𝐾 ∈ OL)
1513, 14syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) → 𝐾 ∈ OL)
1615adantr 485 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) = (0.‘𝐾)) → 𝐾 ∈ OL)
1713hllatd 36933 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) → 𝐾 ∈ Lat)
1817adantr 485 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) = (0.‘𝐾)) → 𝐾 ∈ Lat)
19 simpl22 1250 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) = (0.‘𝐾)) → 𝑌𝐵)
20 simpl23 1251 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) = (0.‘𝐾)) → 𝑍𝐵)
216, 9latmcl 17721 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑌𝐵𝑍𝐵) → (𝑌 𝑍) ∈ 𝐵)
2218, 19, 20, 21syl3anc 1369 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) = (0.‘𝐾)) → (𝑌 𝑍) ∈ 𝐵)
23 eqid 2759 . . . . 5 (0.‘𝐾) = (0.‘𝐾)
246, 8, 23olj02 36795 . . . 4 ((𝐾 ∈ OL ∧ (𝑌 𝑍) ∈ 𝐵) → ((0.‘𝐾) (𝑌 𝑍)) = (𝑌 𝑍))
2516, 22, 24syl2anc 588 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) = (0.‘𝐾)) → ((0.‘𝐾) (𝑌 𝑍)) = (𝑌 𝑍))
26 oveq1 7158 . . . 4 ((𝑋 𝑃) = (0.‘𝐾) → ((𝑋 𝑃) (𝑌 𝑍)) = ((0.‘𝐾) (𝑌 𝑍)))
2726adantl 486 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) = (0.‘𝐾)) → ((𝑋 𝑃) (𝑌 𝑍)) = ((0.‘𝐾) (𝑌 𝑍)))
28 oveq1 7158 . . . . . 6 ((𝑋 𝑃) = (0.‘𝐾) → ((𝑋 𝑃) 𝑌) = ((0.‘𝐾) 𝑌))
2928adantl 486 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) = (0.‘𝐾)) → ((𝑋 𝑃) 𝑌) = ((0.‘𝐾) 𝑌))
306, 8, 23olj02 36795 . . . . . 6 ((𝐾 ∈ OL ∧ 𝑌𝐵) → ((0.‘𝐾) 𝑌) = 𝑌)
3116, 19, 30syl2anc 588 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) = (0.‘𝐾)) → ((0.‘𝐾) 𝑌) = 𝑌)
3229, 31eqtrd 2794 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) = (0.‘𝐾)) → ((𝑋 𝑃) 𝑌) = 𝑌)
3332oveq1d 7166 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) = (0.‘𝐾)) → (((𝑋 𝑃) 𝑌) 𝑍) = (𝑌 𝑍))
3425, 27, 333eqtr4d 2804 . 2 ((((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) ∧ (𝑋 𝑃) = (0.‘𝐾)) → ((𝑋 𝑃) (𝑌 𝑍)) = (((𝑋 𝑃) 𝑌) 𝑍))
35 simp21 1204 . . 3 (((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) → 𝑋𝐵)
36 simp1r 1196 . . 3 (((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) → 𝑃𝐴)
376, 9, 23, 10meetat2 36866 . . 3 ((𝐾 ∈ OL ∧ 𝑋𝐵𝑃𝐴) → ((𝑋 𝑃) ∈ 𝐴 ∨ (𝑋 𝑃) = (0.‘𝐾)))
3815, 35, 36, 37syl3anc 1369 . 2 (((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) → ((𝑋 𝑃) ∈ 𝐴 ∨ (𝑋 𝑃) = (0.‘𝐾)))
3912, 34, 38mpjaodan 957 1 (((𝐾 ∈ HL ∧ 𝑃𝐴) ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑃) 𝑍) → ((𝑋 𝑃) (𝑌 𝑍)) = (((𝑋 𝑃) 𝑌) 𝑍))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 400   ∨ wo 845   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112   class class class wbr 5033  ‘cfv 6336  (class class class)co 7151  Basecbs 16534  lecple 16623  joincjn 17613  meetcmee 17614  0.cp0 17706  Latclat 17714  OLcol 36743  Atomscatm 36832  HLchlt 36919 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-1st 7694  df-2nd 7695  df-proset 17597  df-poset 17615  df-plt 17627  df-lub 17643  df-glb 17644  df-join 17645  df-meet 17646  df-p0 17708  df-lat 17715  df-clat 17777  df-oposet 36745  df-ol 36747  df-oml 36748  df-covers 36835  df-ats 36836  df-atl 36867  df-cvlat 36891  df-hlat 36920  df-psubsp 37072  df-pmap 37073  df-padd 37365 This theorem is referenced by:  dalawlem3  37442  dalawlem6  37445
 Copyright terms: Public domain W3C validator