Metamath Proof Explorer

Theorem paddasslem8

Description: Lemma for paddass . (Contributed by NM, 8-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 paddasslem.l ⊢ ≤ = ( le ‘ 𝐾 )
2 paddasslem.j ⊢ ∨ = ( join ‘ 𝐾 )
3 paddasslem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 paddasslem.p ⊢ + = ( +𝑃 ‘ 𝐾 )
5 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) ) ) → 𝐾 ∈ HL )
6 5 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) ) ) → 𝐾 ∈ Lat )
7 simpl21 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) ) ) → 𝑋 ⊆ 𝐴 )
8 simpl22 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) ) ) → 𝑌 ⊆ 𝐴 )
9 3 4 paddssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) ⊆ 𝐴 )
10 5 7 8 9 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) ) ) → ( 𝑋 + 𝑌 ) ⊆ 𝐴 )
11 simpl23 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) ) ) → 𝑍 ⊆ 𝐴 )
12 simpr11 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) ) ) → 𝑥 ∈ 𝑋 )
13 simpr12 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) ) ) → 𝑦 ∈ 𝑌 )
14 simpl3r ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) ) ) → 𝑠 ∈ 𝐴 )
15 simpr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) ) ) → 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) )
16 1 2 3 4 elpaddri ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) ) → 𝑠 ∈ ( 𝑋 + 𝑌 ) )
17 6 7 8 12 13 14 15 16 syl322anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) ) ) → 𝑠 ∈ ( 𝑋 + 𝑌 ) )
18 simpr13 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) ) ) → 𝑧 ∈ 𝑍 )
19 simpl3l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) ) ) → 𝑝 ∈ 𝐴 )
20 simpr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) ) ) → 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) )
21 1 2 3 4 elpaddri ⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 + 𝑌 ) ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑠 ∈ ( 𝑋 + 𝑌 ) ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
22 6 10 11 17 18 19 20 21 syl322anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )