This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pmapjoin

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)

Ref Expression
Hypotheses pmapjoin.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
pmapjoin.j ⊢ ∨ = ( join ‘ 𝐾 )
pmapjoin.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
pmapjoin.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion pmapjoin ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ⊆ ( 𝑀 ‘ ( 𝑋 ∨ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 pmapjoin.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 pmapjoin.j ⊢ ∨ = ( join ‘ 𝐾 )
3 pmapjoin.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
4 pmapjoin.p ⊢ + = ( +𝑃 ‘ 𝐾 )
5 simpl ⊢ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
6 5 a1i ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) )
7 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
8 1 7 atbase ⊢ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → 𝑝 ∈ 𝐵 )
9 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
10 1 9 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) )
11 10 adantr ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) )
12 simpl1 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → 𝐾 ∈ Lat )
13 simpr ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → 𝑝 ∈ 𝐵 )
14 simpl2 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
15 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
16 15 adantr ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
17 1 9 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) )
18 12 13 14 16 17 syl13anc ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) )
19 11 18 mpan2d ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 ( le ‘ 𝐾 ) 𝑋 → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) )
20 19 expimpd ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑝 ∈ 𝐵 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) )
21 8 20 sylani ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) )
22 6 21 jcad ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) ) )
23 simpl ⊢ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
24 23 a1i ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) )
25 1 9 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) )
26 25 adantr ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → 𝑌 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) )
27 simpl3 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
28 1 9 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) 𝑌 ∧ 𝑌 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) )
29 12 13 27 16 28 syl13anc ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑝 ( le ‘ 𝐾 ) 𝑌 ∧ 𝑌 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) )
30 26 29 mpan2d ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 ( le ‘ 𝐾 ) 𝑌 → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) )
31 30 expimpd ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑝 ∈ 𝐵 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) )
32 8 31 sylani ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) )
33 24 32 jcad ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) ) )
34 22 33 jaod ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) ) )
35 simpl ⊢ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
36 35 a1i ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) )
37 1 9 7 3 elpmap ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ↔ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ) )
38 37 3adant3 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ↔ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ) )
39 1 9 7 3 elpmap ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ) → ( 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) ↔ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ( le ‘ 𝐾 ) 𝑌 ) ) )
40 39 3adant2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) ↔ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ( le ‘ 𝐾 ) 𝑌 ) ) )
41 38 40 anbi12d ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∧ 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) ) ↔ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ( le ‘ 𝐾 ) 𝑌 ) ) ) )
42 an4 ⊢ ( ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ( le ‘ 𝐾 ) 𝑌 ) ) ↔ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑟 ( le ‘ 𝐾 ) 𝑌 ) ) )
43 41 42 bitrdi ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∧ 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) ) ↔ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑟 ( le ‘ 𝐾 ) 𝑌 ) ) ) )
44 43 adantr ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∧ 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) ) ↔ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑟 ( le ‘ 𝐾 ) 𝑌 ) ) ) )
45 1 7 atbase ⊢ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) → 𝑞 ∈ 𝐵 )
46 1 7 atbase ⊢ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → 𝑟 ∈ 𝐵 )
47 45 46 anim12i ⊢ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) )
48 simpll1 ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝐾 ∈ Lat )
49 simprl ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑞 ∈ 𝐵 )
50 simpll2 ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
51 simprr ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑟 ∈ 𝐵 )
52 simpll3 ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
53 1 9 2 latjlej12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑟 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑞 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑟 ( le ‘ 𝐾 ) 𝑌 ) → ( 𝑞 ∨ 𝑟 ) ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) )
54 48 49 50 51 52 53 syl122anc ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑞 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑟 ( le ‘ 𝐾 ) 𝑌 ) → ( 𝑞 ∨ 𝑟 ) ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) )
55 simplr ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑝 ∈ 𝐵 )
56 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) → ( 𝑞 ∨ 𝑟 ) ∈ 𝐵 )
57 48 49 51 56 syl3anc ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝑞 ∨ 𝑟 ) ∈ 𝐵 )
58 15 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
59 1 9 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑞 ∨ 𝑟 ) ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ∧ ( 𝑞 ∨ 𝑟 ) ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) )
60 48 55 57 58 59 syl13anc ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ∧ ( 𝑞 ∨ 𝑟 ) ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) )
61 60 expcomd ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑞 ∨ 𝑟 ) ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) → ( 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) ) )
62 54 61 syld ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑞 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑟 ( le ‘ 𝐾 ) 𝑌 ) → ( 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) ) )
63 62 expimpd ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ∧ ( 𝑞 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑟 ( le ‘ 𝐾 ) 𝑌 ) ) → ( 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) ) )
64 47 63 sylani ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑟 ( le ‘ 𝐾 ) 𝑌 ) ) → ( 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) ) )
65 44 64 sylbid ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∧ 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) ) → ( 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) ) )
66 65 rexlimdvv ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) )
67 66 expimpd ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑝 ∈ 𝐵 ∧ ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) )
68 8 67 sylani ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) )
69 36 68 jcad ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) ) )
70 34 69 jaod ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) ) )
71 simp1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ Lat )
72 1 7 3 pmapssat ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) )
73 72 3adant3 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) )
74 1 7 3 pmapssat ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) )
75 74 3adant2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) )
76 9 2 7 4 elpadd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑀 ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝑀 ‘ 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) ) → ( 𝑝 ∈ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ↔ ( ( 𝑝 ∈ ( 𝑀 ‘ 𝑋 ) ∨ 𝑝 ∈ ( 𝑀 ‘ 𝑌 ) ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ) ) )
77 71 73 75 76 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑝 ∈ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ↔ ( ( 𝑝 ∈ ( 𝑀 ‘ 𝑋 ) ∨ 𝑝 ∈ ( 𝑀 ‘ 𝑌 ) ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ) ) )
78 1 9 7 3 elpmap ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑝 ∈ ( 𝑀 ‘ 𝑋 ) ↔ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ) )
79 78 3adant3 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑝 ∈ ( 𝑀 ‘ 𝑋 ) ↔ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ) )
80 1 9 7 3 elpmap ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ) → ( 𝑝 ∈ ( 𝑀 ‘ 𝑌 ) ↔ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) )
81 80 3adant2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑝 ∈ ( 𝑀 ‘ 𝑌 ) ↔ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) )
82 79 81 orbi12d ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑝 ∈ ( 𝑀 ‘ 𝑋 ) ∨ 𝑝 ∈ ( 𝑀 ‘ 𝑌 ) ) ↔ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) ) )
83 82 orbi1d ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 𝑝 ∈ ( 𝑀 ‘ 𝑋 ) ∨ 𝑝 ∈ ( 𝑀 ‘ 𝑌 ) ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ) ↔ ( ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ) ) )
84 77 83 bitrd ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑝 ∈ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ↔ ( ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ) ) )
85 1 9 7 3 elpmap ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) → ( 𝑝 ∈ ( 𝑀 ‘ ( 𝑋 ∨ 𝑌 ) ) ↔ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) ) )
86 71 15 85 syl2anc ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑝 ∈ ( 𝑀 ‘ ( 𝑋 ∨ 𝑌 ) ) ↔ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) ) )
87 70 84 86 3imtr4d ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑝 ∈ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) → 𝑝 ∈ ( 𝑀 ‘ ( 𝑋 ∨ 𝑌 ) ) ) )
88 87 ssrdv ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑌 ) ) ⊆ ( 𝑀 ‘ ( 𝑋 ∨ 𝑌 ) ) )