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

Theorem atmod2i2 37174
 Description: Version of modular law pmod2iN 37161 that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 14-May-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
atmod2i2 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → ((𝑋 𝑃) 𝑌) = (𝑋 (𝑃 𝑌)))

Proof of Theorem atmod2i2
StepHypRef Expression
1 hllat 36675 . . . . . 6 (𝐾 ∈ HL → 𝐾 ∈ Lat)
213ad2ant1 1130 . . . . 5 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → 𝐾 ∈ Lat)
3 simp21 1203 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → 𝑃𝐴)
4 atmod.b . . . . . . 7 𝐵 = (Base‘𝐾)
5 atmod.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
64, 5atbase 36601 . . . . . 6 (𝑃𝐴𝑃𝐵)
73, 6syl 17 . . . . 5 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → 𝑃𝐵)
8 simp23 1205 . . . . 5 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → 𝑌𝐵)
9 atmod.j . . . . . 6 = (join‘𝐾)
104, 9latjcom 17663 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑃𝐵𝑌𝐵) → (𝑃 𝑌) = (𝑌 𝑃))
112, 7, 8, 10syl3anc 1368 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → (𝑃 𝑌) = (𝑌 𝑃))
1211oveq1d 7150 . . 3 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → ((𝑃 𝑌) 𝑋) = ((𝑌 𝑃) 𝑋))
13 simp22 1204 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → 𝑋𝐵)
144, 9latjcl 17655 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑃𝐵𝑌𝐵) → (𝑃 𝑌) ∈ 𝐵)
152, 7, 8, 14syl3anc 1368 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → (𝑃 𝑌) ∈ 𝐵)
16 atmod.m . . . . 5 = (meet‘𝐾)
174, 16latmcom 17679 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ (𝑃 𝑌) ∈ 𝐵) → (𝑋 (𝑃 𝑌)) = ((𝑃 𝑌) 𝑋))
182, 13, 15, 17syl3anc 1368 . . 3 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → (𝑋 (𝑃 𝑌)) = ((𝑃 𝑌) 𝑋))
19 simp1 1133 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → 𝐾 ∈ HL)
20 simp3 1135 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → 𝑌 𝑋)
21 atmod.l . . . . 5 = (le‘𝐾)
224, 21, 9, 16, 5atmod1i2 37171 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑌𝐵𝑋𝐵) ∧ 𝑌 𝑋) → (𝑌 (𝑃 𝑋)) = ((𝑌 𝑃) 𝑋))
2319, 3, 8, 13, 20, 22syl131anc 1380 . . 3 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → (𝑌 (𝑃 𝑋)) = ((𝑌 𝑃) 𝑋))
2412, 18, 233eqtr4d 2843 . 2 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → (𝑋 (𝑃 𝑌)) = (𝑌 (𝑃 𝑋)))
254, 16latmcl 17656 . . . 4 ((𝐾 ∈ Lat ∧ 𝑃𝐵𝑋𝐵) → (𝑃 𝑋) ∈ 𝐵)
262, 7, 13, 25syl3anc 1368 . . 3 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → (𝑃 𝑋) ∈ 𝐵)
274, 9latjcom 17663 . . 3 ((𝐾 ∈ Lat ∧ 𝑌𝐵 ∧ (𝑃 𝑋) ∈ 𝐵) → (𝑌 (𝑃 𝑋)) = ((𝑃 𝑋) 𝑌))
282, 8, 26, 27syl3anc 1368 . 2 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → (𝑌 (𝑃 𝑋)) = ((𝑃 𝑋) 𝑌))
294, 16latmcom 17679 . . . 4 ((𝐾 ∈ Lat ∧ 𝑃𝐵𝑋𝐵) → (𝑃 𝑋) = (𝑋 𝑃))
302, 7, 13, 29syl3anc 1368 . . 3 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → (𝑃 𝑋) = (𝑋 𝑃))
3130oveq1d 7150 . 2 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → ((𝑃 𝑋) 𝑌) = ((𝑋 𝑃) 𝑌))
3224, 28, 313eqtrrd 2838 1 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑋𝐵𝑌𝐵) ∧ 𝑌 𝑋) → ((𝑋 𝑃) 𝑌) = (𝑋 (𝑃 𝑌)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   class class class wbr 5030  ‘cfv 6324  (class class class)co 7135  Basecbs 16477  lecple 16566  joincjn 17548  meetcmee 17549  Latclat 17649  Atomscatm 36575  HLchlt 36662 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-1st 7673  df-2nd 7674  df-proset 17532  df-poset 17550  df-plt 17562  df-lub 17578  df-glb 17579  df-join 17580  df-meet 17581  df-p0 17643  df-lat 17650  df-clat 17712  df-oposet 36488  df-ol 36490  df-oml 36491  df-covers 36578  df-ats 36579  df-atl 36610  df-cvlat 36634  df-hlat 36663  df-psubsp 36815  df-pmap 36816  df-padd 37108 This theorem is referenced by:  llnexchb2lem  37180  dalawlem2  37184  dalawlem3  37185  dalawlem11  37193  dalawlem12  37194  cdleme15b  37587
 Copyright terms: Public domain W3C validator