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

Theorem pmapjoin 35865
Description: The projective map of the join of two lattice elements. Part of Equation 15.5.3 of [MaedaMaeda] p. 63. (Contributed by NM, 27-Jan-2012.)
Hypotheses
Ref Expression
pmapjoin.b 𝐵 = (Base‘𝐾)
pmapjoin.j = (join‘𝐾)
pmapjoin.m 𝑀 = (pmap‘𝐾)
pmapjoin.p + = (+𝑃𝐾)
Assertion
Ref Expression
pmapjoin ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑀𝑋) + (𝑀𝑌)) ⊆ (𝑀‘(𝑋 𝑌)))

Proof of Theorem pmapjoin
Dummy variables 𝑞 𝑝 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 475 . . . . . . 7 ((𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑋) → 𝑝 ∈ (Atoms‘𝐾))
21a1i 11 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑋) → 𝑝 ∈ (Atoms‘𝐾)))
3 pmapjoin.b . . . . . . . 8 𝐵 = (Base‘𝐾)
4 eqid 2797 . . . . . . . 8 (Atoms‘𝐾) = (Atoms‘𝐾)
53, 4atbase 35302 . . . . . . 7 (𝑝 ∈ (Atoms‘𝐾) → 𝑝𝐵)
6 eqid 2797 . . . . . . . . . . 11 (le‘𝐾) = (le‘𝐾)
7 pmapjoin.j . . . . . . . . . . 11 = (join‘𝐾)
83, 6, 7latlej1 17372 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑋(le‘𝐾)(𝑋 𝑌))
98adantr 473 . . . . . . . . 9 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) → 𝑋(le‘𝐾)(𝑋 𝑌))
10 simpl1 1243 . . . . . . . . . 10 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) → 𝐾 ∈ Lat)
11 simpr 478 . . . . . . . . . 10 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) → 𝑝𝐵)
12 simpl2 1245 . . . . . . . . . 10 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) → 𝑋𝐵)
133, 7latjcl 17363 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
1413adantr 473 . . . . . . . . . 10 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) → (𝑋 𝑌) ∈ 𝐵)
153, 6lattr 17368 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑝𝐵𝑋𝐵 ∧ (𝑋 𝑌) ∈ 𝐵)) → ((𝑝(le‘𝐾)𝑋𝑋(le‘𝐾)(𝑋 𝑌)) → 𝑝(le‘𝐾)(𝑋 𝑌)))
1610, 11, 12, 14, 15syl13anc 1492 . . . . . . . . 9 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) → ((𝑝(le‘𝐾)𝑋𝑋(le‘𝐾)(𝑋 𝑌)) → 𝑝(le‘𝐾)(𝑋 𝑌)))
179, 16mpan2d 686 . . . . . . . 8 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) → (𝑝(le‘𝐾)𝑋𝑝(le‘𝐾)(𝑋 𝑌)))
1817expimpd 446 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑝𝐵𝑝(le‘𝐾)𝑋) → 𝑝(le‘𝐾)(𝑋 𝑌)))
195, 18sylani 598 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑋) → 𝑝(le‘𝐾)(𝑋 𝑌)))
202, 19jcad 509 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑋) → (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)(𝑋 𝑌))))
21 simpl 475 . . . . . . 7 ((𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑌) → 𝑝 ∈ (Atoms‘𝐾))
2221a1i 11 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑌) → 𝑝 ∈ (Atoms‘𝐾)))
233, 6, 7latlej2 17373 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑌(le‘𝐾)(𝑋 𝑌))
2423adantr 473 . . . . . . . . 9 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) → 𝑌(le‘𝐾)(𝑋 𝑌))
25 simpl3 1247 . . . . . . . . . 10 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) → 𝑌𝐵)
263, 6lattr 17368 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑝𝐵𝑌𝐵 ∧ (𝑋 𝑌) ∈ 𝐵)) → ((𝑝(le‘𝐾)𝑌𝑌(le‘𝐾)(𝑋 𝑌)) → 𝑝(le‘𝐾)(𝑋 𝑌)))
2710, 11, 25, 14, 26syl13anc 1492 . . . . . . . . 9 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) → ((𝑝(le‘𝐾)𝑌𝑌(le‘𝐾)(𝑋 𝑌)) → 𝑝(le‘𝐾)(𝑋 𝑌)))
2824, 27mpan2d 686 . . . . . . . 8 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) → (𝑝(le‘𝐾)𝑌𝑝(le‘𝐾)(𝑋 𝑌)))
2928expimpd 446 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑝𝐵𝑝(le‘𝐾)𝑌) → 𝑝(le‘𝐾)(𝑋 𝑌)))
305, 29sylani 598 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑌) → 𝑝(le‘𝐾)(𝑋 𝑌)))
3122, 30jcad 509 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑌) → (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)(𝑋 𝑌))))
3220, 31jaod 886 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (((𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑋) ∨ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑌)) → (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)(𝑋 𝑌))))
33 simpl 475 . . . . . 6 ((𝑝 ∈ (Atoms‘𝐾) ∧ ∃𝑞 ∈ (𝑀𝑋)∃𝑟 ∈ (𝑀𝑌)𝑝(le‘𝐾)(𝑞 𝑟)) → 𝑝 ∈ (Atoms‘𝐾))
3433a1i 11 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑝 ∈ (Atoms‘𝐾) ∧ ∃𝑞 ∈ (𝑀𝑋)∃𝑟 ∈ (𝑀𝑌)𝑝(le‘𝐾)(𝑞 𝑟)) → 𝑝 ∈ (Atoms‘𝐾)))
35 pmapjoin.m . . . . . . . . . . . . . 14 𝑀 = (pmap‘𝐾)
363, 6, 4, 35elpmap 35771 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑋𝐵) → (𝑞 ∈ (𝑀𝑋) ↔ (𝑞 ∈ (Atoms‘𝐾) ∧ 𝑞(le‘𝐾)𝑋)))
37363adant3 1163 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑞 ∈ (𝑀𝑋) ↔ (𝑞 ∈ (Atoms‘𝐾) ∧ 𝑞(le‘𝐾)𝑋)))
383, 6, 4, 35elpmap 35771 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑌𝐵) → (𝑟 ∈ (𝑀𝑌) ↔ (𝑟 ∈ (Atoms‘𝐾) ∧ 𝑟(le‘𝐾)𝑌)))
39383adant2 1162 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑟 ∈ (𝑀𝑌) ↔ (𝑟 ∈ (Atoms‘𝐾) ∧ 𝑟(le‘𝐾)𝑌)))
4037, 39anbi12d 625 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑞 ∈ (𝑀𝑋) ∧ 𝑟 ∈ (𝑀𝑌)) ↔ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑞(le‘𝐾)𝑋) ∧ (𝑟 ∈ (Atoms‘𝐾) ∧ 𝑟(le‘𝐾)𝑌))))
41 an4 647 . . . . . . . . . . 11 (((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑞(le‘𝐾)𝑋) ∧ (𝑟 ∈ (Atoms‘𝐾) ∧ 𝑟(le‘𝐾)𝑌)) ↔ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞(le‘𝐾)𝑋𝑟(le‘𝐾)𝑌)))
4240, 41syl6bb 279 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑞 ∈ (𝑀𝑋) ∧ 𝑟 ∈ (𝑀𝑌)) ↔ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞(le‘𝐾)𝑋𝑟(le‘𝐾)𝑌))))
4342adantr 473 . . . . . . . . 9 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) → ((𝑞 ∈ (𝑀𝑋) ∧ 𝑟 ∈ (𝑀𝑌)) ↔ ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞(le‘𝐾)𝑋𝑟(le‘𝐾)𝑌))))
443, 4atbase 35302 . . . . . . . . . . 11 (𝑞 ∈ (Atoms‘𝐾) → 𝑞𝐵)
453, 4atbase 35302 . . . . . . . . . . 11 (𝑟 ∈ (Atoms‘𝐾) → 𝑟𝐵)
4644, 45anim12i 607 . . . . . . . . . 10 ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) → (𝑞𝐵𝑟𝐵))
47 simpll1 1270 . . . . . . . . . . . . 13 ((((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) ∧ (𝑞𝐵𝑟𝐵)) → 𝐾 ∈ Lat)
48 simprl 788 . . . . . . . . . . . . 13 ((((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) ∧ (𝑞𝐵𝑟𝐵)) → 𝑞𝐵)
49 simpll2 1272 . . . . . . . . . . . . 13 ((((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) ∧ (𝑞𝐵𝑟𝐵)) → 𝑋𝐵)
50 simprr 790 . . . . . . . . . . . . 13 ((((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) ∧ (𝑞𝐵𝑟𝐵)) → 𝑟𝐵)
51 simpll3 1274 . . . . . . . . . . . . 13 ((((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) ∧ (𝑞𝐵𝑟𝐵)) → 𝑌𝐵)
523, 6, 7latjlej12 17379 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑞𝐵𝑋𝐵) ∧ (𝑟𝐵𝑌𝐵)) → ((𝑞(le‘𝐾)𝑋𝑟(le‘𝐾)𝑌) → (𝑞 𝑟)(le‘𝐾)(𝑋 𝑌)))
5347, 48, 49, 50, 51, 52syl122anc 1499 . . . . . . . . . . . 12 ((((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) ∧ (𝑞𝐵𝑟𝐵)) → ((𝑞(le‘𝐾)𝑋𝑟(le‘𝐾)𝑌) → (𝑞 𝑟)(le‘𝐾)(𝑋 𝑌)))
54 simplr 786 . . . . . . . . . . . . . 14 ((((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) ∧ (𝑞𝐵𝑟𝐵)) → 𝑝𝐵)
553, 7latjcl 17363 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ 𝑞𝐵𝑟𝐵) → (𝑞 𝑟) ∈ 𝐵)
5647, 48, 50, 55syl3anc 1491 . . . . . . . . . . . . . 14 ((((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) ∧ (𝑞𝐵𝑟𝐵)) → (𝑞 𝑟) ∈ 𝐵)
5713ad2antrr 718 . . . . . . . . . . . . . 14 ((((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) ∧ (𝑞𝐵𝑟𝐵)) → (𝑋 𝑌) ∈ 𝐵)
583, 6lattr 17368 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑝𝐵 ∧ (𝑞 𝑟) ∈ 𝐵 ∧ (𝑋 𝑌) ∈ 𝐵)) → ((𝑝(le‘𝐾)(𝑞 𝑟) ∧ (𝑞 𝑟)(le‘𝐾)(𝑋 𝑌)) → 𝑝(le‘𝐾)(𝑋 𝑌)))
5947, 54, 56, 57, 58syl13anc 1492 . . . . . . . . . . . . 13 ((((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) ∧ (𝑞𝐵𝑟𝐵)) → ((𝑝(le‘𝐾)(𝑞 𝑟) ∧ (𝑞 𝑟)(le‘𝐾)(𝑋 𝑌)) → 𝑝(le‘𝐾)(𝑋 𝑌)))
6059expcomd 407 . . . . . . . . . . . 12 ((((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) ∧ (𝑞𝐵𝑟𝐵)) → ((𝑞 𝑟)(le‘𝐾)(𝑋 𝑌) → (𝑝(le‘𝐾)(𝑞 𝑟) → 𝑝(le‘𝐾)(𝑋 𝑌))))
6153, 60syld 47 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) ∧ (𝑞𝐵𝑟𝐵)) → ((𝑞(le‘𝐾)𝑋𝑟(le‘𝐾)𝑌) → (𝑝(le‘𝐾)(𝑞 𝑟) → 𝑝(le‘𝐾)(𝑋 𝑌))))
6261expimpd 446 . . . . . . . . . 10 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) → (((𝑞𝐵𝑟𝐵) ∧ (𝑞(le‘𝐾)𝑋𝑟(le‘𝐾)𝑌)) → (𝑝(le‘𝐾)(𝑞 𝑟) → 𝑝(le‘𝐾)(𝑋 𝑌))))
6346, 62sylani 598 . . . . . . . . 9 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) → (((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞(le‘𝐾)𝑋𝑟(le‘𝐾)𝑌)) → (𝑝(le‘𝐾)(𝑞 𝑟) → 𝑝(le‘𝐾)(𝑋 𝑌))))
6443, 63sylbid 232 . . . . . . . 8 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) → ((𝑞 ∈ (𝑀𝑋) ∧ 𝑟 ∈ (𝑀𝑌)) → (𝑝(le‘𝐾)(𝑞 𝑟) → 𝑝(le‘𝐾)(𝑋 𝑌))))
6564rexlimdvv 3216 . . . . . . 7 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑝𝐵) → (∃𝑞 ∈ (𝑀𝑋)∃𝑟 ∈ (𝑀𝑌)𝑝(le‘𝐾)(𝑞 𝑟) → 𝑝(le‘𝐾)(𝑋 𝑌)))
6665expimpd 446 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑝𝐵 ∧ ∃𝑞 ∈ (𝑀𝑋)∃𝑟 ∈ (𝑀𝑌)𝑝(le‘𝐾)(𝑞 𝑟)) → 𝑝(le‘𝐾)(𝑋 𝑌)))
675, 66sylani 598 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑝 ∈ (Atoms‘𝐾) ∧ ∃𝑞 ∈ (𝑀𝑋)∃𝑟 ∈ (𝑀𝑌)𝑝(le‘𝐾)(𝑞 𝑟)) → 𝑝(le‘𝐾)(𝑋 𝑌)))
6834, 67jcad 509 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑝 ∈ (Atoms‘𝐾) ∧ ∃𝑞 ∈ (𝑀𝑋)∃𝑟 ∈ (𝑀𝑌)𝑝(le‘𝐾)(𝑞 𝑟)) → (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)(𝑋 𝑌))))
6932, 68jaod 886 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((((𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑋) ∨ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑌)) ∨ (𝑝 ∈ (Atoms‘𝐾) ∧ ∃𝑞 ∈ (𝑀𝑋)∃𝑟 ∈ (𝑀𝑌)𝑝(le‘𝐾)(𝑞 𝑟))) → (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)(𝑋 𝑌))))
70 simp1 1167 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ Lat)
713, 4, 35pmapssat 35772 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵) → (𝑀𝑋) ⊆ (Atoms‘𝐾))
72713adant3 1163 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑀𝑋) ⊆ (Atoms‘𝐾))
733, 4, 35pmapssat 35772 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑌𝐵) → (𝑀𝑌) ⊆ (Atoms‘𝐾))
74733adant2 1162 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑀𝑌) ⊆ (Atoms‘𝐾))
75 pmapjoin.p . . . . . 6 + = (+𝑃𝐾)
766, 7, 4, 75elpadd 35812 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑀𝑋) ⊆ (Atoms‘𝐾) ∧ (𝑀𝑌) ⊆ (Atoms‘𝐾)) → (𝑝 ∈ ((𝑀𝑋) + (𝑀𝑌)) ↔ ((𝑝 ∈ (𝑀𝑋) ∨ 𝑝 ∈ (𝑀𝑌)) ∨ (𝑝 ∈ (Atoms‘𝐾) ∧ ∃𝑞 ∈ (𝑀𝑋)∃𝑟 ∈ (𝑀𝑌)𝑝(le‘𝐾)(𝑞 𝑟)))))
7770, 72, 74, 76syl3anc 1491 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑝 ∈ ((𝑀𝑋) + (𝑀𝑌)) ↔ ((𝑝 ∈ (𝑀𝑋) ∨ 𝑝 ∈ (𝑀𝑌)) ∨ (𝑝 ∈ (Atoms‘𝐾) ∧ ∃𝑞 ∈ (𝑀𝑋)∃𝑟 ∈ (𝑀𝑌)𝑝(le‘𝐾)(𝑞 𝑟)))))
783, 6, 4, 35elpmap 35771 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑋𝐵) → (𝑝 ∈ (𝑀𝑋) ↔ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑋)))
79783adant3 1163 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑝 ∈ (𝑀𝑋) ↔ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑋)))
803, 6, 4, 35elpmap 35771 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑌𝐵) → (𝑝 ∈ (𝑀𝑌) ↔ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑌)))
81803adant2 1162 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑝 ∈ (𝑀𝑌) ↔ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑌)))
8279, 81orbi12d 943 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑝 ∈ (𝑀𝑋) ∨ 𝑝 ∈ (𝑀𝑌)) ↔ ((𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑋) ∨ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑌))))
8382orbi1d 941 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (((𝑝 ∈ (𝑀𝑋) ∨ 𝑝 ∈ (𝑀𝑌)) ∨ (𝑝 ∈ (Atoms‘𝐾) ∧ ∃𝑞 ∈ (𝑀𝑋)∃𝑟 ∈ (𝑀𝑌)𝑝(le‘𝐾)(𝑞 𝑟))) ↔ (((𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑋) ∨ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑌)) ∨ (𝑝 ∈ (Atoms‘𝐾) ∧ ∃𝑞 ∈ (𝑀𝑋)∃𝑟 ∈ (𝑀𝑌)𝑝(le‘𝐾)(𝑞 𝑟)))))
8477, 83bitrd 271 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑝 ∈ ((𝑀𝑋) + (𝑀𝑌)) ↔ (((𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑋) ∨ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)𝑌)) ∨ (𝑝 ∈ (Atoms‘𝐾) ∧ ∃𝑞 ∈ (𝑀𝑋)∃𝑟 ∈ (𝑀𝑌)𝑝(le‘𝐾)(𝑞 𝑟)))))
853, 6, 4, 35elpmap 35771 . . . 4 ((𝐾 ∈ Lat ∧ (𝑋 𝑌) ∈ 𝐵) → (𝑝 ∈ (𝑀‘(𝑋 𝑌)) ↔ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)(𝑋 𝑌))))
8670, 13, 85syl2anc 580 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑝 ∈ (𝑀‘(𝑋 𝑌)) ↔ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝(le‘𝐾)(𝑋 𝑌))))
8769, 84, 863imtr4d 286 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑝 ∈ ((𝑀𝑋) + (𝑀𝑌)) → 𝑝 ∈ (𝑀‘(𝑋 𝑌))))
8887ssrdv 3802 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑀𝑋) + (𝑀𝑌)) ⊆ (𝑀‘(𝑋 𝑌)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385  wo 874  w3a 1108   = wceq 1653  wcel 2157  wrex 3088  wss 3767   class class class wbr 4841  cfv 6099  (class class class)co 6876  Basecbs 16181  lecple 16271  joincjn 17256  Latclat 17357  Atomscatm 35276  pmapcpmap 35510  +𝑃cpadd 35808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775  ax-rep 4962  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5095  ax-un 7181
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2590  df-eu 2607  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ne 2970  df-ral 3092  df-rex 3093  df-reu 3094  df-rab 3096  df-v 3385  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4114  df-if 4276  df-pw 4349  df-sn 4367  df-pr 4369  df-op 4373  df-uni 4627  df-iun 4710  df-br 4842  df-opab 4904  df-mpt 4921  df-id 5218  df-xp 5316  df-rel 5317  df-cnv 5318  df-co 5319  df-dm 5320  df-rn 5321  df-res 5322  df-ima 5323  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-riota 6837  df-ov 6879  df-oprab 6880  df-mpt2 6881  df-1st 7399  df-2nd 7400  df-poset 17258  df-lub 17286  df-glb 17287  df-join 17288  df-meet 17289  df-lat 17358  df-ats 35280  df-pmap 35517  df-padd 35809
This theorem is referenced by:  pmapjat1  35866  hlmod1i  35869  paddunN  35940  pl42lem2N  35993
  Copyright terms: Public domain W3C validator