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

Metamath Proof Explorer

Theorem pmodlem2

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 pmodlem2 ( ( 𝐾 ∈ 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 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑋 = ∅ ) → 𝑋 = ∅ )
7 6 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑋 = ∅ ) → ( 𝑋 + 𝑌 ) = ( ∅ + 𝑌 ) )
8 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑋 = ∅ ) → 𝐾 ∈ HL )
9 simpl22 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑋 = ∅ ) → 𝑌 ⊆ 𝐴 )
10 3 5 padd02 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ) → ( ∅ + 𝑌 ) = 𝑌 )
11 8 9 10 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑋 = ∅ ) → ( ∅ + 𝑌 ) = 𝑌 )
12 7 11 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑋 = ∅ ) → ( 𝑋 + 𝑌 ) = 𝑌 )
13 12 ineq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑋 = ∅ ) → ( ( 𝑋 + 𝑌 ) ∩ 𝑍 ) = ( 𝑌 ∩ 𝑍 ) )
14 ssinss1 ⊢ ( 𝑌 ⊆ 𝐴 → ( 𝑌 ∩ 𝑍 ) ⊆ 𝐴 )
15 9 14 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑋 = ∅ ) → ( 𝑌 ∩ 𝑍 ) ⊆ 𝐴 )
16 simpl21 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑋 = ∅ ) → 𝑋 ⊆ 𝐴 )
17 3 5 sspadd2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑌 ∩ 𝑍 ) ⊆ 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑌 ∩ 𝑍 ) ⊆ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
18 8 15 16 17 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑋 = ∅ ) → ( 𝑌 ∩ 𝑍 ) ⊆ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
19 13 18 eqsstrd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑋 = ∅ ) → ( ( 𝑋 + 𝑌 ) ∩ 𝑍 ) ⊆ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
20 oveq2 ⊢ ( 𝑌 = ∅ → ( 𝑋 + 𝑌 ) = ( 𝑋 + ∅ ) )
21 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) → 𝐾 ∈ HL )
22 simp21 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) → 𝑋 ⊆ 𝐴 )
23 3 5 padd01 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑋 + ∅ ) = 𝑋 )
24 21 22 23 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) → ( 𝑋 + ∅ ) = 𝑋 )
25 20 24 sylan9eqr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑌 = ∅ ) → ( 𝑋 + 𝑌 ) = 𝑋 )
26 25 ineq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑌 = ∅ ) → ( ( 𝑋 + 𝑌 ) ∩ 𝑍 ) = ( 𝑋 ∩ 𝑍 ) )
27 inss1 ⊢ ( 𝑋 ∩ 𝑍 ) ⊆ 𝑋
28 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑌 = ∅ ) → 𝐾 ∈ HL )
29 simpl21 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑌 = ∅ ) → 𝑋 ⊆ 𝐴 )
30 simpl22 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑌 = ∅ ) → 𝑌 ⊆ 𝐴 )
31 30 14 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑌 = ∅ ) → ( 𝑌 ∩ 𝑍 ) ⊆ 𝐴 )
32 3 5 sspadd1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ ( 𝑌 ∩ 𝑍 ) ⊆ 𝐴 ) → 𝑋 ⊆ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
33 28 29 31 32 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑌 = ∅ ) → 𝑋 ⊆ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
34 27 33 sstrid ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑌 = ∅ ) → ( 𝑋 ∩ 𝑍 ) ⊆ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
35 26 34 eqsstrd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑌 = ∅ ) → ( ( 𝑋 + 𝑌 ) ∩ 𝑍 ) ⊆ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
36 elin ⊢ ( 𝑝 ∈ ( ( 𝑋 + 𝑌 ) ∩ 𝑍 ) ↔ ( 𝑝 ∈ ( 𝑋 + 𝑌 ) ∧ 𝑝 ∈ 𝑍 ) )
37 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ∧ 𝑝 ∈ 𝑍 ) ) → 𝐾 ∈ HL )
38 37 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ∧ 𝑝 ∈ 𝑍 ) ) → 𝐾 ∈ Lat )
39 simpl21 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ∧ 𝑝 ∈ 𝑍 ) ) → 𝑋 ⊆ 𝐴 )
40 simpl22 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ∧ 𝑝 ∈ 𝑍 ) ) → 𝑌 ⊆ 𝐴 )
41 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ∧ 𝑝 ∈ 𝑍 ) ) → ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) )
42 1 2 3 5 elpaddn0 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( 𝑝 ∈ ( 𝑋 + 𝑌 ) ↔ ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) )
43 38 39 40 41 42 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ∧ 𝑝 ∈ 𝑍 ) ) → ( 𝑝 ∈ ( 𝑋 + 𝑌 ) ↔ ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) )
44 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑝 ∈ 𝑍 ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) → 𝐾 ∈ HL )
45 simpl21 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑝 ∈ 𝑍 ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) → 𝑋 ⊆ 𝐴 )
46 simpl22 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑝 ∈ 𝑍 ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) → 𝑌 ⊆ 𝐴 )
47 simpl23 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑝 ∈ 𝑍 ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) → 𝑍 ∈ 𝑆 )
48 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑝 ∈ 𝑍 ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) → 𝑋 ⊆ 𝑍 )
49 simpr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑝 ∈ 𝑍 ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) → 𝑝 ∈ 𝑍 )
50 simpr2l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑝 ∈ 𝑍 ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) → 𝑞 ∈ 𝑋 )
51 simpr2r ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑝 ∈ 𝑍 ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) → 𝑟 ∈ 𝑌 )
52 simpr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑝 ∈ 𝑍 ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) → 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) )
53 1 2 3 4 5 pmodlem1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) → 𝑝 ∈ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
54 44 45 46 47 48 49 50 51 52 53 syl333anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑝 ∈ 𝑍 ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ∧ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) → 𝑝 ∈ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
55 54 3exp2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) → ( 𝑝 ∈ 𝑍 → ( ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) → ( 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ) ) ) )
56 55 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑝 ∈ 𝑍 ) → ( ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) → ( 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ) ) )
57 56 rexlimdvv ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑝 ∈ 𝑍 ) → ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ) )
58 57 adantld ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ 𝑝 ∈ 𝑍 ) → ( ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) → 𝑝 ∈ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ) )
59 58 adantrl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ∧ 𝑝 ∈ 𝑍 ) ) → ( ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) → 𝑝 ∈ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ) )
60 43 59 sylbid ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ∧ 𝑝 ∈ 𝑍 ) ) → ( 𝑝 ∈ ( 𝑋 + 𝑌 ) → 𝑝 ∈ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ) )
61 60 exp32 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) → ( ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) → ( 𝑝 ∈ 𝑍 → ( 𝑝 ∈ ( 𝑋 + 𝑌 ) → 𝑝 ∈ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ) ) ) )
62 61 com34 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) → ( ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) → ( 𝑝 ∈ ( 𝑋 + 𝑌 ) → ( 𝑝 ∈ 𝑍 → 𝑝 ∈ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ) ) ) )
63 62 imp4b ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( ( 𝑝 ∈ ( 𝑋 + 𝑌 ) ∧ 𝑝 ∈ 𝑍 ) → 𝑝 ∈ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ) )
64 36 63 biimtrid ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( 𝑝 ∈ ( ( 𝑋 + 𝑌 ) ∩ 𝑍 ) → 𝑝 ∈ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) ) )
65 64 ssrdv ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( ( 𝑋 + 𝑌 ) ∩ 𝑍 ) ⊆ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )
66 19 35 65 pm2.61da2ne ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ⊆ 𝑍 ) → ( ( 𝑋 + 𝑌 ) ∩ 𝑍 ) ⊆ ( 𝑋 + ( 𝑌 ∩ 𝑍 ) ) )