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

Theorem pmapglb2N 33249
 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
pmapglb2.g
pmapglb2.a
pmapglb2.m
Assertion
Ref Expression
pmapglb2N
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem pmapglb2N
StepHypRef Expression
1 hlop 32841 . . . . 5
2 pmapglb2.g . . . . . . . 8
3 eqid 2420 . . . . . . . 8
42, 3glb0N 32672 . . . . . . 7
54fveq2d 5877 . . . . . 6
6 pmapglb2.a . . . . . . 7
7 pmapglb2.m . . . . . . 7
83, 6, 7pmap1N 33245 . . . . . 6
95, 8eqtrd 2461 . . . . 5
101, 9syl 17 . . . 4
11 fveq2 5873 . . . . . 6
1211fveq2d 5877 . . . . 5
13 riin0 4367 . . . . 5
1412, 13eqeq12d 2442 . . . 4
1510, 14syl5ibrcom 225 . . 3
17 pmapglb2.b . . . . 5
1817, 2, 7pmapglb 33248 . . . 4
19 simpr 462 . . . . . . . . . . 11
20 simpll 758 . . . . . . . . . . . 12
21 ssel2 3456 . . . . . . . . . . . . 13
2221adantll 718 . . . . . . . . . . . 12
2317, 6, 7pmapssat 33237 . . . . . . . . . . . 12
2420, 22, 23syl2anc 665 . . . . . . . . . . 11
2519, 24jca 534 . . . . . . . . . 10
2625ex 435 . . . . . . . . 9
2726eximdv 1754 . . . . . . . 8
28 n0 3768 . . . . . . . 8
29 df-rex 2779 . . . . . . . 8
3027, 28, 293imtr4g 273 . . . . . . 7
31303impia 1202 . . . . . 6
32 iinss 4344 . . . . . 6
3331, 32syl 17 . . . . 5
34 sseqin2 3678 . . . . 5
3533, 34sylib 199 . . . 4
3618, 35eqtr4d 2464 . . 3
37363expia 1207 . 2
3816, 37pm2.61dne 2739 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   w3a 982   wceq 1437  wex 1659   wcel 1867   wne 2616  wrex 2774   cin 3432   wss 3433  c0 3758  ciin 4294  cfv 5593  cbs 15099  cglb 16166  cp1 16262  cops 32651  catm 32742  chlt 32829  cpmap 32975 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4530  ax-sep 4540  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6589 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-iun 4295  df-iin 4296  df-br 4418  df-opab 4477  df-mpt 4478  df-id 4761  df-xp 4852  df-rel 4853  df-cnv 4854  df-co 4855  df-dm 4856  df-rn 4857  df-res 4858  df-ima 4859  df-iota 5557  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6259  df-ov 6300  df-oprab 6301  df-preset 16151  df-poset 16169  df-lub 16198  df-glb 16199  df-join 16200  df-meet 16201  df-p1 16264  df-lat 16270  df-clat 16332  df-oposet 32655  df-ol 32657  df-oml 32658  df-ats 32746  df-hlat 32830  df-pmap 32982 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator