Theorem lvoli2 40244

Description: The join of 4 different atoms is a lattice volume. (Contributed by NM, 8-Jul-2012.)

Hypotheses

Ref	Expression
lvoli2.l	⊢ ≤ = (le‘𝐾)
lvoli2.j	⊢ ∨ = (join‘𝐾)
lvoli2.a	⊢ 𝐴 = (Atoms‘𝐾)
lvoli2.v	⊢ 𝑉 = (LVols‘𝐾)

Assertion

Ref	Expression
lvoli2	⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉)

Proof of Theorem lvoli2

Dummy variables 𝑞 𝑝 𝑟 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp12 1221	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑃 ∈ 𝐴)
2		simp13 1222	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑄 ∈ 𝐴)
3		simp3 1154	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
4		eqidd 2770	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆))
5		neeq1 3026	. . . . . . . . 9 ⊢ (𝑝 = 𝑃 → (𝑝 ≠ 𝑞 ↔ 𝑃 ≠ 𝑞))
6		oveq1 7418	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑃 → (𝑝 ∨ 𝑞) = (𝑃 ∨ 𝑞))
7	6	breq2d 5125	. . . . . . . . . 10 ⊢ (𝑝 = 𝑃 → (𝑅 ≤ (𝑝 ∨ 𝑞) ↔ 𝑅 ≤ (𝑃 ∨ 𝑞)))
8	7	notbid 321	. . . . . . . . 9 ⊢ (𝑝 = 𝑃 → (¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ↔ ¬ 𝑅 ≤ (𝑃 ∨ 𝑞)))
9	6	oveq1d 7426	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑃 → ((𝑝 ∨ 𝑞) ∨ 𝑅) = ((𝑃 ∨ 𝑞) ∨ 𝑅))
10	9	breq2d 5125	. . . . . . . . . 10 ⊢ (𝑝 = 𝑃 → (𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅) ↔ 𝑆 ≤ ((𝑃 ∨ 𝑞) ∨ 𝑅)))
11	10	notbid 321	. . . . . . . . 9 ⊢ (𝑝 = 𝑃 → (¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅) ↔ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑞) ∨ 𝑅)))
12	5, 8, 11	3anbi123d 1462	. . . . . . . 8 ⊢ (𝑝 = 𝑃 → ((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ↔ (𝑃 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑞) ∨ 𝑅))))
13	9	oveq1d 7426	. . . . . . . . 9 ⊢ (𝑝 = 𝑃 → (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆) = (((𝑃 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆))
14	13	eqeq2d 2780	. . . . . . . 8 ⊢ (𝑝 = 𝑃 → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑃 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆)))
15	12, 14	anbi12d 643	. . . . . . 7 ⊢ (𝑝 = 𝑃 → (((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆)) ↔ ((𝑃 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑃 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆))))
16		neeq2 3027	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → (𝑃 ≠ 𝑞 ↔ 𝑃 ≠ 𝑄))
17		oveq2 7419	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑄 → (𝑃 ∨ 𝑞) = (𝑃 ∨ 𝑄))
18	17	breq2d 5125	. . . . . . . . . 10 ⊢ (𝑞 = 𝑄 → (𝑅 ≤ (𝑃 ∨ 𝑞) ↔ 𝑅 ≤ (𝑃 ∨ 𝑄)))
19	18	notbid 321	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → (¬ 𝑅 ≤ (𝑃 ∨ 𝑞) ↔ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)))
20	17	oveq1d 7426	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑄 → ((𝑃 ∨ 𝑞) ∨ 𝑅) = ((𝑃 ∨ 𝑄) ∨ 𝑅))
21	20	breq2d 5125	. . . . . . . . . 10 ⊢ (𝑞 = 𝑄 → (𝑆 ≤ ((𝑃 ∨ 𝑞) ∨ 𝑅) ↔ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
22	21	notbid 321	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → (¬ 𝑆 ≤ ((𝑃 ∨ 𝑞) ∨ 𝑅) ↔ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
23	16, 19, 22	3anbi123d 1462	. . . . . . . 8 ⊢ (𝑞 = 𝑄 → ((𝑃 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑞) ∨ 𝑅)) ↔ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))))
24	20	oveq1d 7426	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → (((𝑃 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆) = (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆))
25	24	eqeq2d 2780	. . . . . . . 8 ⊢ (𝑞 = 𝑄 → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑃 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆)))
26	23, 25	anbi12d 643	. . . . . . 7 ⊢ (𝑞 = 𝑄 → (((𝑃 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑃 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆)) ↔ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆))))
27	15, 26	rspc2ev 3603	. . . . . 6 ⊢ ((𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆))) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆)))
28	1, 2, 3, 4, 27	syl112anc 1399	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆)))
29	28	3exp 1135	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ((𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → ((𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆)))))
30		simplrl 788	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ ((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆))) → 𝑅 ∈ 𝐴)
31		simplrr 789	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ ((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆))) → 𝑆 ∈ 𝐴)
32		simpr 489	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ ((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆))) → ((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆)))
33		breq1 5116	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝑅 → (𝑟 ≤ (𝑝 ∨ 𝑞) ↔ 𝑅 ≤ (𝑝 ∨ 𝑞)))
34	33	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑅 → (¬ 𝑟 ≤ (𝑝 ∨ 𝑞) ↔ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞)))
35		oveq2 7419	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑅 → ((𝑝 ∨ 𝑞) ∨ 𝑟) = ((𝑝 ∨ 𝑞) ∨ 𝑅))
36	35	breq2d 5125	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝑅 → (𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑟) ↔ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)))
37	36	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑅 → (¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑟) ↔ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)))
38	34, 37	3anbi23d 1465	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑅 → ((𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑟)) ↔ (𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅))))
39	35	oveq1d 7426	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑅 → (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑠))
40	39	eqeq2d 2780	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑅 → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑠)))
41	38, 40	anbi12d 643	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (((𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑟)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)) ↔ ((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑠))))
42		breq1 5116	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑆 → (𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅) ↔ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)))
43	42	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → (¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅) ↔ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)))
44	43	3anbi3d 1468	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → ((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ↔ (𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅))))
45		oveq2 7419	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑠) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆))
46	45	eqeq2d 2780	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑠) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆)))
47	44, 46	anbi12d 643	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → (((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑠)) ↔ ((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆))))
48	41, 47	rspc2ev 3603	. . . . . . . . 9 ⊢ ((𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆))) → ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑟)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))
49	30, 31, 32, 48	syl3anc 1396	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ ((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆))) → ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑟)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))
50	49	ex 417	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆)) → ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑟)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
51	50	reximdv 3186	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (∃𝑞 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆)) → ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑟)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
52	51	reximdv 3186	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆)) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑟)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
53	52	ex 417	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ((𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑅 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑆 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑅)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑅) ∨ 𝑆)) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑟)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
54	29, 53	syldd 73	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ((𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → ((𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑟)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
55	54	3imp 1126	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑟)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))
56		simp11 1220	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝐾 ∈ HL)
57	56	hllatd 40027	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝐾 ∈ Lat)
58		eqid 2769	. . . . . . 7 ⊢ (Base‘𝐾) = (Base‘𝐾)
59		lvoli2.j	. . . . . . 7 ⊢ ∨ = (join‘𝐾)
60		lvoli2.a	. . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾)
61	58, 59, 60	hlatjcl 40030	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
62	61	3ad2ant1 1149	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
63		simp2l 1216	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑅 ∈ 𝐴)
64	58, 60	atbase 39952	. . . . . 6 ⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾))
65	63, 64	syl 18	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑅 ∈ (Base‘𝐾))
66	58, 59	latjcl 18494	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))
67	57, 62, 65, 66	syl3anc 1396	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))
68		simp2r 1217	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑆 ∈ 𝐴)
69	58, 60	atbase 39952	. . . . 5 ⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ (Base‘𝐾))
70	68, 69	syl 18	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑆 ∈ (Base‘𝐾))
71	58, 59	latjcl 18494	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ (Base‘𝐾))
72	57, 67, 70, 71	syl3anc 1396	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ (Base‘𝐾))
73		lvoli2.l	. . . 4 ⊢ ≤ = (le‘𝐾)
74		lvoli2.v	. . . 4 ⊢ 𝑉 = (LVols‘𝐾)
75	58, 73, 59, 60, 74	islvol5 40242	. . 3 ⊢ ((𝐾 ∈ HL ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ (Base‘𝐾)) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉 ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑟)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
76	56, 72, 75	syl2anc 595	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉 ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑟)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
77	55, 76	mpbird 260	1 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  ∃wrex 3095   class class class wbr 5113  ‘cfv 6537  (class class class)co 7411  Basecbs 17268  lecple 17316  joincjn 18366  Latclat 18486  Atomscatm 39926  HLchlt 40013  LVolsclvol 40156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-proset 18349  df-poset 18368  df-plt 18383  df-lub 18399  df-glb 18400  df-join 18401  df-meet 18402  df-p0 18478  df-lat 18487  df-clat 18554  df-oposet 39839  df-ol 39841  df-oml 39842  df-covers 39929  df-ats 39930  df-atl 39961  df-cvlat 39985  df-hlat 40014  df-llines 40161  df-lplanes 40162  df-lvols 40163

This theorem is referenced by:  islvol2aN  40255  4atlem3  40259  2lplnja  40282