Theorem paddasslem12 38294

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

Hypotheses

Ref	Expression
paddasslem.l	⊢ ≤ = (le‘𝐾)
paddasslem.j	⊢ ∨ = (join‘𝐾)
paddasslem.a	⊢ 𝐴 = (Atoms‘𝐾)
paddasslem.p	⊢ + = (+𝑃‘𝐾)

Assertion

Ref	Expression
paddasslem12	⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))

Proof of Theorem paddasslem12

Step	Hyp	Ref	Expression
1		simpl1l 1224	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝐾 ∈ HL)
2		simpl21 1251	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑋 ⊆ 𝐴)
3		simpl22 1252	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑌 ⊆ 𝐴)
4		paddasslem.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
5		paddasslem.p	. . . . . 6 ⊢ + = (+𝑃‘𝐾)
6	4, 5	paddssat 38277	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) ⊆ 𝐴)
7	1, 2, 3, 6	syl3anc 1371	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → (𝑋 + 𝑌) ⊆ 𝐴)
8		simpl23 1253	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑍 ⊆ 𝐴)
9	1, 7, 8	3jca 1128	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → (𝐾 ∈ HL ∧ (𝑋 + 𝑌) ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴))
10	4, 5	sspadd2 38279	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝐴) → 𝑌 ⊆ (𝑋 + 𝑌))
11	1, 3, 2, 10	syl3anc 1371	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑌 ⊆ (𝑋 + 𝑌))
12	4, 5	paddss1 38280	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 + 𝑌) ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑌 ⊆ (𝑋 + 𝑌) → (𝑌 + 𝑍) ⊆ ((𝑋 + 𝑌) + 𝑍)))
13	9, 11, 12	sylc 65	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → (𝑌 + 𝑍) ⊆ ((𝑋 + 𝑌) + 𝑍))
14	1	hllatd 37826	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝐾 ∈ Lat)
15		simprll 777	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑦 ∈ 𝑌)
16		simprlr 778	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑧 ∈ 𝑍)
17		simpl3l 1228	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ 𝐴)
18		eqid 2736	. . . 4 ⊢ (Base‘𝐾) = (Base‘𝐾)
19		paddasslem.l	. . . 4 ⊢ ≤ = (le‘𝐾)
20	18, 4	atbase 37751	. . . . 5 ⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ (Base‘𝐾))
21	17, 20	syl 17	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ (Base‘𝐾))
22	3, 15	sseldd 3945	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑦 ∈ 𝐴)
23	18, 4	atbase 37751	. . . . . 6 ⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ (Base‘𝐾))
24	22, 23	syl 17	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑦 ∈ (Base‘𝐾))
25		simpl3r 1229	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑟 ∈ 𝐴)
26	18, 4	atbase 37751	. . . . . 6 ⊢ (𝑟 ∈ 𝐴 → 𝑟 ∈ (Base‘𝐾))
27	25, 26	syl 17	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑟 ∈ (Base‘𝐾))
28		paddasslem.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
29	18, 28	latjcl 18328	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑟 ∈ (Base‘𝐾)) → (𝑦 ∨ 𝑟) ∈ (Base‘𝐾))
30	14, 24, 27, 29	syl3anc 1371	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → (𝑦 ∨ 𝑟) ∈ (Base‘𝐾))
31	8, 16	sseldd 3945	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑧 ∈ 𝐴)
32	18, 4	atbase 37751	. . . . . 6 ⊢ (𝑧 ∈ 𝐴 → 𝑧 ∈ (Base‘𝐾))
33	31, 32	syl 17	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑧 ∈ (Base‘𝐾))
34	18, 28	latjcl 18328	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑦 ∨ 𝑧) ∈ (Base‘𝐾))
35	14, 24, 33, 34	syl3anc 1371	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → (𝑦 ∨ 𝑧) ∈ (Base‘𝐾))
36		simpl1r 1225	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑥 = 𝑦)
37		simprrl 779	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ≤ (𝑥 ∨ 𝑟))
38		oveq1 7364	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ∨ 𝑟) = (𝑦 ∨ 𝑟))
39	38	breq2d 5117	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑝 ≤ (𝑥 ∨ 𝑟) ↔ 𝑝 ≤ (𝑦 ∨ 𝑟)))
40	39	biimpa 477	. . . . 5 ⊢ ((𝑥 = 𝑦 ∧ 𝑝 ≤ (𝑥 ∨ 𝑟)) → 𝑝 ≤ (𝑦 ∨ 𝑟))
41	36, 37, 40	syl2anc 584	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ≤ (𝑦 ∨ 𝑟))
42	18, 19, 28	latlej1 18337	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → 𝑦 ≤ (𝑦 ∨ 𝑧))
43	14, 24, 33, 42	syl3anc 1371	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑦 ≤ (𝑦 ∨ 𝑧))
44		simprrr 780	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑟 ≤ (𝑦 ∨ 𝑧))
45	18, 19, 28	latjle12 18339	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑟 ∈ (Base‘𝐾) ∧ (𝑦 ∨ 𝑧) ∈ (Base‘𝐾))) → ((𝑦 ≤ (𝑦 ∨ 𝑧) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)) ↔ (𝑦 ∨ 𝑟) ≤ (𝑦 ∨ 𝑧)))
46	14, 24, 27, 35, 45	syl13anc 1372	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → ((𝑦 ≤ (𝑦 ∨ 𝑧) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)) ↔ (𝑦 ∨ 𝑟) ≤ (𝑦 ∨ 𝑧)))
47	43, 44, 46	mpbi2and 710	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → (𝑦 ∨ 𝑟) ≤ (𝑦 ∨ 𝑧))
48	18, 19, 14, 21, 30, 35, 41, 47	lattrd 18335	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ≤ (𝑦 ∨ 𝑧))
49	19, 28, 4, 5	elpaddri 38265	. . 3 ⊢ (((𝐾 ∈ Lat ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝 ≤ (𝑦 ∨ 𝑧))) → 𝑝 ∈ (𝑌 + 𝑍))
50	14, 3, 8, 15, 16, 17, 48, 49	syl322anc 1398	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ (𝑌 + 𝑍))
51	13, 50	sseldd 3945	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ⊆ wss 3910   class class class wbr 5105  ‘cfv 6496  (class class class)co 7357  Basecbs 17083  lecple 17140  joincjn 18200  Latclat 18320  Atomscatm 37725  HLchlt 37812  +_𝑃cpadd 38258

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-poset 18202  df-lub 18235  df-glb 18236  df-join 18237  df-meet 18238  df-lat 18321  df-ats 37729  df-atl 37760  df-cvlat 37784  df-hlat 37813  df-padd 38259

This theorem is referenced by:  paddasslem14  38296