Theorem paddasslem11

Description: Lemma for paddass . The case when p = z . (Contributed by NM, 11-Jan-2012)

	Ref	Expression
Hypotheses	paddasslem.l	⊢ ≤ = ( le ‘ 𝐾 )
	paddasslem.j	⊢ ∨ = ( join ‘ 𝐾 )
	paddasslem.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	paddasslem.p	⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion	paddasslem11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) ∧ 𝑧 ∈ 𝑍 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		paddasslem.l	⊢ ≤ = ( le ‘ 𝐾 )
2		paddasslem.j	⊢ ∨ = ( join ‘ 𝐾 )
3		paddasslem.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		paddasslem.p	⊢ + = ( +𝑃 ‘ 𝐾 )
5		simplll	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) ∧ 𝑧 ∈ 𝑍 ) → 𝐾 ∈ HL )
6		simplr3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) ∧ 𝑧 ∈ 𝑍 ) → 𝑍 ⊆ 𝐴 )
7		simplr1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) ∧ 𝑧 ∈ 𝑍 ) → 𝑋 ⊆ 𝐴 )
8		simplr2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) ∧ 𝑧 ∈ 𝑍 ) → 𝑌 ⊆ 𝐴 )
9	3 4	paddssat	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) ⊆ 𝐴 )
10	5 7 8 9	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) ∧ 𝑧 ∈ 𝑍 ) → ( 𝑋 + 𝑌 ) ⊆ 𝐴 )
11	3 4	sspadd2	⊢ ( ( 𝐾 ∈ HL ∧ 𝑍 ⊆ 𝐴 ∧ ( 𝑋 + 𝑌 ) ⊆ 𝐴 ) → 𝑍 ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
12	5 6 10 11	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) ∧ 𝑧 ∈ 𝑍 ) → 𝑍 ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
13		simpllr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) ∧ 𝑧 ∈ 𝑍 ) → 𝑝 = 𝑧 )
14		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) ∧ 𝑧 ∈ 𝑍 ) → 𝑧 ∈ 𝑍 )
15	13 14	eqeltrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) ∧ 𝑧 ∈ 𝑍 ) → 𝑝 ∈ 𝑍 )
16	12 15	sseldd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) ∧ 𝑧 ∈ 𝑍 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )