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

Theorem pmapglb2N 35659
Description: The projective map of the GLB of a set of lattice elements 𝑆. Variant of Theorem 15.5.2 of [MaedaMaeda] p. 62. Allows 𝑆 = ∅. (Contributed by NM, 21-Jan-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
pmapglb2.b 𝐵 = (Base‘𝐾)
pmapglb2.g 𝐺 = (glb‘𝐾)
pmapglb2.a 𝐴 = (Atoms‘𝐾)
pmapglb2.m 𝑀 = (pmap‘𝐾)
Assertion
Ref Expression
pmapglb2N ((𝐾 ∈ HL ∧ 𝑆𝐵) → (𝑀‘(𝐺𝑆)) = (𝐴 𝑥𝑆 (𝑀𝑥)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐾   𝑥,𝑆
Allowed substitution hints:   𝐺(𝑥)   𝑀(𝑥)

Proof of Theorem pmapglb2N
StepHypRef Expression
1 hlop 35250 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ OP)
2 pmapglb2.g . . . . . . . 8 𝐺 = (glb‘𝐾)
3 eqid 2765 . . . . . . . 8 (1.‘𝐾) = (1.‘𝐾)
42, 3glb0N 35081 . . . . . . 7 (𝐾 ∈ OP → (𝐺‘∅) = (1.‘𝐾))
54fveq2d 6379 . . . . . 6 (𝐾 ∈ OP → (𝑀‘(𝐺‘∅)) = (𝑀‘(1.‘𝐾)))
6 pmapglb2.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
7 pmapglb2.m . . . . . . 7 𝑀 = (pmap‘𝐾)
83, 6, 7pmap1N 35655 . . . . . 6 (𝐾 ∈ OP → (𝑀‘(1.‘𝐾)) = 𝐴)
95, 8eqtrd 2799 . . . . 5 (𝐾 ∈ OP → (𝑀‘(𝐺‘∅)) = 𝐴)
101, 9syl 17 . . . 4 (𝐾 ∈ HL → (𝑀‘(𝐺‘∅)) = 𝐴)
11 2fveq3 6380 . . . . 5 (𝑆 = ∅ → (𝑀‘(𝐺𝑆)) = (𝑀‘(𝐺‘∅)))
12 riin0 4750 . . . . 5 (𝑆 = ∅ → (𝐴 𝑥𝑆 (𝑀𝑥)) = 𝐴)
1311, 12eqeq12d 2780 . . . 4 (𝑆 = ∅ → ((𝑀‘(𝐺𝑆)) = (𝐴 𝑥𝑆 (𝑀𝑥)) ↔ (𝑀‘(𝐺‘∅)) = 𝐴))
1410, 13syl5ibrcom 238 . . 3 (𝐾 ∈ HL → (𝑆 = ∅ → (𝑀‘(𝐺𝑆)) = (𝐴 𝑥𝑆 (𝑀𝑥))))
1514adantr 472 . 2 ((𝐾 ∈ HL ∧ 𝑆𝐵) → (𝑆 = ∅ → (𝑀‘(𝐺𝑆)) = (𝐴 𝑥𝑆 (𝑀𝑥))))
16 pmapglb2.b . . . . 5 𝐵 = (Base‘𝐾)
1716, 2, 7pmapglb 35658 . . . 4 ((𝐾 ∈ HL ∧ 𝑆𝐵𝑆 ≠ ∅) → (𝑀‘(𝐺𝑆)) = 𝑥𝑆 (𝑀𝑥))
18 simpr 477 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑆𝐵) ∧ 𝑥𝑆) → 𝑥𝑆)
19 simpll 783 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑆𝐵) ∧ 𝑥𝑆) → 𝐾 ∈ HL)
20 ssel2 3756 . . . . . . . . . . . . 13 ((𝑆𝐵𝑥𝑆) → 𝑥𝐵)
2120adantll 705 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑆𝐵) ∧ 𝑥𝑆) → 𝑥𝐵)
2216, 6, 7pmapssat 35647 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑥𝐵) → (𝑀𝑥) ⊆ 𝐴)
2319, 21, 22syl2anc 579 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑆𝐵) ∧ 𝑥𝑆) → (𝑀𝑥) ⊆ 𝐴)
2418, 23jca 507 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑆𝐵) ∧ 𝑥𝑆) → (𝑥𝑆 ∧ (𝑀𝑥) ⊆ 𝐴))
2524ex 401 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑆𝐵) → (𝑥𝑆 → (𝑥𝑆 ∧ (𝑀𝑥) ⊆ 𝐴)))
2625eximdv 2012 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑆𝐵) → (∃𝑥 𝑥𝑆 → ∃𝑥(𝑥𝑆 ∧ (𝑀𝑥) ⊆ 𝐴)))
27 n0 4095 . . . . . . . 8 (𝑆 ≠ ∅ ↔ ∃𝑥 𝑥𝑆)
28 df-rex 3061 . . . . . . . 8 (∃𝑥𝑆 (𝑀𝑥) ⊆ 𝐴 ↔ ∃𝑥(𝑥𝑆 ∧ (𝑀𝑥) ⊆ 𝐴))
2926, 27, 283imtr4g 287 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑆𝐵) → (𝑆 ≠ ∅ → ∃𝑥𝑆 (𝑀𝑥) ⊆ 𝐴))
30293impia 1145 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑆𝐵𝑆 ≠ ∅) → ∃𝑥𝑆 (𝑀𝑥) ⊆ 𝐴)
31 iinss 4727 . . . . . 6 (∃𝑥𝑆 (𝑀𝑥) ⊆ 𝐴 𝑥𝑆 (𝑀𝑥) ⊆ 𝐴)
3230, 31syl 17 . . . . 5 ((𝐾 ∈ HL ∧ 𝑆𝐵𝑆 ≠ ∅) → 𝑥𝑆 (𝑀𝑥) ⊆ 𝐴)
33 sseqin2 3979 . . . . 5 ( 𝑥𝑆 (𝑀𝑥) ⊆ 𝐴 ↔ (𝐴 𝑥𝑆 (𝑀𝑥)) = 𝑥𝑆 (𝑀𝑥))
3432, 33sylib 209 . . . 4 ((𝐾 ∈ HL ∧ 𝑆𝐵𝑆 ≠ ∅) → (𝐴 𝑥𝑆 (𝑀𝑥)) = 𝑥𝑆 (𝑀𝑥))
3517, 34eqtr4d 2802 . . 3 ((𝐾 ∈ HL ∧ 𝑆𝐵𝑆 ≠ ∅) → (𝑀‘(𝐺𝑆)) = (𝐴 𝑥𝑆 (𝑀𝑥)))
36353expia 1150 . 2 ((𝐾 ∈ HL ∧ 𝑆𝐵) → (𝑆 ≠ ∅ → (𝑀‘(𝐺𝑆)) = (𝐴 𝑥𝑆 (𝑀𝑥))))
3715, 36pm2.61dne 3023 1 ((𝐾 ∈ HL ∧ 𝑆𝐵) → (𝑀‘(𝐺𝑆)) = (𝐴 𝑥𝑆 (𝑀𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107   = wceq 1652  wex 1874  wcel 2155  wne 2937  wrex 3056  cin 3731  wss 3732  c0 4079   ciin 4677  cfv 6068  Basecbs 16132  glbcglb 17211  1.cp1 17306  OPcops 35060  Atomscatm 35151  HLchlt 35238  pmapcpmap 35385
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-proset 17196  df-poset 17214  df-lub 17242  df-glb 17243  df-join 17244  df-meet 17245  df-p1 17308  df-lat 17314  df-clat 17376  df-oposet 35064  df-ol 35066  df-oml 35067  df-ats 35155  df-hlat 35239  df-pmap 35392
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator