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

Theorem pmapj2N 37170
 Description: The projective map of the join of two lattice elements. (Contributed by NM, 14-Mar-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
pmapj2.b 𝐵 = (Base‘𝐾)
pmapj2.j = (join‘𝐾)
pmapj2.m 𝑀 = (pmap‘𝐾)
pmapj2.p + = (+𝑃𝐾)
pmapj2.o = (⊥𝑃𝐾)
Assertion
Ref Expression
pmapj2N ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → (𝑀‘(𝑋 𝑌)) = ( ‘( ‘((𝑀𝑋) + (𝑀𝑌)))))

Proof of Theorem pmapj2N
StepHypRef Expression
1 simp1 1133 . . 3 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ HL)
2 hllat 36604 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ Lat)
323ad2ant1 1130 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ Lat)
4 hlop 36603 . . . . . 6 (𝐾 ∈ HL → 𝐾 ∈ OP)
543ad2ant1 1130 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ OP)
6 simp2 1134 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → 𝑋𝐵)
7 pmapj2.b . . . . . 6 𝐵 = (Base‘𝐾)
8 eqid 2824 . . . . . 6 (oc‘𝐾) = (oc‘𝐾)
97, 8opoccl 36435 . . . . 5 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
105, 6, 9syl2anc 587 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
11 simp3 1135 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → 𝑌𝐵)
127, 8opoccl 36435 . . . . 5 ((𝐾 ∈ OP ∧ 𝑌𝐵) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
135, 11, 12syl2anc 587 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
14 eqid 2824 . . . . 5 (meet‘𝐾) = (meet‘𝐾)
157, 14latmcl 17662 . . . 4 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)) ∈ 𝐵)
163, 10, 13, 15syl3anc 1368 . . 3 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)) ∈ 𝐵)
17 pmapj2.m . . . 4 𝑀 = (pmap‘𝐾)
18 pmapj2.o . . . 4 = (⊥𝑃𝐾)
197, 8, 17, 18polpmapN 37153 . . 3 ((𝐾 ∈ HL ∧ (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)) ∈ 𝐵) → ( ‘(𝑀‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))) = (𝑀‘((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))))
201, 16, 19syl2anc 587 . 2 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → ( ‘(𝑀‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))) = (𝑀‘((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))))
217, 8, 17, 18polpmapN 37153 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑋𝐵) → ( ‘(𝑀𝑋)) = (𝑀‘((oc‘𝐾)‘𝑋)))
22213adant3 1129 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → ( ‘(𝑀𝑋)) = (𝑀‘((oc‘𝐾)‘𝑋)))
237, 8, 17, 18polpmapN 37153 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑌𝐵) → ( ‘(𝑀𝑌)) = (𝑀‘((oc‘𝐾)‘𝑌)))
24233adant2 1128 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → ( ‘(𝑀𝑌)) = (𝑀‘((oc‘𝐾)‘𝑌)))
2522, 24ineq12d 4175 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → (( ‘(𝑀𝑋)) ∩ ( ‘(𝑀𝑌))) = ((𝑀‘((oc‘𝐾)‘𝑋)) ∩ (𝑀‘((oc‘𝐾)‘𝑌))))
26 eqid 2824 . . . . . . 7 (Atoms‘𝐾) = (Atoms‘𝐾)
277, 26, 17pmapssat 37000 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (𝑀𝑋) ⊆ (Atoms‘𝐾))
28273adant3 1129 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → (𝑀𝑋) ⊆ (Atoms‘𝐾))
297, 26, 17pmapssat 37000 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑌𝐵) → (𝑀𝑌) ⊆ (Atoms‘𝐾))
30293adant2 1128 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → (𝑀𝑌) ⊆ (Atoms‘𝐾))
31 pmapj2.p . . . . . 6 + = (+𝑃𝐾)
3226, 31, 18poldmj1N 37169 . . . . 5 ((𝐾 ∈ HL ∧ (𝑀𝑋) ⊆ (Atoms‘𝐾) ∧ (𝑀𝑌) ⊆ (Atoms‘𝐾)) → ( ‘((𝑀𝑋) + (𝑀𝑌))) = (( ‘(𝑀𝑋)) ∩ ( ‘(𝑀𝑌))))
331, 28, 30, 32syl3anc 1368 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → ( ‘((𝑀𝑋) + (𝑀𝑌))) = (( ‘(𝑀𝑋)) ∩ ( ‘(𝑀𝑌))))
347, 14, 26, 17pmapmeet 37014 . . . . 5 ((𝐾 ∈ HL ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (𝑀‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))) = ((𝑀‘((oc‘𝐾)‘𝑋)) ∩ (𝑀‘((oc‘𝐾)‘𝑌))))
351, 10, 13, 34syl3anc 1368 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → (𝑀‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))) = ((𝑀‘((oc‘𝐾)‘𝑋)) ∩ (𝑀‘((oc‘𝐾)‘𝑌))))
3625, 33, 353eqtr4rd 2870 . . 3 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → (𝑀‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))) = ( ‘((𝑀𝑋) + (𝑀𝑌))))
3736fveq2d 6665 . 2 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → ( ‘(𝑀‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))) = ( ‘( ‘((𝑀𝑋) + (𝑀𝑌)))))
38 hlol 36602 . . . 4 (𝐾 ∈ HL → 𝐾 ∈ OL)
39 pmapj2.j . . . . 5 = (join‘𝐾)
407, 39, 14, 8oldmm4 36461 . . . 4 ((𝐾 ∈ OL ∧ 𝑋𝐵𝑌𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))) = (𝑋 𝑌))
4138, 40syl3an1 1160 . . 3 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))) = (𝑋 𝑌))
4241fveq2d 6665 . 2 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → (𝑀‘((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))) = (𝑀‘(𝑋 𝑌)))
4320, 37, 423eqtr3rd 2868 1 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → (𝑀‘(𝑋 𝑌)) = ( ‘( ‘((𝑀𝑋) + (𝑀𝑌)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115   ∩ cin 3918   ⊆ wss 3919  ‘cfv 6343  (class class class)co 7149  Basecbs 16483  occoc 16573  joincjn 17554  meetcmee 17555  Latclat 17655  OPcops 36413  OLcol 36415  Atomscatm 36504  HLchlt 36591  pmapcpmap 36738  +𝑃cpadd 37036  ⊥𝑃cpolN 37143 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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-riotaBAD 36194 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 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-iun 4907  df-iin 4908  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-1st 7684  df-2nd 7685  df-undef 7935  df-proset 17538  df-poset 17556  df-plt 17568  df-lub 17584  df-glb 17585  df-join 17586  df-meet 17587  df-p0 17649  df-p1 17650  df-lat 17656  df-clat 17718  df-oposet 36417  df-ol 36419  df-oml 36420  df-covers 36507  df-ats 36508  df-atl 36539  df-cvlat 36563  df-hlat 36592  df-psubsp 36744  df-pmap 36745  df-padd 37037  df-polarityN 37144 This theorem is referenced by:  pmapocjN  37171  pmapojoinN  37209
 Copyright terms: Public domain W3C validator