Metamath Proof Explorer

Theorem pmodlem1

Description: Lemma for pmod1i . (Contributed by NM, 9-Mar-2012)

Ref Expression
Hypotheses pmodlem.l ⊢ ≤ = ( le ‘ 𝐾 )
pmodlem.j ⊢ ∨ = ( join ‘ 𝐾 )
pmodlem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
pmodlem.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
pmodlem.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion pmodlem1 ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) → 𝑝 ∈ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 pmodlem.l ⊢ ≤ = ( le ‘ 𝐾 )
2 pmodlem.j ⊢ ∨ = ( join ‘ 𝐾 )
3 pmodlem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 pmodlem.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
5 pmodlem.p ⊢ + = ( +𝑃 ‘ 𝐾 )
6 simpl11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 = 𝑞 ) → 𝐾 ∈ HL )
7 simpl12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 = 𝑞 ) → 𝑋 ⊆ 𝐴 )
8 simpl13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 = 𝑞 ) → 𝑌 ⊆ 𝐴 )
9 ssinss1 ⊢ ( 𝑌 ⊆ 𝐴 → ( 𝑌 ∩ 𝑍 ) ⊆ 𝐴 )
10 8 9 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 = 𝑞 ) → ( 𝑌 ∩ 𝑍 ) ⊆ 𝐴 )
11 3 5 sspadd1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ ( 𝑌 ∩ 𝑍 ) ⊆ 𝐴 ) → 𝑋 ⊆ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
12 6 7 10 11 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 = 𝑞 ) → 𝑋 ⊆ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
13 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 = 𝑞 ) → 𝑝 = 𝑞 )
14 simpl31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 = 𝑞 ) → 𝑞 ∈ 𝑋 )
15 13 14 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 = 𝑞 ) → 𝑝 ∈ 𝑋 )
16 12 15 sseldd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 = 𝑞 ) → 𝑝 ∈ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
17 simpl11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝐾 ∈ HL )
18 17 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝐾 ∈ Lat )
19 simpl12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑋 ⊆ 𝐴 )
20 simpl13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑌 ⊆ 𝐴 )
21 20 9 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → ( 𝑌 ∩ 𝑍 ) ⊆ 𝐴 )
22 simpl31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑞 ∈ 𝑋 )
23 simpl32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑟 ∈ 𝑌 )
24 simpl21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑍 ∈ 𝑆 )
25 simpl22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑋 ⊆ 𝑍 )
26 simpl23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑝 ∈ 𝑍 )
27 3 4 psubssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑍 ∈ 𝑆 ) → 𝑍 ⊆ 𝐴 )
28 17 24 27 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑍 ⊆ 𝐴 )
29 28 26 sseldd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑝 ∈ 𝐴 )
30 20 23 sseldd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑟 ∈ 𝐴 )
31 19 22 sseldd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑞 ∈ 𝐴 )
32 29 30 31 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) )
33 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑝 ≠ 𝑞 )
34 simpl33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) )
35 1 2 3 hlatexch1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) → ( 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) )
36 35 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) → 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) )
37 17 32 33 34 36 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) )
38 simp31 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → 𝑞 ∈ 𝑋 )
39 38 snssd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → { 𝑞 } ⊆ 𝑋 )
40 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → 𝑋 ⊆ 𝑍 )
41 39 40 sstrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → { 𝑞 } ⊆ 𝑍 )
42 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → 𝑝 ∈ 𝑍 )
43 42 snssd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → { 𝑝 } ⊆ 𝑍 )
44 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → 𝐾 ∈ HL )
45 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → 𝑋 ⊆ 𝐴 )
46 45 38 sseldd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → 𝑞 ∈ 𝐴 )
47 46 snssd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → { 𝑞 } ⊆ 𝐴 )
48 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → 𝑍 ∈ 𝑆 )
49 44 48 27 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → 𝑍 ⊆ 𝐴 )
50 49 42 sseldd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → 𝑝 ∈ 𝐴 )
51 50 snssd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → { 𝑝 } ⊆ 𝐴 )
52 3 4 5 paddss ⊢ ( ( 𝐾 ∈ HL ∧ ( { 𝑞 } ⊆ 𝐴 ∧ { 𝑝 } ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( ( { 𝑞 } ⊆ 𝑍 ∧ { 𝑝 } ⊆ 𝑍 ) ↔ ( { 𝑞 } + { 𝑝 } ) ⊆ 𝑍 ) )
53 44 47 51 48 52 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → ( ( { 𝑞 } ⊆ 𝑍 ∧ { 𝑝 } ⊆ 𝑍 ) ↔ ( { 𝑞 } + { 𝑝 } ) ⊆ 𝑍 ) )
54 41 43 53 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → ( { 𝑞 } + { 𝑝 } ) ⊆ 𝑍 )
55 simp33 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) )
56 44 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → 𝐾 ∈ Lat )
57 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → 𝑌 ⊆ 𝐴 )
58 simp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → 𝑟 ∈ 𝑌 )
59 57 58 sseldd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → 𝑟 ∈ 𝐴 )
60 1 2 3 5 elpadd2at2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) → ( 𝑟 ∈ ( { 𝑞 } + { 𝑝 } ) ↔ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) )
61 56 46 50 59 60 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → ( 𝑟 ∈ ( { 𝑞 } + { 𝑝 } ) ↔ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) )
62 55 61 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → 𝑟 ∈ ( { 𝑞 } + { 𝑝 } ) )
63 54 62 sseldd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ ( 𝑞 ∨ 𝑝 ) ) ) → 𝑟 ∈ 𝑍 )
64 17 19 20 24 25 26 22 23 37 63 syl333anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑟 ∈ 𝑍 )
65 23 64 elind ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑟 ∈ ( 𝑌 ∩ 𝑍 ) )
66 1 2 3 5 elpaddri ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ ( 𝑌 ∩ 𝑍 ) ⊆ 𝐴 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 ∩ 𝑍 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) → 𝑝 ∈ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
67 18 19 21 22 65 29 34 66 syl322anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑝 ∈ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
68 16 67 pm2.61dane ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) → 𝑝 ∈ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )