Theorem lvolnle3at 40842

Description: A lattice plane (or lattice line or atom) cannot majorize a lattice volume. (Contributed by NM, 8-Jul-2012.)

Hypotheses

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

Assertion

Ref	Expression
lvolnle3at	⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))

Proof of Theorem lvolnle3at

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simplr 781	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑋 ∈ 𝑉)
2		eqid 2763	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		eqid 2763	. . . . . 6 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
4		eqid 2763	. . . . . 6 ⊢ (LPlanes‘𝐾) = (LPlanes‘𝐾)
5		lvolnle3at.v	. . . . . 6 ⊢ 𝑉 = (LVols‘𝐾)
6	2, 3, 4, 5	islvol 40833	. . . . 5 ⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)))
7	6	ad2antrr 739	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)))
8	1, 7	mpbid 235	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋))
9	8	simprd 501	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)
10		oveq1 7453	. . . . . . . . 9 ⊢ (𝑃 = 𝑄 → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑄))
11	10	oveq1d 7461	. . . . . . . 8 ⊢ (𝑃 = 𝑄 → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑄 ∨ 𝑄) ∨ 𝑅))
12	11	breq2d 5118	. . . . . . 7 ⊢ (𝑃 = 𝑄 → (𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ 𝑋 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅)))
13	12	notbid 321	. . . . . 6 ⊢ (𝑃 = 𝑄 → (¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ ¬ 𝑋 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅)))
14		simp1l 1216	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ HL)
15		simp3l 1220	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦 ∈ (LPlanes‘𝐾))
16		simp21 1225	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑃 ∈ 𝐴)
17		simp22 1226	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑄 ∈ 𝐴)
18		lvolnle3at.l	. . . . . . . . . . . . 13 ⊢ ≤ = (le‘𝐾)
19		lvolnle3at.j	. . . . . . . . . . . . 13 ⊢ ∨ = (join‘𝐾)
20		lvolnle3at.a	. . . . . . . . . . . . 13 ⊢ 𝐴 = (Atoms‘𝐾)
21	18, 19, 20, 4	lplnnle2at 40801	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ¬ 𝑦 ≤ (𝑃 ∨ 𝑄))
22	14, 15, 16, 17, 21	syl13anc 1400	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑦 ≤ (𝑃 ∨ 𝑄))
23	2, 4	lplnbase 40794	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (LPlanes‘𝐾) → 𝑦 ∈ (Base‘𝐾))
24	15, 23	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦 ∈ (Base‘𝐾))
25		simp1r 1217	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑋 ∈ 𝑉)
26	2, 5	lvolbase 40838	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ (Base‘𝐾))
27	25, 26	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑋 ∈ (Base‘𝐾))
28		simp3r 1221	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦( ⋖ ‘𝐾)𝑋)
29		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (lt‘𝐾) = (lt‘𝐾)
30	2, 29, 3	cvrlt 40530	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾)) ∧ 𝑦( ⋖ ‘𝐾)𝑋) → 𝑦(lt‘𝐾)𝑋)
31	14, 24, 27, 28, 30	syl31anc 1401	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦(lt‘𝐾)𝑋)
32		hlpos 40626	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
33	14, 32	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ Poset)
34	2, 19, 20	hlatjcl 40627	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
35	14, 16, 17, 34	syl3anc 1399	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
36	2, 18, 29	pltletr 18547	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ (𝑃 ∨ 𝑄)) → 𝑦(lt‘𝐾)(𝑃 ∨ 𝑄)))
37	33, 24, 27, 35, 36	syl13anc 1400	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ (𝑃 ∨ 𝑄)) → 𝑦(lt‘𝐾)(𝑃 ∨ 𝑄)))
38	31, 37	mpand 708	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ (𝑃 ∨ 𝑄) → 𝑦(lt‘𝐾)(𝑃 ∨ 𝑄)))
39	18, 29	pltle 18537	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) → (𝑦(lt‘𝐾)(𝑃 ∨ 𝑄) → 𝑦 ≤ (𝑃 ∨ 𝑄)))
40	14, 15, 35, 39	syl3anc 1399	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑦(lt‘𝐾)(𝑃 ∨ 𝑄) → 𝑦 ≤ (𝑃 ∨ 𝑄)))
41	38, 40	syld 48	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ (𝑃 ∨ 𝑄) → 𝑦 ≤ (𝑃 ∨ 𝑄)))
42	22, 41	mtod 201	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ≤ (𝑃 ∨ 𝑄))
43	42	adantr 486	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑋 ≤ (𝑃 ∨ 𝑄))
44		simprr 785	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑅 ≤ (𝑃 ∨ 𝑄))
45	14	hllatd 40624	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ Lat)
46		simp23 1227	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑅 ∈ 𝐴)
47	2, 20	atbase 40549	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾))
48	46, 47	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑅 ∈ (Base‘𝐾))
49	2, 18, 19	latleeqj2 18658	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) → (𝑅 ≤ (𝑃 ∨ 𝑄) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄)))
50	45, 48, 35, 49	syl3anc 1399	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑅 ≤ (𝑃 ∨ 𝑄) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄)))
51	50	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ≤ (𝑃 ∨ 𝑄) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄)))
52	44, 51	mpbid 235	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄))
53	52	breq2d 5118	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ 𝑋 ≤ (𝑃 ∨ 𝑄)))
54	43, 53	mtbird 328	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
55	54	anassrs 473	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃 ≠ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
56		simpl1l 1243	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝐾 ∈ HL)
57		simpl3l 1247	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑦 ∈ (LPlanes‘𝐾))
58		simpl2 1211	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴))
59		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)))
60	18, 19, 20, 4	lplni2 40797	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (LPlanes‘𝐾))
61	56, 58, 59, 60	syl3anc 1399	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (LPlanes‘𝐾))
62	29, 4	lplnnlt 40825	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (LPlanes‘𝐾)) → ¬ 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅))
63	56, 57, 61, 62	syl3anc 1399	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅))
64	2, 19	latjcl 18645	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))
65	45, 35, 48, 64	syl3anc 1399	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))
66	2, 18, 29	pltletr 18547	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅)))
67	33, 24, 27, 65, 66	syl13anc 1400	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅)))
68	31, 67	mpand 708	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) → 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅)))
69	68	adantr 486	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) → 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅)))
70	63, 69	mtod 201	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
71	70	anassrs 473	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
72	55, 71	pm2.61dan 825	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃 ≠ 𝑄) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
73		eqid 2763	. . . . . . . . . 10 ⊢ (le‘𝐾) = (le‘𝐾)
74	73, 19, 20, 4	lplnnle2at 40801	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ¬ 𝑦(le‘𝐾)(𝑄 ∨ 𝑅))
75	14, 15, 17, 46, 74	syl13anc 1400	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑦(le‘𝐾)(𝑄 ∨ 𝑅))
76	2, 19, 20	hlatjcl 40627	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))
77	14, 17, 46, 76	syl3anc 1399	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))
78	2, 18, 29	pltletr 18547	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ (𝑄 ∨ 𝑅)) → 𝑦(lt‘𝐾)(𝑄 ∨ 𝑅)))
79	33, 24, 27, 77, 78	syl13anc 1400	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ (𝑄 ∨ 𝑅)) → 𝑦(lt‘𝐾)(𝑄 ∨ 𝑅)))
80	31, 79	mpand 708	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ (𝑄 ∨ 𝑅) → 𝑦(lt‘𝐾)(𝑄 ∨ 𝑅)))
81	73, 29	pltle 18537	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾)) → (𝑦(lt‘𝐾)(𝑄 ∨ 𝑅) → 𝑦(le‘𝐾)(𝑄 ∨ 𝑅)))
82	14, 15, 77, 81	syl3anc 1399	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑦(lt‘𝐾)(𝑄 ∨ 𝑅) → 𝑦(le‘𝐾)(𝑄 ∨ 𝑅)))
83	80, 82	syld 48	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ (𝑄 ∨ 𝑅) → 𝑦(le‘𝐾)(𝑄 ∨ 𝑅)))
84	75, 83	mtod 201	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ≤ (𝑄 ∨ 𝑅))
85	19, 20	hlatjidm 40629	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴) → (𝑄 ∨ 𝑄) = 𝑄)
86	14, 17, 85	syl2anc 596	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑄 ∨ 𝑄) = 𝑄)
87	86	oveq1d 7461	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑄 ∨ 𝑄) ∨ 𝑅) = (𝑄 ∨ 𝑅))
88	87	breq2d 5118	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅) ↔ 𝑋 ≤ (𝑄 ∨ 𝑅)))
89	84, 88	mtbird 328	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅))
90	13, 72, 89	pm2.61ne 3044	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
91	90	3expia 1139	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
92	91	expd 421	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑦 ∈ (LPlanes‘𝐾) → (𝑦( ⋖ ‘𝐾)𝑋 → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))))
93	92	rexlimdv 3165	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋 → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
94	9, 93	mpd 16	1 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∃wrex 3090   class class class wbr 5106  ‘cfv 6561  (class class class)co 7446  Basecbs 17419  lecple 17467  Posetcpo 18513  ltcplt 18514  joincjn 18517  Latclat 18637   ⋖ ccvr 40522  Atomscatm 40523  HLchlt 40610  LPlanesclpl 40752  LVolsclvol 40753

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5236  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7403  df-ov 7449  df-oprab 7450  df-proset 18500  df-poset 18519  df-plt 18534  df-lub 18550  df-glb 18551  df-join 18552  df-meet 18553  df-p0 18629  df-lat 18638  df-clat 18705  df-oposet 40436  df-ol 40438  df-oml 40439  df-covers 40526  df-ats 40527  df-atl 40558  df-cvlat 40582  df-hlat 40611  df-llines 40758  df-lplanes 40759  df-lvols 40760

This theorem is used by:  lvolnleat  40843  lvolnlelln  40844  lvolnlelpln  40845  3atnelvolN  40846  4atlem3  40856  dalem39  40971