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

Metamath Proof Explorer

Theorem pmapjat1

Description: The projective map of the join of a lattice element and an atom. (Contributed by NM, 28-Jan-2012)

Ref Expression
Hypotheses pmapjat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
pmapjat.j ⊢ ∨ = ( join ‘ 𝐾 )
pmapjat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
pmapjat.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
pmapjat.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion pmapjat1 ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) = ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) )

Proof

Step Hyp Ref Expression
1 pmapjat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 pmapjat.j ⊢ ∨ = ( join ‘ 𝐾 )
3 pmapjat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 pmapjat.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
5 pmapjat.p ⊢ + = ( +𝑃 ‘ 𝐾 )
6 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → 𝐾 ∈ HL )
7 1 3 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
8 7 3ad2ant3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ∈ 𝐵 )
9 1 3 4 pmapssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑄 ) ⊆ 𝐴 )
10 6 8 9 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑀 ‘ 𝑄 ) ⊆ 𝐴 )
11 3 5 padd02 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑀 ‘ 𝑄 ) ⊆ 𝐴 ) → ( ∅ + ( 𝑀 ‘ 𝑄 ) ) = ( 𝑀 ‘ 𝑄 ) )
12 6 10 11 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( ∅ + ( 𝑀 ‘ 𝑄 ) ) = ( 𝑀 ‘ 𝑄 ) )
13 12 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 = ( 0. ‘ 𝐾 ) ) → ( ∅ + ( 𝑀 ‘ 𝑄 ) ) = ( 𝑀 ‘ 𝑄 ) )
14 fveq2 ⊢ ( 𝑋 = ( 0. ‘ 𝐾 ) → ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ ( 0. ‘ 𝐾 ) ) )
15 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
16 15 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → 𝐾 ∈ AtLat )
17 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
18 17 4 pmap0 ⊢ ( 𝐾 ∈ AtLat → ( 𝑀 ‘ ( 0. ‘ 𝐾 ) ) = ∅ )
19 16 18 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑀 ‘ ( 0. ‘ 𝐾 ) ) = ∅ )
20 14 19 sylan9eqr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 = ( 0. ‘ 𝐾 ) ) → ( 𝑀 ‘ 𝑋 ) = ∅ )
21 20 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 = ( 0. ‘ 𝐾 ) ) → ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) = ( ∅ + ( 𝑀 ‘ 𝑄 ) ) )
22 oveq1 ⊢ ( 𝑋 = ( 0. ‘ 𝐾 ) → ( 𝑋 ∨ 𝑄 ) = ( ( 0. ‘ 𝐾 ) ∨ 𝑄 ) )
23 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
24 23 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → 𝐾 ∈ OL )
25 1 2 17 olj02 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑄 ∈ 𝐵 ) → ( ( 0. ‘ 𝐾 ) ∨ 𝑄 ) = 𝑄 )
26 24 8 25 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( ( 0. ‘ 𝐾 ) ∨ 𝑄 ) = 𝑄 )
27 22 26 sylan9eqr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 = ( 0. ‘ 𝐾 ) ) → ( 𝑋 ∨ 𝑄 ) = 𝑄 )
28 27 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 = ( 0. ‘ 𝐾 ) ) → ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) = ( 𝑀 ‘ 𝑄 ) )
29 13 21 28 3eqtr4rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 = ( 0. ‘ 𝐾 ) ) → ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) = ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) )
30 simpll1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) ∧ 𝑝 ∈ 𝐴 ) → 𝐾 ∈ HL )
31 30 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) → 𝐾 ∈ HL )
32 simpll2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) ∧ 𝑝 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
33 32 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) → 𝑋 ∈ 𝐵 )
34 simplr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) → 𝑝 ∈ 𝐴 )
35 simpll3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) ∧ 𝑝 ∈ 𝐴 ) → 𝑄 ∈ 𝐴 )
36 35 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) → 𝑄 ∈ 𝐴 )
37 33 34 36 3jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ∈ 𝐵 ∧ 𝑝 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
38 simpllr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) → 𝑋 ≠ ( 0. ‘ 𝐾 ) )
39 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) )
40 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
41 1 40 2 17 3 cvrat42 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑝 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ≠ ( 0. ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑄 ) ) ) )
42 41 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑝 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( 𝑋 ≠ ( 0. ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑄 ) ) )
43 31 37 38 39 42 syl22anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑄 ) ) )
44 43 ex ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑄 ) ) ) )
45 1 40 3 4 elpmap ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ↔ ( 𝑞 ∈ 𝐴 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ) )
46 45 3adant3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ↔ ( 𝑞 ∈ 𝐴 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ) )
47 df-rex ⊢ ( ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑄 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ↔ ∃ 𝑟 ( 𝑟 ∈ ( 𝑀 ‘ 𝑄 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) )
48 3 4 elpmapat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) → ( 𝑟 ∈ ( 𝑀 ‘ 𝑄 ) ↔ 𝑟 = 𝑄 ) )
49 48 3adant2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑟 ∈ ( 𝑀 ‘ 𝑄 ) ↔ 𝑟 = 𝑄 ) )
50 49 anbi1d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑟 ∈ ( 𝑀 ‘ 𝑄 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ↔ ( 𝑟 = 𝑄 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ) )
51 50 exbidv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( ∃ 𝑟 ( 𝑟 ∈ ( 𝑀 ‘ 𝑄 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ↔ ∃ 𝑟 ( 𝑟 = 𝑄 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ) )
52 47 51 bitr2id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( ∃ 𝑟 ( 𝑟 = 𝑄 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ↔ ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑄 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) )
53 oveq2 ⊢ ( 𝑟 = 𝑄 → ( 𝑞 ∨ 𝑟 ) = ( 𝑞 ∨ 𝑄 ) )
54 53 breq2d ⊢ ( 𝑟 = 𝑄 → ( 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ↔ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑄 ) ) )
55 54 ceqsexgv ⊢ ( 𝑄 ∈ 𝐴 → ( ∃ 𝑟 ( 𝑟 = 𝑄 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ↔ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑄 ) ) )
56 55 3ad2ant3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( ∃ 𝑟 ( 𝑟 = 𝑄 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ↔ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑄 ) ) )
57 52 56 bitr3d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑄 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ↔ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑄 ) ) )
58 46 57 anbi12d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∧ ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑄 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ↔ ( ( 𝑞 ∈ 𝐴 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑄 ) ) ) )
59 anass ⊢ ( ( ( 𝑞 ∈ 𝐴 ∧ 𝑞 ( le ‘ 𝐾 ) 𝑋 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑄 ) ) ↔ ( 𝑞 ∈ 𝐴 ∧ ( 𝑞 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑄 ) ) ) )
60 58 59 bitrdi ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∧ ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑄 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ↔ ( 𝑞 ∈ 𝐴 ∧ ( 𝑞 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑄 ) ) ) ) )
61 60 rexbidv2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑄 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ↔ ∃ 𝑞 ∈ 𝐴 ( 𝑞 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑄 ) ) ) )
62 61 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑄 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ↔ ∃ 𝑞 ∈ 𝐴 ( 𝑞 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑄 ) ) ) )
63 44 62 sylibrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) → ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑄 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) )
64 63 imdistanda ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) → ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑄 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ) )
65 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
66 65 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → 𝐾 ∈ Lat )
67 simp2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
68 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 )
69 66 67 8 68 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 )
70 1 40 3 4 elpmap ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 ) → ( 𝑝 ∈ ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) ↔ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) ) )
71 6 69 70 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑝 ∈ ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) ↔ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) ) )
72 71 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) → ( 𝑝 ∈ ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) ↔ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) ) )
73 1 3 4 pmapssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) ⊆ 𝐴 )
74 73 3adant3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑀 ‘ 𝑋 ) ⊆ 𝐴 )
75 66 74 10 3jca ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝐾 ∈ Lat ∧ ( 𝑀 ‘ 𝑋 ) ⊆ 𝐴 ∧ ( 𝑀 ‘ 𝑄 ) ⊆ 𝐴 ) )
76 75 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) → ( 𝐾 ∈ Lat ∧ ( 𝑀 ‘ 𝑋 ) ⊆ 𝐴 ∧ ( 𝑀 ‘ 𝑄 ) ⊆ 𝐴 ) )
77 1 17 4 pmapeq0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) = ∅ ↔ 𝑋 = ( 0. ‘ 𝐾 ) ) )
78 77 3adant3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑀 ‘ 𝑋 ) = ∅ ↔ 𝑋 = ( 0. ‘ 𝐾 ) ) )
79 78 necon3bid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑀 ‘ 𝑋 ) ≠ ∅ ↔ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) )
80 79 biimpar ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) → ( 𝑀 ‘ 𝑋 ) ≠ ∅ )
81 simp3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ∈ 𝐴 )
82 17 3 atn0 ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ≠ ( 0. ‘ 𝐾 ) )
83 16 81 82 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ≠ ( 0. ‘ 𝐾 ) )
84 1 17 4 pmapeq0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑄 ) = ∅ ↔ 𝑄 = ( 0. ‘ 𝐾 ) ) )
85 6 8 84 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑀 ‘ 𝑄 ) = ∅ ↔ 𝑄 = ( 0. ‘ 𝐾 ) ) )
86 85 necon3bid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑀 ‘ 𝑄 ) ≠ ∅ ↔ 𝑄 ≠ ( 0. ‘ 𝐾 ) ) )
87 83 86 mpbird ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑀 ‘ 𝑄 ) ≠ ∅ )
88 87 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) → ( 𝑀 ‘ 𝑄 ) ≠ ∅ )
89 40 2 3 5 elpaddn0 ⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑀 ‘ 𝑋 ) ⊆ 𝐴 ∧ ( 𝑀 ‘ 𝑄 ) ⊆ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ≠ ∅ ∧ ( 𝑀 ‘ 𝑄 ) ≠ ∅ ) ) → ( 𝑝 ∈ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) ↔ ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑄 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ) )
90 76 80 88 89 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) → ( 𝑝 ∈ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) ↔ ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ ( 𝑀 ‘ 𝑋 ) ∃ 𝑟 ∈ ( 𝑀 ‘ 𝑄 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ∨ 𝑟 ) ) ) )
91 64 72 90 3imtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) → ( 𝑝 ∈ ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) → 𝑝 ∈ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) ) )
92 91 ssrdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) → ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) ⊆ ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) )
93 1 2 4 5 pmapjoin ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) ⊆ ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) )
94 66 67 8 93 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) ⊆ ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) )
95 94 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) → ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) ⊆ ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) )
96 92 95 eqssd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ( 0. ‘ 𝐾 ) ) → ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) = ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) )
97 29 96 pm2.61dane ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) = ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) )